English
If G is a final functor, then the precomposition Grothendieck construction Grothendieck.pre F G is a final functor.
Русский
Если G — финальная функторa, тогда предоконтекстная конструция Гротендика Grothendieck.pre F G является финальным функтором.
LaTeX
$$$\\text{Final}(\\mathrm{Grothendieck.pre}\\, F\\, G)$, provided $[\\mathrm{Final}\\;G]$$$
Lean4
instance final_pre [hG : Final G] : (Grothendieck.pre F G).Final :=
by
constructor
rintro ⟨d, f⟩
let ⟨u, c, g⟩ : Nonempty (StructuredArrow d G) := inferInstance
letI : Nonempty (StructuredArrow ⟨d, f⟩ (pre F G)) := ⟨u, ⟨c, (F.map g).obj f⟩, ⟨(by exact g), (by exact 𝟙 _)⟩⟩
apply zigzag_isConnected
rintro ⟨⟨⟨⟩⟩, ⟨bi, fi⟩, ⟨gbi, gfi⟩⟩ ⟨⟨⟨⟩⟩, ⟨bj, fj⟩, ⟨gbj, gfj⟩⟩
dsimp at fj fi gfi gbi gbj gfj
apply
Zigzag.trans (j₂ := StructuredArrow.mk (Y := ⟨bi, ((F.map gbi).obj f)⟩) (Grothendieck.Hom.mk gbi (𝟙 _)))
(.of_zag
(.inr
⟨StructuredArrow.homMk (Grothendieck.Hom.mk (by dsimp; exact 𝟙 _) (eqToHom (by simp) ≫ gfi))
(by apply Grothendieck.ext <;> simp)⟩))
refine
Zigzag.trans (j₂ := StructuredArrow.mk (Y := ⟨bj, ((F.map gbj).obj f)⟩) (Grothendieck.Hom.mk gbj (𝟙 _))) ?_
(.of_zag
(.inl
⟨StructuredArrow.homMk (Grothendieck.Hom.mk (by dsimp; exact 𝟙 _) (eqToHom (by simp) ≫ gfj))
(by apply Grothendieck.ext <;> simp)⟩))
exact
zigzag_prefunctor_obj_of_zigzag (Grothendieck.structuredArrowToStructuredArrowPre F G d f)
(isPreconnected_zigzag (.mk gbi) (.mk gbj))
