Documentation

TauCeti.RepresentationTheory.Pseudoreflection

The subgroup generated by the pseudoreflections of a representation #

Let ρ be a representation of a group G on a vector space V over a field K. An element g is a pseudoreflection of ρ when its fixed space (ρ g).fixedSubmodule is a hyperplane, that is, has codimension one in V. Such an element acts nontrivially on V, and need not have order two.

The pseudoreflections of ρ generate the subgroup Representation.pseudoreflectionSubgroup. It is normal: ρ h carries the fixed space of g onto the fixed space of h * g * h⁻¹, so a conjugate of a pseudoreflection is a pseudoreflection. For a faithful representation of a finite group, it is the subgroup H in the converse of the Chevalley–Shephard–Todd theorem: it contains the inertia group of every codimension-one point of Spec Sym(V*), so the residual quotient V/H → V/G by G ⧸ H has trivial inertia in codimension one (Representation.inertia_quotient_pseudoreflectionSubgroup_eq_bot, in TauCeti.RepresentationTheory.SymmetricAlgebra.Inertia).

Main definitions #

Main results #

References #

source
theorem Representation.finrank_quotient_fixedSubmodule_conj {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) (h g : G) :
Module.finrank K (V ⧸ (ρ (h * g * h⁻¹)).fixedSubmodule) = Module.finrank K (V ⧸ (ρ g).fixedSubmodule)

Conjugating g by h does not change the codimension of its fixed space: ρ h carries the fixed space of g onto the fixed space of h * g * h⁻¹.

source
@[simp]
theorem Representation.fixedSubmodule_inv {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) (g : G) :
(ρ g⁻¹).fixedSubmodule = (ρ g).fixedSubmodule

An element and its inverse have the same fixed space, so the inverse of a pseudoreflection is a pseudoreflection.

source
theorem Representation.finrank_fixedSubmodule_eq_iff_mem_ker {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) [FiniteDimensional K V] {g : G} :
Module.finrank K ↥(ρ g).fixedSubmodule = Module.finrank K V ↔ g ∈ MonoidHom.ker ρ

In finite dimension, the fixed space of g is the whole space exactly when g acts trivially.

source
theorem Representation.finrank_quotient_fixedSubmodule_dual {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) (g : G) :
Module.finrank K (Module.Dual K V ⧸ (ρ.dual g).fixedSubmodule) = Module.finrank K (V ⧸ (ρ g).fixedSubmodule)

The quotients of V and of the dual space V*, acted on by the contragredient representation, by the fixed spaces of g have the same finrank. In finite dimension the two fixed spaces thus have the same codimension, and ρ and ρ.dual have the same pseudoreflections.

source
theorem Representation.ne_one_of_finrank_quotient_fixedSubmodule_eq_one {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) {g : G} (hg : Module.finrank K (V ⧸ (ρ g).fixedSubmodule) = 1) :
g ≠ 1

A pseudoreflection is not the identity element.

source
def Representation.pseudoreflectionSubgroup {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) :
Subgroup G

The subgroup of G generated by the pseudoreflections of ρ, the elements whose fixed space in V has codimension one.

Instances For
    source
    theorem Representation.pseudoreflectionSubgroup_def {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) :
    ρ.pseudoreflectionSubgroup = Subgroup.closure {g : G | Module.finrank K (V ⧸ (ρ g).fixedSubmodule) = 1}

    The pseudoreflection subgroup is the subgroup generated by the elements whose fixed space has codimension one.

    source
    theorem Representation.mem_pseudoreflectionSubgroup_of_finrank_quotient_eq_one {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) {g : G} (hg : Module.finrank K (V ⧸ (ρ g).fixedSubmodule) = 1) :
    g ∈ ρ.pseudoreflectionSubgroup

    A pseudoreflection lies in the pseudoreflection subgroup.

    source
    theorem Representation.pseudoreflectionSubgroup_le_iff {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) {H : Subgroup G} :
    ρ.pseudoreflectionSubgroup ≤ H ↔ ∀ (g : G), Module.finrank K (V ⧸ (ρ g).fixedSubmodule) = 1 → g ∈ H

    A subgroup contains the pseudoreflection subgroup exactly when it contains every pseudoreflection.

    source
    theorem Representation.map_pseudoreflectionSubgroup_comp {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] {H : Type u_4} [Group H] (σ : Representation K H V) (f : G →* H) (hf : Function.Surjective ⇑f) :
    Subgroup.map f (pseudoreflectionSubgroup (MonoidHom.comp σ f)) = σ.pseudoreflectionSubgroup

    Under a surjective change of group, the image of the pseudoreflection subgroup is the pseudoreflection subgroup of the target representation.

    source
    theorem Representation.comap_pseudoreflectionSubgroup {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] {H : Type u_4} [Group H] (σ : Representation K H V) (f : G →* H) (hf : Function.Surjective ⇑f) :
    Subgroup.comap f σ.pseudoreflectionSubgroup = pseudoreflectionSubgroup (MonoidHom.comp σ f) ⊔ f.ker

    The preimage of the pseudoreflection subgroup after a surjective change of group is generated by the original pseudoreflections together with the kernel of the group homomorphism.

    source
    theorem Representation.pseudoreflectionSubgroup_ofQuotient_ker_eq_top_iff {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) :
    (ρ.ofQuotient (MonoidHom.ker ρ)).pseudoreflectionSubgroup = ⊤ ↔ ρ.pseudoreflectionSubgroup ⊔ MonoidHom.ker ρ = ⊤

    The faithful quotient is generated by pseudoreflections exactly when pseudoreflections and the kernel generate the original group. No finiteness hypothesis is needed.

    source
    instance Representation.normal_pseudoreflectionSubgroup {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) :
    ρ.pseudoreflectionSubgroup.Normal

    The pseudoreflection subgroup is normal, since a conjugate of a pseudoreflection is a pseudoreflection.

    source
    theorem Representation.sum_inv_one_sub_det_mul_two {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) [Fintype G] (hdet : ∀ (g : G), Module.finrank K (V ⧸ (ρ g).fixedSubmodule) = 1 → LinearMap.det (ρ g) ≠ 1) :
    (∑ g : G with Module.finrank K (V ⧸ (ρ g).fixedSubmodule) = 1, (1 - LinearMap.det (ρ g))⁻¹) * 2 = ↑{g : G | Module.finrank K (V ⧸ (ρ g).fixedSubmodule) = 1}.card

    Pairing a pseudoreflection with its inverse. If no pseudoreflection has determinant 1, then 2 ∑_s (1 - det s)⁻¹, over the pseudoreflections s, is their number, since s⁻¹ is a pseudoreflection of determinant (det s)⁻¹ and (1 - λ)⁻¹ + (1 - λ⁻¹)⁻¹ = 1.

    source
    theorem Representation.card_filter_comp_subtype_eq_of_pseudoreflectionSubgroup_le {K : Type u_1} {G : Type u_2} {V : Type u_3} [Field K] [Group G] [AddCommGroup V] [Module K V] (ρ : Representation K G V) [Fintype G] {H : Subgroup G} [Fintype ↥H] (hH : ρ.pseudoreflectionSubgroup ≤ H) :
    {h : ↥H | Module.finrank K (V ⧸ ((MonoidHom.comp ρ H.subtype) h).fixedSubmodule) = 1}.card = {g : G | Module.finrank K (V ⧸ (ρ g).fixedSubmodule) = 1}.card

    A subgroup containing every pseudoreflection has the same pseudoreflections. If a subgroup H of a finite group contains every pseudoreflection of ρ, then the restriction of ρ to H has as many pseudoreflections as ρ.