Isomorphism theorems for modules. #
- The Noether's first, second, and third isomorphism theorems for modules are proved as
linear_map.quot_ker_equiv_range
,linear_map.quotient_inf_equiv_sup_quotient
andsubmodule.quotient_quotient_equiv_quotient
.
The first and second isomorphism theorems for modules.
noncomputable
def
linear_map.quot_ker_equiv_range
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂) :
(M ⧸ linear_map.ker f) ≃ₗ[R] ↥(linear_map.range f)
The first isomorphism law for modules. The quotient of M
by the kernel of f
is linearly
equivalent to the range of f
.
Equations
- f.quot_ker_equiv_range = (linear_equiv.of_injective ((linear_map.ker f).liftq f _) _).trans (linear_equiv.of_eq (linear_map.range ((linear_map.ker f).liftq f _)) (linear_map.range f) _)
noncomputable
def
linear_map.quot_ker_equiv_of_surjective
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂)
(hf : function.surjective ⇑f) :
(M ⧸ linear_map.ker f) ≃ₗ[R] M₂
The first isomorphism theorem for surjective linear maps.
Equations
@[simp]
theorem
linear_map.quot_ker_equiv_range_apply_mk
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂)
(x : M) :
↑(⇑(f.quot_ker_equiv_range) (submodule.quotient.mk x)) = ⇑f x
@[simp]
theorem
linear_map.quot_ker_equiv_range_symm_apply_image
{R : Type u_1}
{M : Type u_2}
{M₂ : Type u_3}
[ring R]
[add_comm_group M]
[add_comm_group M₂]
[module R M]
[module R M₂]
(f : M →ₗ[R] M₂)
(x : M)
(h : ⇑f x ∈ linear_map.range f) :
⇑(f.quot_ker_equiv_range.symm) ⟨⇑f x, h⟩ = ⇑((linear_map.ker f).mkq) x
def
linear_map.quotient_inf_to_sup_quotient
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M) :
Canonical linear map from the quotient p/(p ∩ p')
to (p+p')/p'
, mapping x + (p ∩ p')
to x + p'
, where p
and p'
are submodules of an ambient module.
Equations
- linear_map.quotient_inf_to_sup_quotient p p' = (submodule.comap p.subtype (p ⊓ p')).liftq ((submodule.comap (p ⊔ p').subtype p').mkq.comp (submodule.of_le _)) _
noncomputable
def
linear_map.quotient_inf_equiv_sup_quotient
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M) :
Second Isomorphism Law : the canonical map from p/(p ∩ p')
to (p+p')/p'
as a linear isomorphism.
Equations
@[simp]
theorem
linear_map.coe_quotient_inf_to_sup_quotient
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M) :
@[simp]
theorem
linear_map.quotient_inf_equiv_sup_quotient_apply_mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M)
(x : ↥p) :
theorem
linear_map.quotient_inf_equiv_sup_quotient_symm_apply_left
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M)
(x : ↥(p ⊔ p'))
(hx : ↑x ∈ p) :
⇑((linear_map.quotient_inf_equiv_sup_quotient p p').symm) (submodule.quotient.mk x) = submodule.quotient.mk ⟨↑x, hx⟩
@[simp]
theorem
linear_map.quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
{p p' : submodule R M}
{x : ↥(p ⊔ p')} :
⇑((linear_map.quotient_inf_equiv_sup_quotient p p').symm) (submodule.quotient.mk x) = 0 ↔ ↑x ∈ p'
theorem
linear_map.quotient_inf_equiv_sup_quotient_symm_apply_right
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(p p' : submodule R M)
{x : ↥(p ⊔ p')}
(hx : ↑x ∈ p') :
⇑((linear_map.quotient_inf_equiv_sup_quotient p p').symm) (submodule.quotient.mk x) = 0
The third isomorphism theorem for modules.
def
submodule.quotient_quotient_equiv_quotient_aux
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(S T : submodule R M)
(h : S ≤ T) :
The map from the third isomorphism theorem for modules: (M / S) / (T / S) → M / T
.
Equations
- S.quotient_quotient_equiv_quotient_aux T h = (submodule.map S.mkq T).liftq (S.mapq T linear_map.id h) _
@[simp]
theorem
submodule.quotient_quotient_equiv_quotient_aux_mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(S T : submodule R M)
(h : S ≤ T)
(x : M ⧸ S) :
⇑(S.quotient_quotient_equiv_quotient_aux T h) (submodule.quotient.mk x) = ⇑(S.mapq T linear_map.id h) x
@[simp]
theorem
submodule.quotient_quotient_equiv_quotient_aux_mk_mk
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(S T : submodule R M)
(h : S ≤ T)
(x : M) :
def
submodule.quotient_quotient_equiv_quotient
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(S T : submodule R M)
(h : S ≤ T) :
Noether's third isomorphism theorem for modules: (M / S) / (T / S) ≃ M / T
.