Theorems · Definition · category theory

CategoryTheory.Limits.Cocone.toCostructuredArrowCocone

{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {K : CategoryTheory.Functor J C} →
              (c : CategoryTheory.Limits.Cocone K) →
                (F : CategoryTheory.Functor C D) →
                  {X : D} →
                    (f : F.obj c.pt ⟶ X) →
                      CategoryTheory.Limits.Cocone
                        ((F.mapCocone c).toCostructuredArrow.comp
                          ((CategoryTheory.CostructuredArrow.map f).comp (CategoryTheory.CostructuredArrow.pre K F X)))

Given a cocone c : Cocone K and a map f : F.obj c.X ⟶ X, we can construct a cocone of costructured arrows over X with f as the cone point.

Defined in

Mathlib.CategoryTheory.Limits.ConeCategory

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category