d₁_eq_zero — Mathlib

English

A general variant expresses D1 for any i1,i1' with a relation h, in terms of the same ε1 and the corresponding i2,i12,h' as in D1_eq.

Русский

Обобщённая версия даёт выражение D1 для любых i1,i1' с relation h через ту же ε1 и соответствующие i2,i12,h' как в D1_eq.

LaTeX

$$$K.D_{1}\\, c_{12}\\; i_{1}\\; i_{2}\\; i_{12} = \\varepsilon_{1} c_{1} c_{2} c_{12} \\{ fst := i_{1}, snd := i_{2} \\} \\circ \\left( (K.d\\; i_{1}\\; i_{1}').f\\ i_{2} \\right) \\;\\cdot\\; K.toGradedObject.ιMapObj (\\mathrm{ComplexShape.π}\\ c_{1} c_{2} c_{12}) \\langle i_{1}', i_{2} \\rangle i_{12} h'$$

Lean4

theorem d₁_eq_zero (h : ¬c₁.Rel i₁ (c₁.next i₁)) : K.d₁ c₁₂ i₁ i₂ i₁₂ = 0 :=
  by
  dsimp [d₁]
  rw [K.shape_f _ _ h, zero_comp, smul_zero]

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