cochainsIso₃ — Mathlib

English

The third cochain group is isomorphic to functions on G×G×G with values in A.

Русский

Третий коочеин-группа изоморфна функциям на G×G×G со значениями в A.

LaTeX

$$$cochainsIso_3 : (inhomogeneousCochains A).X_3 \cong \mathrm{Module}_k(G \times G \times G \to A)$$$

Lean4

/-- The 3rd object in the complex of inhomogeneous cochains of `A : Rep k G` is isomorphic
to `Fun(G³, A)` as a `k`-module. -/
def cochainsIso₃ : (inhomogeneousCochains A).X 3 ≅ ModuleCat.of k (G × G × G → A) :=
  (LinearEquiv.funCongrLeft k A <|
      ((Fin.consEquiv _).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun _ => G)))).toModuleIso.symm

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