cochainsIso₁ — Mathlib

English

The first object in the inhomogeneous cochains complex is isomorphic to the function space G → A as a k-module.

Русский

Первый объект комплекса иногомогенных коочеинов изоморфен пространству функций G → A как модулю над k.

LaTeX

$$$cochainsIso_1 : (inhomogeneousCochains A).X_1 \cong \mathrm{Module}_k(G \to A)$$$

Lean4

/-- The 1st 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 1 ≅ ModuleCat.of k (G → A) :=
  (LinearEquiv.funCongrLeft k A (Equiv.funUnique (Fin 1) G)).toModuleIso.symm

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