Def CategoryTheory.createsColimitOfFullyFaithfulOfPreserves

Modification history

2025-02-02 12:28
Mathlib/CategoryTheory/Limits/Creates.lean
feat: creation of products and equalizers implies creation of limits (#21321)
Deleted CategoryTheory.createsColimitOfFullyFaithfulOfPreservesView on Github →
2024-04-12 14:33
Mathlib/CategoryTheory/Limits/Creates.lean
chore(CategoryTheory): move Full, Faithful, EssSurj, IsEquivalence and ReflectsIsomorphisms to the Functor namespace (#11985) …
Modified CategoryTheory.createsColimitOfFullyFaithfulOfPreservesView on Github →
2024-01-06 17:34
Mathlib/CategoryTheory/Limits/Creates.lean
feat: uliftFunctor preserves arbitrary colimits (#8545) …
Added CategoryTheory.createsColimitOfFullyFaithfulOfPreservesView on Github →