ofConeEquiv_symm_apply_desc — Mathlib

English

Symmetrically, (ofConeEquiv h).symm P has lift described by counit and map of P.liftConeMorphism; i.e., the symmetric version of the previous statement.

Русский

Аналогично, (ofConeEquiv h).symm P имеет lift, описанный через counit и отображение P.liftConeMorphism; симметричная версия вышеизложенного.

LaTeX

$$$ (ofConeEquiv h).symm P .lift s = (h.counitIso.inv.app s).hom \\circ (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).hom $$$

Lean4

@[simp]
theorem ofConeEquiv_symm_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cone G ≌ Cone F) {c : Cone G}
    (P : IsLimit c) (s) :
    ((ofConeEquiv h).symm P).lift s =
      (h.counitIso.inv.app s).hom ≫ (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).hom :=
  rfl

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