isPointwiseLeftKanExtensionEquivOfIso

English

Analogous invariance holds for right extensions: if E and E' are isomorphic, the pointwise right Kan extension property is preserved across Y and Y'.

Русский

Аналогично сохраняется свойство точечного правого Кан-расширения при изоморфизме E и E'.

LaTeX

$$$\\text{isPointwiseRightKanExtensionAtEquivOfIso}(e) : E.IsPointwiseRightKanExtensionAt Y \\iff E'.IsPointwiseRightKanExtensionAt Y'$$$

Lean4

/-- If two left extensions `E` and `E'` are isomorphic, `E` is a pointwise
left Kan extension iff `E'` is. -/
def isPointwiseLeftKanExtensionEquivOfIso (e : E ≅ E') : E.IsPointwiseLeftKanExtension ≃ E'.IsPointwiseLeftKanExtension
    where
  toFun h := fun Y => (isPointwiseLeftKanExtensionAtEquivOfIso e Y) (h Y)
  invFun h := fun Y => (isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm (h Y)
  left_inv h := by simp
  right_inv h := by simp

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