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 quotientssubmodule.quotient_pi_lift: create a map out of the quotient of a direct sumsubmodule.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 : ι), 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) :
Lift a family of maps to the direct sum of quotients.
Equations
- submodule.pi_quotient_lift p q f hf = ⇑(linear_map.lsum R (λ (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 : ι), 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) :
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)) :
Lift a family of maps to a quotient of direct sums.
Equations
- submodule.quotient_pi_lift p f hf = (submodule.pi set.univ p).liftq (linear_map.pi (λ (i : ι), (f i).comp (linear_map.proj i))) _
@[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) :
⇑((submodule.quotient_pi p).symm) ᾰ = ⇑(submodule.pi_quotient_lift p (submodule.pi set.univ p) linear_map.single _) ᾰ
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)) :
The quotient of a direct sum is the direct sum of quotients.
Equations
- submodule.quotient_pi p = {to_fun := ⇑(submodule.quotient_pi_lift p (λ (i : ι), (p i).mkq) _), map_add' := _, map_smul' := _, inv_fun := ⇑(submodule.pi_quotient_lift p (submodule.pi set.univ p) linear_map.single _), left_inv := _, right_inv := _}