ιMapObjOrZero_mapMap — Mathlib

English

The interaction of ιMapObjOrZero with a map φ between graded objects obeys naturality: ιMapObjOrZero p i j followed by mapMap φ p j equals φ i followed by ιMapObjOrZero p i j.

Русский

Взаимодействие ιMapObjOrZero с отображением φ между градуированными объектами подчиняется естественности: ιMapObjOrZero p i j затем mapMap φ p j равняется φ i затем ιMapObjOrZero p i j.

LaTeX

$$$X.ιMapObjOrZero\\; p\\; i\\; j \\;\\circ\\; mapMap\\; φ\\; p\\; j = φ\\; i \\circ\\; X.ιMapObjOrZero\\; p\\; i\\; j$$

Lean4

@[reassoc (attr := simp)]
theorem ιMapObjOrZero_mapMap : X.ιMapObjOrZero p i j ≫ mapMap φ p j = φ i ≫ Y.ιMapObjOrZero p i j :=
  by
  by_cases h : p i = j
  · simp only [ιMapObjOrZero_eq _ _ _ _ h, ι_mapMap]
  · simp only [ιMapObjOrZero_eq_zero _ _ _ _ h, zero_comp, comp_zero]

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