Stabilizers in representations

This file defines the stabilizer of a vector in a representation and proves basic lemmas about stabilizers of zero vectors, scalar multiples, sums, intertwining maps, and translates by group elements.

def Representation.stabilizer {k : Type u_1} {G : Type u_2} [Group G] [Semiring k] {V : Type u_3} [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (v : V) : Subgroup G

The stabilizer of a vector in a representation.

Equations

• ρ.stabilizer v = { carrier := {g : G | (ρ g) v = v}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem Representation.mem_stabilizer {k : Type u_1} {G : Type u_2} [Group G] [Semiring k] {V : Type u_3} [AddCommMonoid V] [Module k V] {ρ : Representation k G V} {v : V} {g : G} : g ∈ ρ.stabilizer v ↔ (ρ g) v = v

theorem Representation.stabilizer_zero {k : Type u_1} {G : Type u_2} [Group G] [Semiring k] {V : Type u_3} [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ρ.stabilizer 0 = ⊤

theorem Representation.le_stabilizer_smul {k : Type u_1} {G : Type u_2} [Group G] [Semiring k] {V : Type u_3} [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (c : k) (v : V) : ρ.stabilizer v ≤ ρ.stabilizer (c • v)

theorem Representation.le_stabilizer_add {k : Type u_1} {G : Type u_2} [Group G] [Semiring k] {V : Type u_3} [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (v1 v2 : V) : ρ.stabilizer v1 ⊓ ρ.stabilizer v2 ≤ ρ.stabilizer (v1 + v2)

theorem Representation.le_stabilizer_sum {k : Type u_1} {G : Type u_2} [Group G] [Semiring k] {V : Type u_3} [AddCommMonoid V] [Module k V] {ι : Type u_5} [Fintype ι] (ρ : Representation k G V) (v : ι → V) : ⨅ (i : ι), ρ.stabilizer (v i) ≤ ρ.stabilizer (∑ i : ι, v i)

theorem Representation.IntertwiningMap.stabilizer_le {k : Type u_1} {G : Type u_2} [Group G] [Semiring k] {V : Type u_3} {V' : Type u_4} [AddCommMonoid V] [Module k V] [AddCommMonoid V'] [Module k V'] {ρ : Representation k G V} {ρ' : Representation k G V'} (f : ρ.IntertwiningMap ρ') (v : V) : ρ.stabilizer v ≤ ρ'.stabilizer (f v)

theorem Representation.stabilizer_conj {k : Type u_1} {G : Type u_2} [Group G] [Semiring k] {V : Type u_3} [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (v : V) : ρ.stabilizer ((ρ g) v) = Subgroup.map (↑(MulAut.conj g)) (ρ.stabilizer v)

The stabilizer of ρ g v is the conjugate of the stabilizer of v.