English
There is a premapping from the category of structured arrows over G at d to the category of structured arrows over the Grothendieck preconstruction ⟨d, f⟩ with fibers acted on by the identity; the action on objects sends (X, h) to the structured arrow with base X.right and fiber (F.map X.hom)(f).
Русский
Существует префунктор от категории структурированных стрел над G в d к категории структурированных стрел над ⟨d, f⟩ в предфункторе pre F G, действующий на волокнах идентичностью; на объектах коэффициентный элемент X — база X.right, волокно (F.map X.hom)(f).
LaTeX
$$$\\text{Prefunctor}\\colon \\mathrm{StructuredArrow}(d,G) \\;\xrightarrow{\\text{to structured arrow pre}}\\; \\mathrm{StructuredArrow}\\langle d,f\\rangle (\\mathrm{pre}\\, F\\, G)$$$
Lean4
/-- A prefunctor mapping structured arrows on `G` to structured arrows on `pre F G` with their
action on fibers being the identity. -/
def structuredArrowToStructuredArrowPre (d : D) (f : F.obj d) : StructuredArrow d G ⥤q StructuredArrow ⟨d, f⟩ (pre F G)
where
obj := fun X =>
StructuredArrow.mk (Y := ⟨X.right, (F.map X.hom).obj f⟩)
(Grothendieck.Hom.mk (by exact X.hom) (by dsimp; exact 𝟙 _))
map := fun g =>
StructuredArrow.homMk
(Grothendieck.Hom.mk (by exact g.right) (eqToHom (by dsimp; rw [← StructuredArrow.w g, map_comp, Cat.comp_obj])))
(by
simp only [StructuredArrow.mk_right]
generalize_proofs
apply Grothendieck.ext <;> simp)
