toCoinvariants — Mathlib

English

Given a normal subgroup S ≤ G, a G-representation A restricts to a G-representation on the kernel of the quotient map to the S-coinvariants A_S.

Русский

Пусть S ≤ G нормальная: G-представление A ограничивается до G-представления на ядре перехода к когонвариантам S.

LaTeX

$$toCoinvariants : Rep k G → (S : Subgroup G) → [S.Normal] → Rep k G$$

Lean4

/-- Given a normal subgroup `S ≤ G`, a `G`-representation `A` induces a `G`-representation on
the `S`-coinvariants `A_S`. -/
abbrev toCoinvariants : Rep k G :=
  Rep.of (A.ρ.toCoinvariants S)

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