ιMapObj_iso_inv — Mathlib

English

For each i with hi: p i = j, the map X.ιMapObj p i j hi composed with the inverse of the cofan iso equals the projection c.inj ⟨i, hi⟩.

Русский

Для каждого i с hi: p i = j, композиция X.ιMapObj p i j hi с обратной стороной кофана-изоморфизма равна c.inj ⟨i, hi⟩.

LaTeX

$$$X.ιMapObj p i j hi ≫ c.iso^{-1} = c.inj ⟨i, hi⟩$$$

Lean4

@[reassoc (attr := simp)]
theorem ιMapObj_iso_inv (i : I) (hi : p i = j) : X.ιMapObj p i j hi ≫ (c.iso hc).inv = c.inj ⟨i, hi⟩ := by
  apply IsColimit.comp_coconePointUniqueUpToIso_inv

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