cochainsIso₂ — Mathlib

English

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

Русский

Второй класс коочеин изоморфен функциям на G×G с значениями в A.

LaTeX

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

Lean4

/-- The 2nd 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 2 ≅ ModuleCat.of k (G × G → A) :=
  (LinearEquiv.funCongrLeft k A <| (piFinTwoEquiv fun _ => G)).toModuleIso.symm

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