# Documentation

Mathlib.LinearAlgebra.Isomorphisms

# Isomorphism theorems for modules. #

• The Noether's first, second, and third isomorphism theorems for modules are proved as LinearMap.quotKerEquivRange, LinearMap.quotientInfEquivSupQuotient and Submodule.quotientQuotientEquivQuotient.

The first and second isomorphism theorems for modules.

noncomputable def LinearMap.quotKerEquivRange {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :
() ≃ₗ[R] { x // }

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

Instances For
noncomputable def LinearMap.quotKerEquivOfSurjective {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (hf : ) :
() ≃ₗ[R] M₂

The first isomorphism theorem for surjective linear maps.

Instances For
@[simp]
theorem LinearMap.quotKerEquivRange_apply_mk {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (x : M) :
↑() = f x
@[simp]
theorem LinearMap.quotKerEquivRange_symm_apply_image {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [] [] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (x : M) (h : f x ) :
↑() { val := f x, property := h } = ↑() x
@[reducible]
def LinearMap.subToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) :
{ x // x p } →ₗ[R] { x // x p p' } Submodule.comap (Submodule.subtype (p p')) p'

Linear map from p to p+p'/p' where p p' are submodules of R

Instances For
theorem LinearMap.comap_leq_ker_subToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) :
def LinearMap.quotientInfToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) :
{ x // x p } Submodule.comap () (p p') →ₗ[R] { x // x p p' } Submodule.comap (Submodule.subtype (p p')) 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.

Instances For
theorem LinearMap.quotientInfEquivSupQuotient_injective {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) :
theorem LinearMap.quotientInfEquivSupQuotient_surjective {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) :
noncomputable def LinearMap.quotientInfEquivSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) :
({ x // x p } Submodule.comap () (p p')) ≃ₗ[R] { x // x p p' } Submodule.comap (Submodule.subtype (p p')) p'

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

Instances For
theorem LinearMap.coe_quotientInfToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) :
@[simp]
theorem LinearMap.quotientInfEquivSupQuotient_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) (x : { x // x p }) :
let map := Submodule.ofLe (_ : p p p'); = Submodule.Quotient.mk (map x)
theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_left {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) (x : { x // x p p' }) (hx : x p) :
= Submodule.Quotient.mk { val := x, property := hx }
theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {p : } {p' : } {x : { x // x p p' }} :
x p'
theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_right {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) {x : { x // x p p' }} (hx : x p') :

The third isomorphism theorem for modules.

def Submodule.quotientQuotientEquivQuotientAux {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (S : ) (T : ) (h : S T) :
(M S) →ₗ[R] M T

The map from the third isomorphism theorem for modules: (M / S) / (T / S) → M / T.

Instances For
@[simp]
theorem Submodule.quotientQuotientEquivQuotientAux_mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (S : ) (T : ) (h : S T) (x : M S) :
= ↑(Submodule.mapQ S T LinearMap.id h) x
theorem Submodule.quotientQuotientEquivQuotientAux_mk_mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (S : ) (T : ) (h : S T) (x : M) :
def Submodule.quotientQuotientEquivQuotient {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (S : ) (T : ) (h : S T) :
((M S) ) ≃ₗ[R] M T

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

Instances For
theorem Submodule.card_quotient_mul_card_quotient {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (S : ) (T : ) (hST : T S) [DecidablePred fun x => x ] [Fintype (M S)] [Fintype (M T)] :

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