hasPointwiseRightKanExtensionAt_iff_of_natIso

English

As above, invariance of HasPointwiseLeftKanExtensionAt under equivalences of D via E.

Русский

Как выше, инвариантность HasPointwiseLeftKanExtensionAt при эквивалентностях D через E.

LaTeX

$$$\\text{HasPointwiseLeftKanExtensionAt}(L,F,Y) \\iff \\text{HasPointwiseLeftKanExtensionAt}(L',F,Y').$$$

Lean4

/-- `HasPointwiseRightKanExtensionAt` is invariant when we replace `L` by an equivalent functor. -/
theorem hasPointwiseRightKanExtensionAt_iff_of_natIso {L' : C ⥤ D} (e : L ≅ L') (Y : D) :
    HasPointwiseRightKanExtensionAt L F Y ↔ HasPointwiseRightKanExtensionAt L' F Y :=
  by
  revert L L' e
  suffices ∀ ⦃L L' : C ⥤ D⦄ (_ : L ≅ L') [HasPointwiseRightKanExtensionAt L F Y], HasPointwiseRightKanExtensionAt L' F Y
    from fun L L' e => ⟨fun _ => this e, fun _ => this e.symm⟩
  intro L L' e _
  let Φ : StructuredArrow Y L' ≌ StructuredArrow Y L := Comma.mapRightIso _ e.symm
  let e' : StructuredArrow.proj Y L' ⋙ F ≅ Φ.functor ⋙ StructuredArrow.proj Y L ⋙ F := Iso.refl _
  exact hasLimit_of_iso e'.symm

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