isPointwiseRightKanExtensionEquivOfIso

English

There is an equivalence of right Kan extension structures for 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 iff `E'` is. -/
def isPointwiseRightKanExtensionEquivOfIso (e : E ≅ E') :
    E.IsPointwiseRightKanExtension ≃ E'.IsPointwiseRightKanExtension
    where
  toFun h := fun Y => (isPointwiseRightKanExtensionAtEquivOfIso e Y) (h Y)
  invFun h := fun Y => (isPointwiseRightKanExtensionAtEquivOfIso e Y).symm (h Y)
  left_inv h := by simp
  right_inv h := by simp

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