Congruence relations and ring homomorphisms

This file contains elementary definitions involving congruence relations and morphisms for rings and semirings

Main definitions

• RingCon.ker: the kernel of a monoid homomorphism as a congruence relation

• RingCon.lift, RingCon.liftₐ: the homomorphism / the algebra morphism on the quotient given that the congruence is in the kernel

• RingCon.map, RingCon.mapₐ: homomorphism / algebra morphism from a smaller to a larger quotient

• RingCon.quotientKerEquivRangeS, RingCon.quotientKerEquivRange, RingCon.quotientKerEquivRangeₐ : the first isomorphism theorem for semirings (using RingHom.rangeS), rings (using RingHom.range) and algebras (using AlgHom.range).

• RingCon.comapQuotientEquivRangeS, RingCon.comapQuotientEquivRange, RingCon.comapQuotientEquivRangeₐ : the second isomorphism theorem for semirings (using RingHom.rangeS), rings (using RingHom.range) and algebras (using AlgHom.range).

• RingCon.quotientQuotientEquivQuotient, RingCon.quotientQuotientEquivQuotientₐ : the third isomorphism theorem for semirings (or rings) and algebras

Tags

congruence, congruence relation, quotient, quotient by congruence relation, ring, quotient ring

def RingCon.ker {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] (f : M →+* N) : RingCon M

The kernel of a ring homomorphism as a ring congruence relation.

theorem RingCon.comap_bot {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] (f : M →+* N) : ⊥.comap f = ker f

@[simp]

theorem RingCon.ker_apply {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] (f : M →+* N) {x y : M} : (ker f) x y ↔ f x = f y

The definition of the ring congruence relation defined by a ring homomorphism's kernel.

theorem RingCon.ker_mk'_eq {M : Type u_1} [NonAssocSemiring M] (c : RingCon M) : ker c.mk' = c

The kernel of the quotient map induced by a ring congruence relation c equals c.

theorem RingCon.ker_comp {M : Type u_1} {N : Type u_2} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring N] [NonAssocSemiring P] {f : M →+* N} {g : N →+* P} : ker (g.comp f) = (ker g).comap f

theorem RingCon.comap_eq {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] {c : RingCon M} {g : N →+* M} : c.comap g = ker (c.mk'.comp g)

def RingCon.congr {M : Type u_1} [NonAssocSemiring M] {c d : RingCon M} (h : c = d) : c.Quotient ≃+* d.Quotient

Makes an isomorphism of quotients by two ring congruence relations, given that the relations are equal.

@[simp]

theorem RingCon.congr_mk {M : Type u_1} [NonAssocSemiring M] {c d : RingCon M} (h : c = d) (a : M) : (RingCon.congr h) ↑a = ↑a

def RingCon.mapGen {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] {c : RingCon M} (f : M → N) : RingCon N

Given a function f, the smallest ring congruence relation containing the binary relation on f's image defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by a ring congruence relation c.'

theorem RingCon.mapGen_eq_map_of_surjective {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] {c : RingCon M} (f : M →+* N) (h : ker f ≤ c) (hf : Function.Surjective ⇑f) : ⇑(mapGen ⇑f) = Relation.Map ⇑c ⇑f ⇑f

If c is a ring congruence on M, then the smallest ring congruence relation on N deduced from c by a ring homomorphism from M to N is the relation deduced from c.

theorem RingCon.mapGen_apply_apply_of_surjective {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] {c : RingCon M} (f : M →+* N) (h : ker f ≤ c) (hf : Function.Surjective ⇑f) {x y : M} : (mapGen ⇑f) (f x) (f y) ↔ c x y

def RingCon.correspondence {M : Type u_1} [NonAssocSemiring M] {c : RingCon M} : ↑(Set.Ici c) ≃o RingCon c.Quotient

Given a ring congruence relation c on a semiring M, the order-preserving bijection between the set of ring congruence relations containing c and the ring congruence relations on the quotient of M by c.

def RingCon.lift {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] (c : RingCon M) (f : M →+* P) (H : c ≤ ker f) : c.Quotient →+* P

The homomorphism on the quotient of a ring by a congruence relation c induced by a homomorphism constant on the equivalence classes of c.

theorem RingCon.lift_mk' {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f : M →+* P} (H : c ≤ ker f) (x : M) : (c.lift f H) (c.mk' x) = f x

The diagram describing the universal property for quotients of ring commutes.

@[simp]

theorem RingCon.lift_coe {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f : M →+* P} (H : c ≤ ker f) (x : M) : (c.lift f H) ↑x = f x

The diagram describing the universal property for quotients of rings commutes.

@[simp]

theorem RingCon.lift_comp_mk' {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f : M →+* P} (H : c ≤ ker f) : (c.lift f H).comp c.mk' = f

The diagram describing the universal property for quotients of rings commutes.

theorem RingCon.lift_apply_mk' {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} (f : c.Quotient →+* P) : c.lift (f.comp c.mk') ⋯ = f

Given a homomorphism f from the quotient of a ring by a ring congruence relation, f equals the homomorphism on the quotient induced by f composed with the natural map from the ring to the quotient.

theorem RingCon.Quotient.hom_ext {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f g : c.Quotient →+* P} (h : f.comp c.mk' = g.comp c.mk') : f = g

Homomorphisms on the quotient of a ring by a ring congruence relation are equal if they are equal on elements that are coercions from the ring.

theorem RingCon.Quotient.hom_ext_iff {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f g : c.Quotient →+* P} : f = g ↔ f.comp c.mk' = g.comp c.mk'

theorem RingCon.lift_unique {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f : M →+* P} (H : c ≤ ker f) (g : c.Quotient →+* P) (Hg : g.comp c.mk' = f) : g = c.lift f H

The uniqueness part of the universal property for quotients of rings.

theorem RingCon.lift_surjective_iff {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f : M →+* P} {h : c ≤ ker f} : Function.Surjective ⇑(c.lift f h) ↔ Function.Surjective ⇑f

Surjective ring homomorphisms constant on the equivalence classes of a ring congruence relation induce a surjective homomorphism on the quotient.

theorem RingCon.lift_surjective_of_surjective {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f : M →+* P} (h : c ≤ ker f) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(c.lift f h)

Surjective ring homomorphisms constant on the equivalence classes of a ring congruence relation induce a surjective homomorphism on the quotient.

theorem RingCon.lift_injective_iff {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f : M →+* P} {h : c ≤ ker f} : Function.Injective ⇑(c.lift f h) ↔ c = ker f

Given a ring homomorphism f from M to P whose kernel contains c, the lift of M to P is injective iff ker f = c.

theorem RingCon.lift_bijective_iff {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f : M →+* P} {h : c ≤ ker f} : Function.Bijective ⇑(c.lift f h) ↔ c = ker f ∧ Function.Surjective ⇑f

theorem RingCon.ker_eq_lift_of_injective {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f : M →+* P} (H : c ≤ ker f) (h : Function.Injective ⇑(c.lift f H)) : ker f = c

Given a ring homomorphism f from M to P, the kernel of f is the unique ring congruence relation on M whose induced map from the quotient of M to P is injective.

def RingCon.kerLift {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] (f : M →+* P) : (ker f).Quotient →+* P

The homomorphism induced on the quotient of a ring by the kernel of a ring homomorphism.

theorem RingCon.kerLift_mk {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {f : M →+* P} (x : M) : (kerLift f) ↑x = f x

The diagram described by the universal property for quotients of rings, when the ring congruence relation is the kernel of the homomorphism, commutes.

theorem RingCon.kerLift_injective {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] (f : M →+* P) : Function.Injective ⇑(kerLift f)

A ring homomorphism f induces an injective homomorphism on the quotient by f's kernel.

def RingCon.map {M : Type u_1} [NonAssocSemiring M] (c d : RingCon M) (h : c ≤ d) : c.Quotient →+* d.Quotient

Given ring congruence relations c, d on a ring such that d contains c, d's quotient map induces a homomorphism from the quotient by c to the quotient by d.

theorem RingCon.map_apply {M : Type u_1} [NonAssocSemiring M] {c d : RingCon M} (h : c ≤ d) (x : c.Quotient) : (c.map d h) x = (c.lift d.mk' ⋯) x

Given ring congruence relations c, d on a ring such that d contains c, the definition of the homomorphism from the quotient by c to the quotient by d induced by d's quotient map.

@[simp]

theorem RingCon.rangeS_mk' {M : Type u_1} [NonAssocSemiring M] {c : RingCon M} : c.mk'.rangeS = ⊤

@[simp]

theorem RingCon.rangeS_lift {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {c : RingCon M} {f : M →+* P} (H : c ≤ ker f) : (c.lift f H).rangeS = f.rangeS

Given a congruence relation c on a semiring and a homomorphism f constant on the equivalence classes of c, f has the same image as the homomorphism that f induces on the quotient.

@[simp]

theorem RingCon.rangeS_kerLift {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] {f : M →+* P} : (kerLift f).rangeS = f.rangeS

Given a ring homomorphism f, the induced homomorphism on the quotient by f's kernel has the same image as f.

noncomputable def RingCon.quotientKerEquivRangeS {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] (f : M →+* P) : (ker f).Quotient ≃+* ↥f.rangeS

The first isomorphism theorem for semirings.

@[simp]

theorem RingCon.coe_quotientKerEquivRangeS_mk {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] (f : M →+* P) (x : M) : ↑((quotientKerEquivRangeS f) ↑x) = f x

def RingCon.quotientKerEquivOfRightInverse {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] (f : M →+* P) (g : P → M) (hf : Function.RightInverse g ⇑f) : (ker f).Quotient ≃+* P

The first isomorphism theorem for semirings in the case of a homomorphism with right inverse.

@[simp]

theorem RingCon.quotientKerEquivOfRightInverse_apply {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] (f : M →+* P) (g : P → M) (hf : Function.RightInverse g ⇑f) (x : (ker f).Quotient) : (quotientKerEquivOfRightInverse f g hf) x = (kerLift f) x

noncomputable def RingCon.quotientKerEquivOfSurjective {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] (f : M →+* P) (hf : Function.Surjective ⇑f) : (ker f).Quotient ≃+* P

The first isomorphism theorem for rings in the case of a surjective homomorphism.

For a computable version, see RingCon.quotientKerEquivOfRightInverse.

@[simp]

theorem RingCon.quotientKerEquivOfSurjective_mk {M : Type u_1} {P : Type u_3} [NonAssocSemiring M] [NonAssocSemiring P] (f : M →+* P) (hf : Function.Surjective ⇑f) (x : M) : (quotientKerEquivOfSurjective f hf) ↑x = f x

noncomputable def RingCon.comapQuotientEquivOfSurj {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] (c : RingCon M) (f : N →+* M) (hf : Function.Surjective ⇑f) {d : RingCon N} (hcd : d = c.comap f) : d.Quotient ≃+* c.Quotient

A surjective ring homomorphism f : M →+* N induces a ring equivalence d.Quotient ≃+* c.Quotient, whenever c : RingCon M and d : RingCon N are such that d = c.comap f.

@[simp]

theorem RingCon.comapQuotientEquivOfSurj_mk {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] (c : RingCon M) {f : N →+* M} (hf : Function.Surjective ⇑f) {d : RingCon N} (hcd : d = c.comap f) (x : N) : (c.comapQuotientEquivOfSurj f hf hcd) ↑x = ↑(f x)

@[simp]

theorem RingCon.comapQuotientEquivOfSurj_symm_mk {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] (c : RingCon M) {f : N →+* M} (hf : Function.Surjective ⇑f) {d : RingCon N} (hcd : d = c.comap f) (x : N) : (c.comapQuotientEquivOfSurj f hf hcd).symm ↑(f x) = ↑x

@[simp]

theorem RingCon.comapQuotientEquivOfSurj_symm_mk' {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] (c : RingCon M) (f : N ≃+* M) {d : RingCon N} (hcd : d = c.comap f) (x : N) : (c.comapQuotientEquivOfSurj ↑f ⋯ hcd).symm ⟦f x⟧ = ↑x

This version infers the surjectivity of the function from a RingEquiv function

noncomputable def RingCon.comapQuotientEquivRangeS {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] (c : RingCon M) (f : N →+* M) {d : RingCon N} (hcd : d = c.comap f) : d.Quotient ≃+* ↥(c.mk'.comp f).rangeS

The second isomorphism theorem for semirings.

@[simp]

theorem RingCon.comapQuotientEquivRangeS_mk {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] (c : RingCon M) (f : N →+* M) {d : RingCon N} (hcd : d = c.comap f) (x : N) : (c.comapQuotientEquivRangeS f hcd) ↑x = ⟨↑(f x), ⋯⟩

@[simp]

theorem RingCon.comapQuotientEquivRangeS_symm_mk {M : Type u_1} {N : Type u_2} [NonAssocSemiring M] [NonAssocSemiring N] (c : RingCon M) (f : N →+* M) {d : RingCon N} (hcd : d = c.comap f) (x : N) : (c.comapQuotientEquivRangeS f hcd).symm ⟨↑(f x), ⋯⟩ = ↑x

def RingCon.quotientQuotientEquivQuotient {M : Type u_1} [NonAssocSemiring M] (c d : RingCon M) (h : c ≤ d) : (ker (c.map d h)).Quotient ≃+* d.Quotient

The third isomorphism theorem for (semi-)rings.

@[simp]

theorem RingCon.quotientQuotientEquivQuotient_mk_mk {M : Type u_1} [NonAssocSemiring M] (c d : RingCon M) (h : c ≤ d) (x : M) : (c.quotientQuotientEquivQuotient d h) ⟦⟦x⟧⟧ = ⟦x⟧

@[simp]

theorem RingCon.quotientQuotientEquivQuotient_coe_coe {M : Type u_1} [NonAssocSemiring M] (c d : RingCon M) (h : c ≤ d) (x : M) : (c.quotientQuotientEquivQuotient d h) ↑↑x = ↑x

@[simp]

theorem RingCon.quotientQuotientEquivQuotient_symm_mk {M : Type u_1} [NonAssocSemiring M] (c d : RingCon M) (h : c ≤ d) (x : M) : (c.quotientQuotientEquivQuotient d h).symm ⟦x⟧ = ⟦⟦x⟧⟧

theorem RingCon.range_mk' {M : Type u_1} [Ring M] {c : RingCon M} : c.mk'.range = ⊤

@[simp]

theorem RingCon.range_lift {M : Type u_1} {P : Type u_3} [Ring M] [Ring P] {c : RingCon M} {f : M →+* P} (H : c ≤ ker f) : (c.lift f H).range = f.range

Given a congruence relation c on a ring and a homomorphism f constant on the equivalence classes of c, f has the same image as the homomorphism that f induces on the quotient.

@[simp]

theorem RingCon.kerLift_range_eq {M : Type u_1} {P : Type u_3} [Ring M] [Ring P] {f : M →+* P} : (kerLift f).range = f.range

Given a ring homomorphism f, the induced homomorphism on the quotient by f's kernel has the same image as f.

noncomputable def RingCon.quotientKerEquivRange {M : Type u_1} {P : Type u_3} [Ring M] [Ring P] (f : M →+* P) : (ker f).Quotient ≃+* ↥f.range

The first isomorphism theorem for rings.

noncomputable def RingCon.comapQuotientEquivRange {M : Type u_1} {N : Type u_2} [Ring M] [Ring N] (c : RingCon M) (f : N →+* M) {d : RingCon N} (hcd : d = c.comap f) : d.Quotient ≃+* ↥(c.mk'.comp f).range

The second isomorphism theorem for rings.

theorem RingCon.comapQuotientEquivRange_mk {M : Type u_1} {N : Type u_2} [Ring M] [Ring N] (c : RingCon M) (f : N →+* M) {d : RingCon N} (hcd : d = c.comap f) (x : N) : (c.comapQuotientEquivRange f hcd) ↑x = ⟨↑(f x), ⋯⟩

@[simp]

theorem RingCon.coe_comapQuotientEquivRange_mk {M : Type u_1} {N : Type u_2} [Ring M] [Ring N] (c : RingCon M) (f : N →+* M) {d : RingCon N} (hcd : d = c.comap f) (x : N) : ↑((c.comapQuotientEquivRange f hcd) ↑x) = ↑(f x)

@[simp]

theorem RingCon.comapQuotientEquivRange_symm_mk {M : Type u_1} {N : Type u_2} [Ring M] [Ring N] (c : RingCon M) (f : N →+* M) {d : RingCon N} (hcd : d = c.comap f) (x : N) : (c.comapQuotientEquivRange f hcd).symm ⟨↑(f x), ⋯⟩ = ↑x

def RingCon.congrₐ {M : Type u_1} (R : Type u_4) [CommSemiring R] [Semiring M] [Algebra R M] {c d : RingCon M} (h : c = d) : c.Quotient ≃ₐ[R] d.Quotient

Makes an algebra isomorphism of quotients by two ring congruence relations, given that the relations are equal.

theorem RingCon.congrₐ_mk {M : Type u_1} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] {c d : RingCon M} (h : c = d) (a : M) : (RingCon.congrₐ R h) ↑a = ↑a

theorem RingCon.range_mkₐ {M : Type u_1} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] {c : RingCon M} : (mkₐ R c).range = ⊤

def RingCon.liftₐ {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] (c : RingCon M) (f : M →ₐ[R] P) (H : c ≤ ker f.toRingHom) : c.Quotient →ₐ[R] P

The algebra homomorphism on the quotient of an algebra by a congruence relation c induced by an algebra homomorphism constant on the equivalence classes of c.

theorem RingCon.liftₐ_coe_toRingHom {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] (c : RingCon M) (f : M →ₐ[R] P) (H : c ≤ ker f.toRingHom) : (c.liftₐ f H).toRingHom = c.lift (↑f) H

theorem RingCon.coe_liftₐ {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] (c : RingCon M) (f : M →ₐ[R] P) (H : c ≤ ker f.toRingHom) : ⇑(c.liftₐ f H) = ⇑(c.lift (↑f) H)

@[simp]

theorem RingCon.liftₐ_mk {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] (c : RingCon M) (f : M →ₐ[R] P) (H : c ≤ ker f.toRingHom) (x : M) : (c.liftₐ f H) ↑x = f x

theorem RingCon.liftₐ_range {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] {c : RingCon M} {f : M →ₐ[R] P} (H : c ≤ ker f.toRingHom) : (c.liftₐ f H).range = f.range

Given a congruence relation c on an algebra and a homomorphism f constant on the equivalence classes of c, f has the same image as the homomorphism that f induces on the quotient.

def RingCon.kerLiftₐ {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] (f : M →ₐ[R] P) : (ker f.toRingHom).Quotient →ₐ[R] P

The homomorphism induced on the quotient of a ring by the kernel of a ring homomorphism.

theorem RingCon.kerLiftₐ_mk {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] {f : M →ₐ[R] P} (x : M) : (kerLiftₐ f) ↑x = f x

The diagram described by the universal property for quotients of rings, when the ring congruence relation is the kernel of the homomorphism, commutes.

theorem RingCon.kerLiftₐ_injective {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] (f : M →ₐ[R] P) : Function.Injective ⇑(kerLiftₐ f)

A ring homomorphism f induces an injective homomorphism on the quotient by f's kernel.

def RingCon.factorₐ {M : Type u_1} (R : Type u_4) [CommSemiring R] [Semiring M] [Algebra R M] {c d : RingCon M} (h : c ≤ d) : c.Quotient →ₐ[R] d.Quotient

Given ring congruence relations c, d on an algebra such that d contains c, d's quotient map induces an algebra homomorphism from the quotient by c to the quotient by d.

theorem RingCon.factorₐ_apply {M : Type u_1} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] {c d : RingCon M} (h : c ≤ d) (x : c.Quotient) : (factorₐ R h) x = (c.liftₐ (mkₐ R d) ⋯) x

Given ring congruence relations c, d on a ring such that d contains c, the definition of the homomorphism from the quotient by c to the quotient by d induced by d's quotient map.

@[simp]

theorem RingCon.factorₐ_mk {M : Type u_1} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] {c d : RingCon M} (h : c ≤ d) (x : M) : (factorₐ R h) ⟦x⟧ = ⟦x⟧

Given ring congruence relations c, d on a ring such that d contains c, the definition of the homomorphism from the quotient by c to the quotient by d induced by d's quotient map.

@[simp]

theorem RingCon.mkₐ_comp_factorₐ_comp_mkₐ {M : Type u_1} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] {c d : RingCon M} (h : c ≤ d) : (factorₐ R h).comp (mkₐ R c) = mkₐ R d

@[simp]

theorem RingCon.kerLiftₐ_range_eq {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] {f : M →ₐ[R] P} : (kerLiftₐ f).range = f.range

Given a ring homomorphism f, the induced homomorphism on the quotient by f's kernel has the same image as f.

noncomputable def RingCon.quotientKerEquivRangeₐ {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] (f : M →ₐ[R] P) : (ker ↑f).Quotient ≃ₐ[R] ↥f.range

The first isomorphism theorem for algebra morphisms.

theorem RingCon.quotientKerEquivRangeₐ_mkₐ {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] (f : M →ₐ[R] P) (x : M) : (quotientKerEquivRangeₐ f) ↑x = ⟨f x, ⋯⟩

@[simp]

theorem RingCon.coe_quotientKerEquivRangeₐ_mkₐ {M : Type u_1} {P : Type u_3} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring P] [Algebra R P] (f : M →ₐ[R] P) (x : M) : ↑((quotientKerEquivRangeₐ f) ↑x) = f x

theorem RingCon.quotientKerEquivRangeₐ_comp_mkₐ {M : Type u_1} {N : Type u_2} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring N] [Algebra R N] (φ : M →ₐ[R] N) : (↑(quotientKerEquivRangeₐ φ)).comp (mkₐ R (ker ↑φ)) = φ.rangeRestrict

noncomputable def RingCon.comapQuotientEquivRangeₐ {M : Type u_1} {N : Type u_2} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring N] [Algebra R N] (c : RingCon M) (f : N →ₐ[R] M) {d : RingCon N} (h : d = c.comap f) : d.Quotient ≃ₐ[R] ↥((mkₐ R c).comp f).range

The second isomorphism theorem for algebras.

theorem RingCon.comapQuotientEquivRangeₐ_mk {M : Type u_1} {N : Type u_2} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring N] [Algebra R N] (c : RingCon M) (f : N →ₐ[R] M) {d : RingCon N} (h : d = c.comap f) (x : N) : (c.comapQuotientEquivRangeₐ f h) ↑x = ⟨↑(f x), ⋯⟩

@[simp]

theorem RingCon.coe_comapQuotientEquivRangeₐ_mk {M : Type u_1} {N : Type u_2} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring N] [Algebra R N] (c : RingCon M) (f : N →ₐ[R] M) (x : N) {d : RingCon N} (h : d = c.comap f) : ↑((c.comapQuotientEquivRangeₐ f h) ↑x) = ↑(f x)

@[simp]

theorem RingCon.coe_comapQuotientEquivRangeₐ_symm_mk {M : Type u_1} {N : Type u_2} {R : Type u_4} [CommSemiring R] [Semiring M] [Algebra R M] [Semiring N] [Algebra R N] (c : RingCon M) (f : N →ₐ[R] M) (x : N) {d : RingCon N} (h : d = c.comap f) : (c.comapQuotientEquivRangeₐ f h).symm ⟨↑(f x), ⋯⟩ = ↑x

def RingCon.quotientQuotientEquivQuotientₐ {M : Type u_1} (R : Type u_4) [CommSemiring R] [Semiring M] [Algebra R M] {c d : RingCon M} (h : c ≤ d) : (ker ↑(factorₐ R h)).Quotient ≃ₐ[R] d.Quotient

The third isomorphism theorem for algebras.

@[simp]

theorem RingCon.quotientQuotientEquivQuotientₐ_mk_mk {M : Type u_1} (R : Type u_4) [CommSemiring R] [Semiring M] [Algebra R M] {c d : RingCon M} (h : c ≤ d) (x : M) : (quotientQuotientEquivQuotientₐ R h) ⟦⟦x⟧⟧ = ⟦x⟧

@[simp]

theorem RingCon.quotientQuotientEquivQuotientₐ_coe_coe {M : Type u_1} (R : Type u_4) [CommSemiring R] [Semiring M] [Algebra R M] {c d : RingCon M} (h : c ≤ d) (x : M) : (quotientQuotientEquivQuotientₐ R h) ↑↑x = ↑x

@[simp]

theorem RingCon.quotientQuotientEquivQuotientₐ_symm_mk {M : Type u_1} (R : Type u_4) [CommSemiring R] [Semiring M] [Algebra R M] {c d : RingCon M} (h : c ≤ d) (x : M) : (quotientQuotientEquivQuotientₐ R h).symm ⟦x⟧ = ⟦⟦x⟧⟧