Quotients by submodules #
- 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 y - x ∈ p.
@[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} :
M → M ⧸ p
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, 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.has_quotient.quotient.has_add
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
Equations
- submodule.quotient.has_quotient.quotient.has_add p = {add := λ (a b : M ⧸ p), quotient.lift_on₂' a b (λ (a b : M), submodule.quotient.mk (a + b)) _}
@[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) :
@[protected, instance]
def
submodule.quotient.has_quotient.quotient.has_neg
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
Equations
- submodule.quotient.has_quotient.quotient.has_neg p = {neg := λ (a : M ⧸ p), quotient.lift_on' a (λ (a : M), submodule.quotient.mk (-a)) _}
@[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) :
@[protected, instance]
def
submodule.quotient.has_quotient.quotient.has_sub
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M) :
Equations
- submodule.quotient.has_quotient.quotient.has_sub p = {sub := λ (a b : M ⧸ p), quotient.lift_on₂' a b (λ (a b : M), submodule.quotient.mk (a - b)) _}
@[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.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)
Equations
- submodule.quotient.add_comm_group p = {add := has_add.add (submodule.quotient.has_quotient.quotient.has_add p), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (x : M ⧸ p), quotient.lift_on' x (λ (x : M), submodule.quotient.mk (n • x)) _, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (submodule.quotient.has_quotient.quotient.has_neg p), sub := has_sub.sub (submodule.quotient.has_quotient.quotient.has_sub p), sub_eq_add_neg := _, zsmul := λ (n : ℤ) (x : M ⧸ p), quotient.lift_on' x (λ (x : M), submodule.quotient.mk (n • x)) _, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected, instance]
def
submodule.quotient.has_scalar'
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{S : Type u_3}
[has_scalar S R]
[has_scalar S M]
[is_scalar_tower S R M]
(P : submodule R M) :
has_scalar S (M ⧸ P)
Equations
- submodule.quotient.has_scalar' P = {smul := λ (a : S), quotient.map' (has_scalar.smul a) _}
@[protected, instance]
def
submodule.quotient.has_scalar
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(P : submodule R M) :
has_scalar R (M ⧸ P)
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_scalar S R]
[has_scalar 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_scalar S R]
[has_scalar S M]
[is_scalar_tower S R M]
(P : submodule R M)
(T : Type u_4)
[has_scalar T R]
[has_scalar 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_scalar S R]
[has_scalar S M]
[is_scalar_tower S R M]
(P : submodule R M)
(T : Type u_4)
[has_scalar T R]
[has_scalar T M]
[is_scalar_tower T R M]
[has_scalar 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_scalar S R]
[has_scalar S M]
[is_scalar_tower S R M]
(P : submodule R M)
[has_scalar Sᵐᵒᵖ R]
[has_scalar 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_scalar 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.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_scalar 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_scalar 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_scalar 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_scalar 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_scalar 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)
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
@[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 ≤ f.ker) :
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.
@[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 ≤ f.ker}
(x : M) :
⇑(p.liftq f h) (submodule.quotient.mk x) = ⇑f x
@[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) :
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'
@[simp]
theorem
submodule.map_mkq_eq_top
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M) :
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.mapq_pow
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p : submodule R M)
{f : M →ₗ[R] M}
(h : p ≤ submodule.comap f p)
(k : ℕ)
(h' : p ≤ submodule.comap (f ^ k) p := _) :
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 ≤ f.ker) :
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 ≤ f.ker)
(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 ≤ f.ker) :
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 ≤ f.ker) :
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 ⊆ ↑(f.range)) :
submodule.span R (⇑f ⁻¹' s) = submodule.comap f (submodule.span R₂ s)
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₂) :
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₃} :
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₂ ⧸ f.range), 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
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' := _}