d_eq — Mathlib

English

A reformulation of the equality H2π_eq_zero_iff in terms of subtype cocycles and coboundaries.

Русский

Переформулирование равенства H2π_eq_zero_iff через подтип cocycles и coboundaries.

LaTeX

$$groupCohomology.H2π_eq_zero_iff_A : ∀ x y ∈ cocycles_2(A), H2π_A x = H2π_A y ↔ x - y ∈ coboundaries_2(A)$$

Lean4

theorem d_eq [DecidableEq G] :
    d A n =
      (coinvariantsTensorFreeLEquiv A (Fin (n + 1) → G)).toModuleIso.inv ≫
        ((barComplex k G).coinvariantsTensorObj A).d (n + 1) n ≫
          (coinvariantsTensorFreeLEquiv A (Fin n → G)).toModuleIso.hom :=
  by
  ext : 3
  simp [d_single (k := k), ModuleCat.MonoidalCategory.tensorObj, ModuleCat.MonoidalCategory.whiskerLeft, tensorObj_def,
    whiskerLeft_def, TensorProduct.tmul_add, TensorProduct.tmul_sum, barComplex.d_single (k := k)]

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