toCoinvariantsKer — Mathlib

English

For a normal subgroup S of G, the kernel of the restricted representation ρ|_S forms a G-representation on ker(ρ|_S).

Русский

Для нормальной подгруппы S представление ρ ограничивается на ядро и само ядро образует G-представление на ker(ρ|_S).

LaTeX

$$toCoinvariantsKer : Representation k G (ker (ρ \\circ S.subtype))$$

Lean4

/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` restricts to a `G`-representation on
the kernel of the quotient map to the coinvariants of `ρ|_S`. -/
noncomputable abbrev toCoinvariantsKer : Representation k G (ker <| ρ.comp S.subtype) :=
  subrepresentation ρ (ker <| ρ.comp S.subtype) fun g => le_comap_ker ρ S g

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