toCycles_i — Mathlib

English

For a fixed i with K.HasHomology i, we have the identity toCycles_i: K.toCycles i j ≫ K.iCycles j = K.d i j.

Русский

Для фиксированного i с K.HasHomology i имеет место тождество toCycles_i: K.toCycles i j ≫ K.iCycles j = K.d i j.

LaTeX

$$$K.toCycles i j \;\; \circ K.iCycles j = K.d i j$$$

Lean4

@[reassoc (attr := simp)]
theorem toCycles_i [K.HasHomology j] : K.toCycles i j ≫ K.iCycles j = K.d i j :=
  liftCycles_i _ _ _ _ _

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