d₀₁_ker_eq_invariants — Mathlib

English

Let A be a representation of G over k. Then the kernel of the first differential in the inhomogeneous cochain complex associated to A equals the subspace of invariants under G.

Русский

Пусть A — представление G над полем k. Тогда ядро первого дифференциала в комплексe ин-гомогенных коцепрёнт равно подпространству инвариантов по G.

LaTeX

$$$\\ker(d_{01} A) = A^{\\rho}$$$

Lean4

theorem d₀₁_ker_eq_invariants : LinearMap.ker (d₀₁ A).hom = invariants A.ρ :=
  by
  ext x
  simp only [LinearMap.mem_ker, mem_invariants, ← @sub_eq_zero _ _ _ x, funext_iff]
  rfl

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