Theorems · Theorem · category theory

CategoryTheory.Limits.IndObjectPresentation.extend_isColimit_desc_app_hom_apply

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A) (η : A ⟶ B) [inst_1 : CategoryTheory.IsIso η]
  (s : CategoryTheory.Limits.Cocone (P.F.comp CategoryTheory.yoneda)) (X : Cᵒᵖ) (a : (P.cocone.extend η).pt.obj X),
  (CategoryTheory.ConcreteCategory.hom (((P.extend η).isColimit.desc s).app X)) a =
    ((P.coconeIsColimit.desc s).app X).hom' ((CategoryTheory.inv (η.app X)).hom' a)

Defined in

Mathlib.CategoryTheory.Limits.Indization.IndObject

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsIso