homologyι_naturality — Mathlib

English

For a morphism φ: K → L, the naturality relation between homology maps and opcycles maps holds at i: homology map followed by L.homologyι i equals K.homologyι i followed by opcyclesMap φ i.

Русский

Для морфизма φ: K → L выполняется естественность перехода на гомологии: homologyMap φ i затем L.homologyι i равно K.homologyι i затем opcyclesMap φ i.

LaTeX

$$$$ homologyMap(\varphi,i) \;\circ\; L.homologyι i = K.homologyι i \;\circ\; opcyclesMap(\varphi,i) $$$$

Lean4

@[reassoc (attr := simp)]
theorem homologyι_naturality : homologyMap φ i ≫ L.homologyι i = K.homologyι i ≫ opcyclesMap φ i :=
  ShortComplex.homologyι_naturality _

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