isRightKanExtension_iff_of_iso₂

English

If F1 ≅ F2, then HasRightKanExtension L F1 iff HasRightKanExtension L F2; data correspond via rightExtensionEquivalenceOfIso₂.

Русский

Если F1 ≅ F2, то HasRightKanExtension L F1 эквивалентно HasRightKanExtension L F2; данные соответствуют через rightExtensionEquivalenceOfIso₂.

LaTeX

$$$HasRightKanExtension\\ L\\ F_1 \\iff HasRightKanExtension\\ L\\ F_2$$$

Lean4

theorem isRightKanExtension_iff_of_iso₂ {F₁' F₂' : D ⥤ H} (α₁ : L ⋙ F₁' ⟶ F₁) (α₂ : L ⋙ F₂' ⟶ F₂) (e : F₁ ≅ F₂)
    (e' : F₁' ≅ F₂') (h : whiskerLeft L e'.hom ≫ α₂ = α₁ ≫ e.hom) :
    F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂ :=
  by
  let eq := RightExtension.isUniversalEquivOfIso₂ (RightExtension.mk _ α₁) (RightExtension.mk _ α₂) e e' h
  constructor
  · exact fun _ => ⟨⟨eq.1 (isUniversalOfIsRightKanExtension F₁' α₁)⟩⟩
  · exact fun _ => ⟨⟨eq.2 (isUniversalOfIsRightKanExtension F₂' α₂)⟩⟩

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