Commit 2024-01-06 17:34 9cbd1e21

View on Github →

feat: uliftFunctor preserves arbitrary colimits (#8545) Rescuing and porting my old proof now that @dagurtomas created a file for it. Also includes some universe generalizations in the file Limits/Types which overlap with @joelriou's #7020.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Creates.lean

added def CategoryTheory.createsColimitOfFullyFaithfulOfPreserves

added def CategoryTheory.createsLimitOfFullyFaithfulOfPreserves

Modified Mathlib/CategoryTheory/Limits/Preserves/Ulift.lean

added def CategoryTheory.Limits.Types.coconeOfSet

added theorem CategoryTheory.Limits.Types.descFun_apply_spec

added theorem CategoryTheory.Limits.Types.descFun_spec

added def CategoryTheory.Limits.Types.descSet

added theorem CategoryTheory.Limits.Types.descSet_empty

added theorem CategoryTheory.Limits.Types.descSet_inter_of_ne

added theorem CategoryTheory.Limits.Types.descSet_spec

added theorem CategoryTheory.Limits.Types.descSet_univ

added theorem CategoryTheory.Limits.Types.exists_unique_mem_descSet

added theorem CategoryTheory.Limits.Types.iUnion_descSet_singleton

added theorem CategoryTheory.Limits.Types.mem_descSet_singleton

deleted def CategoryTheory.Limits.Types.quotEquiv

deleted def CategoryTheory.Limits.Types.sectionsEquiv'

modified def CategoryTheory.Limits.Types.sectionsEquiv

Modified Mathlib/CategoryTheory/Limits/Types.lean

modified def CategoryTheory.Limits.Types.colimitCoconeIsColimit

added theorem CategoryTheory.Limits.Types.jointly_surjective_of_isColimit