English
Let F', F'' : D ⥤ H and φ : F'' ⟶ F' be an isomorphism. For α and α' with a commutativity relation, F'' IsRightKanExtension α' iff IsIso φ when F' IsRightKanExtension α.
Русский
Пусть F', F'' : D ⥤ H и φ : F'' ⟶ F' — изоморфизм. При заданных α, α' и условии коммутатора, F'' IsRightKanExtension α' тогда и только тогда, когда φ изоморфен, если F' IsRightKanExtension α.
LaTeX
$$$ \\forall {F',F''} (φ : F'' \\to F') {L} {F} (α : L\\circ F' \\to F) (α' : L\\circ F'' \\to F) (comm : whiskerLeft L φ \\; α' = α) [F'.IsRightKanExtension α] : F''.IsRightKanExtension α' \\iff IsIso φ$$
Lean4
theorem isRightKanExtension_iff_isIso {F' : D ⥤ H} {F'' : D ⥤ H} (φ : F'' ⟶ F') {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F)
(α' : L ⋙ F'' ⟶ F) (comm : whiskerLeft L φ ≫ α = α') [F'.IsRightKanExtension α] :
F''.IsRightKanExtension α' ↔ IsIso φ := by
constructor
· intro
rw [F'.hom_ext_of_isRightKanExtension α φ (rightKanExtensionUnique _ α' _ α).hom (by simp [comm])]
infer_instance
· intro
rw [isRightKanExtension_iff_of_iso (asIso φ) α' α comm]
infer_instance
