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 and submodule.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 ⧸ f.ker) ≃ₗ[R] ↥(f.range)

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 (f.ker.liftq f _) _).trans (linear_equiv.of_eq (f.ker.liftq f _).range f.range _)

source

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 ⧸ f.ker) ≃ₗ[R] M₂

The first isomorphism theorem for surjective linear maps.

Equations

f.quot_ker_equiv_of_surjective hf = f.quot_ker_equiv_range.trans (linear_equiv.of_top f.range _)

source

@[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

source

@[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 ∈ f.range) :

⇑(f.quot_ker_equiv_range.symm) ⟨⇑f x, h⟩ = ⇑(f.ker.mkq) x

source

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) :

↥p ⧸ submodule.comap p.subtype (p ⊓ p') →ₗ[R] ↥(p ⊔ p') ⧸ submodule.comap (p ⊔ p').subtype p'

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 _)) _

source

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) :

(↥p ⧸ submodule.comap p.subtype (p ⊓ p')) ≃ₗ[R] ↥(p ⊔ p') ⧸ submodule.comap (p ⊔ p').subtype p'

Second Isomorphism Law : the canonical map from p/(p ∩ p') to (p+p')/p' as a linear isomorphism.

Equations

linear_map.quotient_inf_equiv_sup_quotient p p' = linear_equiv.of_bijective (linear_map.quotient_inf_to_sup_quotient p p') _ _

source

@[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) :

⇑(linear_map.quotient_inf_to_sup_quotient p p') = ⇑(linear_map.quotient_inf_equiv_sup_quotient p p')

source

@[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) :

⇑(linear_map.quotient_inf_equiv_sup_quotient p p') (submodule.quotient.mk x) = submodule.quotient.mk (⇑(submodule.of_le le_sup_left) x)

source

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⟩

source

@[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'

source

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.

source

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) :

(M ⧸ S) ⧸ submodule.map S.mkq T →ₗ[R] M ⧸ 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) _

source

@[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

source

@[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) :

⇑(S.quotient_quotient_equiv_quotient_aux T h) (submodule.quotient.mk (submodule.quotient.mk x)) = submodule.quotient.mk x

source

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) :

((M ⧸ S) ⧸ submodule.map S.mkq T) ≃ₗ[R] M ⧸ T

Noether's third isomorphism theorem for modules: (M / S) / (T / S) ≃ M / T.

Equations

S.quotient_quotient_equiv_quotient T h = {to_fun := ⇑(S.quotient_quotient_equiv_quotient_aux T h), map_add' := _, map_smul' := _, inv_fun := ⇑(T.mapq (submodule.map S.mkq T) S.mkq _), left_inv := _, right_inv := _}