English
RightKanExtension α for F' is equivalent to RightKanExtension α' for F'' if there is an isomorphism e: F' ≅ F'' and a commutativity condition linking α, α' and the iso.
Русский
Правое каноническое расширение α на F' эквивалентно правому каноническому расширению α' на F'' при существовании изоморфизма e: 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 \\; α' = α) : F'.IsRightKanExtension α \\iff F'' .IsRightKanExtension α'$$$
Lean4
theorem isRightKanExtension_iff_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 α' :=
by
constructor
· intro
exact isRightKanExtension_of_iso e α α' comm
· intro
refine isRightKanExtension_of_iso e.symm α' α ?_
rw [← comm, ← whiskerLeft_comp_assoc, Iso.symm_hom, e.inv_hom_id, whiskerLeft_id', id_comp]
