ι_mapMap — Mathlib

English

Similarly to the previous iso_inv, but now treating the general i in X and hi for a fixed j, the equality expresses the functorial compatibility of the i-indexed maps with the cofan isomorphism.

Русский

Аналогично предыдущему, но рассматривая общий i в X и hi для фиксированного j, равенство выражает совместимость отображений с индексом i с кофановым изоморфизмом.

LaTeX

$$$X.ιMapObj p i j hi ≫ (c.iso hc).inv = c.inj ⟨i, hi⟩$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_mapMap (i : I) (j : J) (hij : p i = j) : X.ιMapObj p i j hij ≫ mapMap φ p j = φ i ≫ Y.ιMapObj p i j hij := by
  simp only [mapMap, ι_descMapObj]

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