comp_zero_cochain_v — Mathlib

English

If z1 is a zero cochain and z2 has degree n, then the v-component of z1.comp z2 is equal to z1.v p p (add_zero p) composed with z2.v p q, i.e., (z1.comp z2 (n)).v p q = z1.v p p (add_zero p) ∘ z2.v p q hpq.

Русский

Если z1 нулевой коцепоинт, то v-компонента z1.comp z2 равна произведению нулевой компоненты и z2: (z1.comp z2(n)).v = z1.v p p ∘ z2.v p q.

LaTeX

$$$$ (z_1.comp z_2 (n)).v(p,q) = z_1.v(p,p) (add_zero p) \circ z_2.v(p,q). $$$$

Lean4

@[simp]
theorem comp_zero_cochain_v (z₁ : Cochain F G n) (z₂ : Cochain G K 0) (p q : ℤ) (hpq : p + n = q) :
    (z₁.comp z₂ (add_zero n)).v p q hpq = z₁.v p q hpq ≫ z₂.v q q (add_zero q) :=
  comp_v z₁ z₂ (add_zero n) p q q hpq (add_zero q)

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