Commit 2024-10-29 13:37 43e571a7

View on Github →

feat(CategoryTheory/Limits): the end of a functor (#18082) In this file, given a functor F : Jᵒᵖ ⥤ J ⥤ C, we define its end end_ F. It is a particular case of multiequalizer. The abbreviation Wedge for the corresponding category of cones is also introduced.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/End.lean

added theorem CategoryTheory.Limits.Wedge.IsLimit.hom_ext

added def CategoryTheory.Limits.Wedge.IsLimit.lift

added theorem CategoryTheory.Limits.Wedge.IsLimit.lift_ι

added theorem CategoryTheory.Limits.Wedge.condition

added theorem CategoryTheory.Limits.Wedge.mk_ι

added theorem CategoryTheory.Limits.end_.condition

added theorem CategoryTheory.Limits.end_.lift_π

added theorem CategoryTheory.Limits.hom_ext

added def CategoryTheory.Limits.multicospanIndexEnd