Theorems · Definition · category theory

CategoryTheory.Limits.end_.lift

{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)} →
          [inst_2 : CategoryTheory.Limits.HasEnd F] →
            {X : C} →
              (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j) →
                (∀ ⦃i j : J⦄ (g : i ⟶ j),
                    CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
                      CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j)) →
                  (X ⟶ CategoryTheory.Limits.end_ F)

Constructor for morphisms to the end of a functor.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.End

Cited by

5 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasEnd