hasPointwiseRightKanExtensionAt_iff_of_iso

English

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

Русский

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

LaTeX

$$$HasPointwiseRightKanExtensionAt\\ L F Y \\iff HasPointwiseRightKanExtensionAt\\ L' F Y$$$

Lean4

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

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