English
For any X ∈ C and d ∈ F.obj X, the canonical isomorphism relating the fiberwise colimit and the total colimit satisfies a natural equality of cocone maps: colimit.ι (Grothendieck.ι F X ⋙ G) d followed by colimit.ι (fiberwiseColimit G) X then by the isoHom equals colimit.ι G ⟨X,d⟩.
Русский
Для любого X и d ∈ F.obj X верна естественная равенство ортомобразующих колимитов: колимит.ι (Grothendieck.ι F X ⋙ G) d затем колимит.ι (fiberwiseColimit G) X затем через изоморфизм достигается колимит.ι G ⟨X,d⟩.
LaTeX
$$$\forall X,d,\; \operatorname{colimit.ι}(\operatorname{Grothendieck.ι} F X \circ G) d \;\circ\; \operatorname{colimit.ι}(\mathrm{fiberwiseColimit}\, G) X \;\circ\; (\operatorname{colimitFiberwiseColimitIso} G).hom = \operatorname{colimit.ι} G \langle X,d \rangle.$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_colimitFiberwiseColimitIso_hom (X : C) (d : F.obj X) :
colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ colimit.ι (fiberwiseColimit G) X ≫ (colimitFiberwiseColimitIso G).hom =
colimit.ι G ⟨X, d⟩ :=
by simp [colimitFiberwiseColimitIso]
