mathlib documentation

linear_algebra.isomorphisms

Isomorphism theorems for modules. #

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

The first isomorphism law for modules. The quotient of M by the kernel of f is linearly equivalent to the range of f.

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

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