English
Let A and B be filtered categories, L and R functors with R final. Then snd L R is final.
Русский
Пусть A и B — фильтрованные категории, L и R — функторы; R финальная. Тогда snd L R финальна.
LaTeX
$$$\\\\operatorname{Final}(\\\\operatorname{snd}(L,R))$$$
Lean4
/-- Let `A` and `B` be filtered categories, `R : B ⥤ T` be final and `R : A ⥤ T`. Then, the
projection `snd L R : Comma L R ⥤ B` is final. -/
instance final_snd [IsFiltered A] [IsFiltered B] [R.Final] : (snd L R).Final :=
by
let iL : star.{1} A ⋙ 𝟭 _ ≅ L ⋙ star _ := Iso.refl _
let iR : 𝟭 B ⋙ star.{1} B ≅ R ⋙ star _ := Iso.refl _
have := map_final iL iR
let s := (equivProd (𝟭 _) (star B)).trans <| prod.leftUnitorEquivalence B
let iS : map iL.hom iR.inv ⋙ s.functor ≅ snd L R :=
NatIso.ofComponents (fun _ => Iso.refl _) (fun f => by simp [iL, iR, s])
apply final_of_natIso iS
