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 ⧸ LinearMap.ker f) ≃ₗ[R] { x // x ∈ LinearMap.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

• One or more equations did not get rendered due to their size.

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 ⧸ LinearMap.ker f) ≃ₗ[R] M₂

The first isomorphism theorem for surjective linear maps.

Equations

• LinearMap.quotKerEquivOfSurjective f hf = LinearEquiv.trans (LinearMap.quotKerEquivRange f) (LinearEquiv.ofTop (LinearMap.range f) (_ : 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) : ↑(↑(LinearMap.quotKerEquivRange f) (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 ∈ LinearMap.range f) : ↑(LinearEquiv.symm (LinearMap.quotKerEquivRange f)) { val := ↑f x, property := h } = ↑(Submodule.mkQ (LinearMap.ker f)) x

@[reducible]

def LinearMap.subToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) : { 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

Equations

• LinearMap.subToSupQuotient p p' = LinearMap.comp (Submodule.mkQ (Submodule.comap (Submodule.subtype (p ⊔ p')) p')) (Submodule.ofLe (_ : p ≤ p ⊔ p'))

theorem LinearMap.comap_leq_ker_subToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) : Submodule.comap (Submodule.subtype p) (p ⊓ p') ≤ LinearMap.ker (LinearMap.subToSupQuotient p p')

def LinearMap.quotientInfToSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) : { x // x ∈ p } ⧸ Submodule.comap (Submodule.subtype p) (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.

Equations

• One or more equations did not get rendered due to their size.

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

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

noncomputable def LinearMap.quotientInfEquivSupQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) : ({ x // x ∈ p } ⧸ Submodule.comap (Submodule.subtype p) (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.

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

theorem LinearMap.quotientInfEquivSupQuotient_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) (x : { x // x ∈ p }) : let map := Submodule.ofLe (_ : p ≤ p ⊔ p'); ↑(LinearMap.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 : Submodule R M) (p' : Submodule R M) (x : { x // x ∈ p ⊔ p' }) (hx : ↑x ∈ p) : ↑(LinearEquiv.symm (LinearMap.quotientInfEquivSupQuotient p p')) (Submodule.Quotient.mk x) = 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] [AddCommGroup M] [Module R M] {p : Submodule R M} {p' : Submodule R M} {x : { x // x ∈ p ⊔ p' }} : ↑(LinearEquiv.symm (LinearMap.quotientInfEquivSupQuotient p p')) (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 : Submodule R M) (p' : Submodule R M) {x : { x // x ∈ p ⊔ p' }} (hx : ↑x ∈ p') : ↑(LinearEquiv.symm (LinearMap.quotientInfEquivSupQuotient p p')) (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 : Submodule R M) (T : Submodule R M) (h : S ≤ T) : (M ⧸ S) ⧸ Submodule.map (Submodule.mkQ S) T →ₗ[R] M ⧸ T

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Submodule.quotientQuotientEquivQuotientAux_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) (h : S ≤ T) (x : M ⧸ S) : ↑(Submodule.quotientQuotientEquivQuotientAux S T h) (Submodule.Quotient.mk x) = ↑(Submodule.mapQ S T LinearMap.id h) x

theorem Submodule.quotientQuotientEquivQuotientAux_mk_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) (h : S ≤ T) (x : M) : ↑(Submodule.quotientQuotientEquivQuotientAux S T h) (Submodule.Quotient.mk (Submodule.Quotient.mk x)) = Submodule.Quotient.mk x

def Submodule.quotientQuotientEquivQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) (h : S ≤ T) : ((M ⧸ S) ⧸ Submodule.map (Submodule.mkQ S) 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.

theorem Submodule.card_quotient_mul_card_quotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Submodule R M) (T : Submodule R M) (hST : T ≤ S) [DecidablePred fun x => x ∈ Submodule.map (Submodule.mkQ T) S] [Fintype (M ⧸ S)] [Fintype (M ⧸ T)] : Fintype.card { x // x ∈ Submodule.map (Submodule.mkQ T) S } * Fintype.card (M ⧸ S) = Fintype.card (M ⧸ T)

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