isPointwiseRightKanExtensionAtEquivOfIso'

English

Equivalence of IsPointwiseRightKanExtensionAt under an isomorphism for right extensions.

Русский

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

LaTeX

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

Lean4

/-- The condition of being a pointwise right Kan extension at an object `Y` is
unchanged by replacing `Y` by an isomorphic object `Y'`. -/
def isPointwiseRightKanExtensionAtEquivOfIso' {Y Y' : D} (e : Y ≅ Y') :
    E.IsPointwiseRightKanExtensionAt Y ≃ E.IsPointwiseRightKanExtensionAt Y'
    where
  toFun h := E.isPointwiseRightKanExtensionAtOfIso' h e
  invFun h := E.isPointwiseRightKanExtensionAtOfIso' h e.symm
  left_inv
    h := by
    dsimp only [IsPointwiseRightKanExtensionAt]
    apply Subsingleton.elim
  right_inv
    h := by
    dsimp only [IsPointwiseRightKanExtensionAt]
    apply Subsingleton.elim

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