English
Let F,G : C ⥤ Cat and α : F ⟶ G. If for every X, α.app X is final, then map α is final.
Русский
Пусть F,G : C ⥤ Cat и α : F ⟶ G. Если для каждого X стрелка α.app X финальна, то отображение map α финально.
LaTeX
$$$\\forall X,\\ Final(\\alpha_{X}) \\implies Final(\\mathrm{map}\\ \\alpha)$$$
Lean4
/-- The functor `Grothendieck.map α` for a natural transformation `α : F ⟶ G`, with
`F G : C ⥤ Cat`, is final if for each `X : C`, the functor `α.app X` is final. -/
theorem final_map {F G : C ⥤ Cat.{v₂, u₂}} (α : F ⟶ G) [hα : ∀ X, Final (α.app X)] : Final (map α) :=
by
let sC : C ≌ AsSmall.{max u₁ u₂ v₁ v₂} C := AsSmall.equiv
let F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor.{max v₁ u₁ v₂ u₂}
let G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor.{max v₁ u₁ v₂ u₂}
let α' : F' ⟶ G' := whiskerLeft _ (whiskerRight α _)
have : ∀ X, Final (α'.app X) := fun X => inferInstanceAs (AsSmall.equiv.inverse ⋙ _ ⋙ AsSmall.equiv.functor).Final
have hα' : (map α').Final := final_map_small _
dsimp only [α', ← Equivalence.symm_functor] at hα'
have i :=
mapWhiskerLeftIsoConjPreMap sC.symm (whiskerRight α Cat.asSmallFunctor) ≪≫
isoWhiskerLeft _ (isoWhiskerRight (mapWhiskerRightAsSmallFunctor α) _)
have := final_of_natIso i
rwa [← final_iff_equivalence_comp, ← final_iff_comp_equivalence, ← final_iff_equivalence_comp, ←
final_iff_comp_equivalence] at this
