isPointwiseRightKanExtensionAtEquivOfIso

English

Equivalence between the pointwise right Kan extension structures of isomorphic right extensions.

Русский

Эквивалентность точечных правых Кан-расширений между изоморфными правыми расширениями.

LaTeX

$$$\\text{isPointwiseRightKanExtensionEquivOfIso}(e) : E.IsPointwiseRightKanExtension \\simeq E'.IsPointwiseRightKanExtension$$$

Lean4

/-- If two right extensions `E` and `E'` are isomorphic, `E` is a pointwise
right Kan extension at `Y` iff `E'` is. -/
def isPointwiseRightKanExtensionAtEquivOfIso (e : E ≅ E') (Y : D) :
    E.IsPointwiseRightKanExtensionAt Y ≃ E'.IsPointwiseRightKanExtensionAt Y :=
  IsLimit.equivIsoLimit ((coneAtFunctor L F Y).mapIso e)

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