English
In a diagram of functors with iL, iR forming a commutative square up to isomorphism, the induced map between the comma categories is final.
Русский
В диаграмме функторов с iL, iR, образующей квадрат коммутирования до изоморфизма, индуцированная функция между категориями запятой финальная.
LaTeX
$$$\\\\mathrm{Final}(\\\\mathrm{Comma.map}(iL.hom,iR.inv))$$$
Lean4
instance final_fst [R.Final] : (fst L R).Final :=
by
let sA : A ≌ AsSmall.{max u₁ u₂ u₃ v₁ v₂ v₃} A := AsSmall.equiv
let sB : B ≌ AsSmall.{max u₁ u₂ u₃ v₁ v₂ v₃} B := AsSmall.equiv
let sT : T ≌ AsSmall.{max u₁ u₂ u₃ v₁ v₂ v₃} T := AsSmall.equiv
let L' := sA.inverse ⋙ L ⋙ sT.functor
let R' := sB.inverse ⋙ R ⋙ sT.functor
let fC : Comma L R ⥤ Comma L' R' :=
map (F₁ := sA.functor) (F := sT.functor) (F₂ := sB.functor) (isoWhiskerRight sA.unitIso (L ⋙ sT.functor)).hom
(isoWhiskerRight sB.unitIso (R ⋙ sT.functor)).hom
have : Final (fst L' R') := final_fst_small _ _
apply final_of_natIso (F := (fC ⋙ fst L' R' ⋙ sA.inverse))
exact (Functor.associator _ _ _).symm.trans (Iso.compInverseIso (mapFst _ _))
