Commit 2024-03-24 13:55 a746c523

View on Github →

refactor(Algebra/Category): replace TypeMax constructions by UnivLE assumptions (#11420) Replaces TypeMax limit constructions in MonCat, GroupCat, Ring, AlgebraCat and ModuleCat by the UnivLE analogs. Also generalizes some universe assumptions.

Estimated changes

Modified Mathlib/Algebra/Category/AlgebraCat/Limits.lean

modified def AlgebraCat.HasLimits.limitCone

modified def AlgebraCat.HasLimits.limitConeIsLimit

modified theorem AlgebraCat.hasLimitsOfSize

modified def AlgebraCat.limitπAlgHom

modified def AlgebraCat.sectionsSubalgebra

Modified Mathlib/Algebra/Category/GroupCat/Limits.lean

modified def GroupCat.sectionsSubgroup

Modified Mathlib/Algebra/Category/ModuleCat/Abelian.lean

Modified Mathlib/Algebra/Category/ModuleCat/Limits.lean

modified def ModuleCat.HasLimits.limitCone

modified def ModuleCat.HasLimits.limitConeIsLimit

modified def ModuleCat.forget₂AddCommGroupPreservesLimitsAux

added theorem ModuleCat.hasLimit

added theorem ModuleCat.hasLimitsOfShape

modified theorem ModuleCat.hasLimitsOfSize

modified def ModuleCat.limitπLinearMap

modified def ModuleCat.sectionsSubmodule

Modified Mathlib/Algebra/Category/MonCat/Limits.lean

modified def MonCat.sectionsSubmonoid

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

modified def CommRingCat.forget₂CommSemiRingPreservesLimitsAux

modified def CommRingCat.limitCone

modified def CommRingCat.limitConeIsLimit

modified def CommSemiRingCat.limitCone

modified def CommSemiRingCat.limitConeIsLimit

modified def RingCat.forget₂AddCommGroupPreservesLimitsAux

modified def RingCat.limitCone

modified def RingCat.limitConeIsLimit

modified def RingCat.sectionsSubring

modified def SemiRingCat.HasLimits.limitCone

modified def SemiRingCat.HasLimits.limitConeIsLimit

modified def SemiRingCat.forget₂AddCommMonPreservesLimitsAux

modified def SemiRingCat.forget₂MonPreservesLimitsAux

modified def SemiRingCat.limitπRingHom

modified def SemiRingCat.sectionsSubsemiring

Modified Mathlib/Logic/Equiv/TransferInstance.lean

added theorem Equiv.algEquiv_apply

added theorem Equiv.algEquiv_symm_apply