cochainsIso₀ — Mathlib

English

The isomorphism cochainsIso₀ is induced by the unique linear isomorphism on the zero-th finite set, giving an isomorphism of the 0th inhomogeneous cochains with A.

Русский

Изоморфизм cochainsIso₀ задаётся уникальным линейным изоморфизмом на нулевом множестве и устанавливает изоморфность с A на уровне нулевых коочеин.

LaTeX

$$$cochainsIso_0(A) = (LinearEquiv.funUnique (Fin 0 \to G) k A).toModuleIso$$$

Lean4

/-- The 0th object in the complex of inhomogeneous cochains of `A : Rep k G` is isomorphic
to `A` as a `k`-module. -/
def cochainsIso₀ : (inhomogeneousCochains A).X 0 ≅ A.V :=
  (LinearEquiv.funUnique (Fin 0 → G) k A).toModuleIso

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