hasPointwiseLeftKanExtensionAt_iff_of_iso

English

HasPointwiseLeftKanExtensionAt is invariant under a natural isomorphism between L and L'.

Русский

У HasPointwiseLeftKanExtensionAt сохраняется инвариантность при натуральной изоморфности между L и L'.

LaTeX

$$$HasPointwiseLeftKanExtensionAt\\ L F Y \\iff HasPointwiseLeftKanExtensionAt\\ L' F Y$$$

Lean4

theorem hasPointwiseLeftKanExtensionAt_iff_of_iso {Y₁ Y₂ : D} (e : Y₁ ≅ Y₂) :
    HasPointwiseLeftKanExtensionAt L F Y₁ ↔ HasPointwiseLeftKanExtensionAt L F Y₂ :=
  by
  revert Y₁ Y₂ e
  suffices ∀ ⦃Y₁ Y₂ : D⦄ (_ : Y₁ ≅ Y₂) [HasPointwiseLeftKanExtensionAt L F Y₁], HasPointwiseLeftKanExtensionAt L F Y₂
    from fun Y₁ Y₂ e => ⟨fun _ => this e, fun _ => this e.symm⟩
  intro Y₁ Y₂ e _
  change HasColimit ((CostructuredArrow.mapIso e.symm).functor ⋙ CostructuredArrow.proj L Y₁ ⋙ F)
  infer_instance

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