# mathlib3documentation

linear_algebra.isomorphisms

# 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_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₂] [ M] [ 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₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (hf : function.surjective f) :
(M ≃ₗ[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₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (x : M) :
= 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₂] [ M] [ M₂] (f : M →ₗ[R] M₂) (x : M) (h : f x ) :
def linear_map.quotient_inf_to_sup_quotient {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : M) :
p (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
noncomputable def linear_map.quotient_inf_equiv_sup_quotient {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : M) :
(p (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
@[simp]
theorem linear_map.coe_quotient_inf_to_sup_quotient {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : M) :
@[simp]
theorem linear_map.quotient_inf_equiv_sup_quotient_apply_mk {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : M) (x : p) :
theorem linear_map.quotient_inf_equiv_sup_quotient_symm_apply_left {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : M) (x : (p p')) (hx : x p) :
@[simp]
theorem linear_map.quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff {R : Type u_1} {M : Type u_2} [ring R] [ M] {p p' : M} {x : (p p')} :
x p'
theorem linear_map.quotient_inf_equiv_sup_quotient_symm_apply_right {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : 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] [ M] (S T : M) (h : S T) :
(M S) T →ₗ[R] M 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] [ M] (S T : M) (h : S T) (x : M S) :
@[simp]
theorem submodule.quotient_quotient_equiv_quotient_aux_mk_mk {R : Type u_1} {M : Type u_2} [ring R] [ M] (S T : M) (h : S T) (x : M) :
def submodule.quotient_quotient_equiv_quotient {R : Type u_1} {M : Type u_2} [ring R] [ M] (S T : M) (h : S T) :
((M S) T) ≃ₗ[R] M T

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

Equations
theorem submodule.card_quotient_mul_card_quotient {R : Type u_1} {M : Type u_2} [ring R] [ M] (S T : M) (hST : T S) [decidable_pred (λ (x : M T), x S)] [fintype (M S)] [fintype (M T)] :

Corollary of the third isomorphism theorem: [S : T] [M : S] = [M : T]