ofCoconeEquiv_apply_desc — Mathlib

English

Given an equivalence h between cocone categories and a colimit P on h.functor.obj c, the described desc of s equals the composite shown involving h.unit and h.inverse.

Русский

Дано эквивалентность h между категориями коконов и из колимита P на h.functor.obj c; описанный desc кокона равен композиции через h.unit и h.inverse.

LaTeX

$$$ (ofCoconeEquiv h P).desc s = (h.unit.app c).hom \;\circ\; (h.inverse.map (P.descCoconeMorphism (h.functor.obj s))).hom \;\circ\; (h.unitInv.app s).hom $$$

Lean4

@[simp]
theorem ofCoconeEquiv_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cocone G ≌ Cocone F) {c : Cocone G}
    (P : IsColimit (h.functor.obj c)) (s) :
    (ofCoconeEquiv h P).desc s =
      (h.unit.app c).hom ≫ (h.inverse.map (P.descCoconeMorphism (h.functor.obj s))).hom ≫ (h.unitInv.app s).hom :=
  rfl

Похожие утверждения