Documentation

Mathlib.Algebra.Module.Submodule.Equiv

Linear equivalences involving submodules #

def LinearEquiv.ofEq {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (q : Submodule R M) (h : p = q) :
p ≃ₗ[R] q

Linear equivalence between two equal submodules.

Equations
Instances For
    @[simp]
    theorem LinearEquiv.coe_ofEq_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {q : Submodule R M} (h : p = q) (x : p) :
    ((LinearEquiv.ofEq p q h) x) = x
    @[simp]
    theorem LinearEquiv.ofEq_symm {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {q : Submodule R M} (h : p = q) :
    (LinearEquiv.ofEq p q h).symm = LinearEquiv.ofEq q p
    @[simp]
    theorem LinearEquiv.ofEq_rfl {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} :
    def LinearEquiv.ofSubmodules {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : Submodule R M) (q : Submodule R₂ M₂) (h : Submodule.map (↑e) p = q) :
    p ≃ₛₗ[σ₁₂] q

    A linear equivalence which maps a submodule of one module onto another, restricts to a linear equivalence of the two submodules.

    Equations
    Instances For
      @[simp]
      theorem LinearEquiv.ofSubmodules_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (h : Submodule.map e p = q) (x : p) :
      ((e.ofSubmodules p q h) x) = e x
      @[simp]
      theorem LinearEquiv.ofSubmodules_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (h : Submodule.map e p = q) (x : q) :
      ((e.ofSubmodules p q h).symm x) = e.symm x
      def LinearEquiv.ofSubmodule' {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) :
      (Submodule.comap (↑f) U) ≃ₛₗ[σ₁₂] U

      A linear equivalence of two modules restricts to a linear equivalence from the preimage of any submodule to that submodule.

      This is LinearEquiv.ofSubmodule but with comap on the left instead of map on the right.

      Equations
      • f.ofSubmodule' U = (f.symm.ofSubmodules U (Submodule.comap (↑f.symm.symm) U) ).symm
      Instances For
        theorem LinearEquiv.ofSubmodule'_toLinearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) :
        (f.ofSubmodule' U) = LinearMap.codRestrict U ((↑f).domRestrict (Submodule.comap (↑f) U))
        @[simp]
        theorem LinearEquiv.ofSubmodule'_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : (Submodule.comap (↑f) U)) :
        ((f.ofSubmodule' U) x) = f x
        @[simp]
        theorem LinearEquiv.ofSubmodule'_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] (f : M ≃ₛₗ[σ₁₂] M₂) (U : Submodule R₂ M₂) (x : U) :
        ((f.ofSubmodule' U).symm x) = f.symm x
        def LinearEquiv.ofTop {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (h : p = ) :
        p ≃ₗ[R] M

        The top submodule of M is linearly equivalent to M.

        Equations
        • LinearEquiv.ofTop p h = { toLinearMap := p.subtype, invFun := fun (x : M) => x, , left_inv := , right_inv := }
        Instances For
          @[simp]
          theorem LinearEquiv.ofTop_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {h : p = } (x : p) :
          (LinearEquiv.ofTop p h) x = x
          @[simp]
          theorem LinearEquiv.coe_ofTop_symm_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {h : p = } (x : M) :
          ((LinearEquiv.ofTop p h).symm x) = x
          theorem LinearEquiv.ofTop_symm_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {h : p = } (x : M) :
          (LinearEquiv.ofTop p h).symm x = x,
          @[simp]
          theorem LinearEquiv.range {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) :
          @[simp]
          theorem LinearEquivClass.range {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [Module R M] [Module R₂ M₂] {F : Type u_10} [EquivLike F M M₂] [SemilinearEquivClass F σ₁₂ M M₂] (e : F) :
          theorem LinearEquiv.eq_bot_of_equiv {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (p : Submodule R M) [Module R₂ M₂] (e : p ≃ₛₗ[σ₁₂] ) :
          p =
          @[simp]
          theorem LinearEquiv.range_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] :
          def LinearEquiv.ofLeftInverse {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {g : M₂M} (h : Function.LeftInverse g f) :
          M ≃ₛₗ[σ₁₂] (LinearMap.range f)

          A linear map f : M →ₗ[R] M₂ with a left-inverse g : M₂ →ₗ[R] M defines a linear equivalence between M and f.range.

          This is a computable alternative to LinearEquiv.ofInjective, and a bidirectional version of LinearMap.rangeRestrict.

          Equations
          Instances For
            @[simp]
            theorem LinearEquiv.ofLeftInverse_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₁] M} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.LeftInverse g f) (x : M) :
            @[simp]
            theorem LinearEquiv.ofLeftInverse_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {f : M →ₛₗ[σ₁₂] M₂} {g : M₂ →ₛₗ[σ₂₁] M} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.LeftInverse g f) (x : (LinearMap.range f)) :
            (LinearEquiv.ofLeftInverse h).symm x = g x
            noncomputable def LinearEquiv.ofInjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (h : Function.Injective f) :
            M ≃ₛₗ[σ₁₂] (LinearMap.range f)

            An Injective linear map f : M →ₗ[R] M₂ defines a linear equivalence between M and f.range. See also LinearMap.ofLeftInverse.

            Equations
            Instances For
              @[simp]
              theorem LinearEquiv.ofInjective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Function.Injective f} (x : M) :
              ((LinearEquiv.ofInjective f h) x) = f x
              noncomputable def LinearEquiv.ofBijective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (hf : Function.Bijective f) :
              M ≃ₛₗ[σ₁₂] M₂

              A bijective linear map is a linear equivalence.

              Equations
              Instances For
                @[simp]
                theorem LinearEquiv.ofBijective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {hf : Function.Bijective f} (x : M) :
                @[simp]
                theorem LinearEquiv.ofBijective_symm_apply_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Function.Bijective f} (x : M) :
                (LinearEquiv.ofBijective f h).symm (f x) = x
                @[simp]
                theorem LinearEquiv.apply_ofBijective_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} (f : M →ₛₗ[σ₁₂] M₂) [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {h : Function.Bijective f} (x : M₂) :
                f ((LinearEquiv.ofBijective f h).symm x) = x
                def Submodule.equivSubtypeMap {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R p) :
                q ≃ₗ[R] (Submodule.map p.subtype q)

                Given p a submodule of the module M and q a submodule of p, p.equivSubtypeMap q is the natural LinearEquiv between q and q.map p.subtype.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem Submodule.equivSubtypeMap_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R p} (x : q) :
                  ((p.equivSubtypeMap q) x) = (p.subtype.domRestrict q) x
                  @[simp]
                  theorem Submodule.equivSubtypeMap_symm_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R p} (x : (Submodule.map p.subtype q)) :
                  ((p.equivSubtypeMap q).symm x) = x
                  @[simp]
                  theorem Submodule.comap_equiv_self_of_inj_of_le_apply {R : Type u_1} {M : Type u_5} {N : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} {p : Submodule R N} (hf : Function.Injective f) (h : p LinearMap.range f) :
                  ∀ (a : (Submodule.comap f p)), (Submodule.comap_equiv_self_of_inj_of_le hf h) a = (LinearMap.codRestrict p (f ∘ₗ (Submodule.comap f p).subtype) ) a
                  noncomputable def Submodule.comap_equiv_self_of_inj_of_le {R : Type u_1} {M : Type u_5} {N : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} {p : Submodule R N} (hf : Function.Injective f) (h : p LinearMap.range f) :
                  (Submodule.comap f p) ≃ₗ[R] p

                  A linear injection M ↪ N restricts to an equivalence f⁻¹ p ≃ p for any submodule p contained in its range.

                  Equations
                  Instances For