# mathlib3documentation

linear_algebra.quotient_pi

# Submodule quotients and direct sums #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.pi_quotient_lift: create a map out of the direct sum of quotients
• submodule.quotient_pi_lift: create a map out of the quotient of a direct sum
• submodule.quotient_pi: the quotient of a direct sum is the direct sum of quotients.
def submodule.pi_quotient_lift {ι : Type u_1} {R : Type u_2} [comm_ring R] {Ms : ι Type u_3} [Π (i : ι), add_comm_group (Ms i)] [Π (i : ι), (Ms i)] {N : Type u_4} [ N] [fintype ι] [decidable_eq ι] (p : Π (i : ι), (Ms i)) (q : 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
• hf = (λ (i : ι), Ms i p i) R) (λ (i : ι), (p i).mapq q (f i) _)
@[simp]
theorem submodule.pi_quotient_lift_mk {ι : Type u_1} {R : Type u_2} [comm_ring R] {Ms : ι Type u_3} [Π (i : ι), add_comm_group (Ms i)] [Π (i : ι), (Ms i)] {N : Type u_4} [ N] [fintype ι] [decidable_eq ι] (p : Π (i : ι), (Ms i)) (q : N) (f : Π (i : ι), Ms i →ₗ[R] N) (hf : (i : ι), p i submodule.comap (f i) q) (x : Π (i : ι), Ms i) :
hf) (λ (i : ι), submodule.quotient.mk (x i)) = submodule.quotient.mk (( (λ (i : ι), Ms i) R) f) x)
@[simp]
theorem submodule.pi_quotient_lift_single {ι : Type u_1} {R : Type u_2} [comm_ring R] {Ms : ι Type u_3} [Π (i : ι), add_comm_group (Ms i)] [Π (i : ι), (Ms i)] {N : Type u_4} [ N] [fintype ι] [decidable_eq ι] (p : Π (i : ι), (Ms i)) (q : N) (f : Π (i : ι), Ms i →ₗ[R] N) (hf : (i : ι), p i submodule.comap (f i) q) (i : ι) (x : Ms i p i) :
hf) x) = ((p i).mapq q (f i) _) x
def submodule.quotient_pi_lift {ι : Type u_1} {R : Type u_2} [comm_ring R] {Ms : ι Type u_3} [Π (i : ι), add_comm_group (Ms i)] [Π (i : ι), (Ms i)] {Ns : ι Type u_5} [Π (i : ι), add_comm_group (Ns i)] [Π (i : ι), (Ns i)] (p : Π (i : ι), (Ms i)) (f : Π (i : ι), Ms i →ₗ[R] Ns i) (hf : (i : ι), p i linear_map.ker (f i)) :
(Π (i : ι), Ms i) →ₗ[R] Π (i : ι), Ns i

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

Equations
@[simp]
theorem submodule.quotient_pi_lift_mk {ι : Type u_1} {R : Type u_2} [comm_ring R] {Ms : ι Type u_3} [Π (i : ι), add_comm_group (Ms i)] [Π (i : ι), (Ms i)] {Ns : ι Type u_5} [Π (i : ι), add_comm_group (Ns i)] [Π (i : ι), (Ns i)] (p : Π (i : ι), (Ms i)) (f : Π (i : ι), Ms i →ₗ[R] Ns i) (hf : (i : ι), p i linear_map.ker (f i)) (x : Π (i : ι), Ms i) :
hf) = λ (i : ι), (f i) (x i)
@[simp]
theorem submodule.quotient_pi_apply {ι : Type u_1} {R : Type u_2} [comm_ring R] {Ms : ι Type u_3} [Π (i : ι), add_comm_group (Ms i)] [Π (i : ι), (Ms i)] [fintype ι] [decidable_eq ι] (p : Π (i : ι), (Ms i)) (ᾰ : (Π (i : ι), (λ (i : ι), Ms i) i) ) (i : ι) :
i = (λ (i : ι), (p i).mkq) _) i
@[simp]
theorem submodule.quotient_pi_symm_apply {ι : Type u_1} {R : Type u_2} [comm_ring R] {Ms : ι Type u_3} [Π (i : ι), add_comm_group (Ms i)] [Π (i : ι), (Ms i)] [fintype ι] [decidable_eq ι] (p : Π (i : ι), (Ms i)) (ᾰ : Π (i : ι), (λ (i : ι), Ms i) i p i) :
.symm) =
def submodule.quotient_pi {ι : Type u_1} {R : Type u_2} [comm_ring R] {Ms : ι Type u_3} [Π (i : ι), add_comm_group (Ms i)] [Π (i : ι), (Ms i)] [fintype ι] [decidable_eq ι] (p : Π (i : ι), (Ms i)) :
((Π (i : ι), Ms i) ≃ₗ[R] Π (i : ι), Ms i p i

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

Equations