chainsIso₂ — Mathlib

English

The second object of the inhomogeneous chain complex is isomorphic to G × G →₀ A, i.e., H_2 is naturally represented by functions of two group elements into A.

Русский

Второй объект комплекса бесконечно однородных цепей изоморфен G × G →₀ A, то есть H_2 естественно задаётся функциями от двух элементов группы в A.

LaTeX

$$$\text{chainsIso}_2 : (\mathrm{inhomogeneousChains} A).X 2 \cong \mathrm{ModuleCat.of}\, k (G \times G \to_0 A)$$$

Lean4

/-- The 2nd object in the complex of inhomogeneous chains of `A : Rep k G` is isomorphic
to `G² →₀ A` as a `k`-module. -/
def chainsIso₂ : (inhomogeneousChains A).X 2 ≅ ModuleCat.of k (G × G →₀ A) :=
  (Finsupp.domLCongr (piFinTwoEquiv fun _ => G)).toModuleIso

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