isLeftKanExtensionAlongEquivalence'

English

If L is an equivalence and α is an isomorphism, then F₁.IsLeftKanExtension α.hom holds via the equivalence to the transformed problem.

Русский

Если L — эквивалентность и α — изоморфизм, то выполняется левое каноновое расширение α.hom вдоль преобразованной задачи через эквивалентность.

LaTeX

$$$F_1.IsLeftKanExtension\\alpha.hom$$$

Lean4

instance isLeftKanExtensionAlongEquivalence' (L : C ⥤ D) (α : F₀ ⟶ L ⋙ F₁) [IsEquivalence L] [IsIso α] :
    F₁.IsLeftKanExtension α :=
  inferInstanceAs <| F₁.IsLeftKanExtension (asIso α : F₀ ≅ (asEquivalence L).functor ⋙ F₁).hom

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