ofCoconeEquiv_symm_apply_desc — Mathlib

English

Symmetric version of the previous description: the desc computed via the symmetric equivalence equals the described composite using h.inverse and counit.

Русский

Симметрическая версия описания: desc, вычисленный через симметрическую эквиваленцию, равен указанной композиции с h.inverse и counit.

LaTeX

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

Lean4

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

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