mathlib3 documentation

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 #

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 : ι), module R (Ms i)] {N : Type u_4} [add_comm_group N] [module R N] [fintype ι] [decidable_eq ι] (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
@[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 : ι), module R (Ms i)] {N : Type u_4} [add_comm_group N] [module R N] [fintype ι] [decidable_eq ι] (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.pi_quotient_lift p q f hf) (λ (i : ι), submodule.quotient.mk (x i)) = submodule.quotient.mk (((linear_map.lsum R (λ (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 : ι), module R (Ms i)] {N : Type u_4} [add_comm_group N] [module R N] [fintype ι] [decidable_eq ι] (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.pi_quotient_lift p q f hf) (pi.single i 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 : ι), module R (Ms i)] {Ns : ι Type u_5} [Π (i : ι), add_comm_group (Ns i)] [Π (i : ι), module R (Ns i)] (p : Π (i : ι), submodule R (Ms i)) (f : Π (i : ι), Ms i →ₗ[R] Ns i) (hf : (i : ι), p i linear_map.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
@[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 : ι), module R (Ms i)] {Ns : ι Type u_5} [Π (i : ι), add_comm_group (Ns i)] [Π (i : ι), module R (Ns i)] (p : Π (i : ι), submodule R (Ms i)) (f : Π (i : ι), Ms i →ₗ[R] Ns i) (hf : (i : ι), p i linear_map.ker (f i)) (x : Π (i : ι), Ms i) :
(submodule.quotient_pi_lift p f hf) (submodule.quotient.mk x) = λ (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 : ι), module R (Ms i)] [fintype ι] [decidable_eq ι] (p : Π (i : ι), submodule R (Ms i)) (ᾰ : (Π (i : ι), (λ (i : ι), Ms i) i) submodule.pi set.univ p) (i : ι) :
(submodule.quotient_pi p) i = (submodule.quotient_pi_lift p (λ (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 : ι), module R (Ms i)] [fintype ι] [decidable_eq ι] (p : Π (i : ι), submodule R (Ms i)) (ᾰ : Π (i : ι), (λ (i : ι), Ms i) i p i) :
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 : ι), module R (Ms i)] [fintype ι] [decidable_eq ι] (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