Theorem CategoryTheory.Limits.hasColimits_of_hasLimits_of_hasCoseparator

Modification history

2026-08-11 14:33

Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean

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

Modified CategoryTheory.Limits.hasColimits_of_hasLimits_of_hasCoseparator View on Github →

2024-12-16 16:45

Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean

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

Added CategoryTheory.Limits.hasColimits_of_hasLimits_of_hasCoseparator View on Github →