chainsIso₃ — Mathlib

English

The third object in the chain of inhomogeneous groups is isomorphic to G³ →₀ A, i.e., H_3 is represented by triples of group elements acting on A.

Русский

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

LaTeX

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

Lean4

/-- The 3rd 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 3 ≅ ModuleCat.of k (G × G × G →₀ A) :=
  (Finsupp.domLCongr ((Fin.consEquiv _).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun _ => G)))).toModuleIso

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