# 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 #

• Submodule.piQuotientLift: create a map out of the direct sum of quotients
• Submodule.quotientPiLift: create a map out of the quotient of a direct sum
• Submodule.quotientPi: the quotient of a direct sum is the direct sum of quotients.
def Submodule.piQuotientLift {ι : Type u_1} {R : Type u_2} [] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] {N : Type u_4} [] [Module R N] [] [] (p : (i : ι) → Submodule R (Ms i)) (q : ) (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
• = (LinearMap.lsum R (fun (i : ι) => Ms i p i) R) fun (i : ι) => (p i).mapQ q (f i)
Instances For
@[simp]
theorem Submodule.piQuotientLift_mk {ι : Type u_1} {R : Type u_2} [] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] {N : Type u_4} [] [Module R N] [] [] (p : (i : ι) → Submodule R (Ms i)) (q : ) (f : (i : ι) → Ms i →ₗ[R] N) (hf : ∀ (i : ι), p i Submodule.comap (f i) q) (x : (i : ι) → Ms i) :
(() fun (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} [] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] {N : Type u_4} [] [Module R N] [] [] (p : (i : ι) → Submodule R (Ms i)) (q : ) (f : (i : ι) → Ms i →ₗ[R] N) (hf : ∀ (i : ι), p i Submodule.comap (f i) q) (i : ι) (x : Ms i p i) :
() () = ((p i).mapQ q (f i) ) x
def Submodule.quotientPiLift {ι : Type u_1} {R : Type u_2} [] {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} [] {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) :
() = fun (i : ι) => (f i) (x i)
def Submodule.quotientPi_aux.toFun {ι : Type u_1} {R : Type u_2} [] {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} [] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [] [] (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} [] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [] [] (p : (i : ι) → Submodule R (Ms i)) :
theorem Submodule.quotientPi_aux.right_inv {ι : Type u_1} {R : Type u_2} [] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [] [] (p : (i : ι) → Submodule R (Ms i)) :
theorem Submodule.quotientPi_aux.map_add {ι : Type u_1} {R : Type u_2} [] {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} [] {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} [] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [] [] (p : (i : ι) → Submodule R (Ms i)) :
∀ (a : (i : ι) → Ms i p i), .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} [] {Ms : ιType u_3} [(i : ι) → AddCommGroup (Ms i)] [(i : ι) → Module R (Ms i)] [] [] (p : (i : ι) → Submodule R (Ms i)) :
∀ (a : ((i : ι) → Ms i) Submodule.pi Set.univ p) (i : ι), a i = (Submodule.quotientPiLift p (fun (i : ι) => (p i).mkQ) ) a i
def Submodule.quotientPi {ι : Type u_1} {R : Type u_2} [] {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) ≃ₗ[R] (i : ι) → Ms i p i

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

Equations
• = { toFun := , map_add' := , map_smul' := , invFun := , left_inv := , right_inv := }
Instances For