English
The inverse of the canonical fiberwise–colimit isomorphism composes correctly: colimit.ι G X followed by the inverse of the fiberwiseIso equals colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber then colimit.ι (fiberwiseColimit G) X.base.
Русский
Обратное к каноническому изоморфизму между колимитами по слоям корректно калибруется: colimit.ι G X после обратного изображения из отображения волокна равно colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber затем colimit.ι (fiberwiseColimit G) X.base.
LaTeX
$$$\operatorname{colimit.ι} G X \; \circ\; (\operatorname{colimitFiberwiseColimitIso} G)^{-1} = \operatorname{colimit.ι}(\operatorname{Grothendieck.ι} F X.{base} \circ G) X.{fiber} \circ \operatorname{colimit.ι}(\mathrm{fiberwiseColimit}\, G) X.{base}.$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_colimitFiberwiseColimitIso_inv (X : Grothendieck F) :
colimit.ι G X ≫ (colimitFiberwiseColimitIso G).inv =
colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ colimit.ι (fiberwiseColimit G) X.base :=
by
rw [Iso.comp_inv_eq]
simp
