toCoinvariants — Mathlib

English

There is a natural G-representation on the coinvariants of the restricted representation ρ|_S, i.e., ρ induces a G-action on the quotient V_S.

Русский

Существует естественное G-образование на когонвариантах ограниченного представления ρ|_S, то есть G-действие индуцируется на пространстве V_S.

LaTeX

$$toCoinvariants : Representation k G (Coinvariants (ρ \\cdot S.subtype))$$

Lean4

/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` induces a `G`-representation on the
coinvariants of `ρ|_S`. -/
noncomputable def toCoinvariants : Representation k G (Coinvariants <| ρ.comp S.subtype) :=
  quotient ρ (ker <| ρ.comp S.subtype) fun g => le_comap_ker ρ S g

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