Commit 2023-05-25 17:58 e53aed11

View on Github →

feat: port Algebra.Category.Ring.Limits (#4235)

Estimated changes

Modified Mathlib.lean

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

added def RingEquiv.toCommSemiRingCatIso

added def RingEquiv.toSemiRingCatIso

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

Created Mathlib/Algebra/Category/Ring/Limits.lean

added def CommRingCat.forget₂CommSemiRingPreservesLimitsAux

added def CommRingCat.limitCone

added def CommRingCat.limitConeIsLimit

added def CommSemiRingCat.limitCone

added def CommSemiRingCat.limitConeIsLimit

added def RingCat.forget₂AddCommGroupPreservesLimitsAux

added def RingCat.limitCone

added def RingCat.limitConeIsLimit

added def RingCat.sectionsSubring

added def SemiRingCat.HasLimits.limitCone

added def SemiRingCat.HasLimits.limitConeIsLimit

added def SemiRingCat.forget₂AddCommMonPreservesLimitsAux

added def SemiRingCat.forget₂MonPreservesLimitsAux

added def SemiRingCat.limitπRingHom

added def SemiRingCat.sectionsSubsemiring