English
If F is final and F ⋙ G is final, then G is final.
Русский
Если F финальная и F ⋙ G финальная, то G финальная.
LaTeX
$$$\operatorname{Final}(F) \land \operatorname{Final}(F \circ G) \Rightarrow \operatorname{Final}(G)$$$
Lean4
theorem final_of_final_comp [hF : Final F] [hFG : Final (F ⋙ G)] : Final G :=
by
let s₁ : C ≌ AsSmall.{max u₁ v₁ u₂ v₂ u₃ v₃} C := AsSmall.equiv
let s₂ : D ≌ AsSmall.{max u₁ v₁ u₂ v₂ u₃ v₃} D := AsSmall.equiv
let s₃ : E ≌ AsSmall.{max u₁ v₁ u₂ v₂ u₃ v₃} E := AsSmall.equiv
let _i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ (s₂.inverse ⋙ G ⋙ s₃.functor) :=
isoWhiskerLeft (s₁.inverse ⋙ F) (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
rw [final_iff_comp_equivalence G s₃.functor, final_iff_equivalence_comp s₂.inverse, final_iff_isIso_colimit_pre]
rw [final_iff_comp_equivalence F s₂.functor, final_iff_equivalence_comp s₁.inverse, final_iff_isIso_colimit_pre] at hF
rw [final_iff_comp_equivalence (F ⋙ G) s₃.functor, final_iff_equivalence_comp s₁.inverse, final_natIso_iff _i,
final_iff_isIso_colimit_pre] at hFG
intro H
replace hFG := hFG H
rw [← colimit.pre_pre] at hFG
exact IsIso.of_isIso_comp_left (colimit.pre _ (s₁.inverse ⋙ F ⋙ s₂.functor)) _
