English
If e: F' ≅ F'' and α, α' satisfy a commutativity condition, then F'' is RightKanExtension α' whenever F' is RightKanExtension α, and vice versa via the iso.
Русский
Если e: F' ≅ F'' и α, α' удовлетворяют условию коммутативности, то из правого канонического расширения следует соответствующее свойство для F'' и α', и обратно через изоморфизм.
LaTeX
$$$ {F',F'' : D \\to H} (e : F' \\cong F'') \\{L : C \\to D\\} {F : C \\to H} (α : L\\circ F' \\to F) (α' : L\\circ F'' \\to F) (comm : whiskerLeft L e.hom \\to α' = α) [F'.IsRightKanExtension α] : F''.IsRightKanExtension α'$$$
Lean4
theorem isRightKanExtension_of_iso {F' F'' : D ⥤ H} (e : F' ≅ F'') {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F)
(α' : L ⋙ F'' ⟶ F) (comm : whiskerLeft L e.hom ≫ α' = α) [F'.IsRightKanExtension α] : F''.IsRightKanExtension α'
where
nonempty_isUniversal := ⟨IsTerminal.ofIso (F'.isUniversalOfIsRightKanExtension α) (CostructuredArrow.isoMk e comm)⟩
