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} [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

• Submodule.piQuotientLift p q f hf = (LinearMap.lsum R (fun (i : ι) => Ms i ⧸ p i) R) fun (i : ι) => (p i).mapQ q (f i) ⋯

@[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 Ms 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

• Submodule.quotientPiLift p f hf = (Submodule.pi Set.univ p).liftQ (LinearMap.pi fun (i : ι) => f i ∘ₗ LinearMap.proj i) ⋯

@[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

• Submodule.quotientPi_aux.toFun p = ⇑(Submodule.quotientPiLift p (fun (i : ι) => (p i).mkQ) ⋯)

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

• Submodule.quotientPi_aux.invFun p = ⇑(Submodule.piQuotientLift p (Submodule.pi Set.univ p) LinearMap.single ⋯)

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)) : Function.LeftInverse (Submodule.quotientPi_aux.invFun p) (Submodule.quotientPi_aux.toFun p)

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)) : Function.RightInverse (Submodule.quotientPi_aux.invFun p) (Submodule.quotientPi_aux.toFun p)

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) : Submodule.quotientPi_aux.toFun p (x + y) = Submodule.quotientPi_aux.toFun p x + Submodule.quotientPi_aux.toFun p y

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) : Submodule.quotientPi_aux.toFun p (r • x) = (RingHom.id R) r • Submodule.quotientPi_aux.toFun p x

@[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

• Submodule.quotientPi p = { toFun := Submodule.quotientPi_aux.toFun p, map_add' := ⋯, map_smul' := ⋯, invFun := Submodule.quotientPi_aux.invFun p, left_inv := ⋯, right_inv := ⋯ }