comp — Mathlib

English

The composition of cochains is defined by a formula: (z1.comp z2 h)(p,q) = z1.v(p, p+n1) ∘ z2.v(p+n1, q) for h: n1+n2 = n12.

Русский

Композиция коцепеев задаётся формулой: (z1.comp z2 h)(p,q) = z1.v(p, p+n1) ∘ z2.v(p+n1, q).

LaTeX

$$$$ (z_1 \cdot z_2)(p,q) = z_1.v(p, p+n_1) \circ z_2.v(p+n_1, q) \quad (h: n_1 + n_2 = n_{12}). $$$$

Lean4

/-- The composition of cochains. -/
def comp {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂) : Cochain F K n₁₂ :=
  Cochain.mk (fun p q hpq => z₁.v p (p + n₁) rfl ≫ z₂.v (p + n₁) q (by cutsat))

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