shortComplexH2 — Mathlib

English

The short complex Fun(G, A) --d12--> Fun(G × G, A) --d23--> Fun(G × G × G, A) is a complex since d12 ∘ d23 = 0.

Русский

Короткий комплекс Fun(G, A) --d12--> Fun(G × G, A) --d23--> Fun(G × G × G, A) — комплекс, так как d12 ∘ d23 = 0.

LaTeX

$$$d_{12} A \\circ d_{23} A = 0$$$

Lean4

/-- The short complex `Fun(G, A) --d₁₂--> Fun(G × G, A) --d₂₃--> Fun(G × G × G, A)`. -/
@[simps! -isSimp f g]
def shortComplexH2 : ShortComplex (ModuleCat k) :=
  mk (d₁₂ A) (d₂₃ A) (d₁₂_comp_d₂₃ A)

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