Commit 2024-11-15 06:49 44738833

View on Github →

feat(CategoryTheory/Comma): Comma.fst L R is final if R is (#19015)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Comma/Basic.lean

added def CategoryTheory.Comma.opEquiv

added def CategoryTheory.Comma.opFunctor

added def CategoryTheory.Comma.opFunctorCompFst

added def CategoryTheory.Comma.opFunctorCompSnd

added def CategoryTheory.Comma.postIso

added def CategoryTheory.Comma.unopFunctor

added def CategoryTheory.Comma.unopFunctorCompFst

added def CategoryTheory.Comma.unopFunctorCompSnd

Created Mathlib/CategoryTheory/Comma/Final.lean

Modified Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean

added theorem CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom

added theorem CategoryTheory.Functor.leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom

modified theorem CategoryTheory.Functor.ι_leftKanExtensionObjIsoColimit_hom

Modified Mathlib/CategoryTheory/Limits/Final.lean

added theorem CategoryTheory.Functor.Final.ι_colimitIso_hom

added theorem CategoryTheory.Functor.Final.ι_colimitIso_inv

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

added theorem CategoryTheory.Limits.colimit.ι_inv_pre