Quotients by submodules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
- If
pis a submodule ofM,M ⧸ pis the quotient ofMwith respect top: that is, elements ofMare identified if their difference is inp. This is itself a module.
def
submodule.quotient_rel
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
setoid M
The equivalence relation associated to a submodule p, defined by x ≈ y iff -x + y ∈ p.
Note this is equivalent to y - x ∈ p, but defined this way to be be defeq to the add_subgroup
version, where commutativity can't be assumed.
Equations
@[protected, instance]
def
submodule.has_quotient
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M] :
has_quotient M (submodule R M)
The quotient of a module M by a submodule p ⊆ M.
Equations
- submodule.has_quotient = {quotient' := λ (p : submodule R M), quotient p.quotient_rel}
def
submodule.quotient.mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{p : submodule R M} :
Map associating to an element of M the corresponding element of M/p,
when p is a submodule of M.
Equations
@[simp]
theorem
submodule.quotient.mk_eq_mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{p : submodule R M}
(x : M) :
@[simp]
theorem
submodule.quotient.mk'_eq_mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{p : submodule R M}
(x : M) :
@[simp]
theorem
submodule.quotient.quot_mk_eq_mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{p : submodule R M}
(x : M) :
quot.mk setoid.r x = submodule.quotient.mk x
@[protected]
theorem
submodule.quotient.eq'
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{x y : M} :
submodule.quotient.mk x = submodule.quotient.mk y ↔ -x + y ∈ p
@[protected]
theorem
submodule.quotient.eq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{x y : M} :
submodule.quotient.mk x = submodule.quotient.mk y ↔ x - y ∈ p
@[protected, instance]
def
submodule.quotient.has_quotient.quotient.has_zero
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
Equations
@[protected, instance]
def
submodule.quotient.has_quotient.quotient.inhabited
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
Equations
@[simp]
theorem
submodule.quotient.mk_zero
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
@[simp]
theorem
submodule.quotient.mk_eq_zero
{R : Type u_1}
{M : Type u_2}
{x : M}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
submodule.quotient.mk x = 0 ↔ x ∈ p
@[protected, instance]
def
submodule.quotient.add_comm_group
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
add_comm_group (M ⧸ p)
@[simp]
theorem
submodule.quotient.mk_add
{R : Type u_1}
{M : Type u_2}
{x y : M}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
@[simp]
theorem
submodule.quotient.mk_neg
{R : Type u_1}
{M : Type u_2}
{x : M}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
@[simp]
theorem
submodule.quotient.mk_sub
{R : Type u_1}
{M : Type u_2}
{x y : M}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
@[protected, instance]
def
submodule.quotient.has_smul'
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{S : Type u_3}
[has_smul S R]
[has_smul S M]
[is_scalar_tower S R M]
(P : submodule R M) :
Equations
- submodule.quotient.has_smul' P = {smul := λ (a : S), quotient.map' (has_smul.smul a) _}
@[protected, instance]
def
submodule.quotient.has_smul
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(P : submodule R M) :
Shortcut to help the elaborator in the common case.
Equations
@[simp]
theorem
submodule.quotient.mk_smul
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{S : Type u_3}
[has_smul S R]
[has_smul S M]
[is_scalar_tower S R M]
(r : S)
(x : M) :
submodule.quotient.mk (r • x) = r • submodule.quotient.mk x
@[protected, instance]
def
submodule.quotient.smul_comm_class
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{S : Type u_3}
[has_smul S R]
[has_smul S M]
[is_scalar_tower S R M]
(P : submodule R M)
(T : Type u_4)
[has_smul T R]
[has_smul T M]
[is_scalar_tower T R M]
[smul_comm_class S T M] :
smul_comm_class S T (M ⧸ P)
@[protected, instance]
def
submodule.quotient.is_scalar_tower
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{S : Type u_3}
[has_smul S R]
[has_smul S M]
[is_scalar_tower S R M]
(P : submodule R M)
(T : Type u_4)
[has_smul T R]
[has_smul T M]
[is_scalar_tower T R M]
[has_smul S T]
[is_scalar_tower S T M] :
is_scalar_tower S T (M ⧸ P)
@[protected, instance]
def
submodule.quotient.is_central_scalar
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{S : Type u_3}
[has_smul S R]
[has_smul S M]
[is_scalar_tower S R M]
(P : submodule R M)
[has_smul Sᵐᵒᵖ R]
[has_smul Sᵐᵒᵖ M]
[is_scalar_tower Sᵐᵒᵖ R M]
[is_central_scalar S M] :
is_central_scalar S (M ⧸ P)
@[protected, instance]
def
submodule.quotient.mul_action'
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{S : Type u_3}
[monoid S]
[has_smul S R]
[mul_action S M]
[is_scalar_tower S R M]
(P : submodule R M) :
mul_action S (M ⧸ P)
@[protected, instance]
def
submodule.quotient.mul_action
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(P : submodule R M) :
mul_action R (M ⧸ P)
Equations
@[protected, instance]
def
submodule.quotient.smul_zero_class'
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{S : Type u_3}
[has_smul S R]
[smul_zero_class S M]
[is_scalar_tower S R M]
(P : submodule R M) :
smul_zero_class S (M ⧸ P)
Equations
@[protected, instance]
def
submodule.quotient.smul_zero_class
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(P : submodule R M) :
smul_zero_class R (M ⧸ P)
@[protected, instance]
def
submodule.quotient.distrib_smul'
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{S : Type u_3}
[has_smul S R]
[distrib_smul S M]
[is_scalar_tower S R M]
(P : submodule R M) :
distrib_smul S (M ⧸ P)
Equations
- submodule.quotient.distrib_smul' P = function.surjective.distrib_smul {to_fun := submodule.quotient.mk P, map_zero' := _, map_add' := _} _ _
@[protected, instance]
def
submodule.quotient.distrib_smul
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(P : submodule R M) :
distrib_smul R (M ⧸ P)
Equations
@[protected, instance]
def
submodule.quotient.distrib_mul_action'
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{S : Type u_3}
[monoid S]
[has_smul S R]
[distrib_mul_action S M]
[is_scalar_tower S R M]
(P : submodule R M) :
distrib_mul_action S (M ⧸ P)
Equations
@[protected, instance]
def
submodule.quotient.distrib_mul_action
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(P : submodule R M) :
distrib_mul_action R (M ⧸ P)
@[protected, instance]
def
submodule.quotient.module'
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{S : Type u_3}
[semiring S]
[has_smul S R]
[module S M]
[is_scalar_tower S R M]
(P : submodule R M) :
Equations
- submodule.quotient.module' P = function.surjective.module S {to_fun := submodule.quotient.mk P, map_zero' := _, map_add' := _} _ _
@[protected, instance]
def
submodule.quotient.module
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(P : submodule R M) :
Equations
def
submodule.quotient.restrict_scalars_equiv
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(S : Type u_3)
[ring S]
[has_smul S R]
[module S M]
[is_scalar_tower S R M]
(P : submodule R M) :
(M ⧸ submodule.restrict_scalars S P) ≃ₗ[S] M ⧸ P
The quotient of P as an S-submodule is the same as the quotient of P as an R-submodule,
where P : submodule R M.
Equations
- submodule.quotient.restrict_scalars_equiv S P = {to_fun := (quotient.congr_right _).to_fun, map_add' := _, map_smul' := _, inv_fun := (quotient.congr_right _).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
submodule.quotient.restrict_scalars_equiv_mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(S : Type u_3)
[ring S]
[has_smul S R]
[module S M]
[is_scalar_tower S R M]
(P : submodule R M)
(x : M) :
@[simp]
theorem
submodule.quotient.restrict_scalars_equiv_symm_mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(S : Type u_3)
[ring S]
[has_smul S R]
[module S M]
[is_scalar_tower S R M]
(P : submodule R M)
(x : M) :
theorem
submodule.quotient.mk_surjective
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
theorem
submodule.quotient.nontrivial_of_lt_top
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(h : p < ⊤) :
nontrivial (M ⧸ p)
@[protected, instance]
def
submodule.quotient_top.unique
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M] :
Equations
- submodule.quotient_top.unique = {to_inhabited := {default := 0}, uniq := _}
@[protected, instance]
def
submodule.quotient_top.fintype
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M] :
Equations
theorem
submodule.subsingleton_quotient_iff_eq_top
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{p : submodule R M} :
subsingleton (M ⧸ p) ↔ p = ⊤
@[protected, instance]
noncomputable
def
submodule.quotient.fintype
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[fintype M]
(S : submodule R M) :
Equations
theorem
submodule.card_eq_card_quotient_mul_card
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[fintype M]
(S : submodule R M)
[decidable_pred (λ (_x : M), _x ∈ S)] :
fintype.card M = fintype.card ↥S * fintype.card (M ⧸ S)
theorem
submodule.quot_hom_ext
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{M₂ : Type u_3}
[add_comm_group M₂]
[module R M₂]
⦃f g : M ⧸ p →ₗ[R] M₂⦄
(h : ∀ (x : M), ⇑f (submodule.quotient.mk x) = ⇑g (submodule.quotient.mk x)) :
f = g
@[simp]
theorem
submodule.mkq_apply
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(x : M) :
⇑(p.mkq) x = submodule.quotient.mk x
theorem
submodule.mkq_surjective
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(A : submodule R M) :
@[ext]
theorem
submodule.linear_map_qext
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
⦃f g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄
(h : f.comp p.mkq = g.comp p.mkq) :
f = g
Two linear_maps from a quotient module are equal if their compositions with
submodule.mkq are equal.
def
submodule.liftq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f : M →ₛₗ[τ₁₂] M₂)
(h : p ≤ linear_map.ker f) :
The map from the quotient of M by a submodule p to M₂ induced by a linear map f : M → M₂
vanishing on p, as a linear map.
Equations
- p.liftq f h = {to_fun := (quotient_add_group.lift p.to_add_subgroup f.to_add_monoid_hom h).to_fun, map_add' := _, map_smul' := _}
@[simp]
theorem
submodule.liftq_apply
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f : M →ₛₗ[τ₁₂] M₂)
{h : p ≤ linear_map.ker f}
(x : M) :
⇑(p.liftq f h) (submodule.quotient.mk x) = ⇑f x
@[simp]
def
submodule.liftq_span_singleton
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(x : M)
(f : M →ₛₗ[τ₁₂] M₂)
(h : ⇑f x = 0) :
M ⧸ submodule.span R {x} →ₛₗ[τ₁₂] M₂
Special case of liftq when p is the span of x. In this case, the condition on f simply
becomes vanishing at x.
Equations
- submodule.liftq_span_singleton x f h = (submodule.span R {x}).liftq f _
@[simp]
theorem
submodule.liftq_span_singleton_apply
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(x : M)
(f : M →ₛₗ[τ₁₂] M₂)
(h : ⇑f x = 0)
(y : M) :
⇑(submodule.liftq_span_singleton x f h) (submodule.quotient.mk y) = ⇑f y
@[simp]
theorem
submodule.range_mkq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
@[simp]
theorem
submodule.ker_mkq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
linear_map.ker p.mkq = p
theorem
submodule.le_comap_mkq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(p' : submodule R (M ⧸ p)) :
p ≤ submodule.comap p.mkq p'
@[simp]
theorem
submodule.mkq_map_self
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
submodule.map p.mkq p = ⊥
@[simp]
theorem
submodule.comap_map_mkq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M) :
submodule.comap p.mkq (submodule.map p.mkq p') = p ⊔ p'
def
submodule.mapq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(q : submodule R₂ M₂)
(f : M →ₛₗ[τ₁₂] M₂)
(h : p ≤ submodule.comap f q) :
The map from the quotient of M by submodule p to the quotient of M₂ by submodule q along
f : M → M₂ is linear.
@[simp]
theorem
submodule.mapq_apply
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(q : submodule R₂ M₂)
(f : M →ₛₗ[τ₁₂] M₂)
{h : p ≤ submodule.comap f q}
(x : M) :
⇑(p.mapq q f h) (submodule.quotient.mk x) = submodule.quotient.mk (⇑f x)
theorem
submodule.mapq_mkq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(q : submodule R₂ M₂)
(f : M →ₛₗ[τ₁₂] M₂)
{h : p ≤ submodule.comap f q} :
@[simp]
theorem
submodule.mapq_zero
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(q : submodule R₂ M₂)
(h : p ≤ submodule.comap 0 q := _) :
theorem
submodule.mapq_comp
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
{R₃ : Type u_5}
{M₃ : Type u_6}
[ring R₃]
[add_comm_group M₃]
[module R₃ M₃]
(p₂ : submodule R₂ M₂)
(p₃ : submodule R₃ M₃)
{τ₂₃ : R₂ →+* R₃}
{τ₁₃ : R →+* R₃}
[ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃]
(f : M →ₛₗ[τ₁₂] M₂)
(g : M₂ →ₛₗ[τ₂₃] M₃)
(hf : p ≤ submodule.comap f p₂)
(hg : p₂ ≤ submodule.comap g p₃)
(h : p ≤ submodule.comap f (submodule.comap g p₃) := _) :
Given submodules p ⊆ M, p₂ ⊆ M₂, p₃ ⊆ M₃ and maps f : M → M₂, g : M₂ → M₃ inducing
mapq f : M ⧸ p → M₂ ⧸ p₂ and mapq g : M₂ ⧸ p₂ → M₃ ⧸ p₃ then
mapq (g ∘ f) = (mapq g) ∘ (mapq f).
@[simp]
theorem
submodule.mapq_id
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(h : p ≤ submodule.comap linear_map.id p := _) :
p.mapq p linear_map.id h = linear_map.id
theorem
submodule.comap_liftq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(q : submodule R₂ M₂)
(f : M →ₛₗ[τ₁₂] M₂)
(h : p ≤ linear_map.ker f) :
submodule.comap (p.liftq f h) q = submodule.map p.mkq (submodule.comap f q)
theorem
submodule.map_liftq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
(h : p ≤ linear_map.ker f)
(q : submodule R (M ⧸ p)) :
submodule.map (p.liftq f h) q = submodule.map f (submodule.comap p.mkq q)
theorem
submodule.ker_liftq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f : M →ₛₗ[τ₁₂] M₂)
(h : p ≤ linear_map.ker f) :
linear_map.ker (p.liftq f h) = submodule.map p.mkq (linear_map.ker f)
theorem
submodule.range_liftq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
(h : p ≤ linear_map.ker f) :
linear_map.range (p.liftq f h) = linear_map.range f
theorem
submodule.ker_liftq_eq_bot
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f : M →ₛₗ[τ₁₂] M₂)
(h : p ≤ linear_map.ker f)
(h' : linear_map.ker f ≤ p) :
linear_map.ker (p.liftq f h) = ⊥
def
submodule.comap_mkq.rel_iso
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
The correspondence theorem for modules: there is an order isomorphism between submodules of the
quotient of M by p, and submodules of M larger than p.
Equations
- submodule.comap_mkq.rel_iso p = {to_equiv := {to_fun := λ (p' : submodule R (M ⧸ p)), ⟨submodule.comap p.mkq p', _⟩, inv_fun := λ (q : {p' // p ≤ p'}), submodule.map p.mkq ↑q, left_inv := _, right_inv := _}, map_rel_iff' := _}
def
submodule.comap_mkq.order_embedding
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
The ordering on submodules of the quotient of M by p embeds into the ordering on submodules
of M.
Equations
- submodule.comap_mkq.order_embedding p = (rel_iso.to_rel_embedding (submodule.comap_mkq.rel_iso p)).trans (subtype.rel_embedding has_le.le (λ (p' : submodule R M), p ≤ p'))
@[simp]
theorem
submodule.comap_mkq_embedding_eq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(p' : submodule R (M ⧸ p)) :
⇑(submodule.comap_mkq.order_embedding p) p' = submodule.comap p.mkq p'
theorem
submodule.span_preimage_eq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R₂]
[add_comm_group M₂]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
{f : M →ₛₗ[τ₁₂] M₂}
{s : set M₂}
(h₀ : s.nonempty)
(h₁ : s ⊆ ↑(linear_map.range f)) :
submodule.span R (⇑f ⁻¹' s) = submodule.comap f (submodule.span R₂ s)
@[simp]
theorem
submodule.quotient.equiv_symm_apply
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{N : Type u_3}
[add_comm_group N]
[module R N]
(P : submodule R M)
(Q : submodule R N)
(f : M ≃ₗ[R] N)
(hf : submodule.map f P = Q)
(ᾰ : N ⧸ Q) :
def
submodule.quotient.equiv
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{N : Type u_3}
[add_comm_group N]
[module R N]
(P : submodule R M)
(Q : submodule R N)
(f : M ≃ₗ[R] N)
(hf : submodule.map f P = Q) :
If P is a submodule of M and Q a submodule of N,
and f : M ≃ₗ N maps P to Q, then M ⧸ P is equivalent to N ⧸ Q.
@[simp]
theorem
submodule.quotient.equiv_apply
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{N : Type u_3}
[add_comm_group N]
[module R N]
(P : submodule R M)
(Q : submodule R N)
(f : M ≃ₗ[R] N)
(hf : submodule.map f P = Q)
(ᾰ : M ⧸ P) :
@[simp]
theorem
submodule.quotient.equiv_symm
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[comm_ring R]
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
(P : submodule R M)
(Q : submodule R N)
(f : M ≃ₗ[R] N)
(hf : submodule.map f P = Q) :
(submodule.quotient.equiv P Q f hf).symm = submodule.quotient.equiv Q P f.symm _
@[simp]
theorem
submodule.quotient.equiv_trans
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{N : Type u_3}
{O : Type u_4}
[add_comm_group N]
[module R N]
[add_comm_group O]
[module R O]
(P : submodule R M)
(Q : submodule R N)
(S : submodule R O)
(e : M ≃ₗ[R] N)
(f : N ≃ₗ[R] O)
(he : submodule.map e P = Q)
(hf : submodule.map f Q = S)
(hef : submodule.map (e.trans f) P = S) :
submodule.quotient.equiv P S (e.trans f) hef = (submodule.quotient.equiv P Q e he).trans (submodule.quotient.equiv Q S f hf)
theorem
linear_map.range_mkq_comp
{R : Type u_1}
{M : Type u_2}
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R]
[ring R₂]
[add_comm_monoid M]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂) :
(linear_map.range f).mkq.comp f = 0
theorem
linear_map.ker_le_range_iff
{R : Type u_1}
{M : Type u_2}
{R₂ : Type u_3}
{M₂ : Type u_4}
{R₃ : Type u_5}
{M₃ : Type u_6}
[ring R]
[ring R₂]
[ring R₃]
[add_comm_monoid M]
[add_comm_group M₂]
[add_comm_monoid M₃]
[module R M]
[module R₂ M₂]
[module R₃ M₃]
{τ₁₂ : R →+* R₂}
{τ₂₃ : R₂ →+* R₃}
[ring_hom_surjective τ₁₂]
{f : M →ₛₗ[τ₁₂] M₂}
{g : M₂ →ₛₗ[τ₂₃] M₃} :
linear_map.ker g ≤ linear_map.range f ↔ (linear_map.range f).mkq.comp (linear_map.ker g).subtype = 0
theorem
linear_map.range_eq_top_of_cancel
{R : Type u_1}
{M : Type u_2}
{R₂ : Type u_3}
{M₂ : Type u_4}
[ring R]
[ring R₂]
[add_comm_monoid M]
[add_comm_group M₂]
[module R M]
[module R₂ M₂]
{τ₁₂ : R →+* R₂}
[ring_hom_surjective τ₁₂]
{f : M →ₛₗ[τ₁₂] M₂}
(h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ linear_map.range f), u.comp f = v.comp f → u = v) :
An epimorphism is surjective.
def
submodule.quot_equiv_of_eq_bot
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(hp : p = ⊥) :
If p = ⊥, then M / p ≃ₗ[R] M.
Equations
- p.quot_equiv_of_eq_bot hp = linear_equiv.of_linear (p.liftq linear_map.id _) p.mkq _ _
@[simp]
theorem
submodule.quot_equiv_of_eq_bot_apply_mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(hp : p = ⊥)
(x : M) :
⇑(p.quot_equiv_of_eq_bot hp) (submodule.quotient.mk x) = x
@[simp]
theorem
submodule.quot_equiv_of_eq_bot_symm_apply
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(hp : p = ⊥)
(x : M) :
⇑((p.quot_equiv_of_eq_bot hp).symm) x = submodule.quotient.mk x
@[simp]
theorem
submodule.coe_quot_equiv_of_eq_bot_symm
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
(hp : p = ⊥) :
↑((p.quot_equiv_of_eq_bot hp).symm) = p.mkq
def
submodule.quot_equiv_of_eq
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M)
(h : p = p') :
Quotienting by equal submodules gives linearly equivalent quotients.
Equations
- p.quot_equiv_of_eq p' h = {to_fun := (quotient.congr (equiv.refl M) _).to_fun, map_add' := _, map_smul' := _, inv_fun := (quotient.congr (equiv.refl M) _).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
submodule.quot_equiv_of_eq_mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M)
(h : p = p')
(x : M) :
⇑(p.quot_equiv_of_eq p' h) (submodule.quotient.mk x) = submodule.quotient.mk x
@[simp]
theorem
submodule.quotient.equiv_refl
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(P Q : submodule R M)
(hf : submodule.map ↑(linear_equiv.refl R M) P = Q) :
submodule.quotient.equiv P Q (linear_equiv.refl R M) hf = P.quot_equiv_of_eq Q _
def
submodule.mapq_linear
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[comm_ring R]
[add_comm_group M]
[module R M]
[add_comm_group M₂]
[module R M₂]
(p : submodule R M)
(q : submodule R M₂) :
Given modules M, M₂ over a commutative ring, together with submodules p ⊆ M, q ⊆ M₂,
the natural map $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \} \to Hom(M/p, M₂/q)$ is linear.
Equations
- p.mapq_linear q = {to_fun := λ (f : ↥(p.compatible_maps q)), p.mapq q f.val _, map_add' := _, map_smul' := _}