English
Same as map_final: the induced map between comma categories is final.
Русский
То же самое, что и map_final: индуцированная карта между категориями запятой финальная.
LaTeX
$$$\\\\operatorname{Final}(\\\\mathrm{Comma.map}(iL.hom,iR.inv))$$$
Lean4
/-- Let `A` and `B` be filtered categories, `R : B ⥤ T` be final and `L : A ⥤ T`. Then, the
comma category `Comma L R` is filtered. -/
instance isFiltered_of_final [IsFiltered A] [IsFiltered B] [R.Final] : IsFiltered (Comma L R) :=
by
haveI (a : A) : IsFiltered (Comma (fromPUnit (L.obj a)) R) :=
R.final_iff_isFiltered_structuredArrow.mp inferInstance (L.obj a)
have (a : A) : (fromPUnit (Over.mk (𝟙 a))).Final := final_const_of_isTerminal Over.mkIdTerminal
let η (a : A) : fromPUnit (Over.mk (𝟙 a)) ⋙ Over.forget a ⋙ L ≅ fromPUnit (L.obj a) :=
NatIso.ofComponents (fun _ => Iso.refl _)
have (a : A) := IsFiltered.of_final (map (L := fromPUnit (L.obj a)) (F := 𝟭 T) (η a).hom ((Iso.refl (𝟭 B ⋙ R)).inv))
have : RepresentablyCoflat (fst L R) :=
⟨fun a => IsFiltered.of_equivalence (CostructuredArrow.ofCommaFstEquivalence L R a).symm⟩
apply isFiltered_of_representablyCoflat (fst L R)
