Documentation

Mathlib.LinearAlgebra.QuotientPi

Submodule quotients and direct sums #

This file contains some results on the quotient of a module by a direct sum of submodules, and the direct sum of quotients of modules by submodules.

Main definitions #

def Submodule.piQuotientLift {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] {N : Type u_4} [AddCommGroup N] [Module R N] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) (q : Submodule R N) (f : (i : ι) → Ms i →ₗ[R] N) (hf : ∀ (i : ι), p i Submodule.comap (f i) q) :
((i : ι) → Ms i p i) →ₗ[R] N q

Lift a family of maps to the direct sum of quotients.

Equations
Instances For
    @[simp]
    theorem Submodule.piQuotientLift_mk {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] {N : Type u_4} [AddCommGroup N] [Module R N] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) (q : Submodule R N) (f : (i : ι) → Ms i →ₗ[R] N) (hf : ∀ (i : ι), p i Submodule.comap (f i) q) (x : (i : ι) → Ms i) :
    ((Submodule.piQuotientLift p q f hf) fun (i : ι) => Submodule.Quotient.mk (x i)) = Submodule.Quotient.mk (((LinearMap.lsum R (fun (i : ι) => Ms i) R) f) x)
    @[simp]
    theorem Submodule.piQuotientLift_single {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] {N : Type u_4} [AddCommGroup N] [Module R N] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) (q : Submodule R N) (f : (i : ι) → Ms i →ₗ[R] N) (hf : ∀ (i : ι), p i Submodule.comap (f i) q) (i : ι) (x : Ms i p i) :
    (Submodule.piQuotientLift p q f hf) (Pi.single i x) = ((p i).mapQ q (f i) ) x
    def Submodule.quotientPiLift {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] {Ns : ιType u_5} [(i : ι) → AddCommGroup (Ns i)] [(i : ι) → Module R (Ns i)] (p : (i : ι) → Submodule R (Ms i)) (f : (i : ι) → Ms i →ₗ[R] Ns i) (hf : ∀ (i : ι), p i LinearMap.ker (f i)) :
    ((i : ι) → Ms i) Submodule.pi Set.univ p →ₗ[R] (i : ι) → Ns i

    Lift a family of maps to a quotient of direct sums.

    Equations
    Instances For
      @[simp]
      theorem Submodule.quotientPiLift_mk {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] {Ns : ιType u_5} [(i : ι) → AddCommGroup (Ns i)] [(i : ι) → Module R (Ns i)] (p : (i : ι) → Submodule R (Ms i)) (f : (i : ι) → Ms i →ₗ[R] Ns i) (hf : ∀ (i : ι), p i LinearMap.ker (f i)) (x : (i : ι) → Ms i) :
      (Submodule.quotientPiLift p f hf) (Submodule.Quotient.mk x) = fun (i : ι) => (f i) (x i)
      def Submodule.quotientPi_aux.toFun {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] (p : (i : ι) → Submodule R (Ms i)) :
      ((i : ι) → Ms i) Submodule.pi Set.univ p(i : ι) → Ms i p i
      Equations
      Instances For
        def Submodule.quotientPi_aux.invFun {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) :
        ((i : ι) → Ms i p i)((i : ι) → Ms i) Submodule.pi Set.univ p
        Equations
        Instances For
          theorem Submodule.quotientPi_aux.left_inv {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) :
          theorem Submodule.quotientPi_aux.right_inv {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) :
          theorem Submodule.quotientPi_aux.map_add {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] (p : (i : ι) → Submodule R (Ms i)) (x : ((i : ι) → Ms i) Submodule.pi Set.univ p) (y : ((i : ι) → Ms i) Submodule.pi Set.univ p) :
          theorem Submodule.quotientPi_aux.map_smul {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] (p : (i : ι) → Submodule R (Ms i)) (r : R) (x : ((i : ι) → Ms i) Submodule.pi Set.univ p) :
          @[simp]
          theorem Submodule.quotientPi_symm_apply {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) :
          ∀ (a : (i : ι) → Ms i p i), (Submodule.quotientPi p).symm a = (Submodule.piQuotientLift p (Submodule.pi Set.univ p) LinearMap.single ) a
          @[simp]
          theorem Submodule.quotientPi_apply {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) :
          ∀ (a : ((i : ι) → Ms i) Submodule.pi Set.univ p) (i : ι), (Submodule.quotientPi p) a i = (Submodule.quotientPiLift p (fun (i : ι) => (p i).mkQ) ) a i
          def Submodule.quotientPi {ι : Type u_1} {R : Type u_2} [CommRing R] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [Fintype ι] [DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) :
          (((i : ι) → Ms i) Submodule.pi Set.univ p) ≃ₗ[R] (i : ι) → Ms i p i

          The quotient of a direct sum is the direct sum of quotients.

          Equations
          Instances For