Theorems · Definition · category theory

CategoryTheory.Limits.end_

{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) → [CategoryTheory.Limits.HasEnd F] → C

The end of a functor F : Jᵒᵖ ⥤ J ⥤ C.

Defined in: Mathlib.CategoryTheory.Limits.Shapes.End
Cited by: 20 results in Mathlib
Foundations: Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Category CategoryTheory.Limits.HasEnd

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Functorstatement and proof · cited by 16,252
Oppositestatement and proof · cited by 8,081
CategoryTheory.Limits.multiequalizerproof · cited by 33
CategoryTheory.Limits.multicospanIndexEndproof · cited by 22
CategoryTheory.Limits.HasEndstatement and proof · cited by 14

Cited by25

Results whose statement or proof uses this declaration.

CategoryTheory.Enriched.FunctorCategory.enrichedHomproof · cited by 33
CategoryTheory.Limits.end_.πstatement · cited by 22
CategoryTheory.Limits.end_.hom_extstatement and proof · cited by 11
CategoryTheory.Limits.end_.lift_πstatement · cited by 9
CategoryTheory.Enriched.FunctorCategory.enrichedComp_πstatement · cited by 7
CategoryTheory.Limits.end_.mapstatement · cited by 6
CategoryTheory.Limits.end_.liftstatement · cited by 5
CategoryTheory.Limits.end_.conditionstatement · cited by 3
CategoryTheory.Limits.end_.map_πstatement · cited by 3
CategoryTheory.Limits.endFunctorproof · cited by 2
CategoryTheory.Enriched.FunctorCategory.enriched_assocproof · cited by 2
CategoryTheory.Enriched.FunctorCategory.enriched_comp_idproof · cited by 2