ι_preservesColimitIso_inv — Mathlib

English

The projection morphism ι commutes with the inverse of preservesColimitIso: ι ≫ preservesColimitIso.inv = G.map (ι).

Русский

Проекция ι коммутирует с обратной стороны preservesColimitIso: ι ∘ inv = G.map(ι).

LaTeX

$$$\\mathrm{colimit.ι}\\ _ j \\; ≫ (\\mathrm{preservesColimitIso}\\ G\\ F)\\mathrm{inv} = G.map(\\mathrm{colimit.ι}\\ F j)$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_preservesColimitIso_inv (j : J) : colimit.ι _ j ≫ (preservesColimitIso G F).inv = G.map (colimit.ι F j) :=
  IsColimit.comp_coconePointUniqueUpToIso_inv _ (colimit.isColimit (F ⋙ G)) j

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