toCoinvariantsKer — Mathlib

English

Given a normal subgroup S ≤ G, a G-representation ρ induces a G ⧸ S-representation on the coinvariants of ρ|_S.

Русский

Пусть S — нормальная подгруппа G. Представление ρ порождает G/S-представление на когонвариантах ρ|_S.

LaTeX

$$quotientToCoinvariants : Representation k (G ⧸ S) (Coinvariants (ρ.comp S.subtype))$$

Lean4

/-- 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`. -/
abbrev toCoinvariantsKer : Rep k G :=
  Rep.of (A.ρ.toCoinvariantsKer S)

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