restrictionLTOfCoconeIso — Mathlib

English

There is a natural isomorphism between the restriction of the extended cocone to Set.Iic j and the original functor F, encoded as a natural isomorphism of functors.

Русский

Существует естественный изоморфизм между ограничением расширённого кокона до Set.Iic j и исходным функтором F, закодированный как естественный изоморфизм функторов.

LaTeX

$$$\\mathrm{restrictionLT}(\\text{ofCocone } c) \\cong F$$$

Lean4

/-- The isomorphism expressing that `ofCocone c` extends the functor `F`
when `c : Cocone F`. -/
@[simps!]
def restrictionLTOfCoconeIso : SmallObject.restrictionLT (ofCocone c) (Preorder.le_refl j) ≅ F :=
  NatIso.ofComponents (fun ⟨i, hi⟩ ↦ ofCoconeObjIso c i hi) (by intros; apply ofCoconeObjIso_hom_naturality)

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