shortComplexH2 — Mathlib

English

The first cycles Z1(G,A) are defined as the kernel of the boundary map d10: (G →₀ A) → A, i.e. Z1(G,A) = ker(d10).

Русский

Первые циклы Z1(G,A) определяются как ядро отображения границы d10: (G →₀ A) → A, то есть Z1(G,A) = ker(d10).

LaTeX

$$Z_1(G,A) = \ker(d_{10}).$$

Lean4

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

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