Commit 2026-06-19 09:20 65e1648a

View on Github →

feat(Algebra/Category/Ring): IsLocalRing for limits (#37008) This PR introduces theorems establishing that limits in CommRingCat (specifically pullbacks and equalizers) preserve local homomorphisms and IsLocalRing properties under suitable conditions.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

added theorem CommRingCat.Limits.isLocalRing

added theorem CommRingCat.Limits.isUnit_iff_forall_isUnit

added theorem CommRingCat.Limits.π_isLocalHom

added theorem CommRingCat.equalizer_limit_isLocalRing

deleted theorem CommRingCat.equalizer_ι_isLocalHom

modified def CommRingCat.pullbackCone

modified def CommRingCat.pullbackConeIsLimit

added theorem CommRingCat.pullback_isLocalRing

Created Mathlib/RingTheory/LocalRing/Pullback.lean

added theorem AlgHom.isLocalRing_pullback

added theorem AlgHom.isUnit_pullback_mk_iff

added theorem AlgHom.pullback_comm_sq

added theorem AlgHom.surjective_pullbackFst_of_surjective

added theorem AlgHom.surjective_pullbackSnd_of_surjective

added theorem RingHom.isLocalRing_eqLocus

added theorem RingHom.isLocalRing_pullback

added theorem RingHom.isUnit_pullback_mk_iff

added theorem RingHom.map_pullbackSnd_ker_pullbackFst_eq

added theorem RingHom.pullback_comm_sq

added theorem RingHom.surjective_pullbackFst_of_surjective

added theorem RingHom.surjective_pullbackSnd_of_surjective

Modified Mathlib/RingTheory/LocalRing/RingHom/Basic.lean

modified theorem RingHom.domain_isLocalRing