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

• f.quotKerEquivRange = (LinearEquiv.ofInjective ((LinearMap.ker f).liftQ f ⋯) ⋯).trans (LinearEquiv.ofEq (LinearMap.range ((LinearMap.ker f).liftQ f ⋯)) (LinearMap.range f) ⋯)

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

• f.quotKerEquivOfSurjective hf = f.quotKerEquivRange.trans (LinearEquiv.ofTop (LinearMap.range f) ⋯)

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

• LinearMap.subToSupQuotient p p' = (Submodule.comap (p ⊔ p').subtype p').mkQ ∘ₗ Submodule.inclusion ⋯

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 ⊓ Submodule.comap p.subtype 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.

Note that in the following declaration the type of the domain is expressed using ``comap p.subtype p ⊓ comap p.subtype p'instead of `comap p.subtype (p ⊓ p')because the former is the simp normal form (see alsoSubmodule.comap_inf`).

Equations

• LinearMap.quotientInfToSupQuotient p p' = (Submodule.comap p.subtype (p ⊓ p')).liftQ (LinearMap.subToSupQuotient p p') ⋯

theorem LinearMap.quotientInfEquivSupQuotient_injective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) : Function.Injective ⇑(quotientInfToSupQuotient p p')

theorem LinearMap.quotientInfEquivSupQuotient_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) : Function.Surjective ⇑(quotientInfToSupQuotient p p')

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 ⊓ Submodule.comap p.subtype 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.

Note that in the following declaration the type of the domain is expressed using ``comap p.subtype p ⊓ comap p.subtype p'instead of `comap p.subtype (p ⊓ p')because the former is the simp normal form (see alsoSubmodule.comap_inf`).

Equations

• LinearMap.quotientInfEquivSupQuotient p p' = LinearEquiv.ofBijective (LinearMap.quotientInfToSupQuotient p p') ⋯

@[simp]

theorem LinearMap.coe_quotientInfToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) : ⇑(quotientInfToSupQuotient p p') = ⇑(quotientInfEquivSupQuotient p p')

theorem LinearMap.quotientInfEquivSupQuotient_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) (x : ↥p) : let map := Submodule.inclusion ⋯; (quotientInfEquivSupQuotient p p') (Submodule.Quotient.mk x) = Submodule.Quotient.mk (map x)

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) : (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨↑x, hx⟩

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')} : (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 ↔ ↑x ∈ 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') : (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0

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

• S.quotientQuotientEquivQuotientAux T h = (Submodule.map S.mkQ T).liftQ (S.mapQ T LinearMap.id h) ⋯

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