Commit 2024-12-21 09:50 e638cadf

View on Github →

feat(CategoryTheory/SmallObject/Iteration): Functor.ofCocone (#19643) Given a functor F : Set.Iio j ⥤ C and c : Cocone F, we define an extension of F as a functor Set.Iic j ⥤ C for which the top element is mapped to c.pt.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean

added def CategoryTheory.Functor.isColimitCoconeOfLEOfCocone

added def CategoryTheory.Functor.ofCocone.map

added theorem CategoryTheory.Functor.ofCocone.map_comp

added theorem CategoryTheory.Functor.ofCocone.map_id

added def CategoryTheory.Functor.ofCocone.obj

added def CategoryTheory.Functor.ofCocone.objIso

added def CategoryTheory.Functor.ofCocone.objIsoPt

added def CategoryTheory.Functor.ofCocone

added def CategoryTheory.Functor.ofCoconeObjIso

added def CategoryTheory.Functor.ofCoconeObjIsoPt

added theorem CategoryTheory.Functor.ofCoconeObjIso_hom_naturality

added theorem CategoryTheory.Functor.ofCocone_map

added theorem CategoryTheory.Functor.ofCocone_map_to_top

added def CategoryTheory.Functor.restrictionLTOfCoconeIso