Isomorphism theorems for modules. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
- 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_quotientandsubmodule.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.
theorem
submodule.card_quotient_mul_card_quotient
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
(S T : submodule R M)
(hST : T ≤ S)
[decidable_pred (λ (x : M ⧸ T), x ∈ submodule.map T.mkq S)]
[fintype (M ⧸ S)]
[fintype (M ⧸ T)] :
fintype.card ↥(submodule.map T.mkq S) * fintype.card (M ⧸ S) = fintype.card (M ⧸ T)
Corollary of the third isomorphism theorem: [S : T] [M : S] = [M : T]