shortComplexH1 — Mathlib

English

Let A be a representation of G over k. There is an exact short complex (G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A, i.e. im(d₂₁) = ker(d₁₀).

Русский

Пусть A — представление G над k. Существует точный короткий комплекс (G² →₀ A) --d₂₁--> (G →₀ A) --d₁₀--> A, то есть образ d₂₁ равен ядру d₁₀.

LaTeX

$$$\operatorname{im}(d_{21}) = \ker(d_{10}).$$$

Lean4

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

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