English
If F and G are final, then their composition F ⋙ G is final.
Русский
Если F и G финальные, то их композиция F ⋙ G финальная.
LaTeX
$$$\operatorname{Final}(F) \land \operatorname{Final}(G) \Rightarrow \operatorname{Final}(F \circ G)$$$
Lean4
instance final_comp [hF : Final F] [hG : Final G] : Final (F ⋙ 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 (F ⋙ G) s₃.functor, final_iff_equivalence_comp s₁.inverse, final_natIso_iff i,
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 G s₃.functor, final_iff_equivalence_comp s₂.inverse, final_iff_isIso_colimit_pre] at hG
intro H
rw [← colimit.pre_pre]
infer_instance
