shortComplexH0 — Mathlib

English

Let k be a commutative ring, G a group, and A a representation of G over k. Then there is an exact short complex of k-modules connecting the permutation module G →₀ A, A, and the coinvariants A ρ-coinvariants, i.e. im(d10) = ker(A → Aρ.coinvariants).

Русский

Пусть k — коммутативная кольцевая единица, G — группа, и A — представление G над k. Существует точный короткий комплекс модулей над k, связанный с модулем G →₀ A, модулем A и кофинитами A ρ. То естьобраз d10 равен ядру проекции на кофинитианты: im(d10) = ker(A → Aρ.coinvariants).

LaTeX

$$$\operatorname{im}(d_{10}) = \ker\bigl(A \to A_{\rho}\text{-coinvariants}\bigr).$$$

Lean4

/-- The (exact) short complex `(G →₀ A) ⟶ A ⟶ A.ρ.coinvariants`. -/
@[simps! -isSimp f g]
def shortComplexH0 : ShortComplex (ModuleCat k) :=
  mk _ _ (d₁₀_comp_coinvariantsMk A)

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