ι_inv_pre — Mathlib

English

If E : K ⥤ J and F : J ⥤ C admit colimits and the precomposition map pre F E is an isomorphism, then for every k ∈ K one has colimit.ι F (E.obj k) ≫ inv(colimit.pre F E) = colimit.ι (E ⋙ F) k.

Русский

Если E : K ⥤ J, F : J ⥤ C имеют колимиты и отображение pre F E является изоморфизмом, то для каждого k ∈ K выполняется colimit.ι F (E.obj k) ≫ inv(colimit.pre F E) = colimit.ι (E ⋙ F) k.

LaTeX

$$$ \\operatorname{colimit.ι} F (E.{\\mathrm{obj}}\\, k) \\; \\circ \\operatorname{inv} (\\operatorname{colimit.pre} F E) = \\operatorname{colimit.ι} (E \\circ F) k $$$

Lean4

@[reassoc (attr := simp)]
theorem ι_inv_pre [IsIso (pre F E)] (k : K) : colimit.ι F (E.obj k) ≫ inv (colimit.pre F E) = colimit.ι (E ⋙ F) k := by
  simp [IsIso.comp_inv_eq]

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