Theorem CategoryTheory.Limits.hasLimits_of_hasColimits_of_hasSeparator

Modification history

2026-08-11 14:33

Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean

chore(CategoryTheory/Adjunction/AdjointFunctorTheorems): generalize universes (#41244) …

Modified CategoryTheory.Limits.hasLimits_of_hasColimits_of_hasSeparator View on Github →

2024-12-16 16:45

Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean

feat(CategoryTheory/Abelian/GrothendieckAxioms): introduce Grothendieck categories (#18510) …

Added CategoryTheory.Limits.hasLimits_of_hasColimits_of_hasSeparator View on Github →