isPointwiseLeftKanExtensionAtEquivOfIso'

English

If two left extensions E and E' are isomorphic, then E is a pointwise left Kan extension iff E' is a pointwise left Kan extension (evaluated at any object Y).

Русский

Если два левых Кан-расширения E и E' изоморфны, то E является точечным лево-кановским расширением тогда и только тогда, когда E' также является таковым (для произвольного Y).

LaTeX

$$$\\text{IsPointwiseLeftKanExtension}(E, Y) \\iff \\text{IsPointwiseLeftKanExtension}(E', Y)$$$

Lean4

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

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