Commit 2025-11-26 15:01 75ee4adc

feat(RingTheory/Congruence/Hom): prove basic isomorphisms theorems for ring congruences (#26277) This file contains elementary definitions involving congruence relations and morphisms for semirings, rings, and algebras.

• 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 It is an adaptation of what existed for multiplicative congruences (docs#Con) and is only useful for semirings which are not rings.