ι_colimitIso_inv — Mathlib

English

For HasColimit G, the morphism colimit.ι G (F.obj X) composed with (colimitIso F G).inv equals colimit.ι(F ⋙ G) X.

Русский

При наличии колимита G композиция colimit.ι G (F.obj X) с обратным коллимит-изоморфизмом (colimitIso F G).inv даёт colimit.ι(F ⋙ G) X.

LaTeX

$$$$ \operatorname{colimit.\iota} G (F(X)) \;\gg \; (\operatorname{colimitIso} F G)^{-1} = \operatorname{colimit.\iota}(F \circ G)(X). $$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimitIso_inv [HasColimit G] (X : C) : colimit.ι G (F.obj X) ≫ (colimitIso F G).inv = colimit.ι (F ⋙ G) X :=
  by simp [colimitIso]

Похожие утверждения