Documentation

Mathlib.LinearAlgebra.Isomorphisms

Isomorphism theorems for modules. #

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] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) :
(M ker f) ≃ₗ[R] (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
noncomputable def LinearMap.quotKerEquivOfSurjective {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (hf : Function.Surjective f) :
(M ker f) ≃ₗ[R] M₂

The first isomorphism theorem for surjective linear maps.

Equations
@[simp]
theorem LinearMap.quotKerEquivRange_apply_mk {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (x : M) :
(f.quotKerEquivRange (Submodule.Quotient.mk x)) = f x
@[simp]
theorem LinearMap.quotKerEquivRange_symm_apply_image {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] (f : M →ₗ[R] M₂) (x : M) (h : f x range f) :
f.quotKerEquivRange.symm f x, h = (ker f).mkQ x
@[reducible, inline]
abbrev LinearMap.subToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) :
p →ₗ[R] (p p') Submodule.comap (p p').subtype p'

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

Equations
theorem LinearMap.comap_leq_ker_subToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) :
Submodule.comap p.subtype (p p') ker (subToSupQuotient p p')
def LinearMap.quotientInfToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup 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
noncomputable def LinearMap.quotientInfEquivSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup 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
theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_left {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) (x : (p p')) (hx : x p) :
theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p p' : Submodule R M} {x : (p p')} :
theorem LinearMap.quotientInfEquivSupQuotient_symm_apply_right {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) {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] [AddCommGroup M] [Module R M] (S T : Submodule R M) (h : S T) :
(M S) map S.mkQ T →ₗ[R] M T

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

Equations
@[simp]
theorem Submodule.quotientQuotientEquivQuotientAux_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) (h : S T) (x : M S) :
(S.quotientQuotientEquivQuotientAux T h) (Quotient.mk x) = (S.mapQ T LinearMap.id h) x
@[simp]
theorem Submodule.quotientQuotientEquivQuotientAux_mk_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) (h : S T) (x : M) :
(S.quotientQuotientEquivQuotientAux T h) (Quotient.mk (Quotient.mk x)) = Quotient.mk x
def Submodule.quotientQuotientEquivQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) (h : S T) :
((M S) map S.mkQ T) ≃ₗ[R] M T

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

Equations
  • One or more equations did not get rendered due to their size.
def Submodule.quotientQuotientEquivQuotientSup {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) :
((M S) map S.mkQ T) ≃ₗ[R] M S T

Essentially the same equivalence as in the third isomorphism theorem, except restated in terms of suprema/addition of submodules instead of .

Equations
  • S.quotientQuotientEquivQuotientSup T = ((Submodule.map S.mkQ T).quotEquivOfEq (Submodule.map S.mkQ (S T)) ).trans (S.quotientQuotientEquivQuotient (S T) )
theorem Submodule.card_quotient_mul_card_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S T : Submodule R M) (hST : T S) :
Nat.card (map T.mkQ S) * Nat.card (M S) = Nat.card (M T)

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