Commit 2026-08-11 14:33 9aa55045

View on Github →

chore(CategoryTheory/Adjunction/AdjointFunctorTheorems): generalize universes (#41244) For theorems involving a category C : Type u (with Category.{v} C), the smallness assumptions or the existence of limits/colimits are expressed relative to an arbitrary universe w (instead of w = v), provided the assumption LocallySmall.{w} C is added. (This makes this more coherent with the API about locally presentable/accessible categories.)

Estimated changes

Modified Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean

modified theorem CategoryTheory.Limits.hasColimits_of_hasLimits_of_hasCoseparator

modified theorem CategoryTheory.Limits.hasColimits_of_hasLimits_of_isCoseparating

modified theorem CategoryTheory.Limits.hasLimits_of_hasColimits_of_hasSeparator

modified theorem CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparating

modified theorem CategoryTheory.isLeftAdjoint_of_preservesColimits_of_isSeparating

modified theorem CategoryTheory.isRightAdjoint_of_preservesLimits_of_isCoseparating

modified theorem CategoryTheory.isRightAdjoint_of_preservesLimits_of_solutionSetCondition

Modified Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/WeaklyInitial.lean

modified theorem CategoryTheory.hasInitial_of_weakly_initial_and_hasWideEqualizers

modified theorem CategoryTheory.has_weakly_initial_of_weakly_initial_set_and_hasProducts

Modified Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean

added def CategoryTheory.Limits.WalkingParallelFamily.equivalenceOfEquiv