Documentation

Mathlib.Algebra.Module.Submodule.LinearMap

Linear maps involving submodules of a module #

In this file we define a number of linear maps involving submodules of a module.

Main declarations #

Tags #

submodule, subspace, linear map

def SMulMemClass.subtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] [SMulMemClass A R M] (S' : A) :
S' →ₗ[R] M

The natural R-linear map from a submodule of an R-module M to M.

Equations
Instances For
    @[simp]
    theorem SMulMemClass.coeSubtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] [SMulMemClass A R M] (S' : A) :
    (SMulMemClass.subtype S') = Subtype.val
    def Submodule.subtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
    p →ₗ[R] M

    Embedding of a submodule p to the ambient space M.

    Equations
    • p.subtype = { toFun := Subtype.val, map_add' := , map_smul' := }
    Instances For
      theorem Submodule.subtype_apply {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (x : p) :
      p.subtype x = x
      @[simp]
      theorem Submodule.coeSubtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
      p.subtype = Subtype.val
      theorem Submodule.injective_subtype {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :
      Function.Injective p.subtype
      theorem Submodule.coe_sum {R : Type u} {M : Type v} {ι : Type w} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) (x : ιp) (s : Finset ι) :
      (is, x i) = is, (x i)

      Note the AddSubmonoid version of this lemma is called AddSubmonoid.coe_finset_sum.

      instance Submodule.instAddActionSubtypeMem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} [AddAction M α] :
      AddAction (p) α

      The action by a submodule is the action by the underlying module.

      Equations
      def LinearMap.domRestrict {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 R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) :
      p →ₛₗ[σ₁₂] M₂

      The restriction of a linear map f : M → M₂ to a submodule p ⊆ M gives a linear map p → M₂.

      Equations
      • f.domRestrict p = f.comp p.subtype
      Instances For
        @[simp]
        theorem LinearMap.domRestrict_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 R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) (x : p) :
        (f.domRestrict p) x = f x
        def LinearMap.codRestrict {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 R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) (h : ∀ (c : M), f c p) :
        M →ₛₗ[σ₁₂] p

        A linear map f : M₂ → M whose values lie in a submodule p ⊆ M can be restricted to a linear map M₂ → p.

        Equations
        Instances For
          @[simp]
          theorem LinearMap.codRestrict_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 R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R₂ M₂) (f : M →ₛₗ[σ₁₂] M₂) {h : ∀ (c : M), f c p} (x : M) :
          ((LinearMap.codRestrict p f h) x) = f x
          @[simp]
          theorem LinearMap.comp_codRestrict {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 R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R₃ M₃) (h : ∀ (b : M₂), g b p) :
          (LinearMap.codRestrict p g h).comp f = LinearMap.codRestrict p (g.comp f)
          @[simp]
          theorem LinearMap.subtype_comp_codRestrict {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 R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ (b : M), f b p) :
          p.subtype.comp (LinearMap.codRestrict p f h) = f
          def LinearMap.restrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁} (hf : xp, f x q) :
          p →ₗ[R] q

          Restrict domain and codomain of a linear map.

          Equations
          Instances For
            @[simp]
            theorem LinearMap.restrict_coe_apply {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : Submodule R M} {q : Submodule R M₁} (hf : xp, f x q) (x : p) :
            ((f.restrict hf) x) = f x
            theorem LinearMap.restrict_apply {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : xp, f x q) (x : p) :
            (f.restrict hf) x = f x,
            theorem LinearMap.restrict_sub {R : Type u_10} {M : Type u_11} {M₁ : Type u_12} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] {p : Submodule R M} {q : Submodule R M₁} {f : M →ₗ[R] M₁} {g : M →ₗ[R] M₁} (hf : Set.MapsTo f p q) (hg : Set.MapsTo g p q) (hfg : optParam (Set.MapsTo (f - g) p q) ) :
            f.restrict hf - g.restrict hg = (f - g).restrict hfg
            theorem LinearMap.restrict_comp {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {M₂ : Type u_10} {M₃ : Type u_11} [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M₂] [Module R M₃] {p : Submodule R M} {p₂ : Submodule R M₂} {p₃ : Submodule R M₃} {f : M →ₗ[R] M₂} {g : M₂ →ₗ[R] M₃} (hf : Set.MapsTo f p p₂) (hg : Set.MapsTo g p₂ p₃) (hfg : optParam (Set.MapsTo (g ∘ₗ f) p p₃) ) :
            (g ∘ₗ f).restrict hfg = g.restrict hg ∘ₗ f.restrict hf
            theorem LinearMap.restrict_commute {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] M} {g : M →ₗ[R] M} (h : Commute f g) {p : Submodule R M} (hf : Set.MapsTo f p p) (hg : Set.MapsTo g p p) :
            Commute (f.restrict hf) (g.restrict hg)
            theorem LinearMap.subtype_comp_restrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : xp, f x q) :
            q.subtype ∘ₗ f.restrict hf = f.domRestrict p
            theorem LinearMap.restrict_eq_codRestrict_domRestrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : xp, f x q) :
            f.restrict hf = LinearMap.codRestrict q (f.domRestrict p)
            theorem LinearMap.restrict_eq_domRestrict_codRestrict {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] {f : M →ₗ[R] M₁} {p : Submodule R M} {q : Submodule R M₁} (hf : ∀ (x : M), f x q) :
            f.restrict = (LinearMap.codRestrict q f hf).domRestrict p
            theorem LinearMap.sum_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} {ι : Type u_9} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (t : Finset ι) (f : ιM →ₛₗ[σ₁₂] M₂) (b : M) :
            (dt, f d) b = dt, (f d) b
            @[simp]
            theorem LinearMap.coeFn_sum {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 R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {ι : Type u_10} (t : Finset ι) (f : ιM →ₛₗ[σ₁₂] M₂) :
            (it, f i) = it, (f i)
            theorem LinearMap.submodule_pow_eq_zero_of_pow_eq_zero {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {g : Module.End R N} {G : Module.End R M} (h : G ∘ₗ N.subtype = N.subtype ∘ₗ g) {k : } (hG : G ^ k = 0) :
            g ^ k = 0
            theorem LinearMap.pow_apply_mem_of_forall_mem {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} {p : Submodule R M} (n : ) (h : xp, f' x p) (x : M) (hx : x p) :
            (f' ^ n) x p
            theorem LinearMap.pow_restrict {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f' : M →ₗ[R] M} {p : Submodule R M} (n : ) (h : xp, f' x p) (h' : optParam (xp, (f' ^ n) x p) ) :
            f'.restrict h ^ n = (f' ^ n).restrict h'
            def LinearMap.domRestrict' {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (p : Submodule R M) :
            (M →ₗ[R] M₂) →ₗ[R] p →ₗ[R] M₂

            Alternative version of domRestrict as a linear map.

            Equations
            Instances For
              @[simp]
              theorem LinearMap.domRestrict'_apply {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (p : Submodule R M) (x : p) :
              ((LinearMap.domRestrict' p) f) x = f x
              def Submodule.inclusion {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : p p') :
              p →ₗ[R] p'

              If two submodules p and p' satisfy p ⊆ p', then inclusion p p' is the linear map version of this inclusion.

              Equations
              Instances For
                @[simp]
                theorem Submodule.coe_inclusion {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : p p') (x : p) :
                ((Submodule.inclusion h) x) = x
                theorem Submodule.inclusion_apply {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : p p') (x : p) :
                (Submodule.inclusion h) x = x,
                theorem Submodule.inclusion_injective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : p p') :
                theorem Submodule.subtype_comp_inclusion {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R M) (h : p q) :
                q.subtype ∘ₗ Submodule.inclusion h = p.subtype