Documentation

Mathlib.Algebra.Module.Submodule.Equiv

Linear equivalences involving submodules #

source
πŸ”Έ coverage
def LinearEquiv.ofEq {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p q : Submodule R M) (h : p = q) :
β†₯p ≃ₗ[R] β†₯q

Linear equivalence between two equal submodules.

Equations
    Instances For
      source
      πŸ“ coverage
      @[simp]
      theorem LinearEquiv.coe_ofEq_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p q : Submodule R M} (h : p = q) (x : β†₯p) :
      ↑((ofEq p q h) x) = ↑x
      source
      πŸ“ coverage
      @[simp]
      theorem LinearEquiv.ofEq_symm {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p q : Submodule R M} (h : p = q) :
      (ofEq p q h).symm = ofEq q p β‹―
      source
      πŸ“ coverage
      @[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} :
      ofEq p p β‹― = refl R β†₯p
      source
      πŸ”Έ coverage
      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
          source
          πŸ“ coverage
          @[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
          source
          πŸ“ coverage
          @[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
          source
          πŸ”Έ coverage
          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
            Instances For
              source
              πŸ“ coverage
              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)) β‹―
              source
              πŸ“ coverage
              @[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
              source
              πŸ“ coverage
              @[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
              source
              πŸ”Έ coverage
              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
                Instances For
                  source
                  πŸ“ coverage
                  @[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) :
                  (ofTop p h) x = ↑x
                  source
                  πŸ“ coverage
                  @[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) :
                  ↑((ofTop p h).symm x) = x
                  source
                  πŸ“ coverage
                  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) :
                  (ofTop p h).symm x = ⟨x, β‹―βŸ©
                  source
                  πŸ“ coverage
                  @[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β‚‚) :
                  (↑e).range = ⊀
                  source
                  πŸ“ coverage
                  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 = βŠ₯
                  source
                  πŸ“ coverage
                  @[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 σ₁₃] :
                  (h βˆ˜β‚›β‚— ↑e).range = h.range
                  source
                  πŸ”Έ coverage
                  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 ≃ₛₗ[σ₁₂] β†₯f.range

                  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
                      source
                      πŸ“ coverage
                      @[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) :
                      ↑((ofLeftInverse h) x) = f x
                      source
                      πŸ“ coverage
                      @[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 : β†₯f.range) :
                      (ofLeftInverse h).symm x = g ↑x
                      source
                      πŸ”Έ coverage
                      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 ≃ₛₗ[σ₁₂] β†₯f.range

                      An Injective linear map f : M β†’β‚—[R] Mβ‚‚ defines a linear equivalence between M and f.range. See also LinearMap.ofLeftInverse.

                      Equations
                        Instances For
                          source
                          πŸ“ coverage
                          @[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) :
                          ↑((ofInjective f h) x) = f x
                          source
                          πŸ“ coverage
                          @[simp]
                          theorem LinearEquiv.ofInjective_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.Injective ⇑f} (x : β†₯f.range) :
                          f ((ofInjective f h).symm x) = ↑x
                          source
                          πŸ”Έ coverage
                          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
                              source
                              πŸ“ coverage
                              @[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) :
                              (ofBijective f hf) x = f x
                              source
                              πŸ“ coverage
                              @[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) :
                              (ofBijective f h).symm (f x) = x
                              source
                              πŸ“ coverage
                              @[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 ((ofBijective f h).symm x) = x
                              source
                              πŸ”Έ coverage
                              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] β†₯(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
                                Instances For
                                  source
                                  πŸ“ coverage
                                  @[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
                                  source
                                  πŸ“ coverage
                                  @[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 : β†₯(map p.subtype q)) :
                                  ↑↑((p.equivSubtypeMap q).symm x) = ↑x
                                  source
                                  πŸ”Έ coverage
                                  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 ≀ f.range) :
                                  β†₯(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
                                      source
                                      πŸ“ coverage
                                      @[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 ≀ f.range) (a✝ : β†₯(comap f p)) :
                                      (comap_equiv_self_of_inj_of_le hf h) a✝ = (LinearMap.codRestrict p (f βˆ˜β‚— (comap f p).subtype) β‹―) a✝
                                      source
                                      πŸ”Έ coverage
                                      noncomputable def LinearMap.codRestrictOfInjective {R : Type u_1} {M₁ : Type u_6} {Mβ‚‚ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid Mβ‚‚] [AddCommMonoid M₃] [Module R M₁] [Module R Mβ‚‚] [Module R M₃] (f : M₁ β†’β‚—[R] Mβ‚‚) (i : M₃ β†’β‚—[R] Mβ‚‚) (hi : Function.Injective ⇑i) (hf : βˆ€ (x : M₁), f x ∈ i.range) :
                                      M₁ β†’β‚—[R] M₃

                                      The restriction of a linear map on the target to a submodule of the target given by an inclusion.

                                      Equations
                                        Instances For
                                          source
                                          πŸ“ coverage
                                          @[simp]
                                          theorem LinearMap.codRestrictOfInjective_comp_apply {R : Type u_1} {M₁ : Type u_6} {Mβ‚‚ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid Mβ‚‚] [AddCommMonoid M₃] [Module R M₁] [Module R Mβ‚‚] [Module R M₃] (f : M₁ β†’β‚—[R] Mβ‚‚) (i : M₃ β†’β‚—[R] Mβ‚‚) (hi : Function.Injective ⇑i) (hf : βˆ€ (x : M₁), f x ∈ i.range) (x : M₁) :
                                          i ((f.codRestrictOfInjective i hi hf) x) = f x
                                          source
                                          πŸ“ coverage
                                          @[simp]
                                          theorem LinearMap.codRestrictOfInjective_comp {R : Type u_1} {M₁ : Type u_6} {Mβ‚‚ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid Mβ‚‚] [AddCommMonoid M₃] [Module R M₁] [Module R Mβ‚‚] [Module R M₃] (f : M₁ β†’β‚—[R] Mβ‚‚) (i : M₃ β†’β‚—[R] Mβ‚‚) (hi : Function.Injective ⇑i) (hf : βˆ€ (x : M₁), f x ∈ i.range) :
                                          i βˆ˜β‚— f.codRestrictOfInjective i hi hf = f
                                          source
                                          πŸ”Έ coverage
                                          noncomputable def LinearMap.codRestrictβ‚‚ {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {Mβ‚‚ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid Mβ‚‚] [AddCommMonoid M₃] [Module R M] [Module R M₁] [Module R Mβ‚‚] [Module R M₃] (f : M₁ β†’β‚—[R] Mβ‚‚ β†’β‚—[R] M) (i : M₃ β†’β‚—[R] M) (hi : Function.Injective ⇑i) (hf : βˆ€ (x : M₁) (y : Mβ‚‚), (f x) y ∈ i.range) :
                                          M₁ β†’β‚—[R] Mβ‚‚ β†’β‚—[R] M₃

                                          The restriction of a bilinear map to a submodule in which it takes values.

                                          Equations
                                            Instances For
                                              source
                                              πŸ“ coverage
                                              @[simp]
                                              theorem LinearMap.codRestrictβ‚‚_apply {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} {Mβ‚‚ : Type u_7} {M₃ : Type u_8} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid Mβ‚‚] [AddCommMonoid M₃] [Module R M] [Module R M₁] [Module R Mβ‚‚] [Module R M₃] (f : M₁ β†’β‚—[R] Mβ‚‚ β†’β‚—[R] M) (i : M₃ β†’β‚—[R] M) (hi : Function.Injective ⇑i) (hf : βˆ€ (x : M₁) (y : Mβ‚‚), (f x) y ∈ i.range) (x : M₁) (y : Mβ‚‚) :
                                              i (((f.codRestrictβ‚‚ i hi hf) x) y) = (f x) y