From 03612d8bc578f1b146133a76109dd0a07d6b21ef Mon Sep 17 00:00:00 2001 From: JX-Mo Date: Tue, 23 Jun 2026 18:21:15 +0800 Subject: [PATCH 1/8] add Stabilizer in RepresentationTheory --- Mathlib/RepresentationTheory/Stabilizer.lean | 125 +++++++++++++++++++ 1 file changed, 125 insertions(+) create mode 100644 Mathlib/RepresentationTheory/Stabilizer.lean diff --git a/Mathlib/RepresentationTheory/Stabilizer.lean b/Mathlib/RepresentationTheory/Stabilizer.lean new file mode 100644 index 00000000000000..d1d79745e22600 --- /dev/null +++ b/Mathlib/RepresentationTheory/Stabilizer.lean @@ -0,0 +1,125 @@ +/- +Copyright (c) 2026 Jiaxi Mo. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jiaxi Mo +-/ +module + +public import Mathlib.Algebra.Group.Action.Pointwise.Set.Basic +public import Mathlib.Algebra.Group.Opposite +public import Mathlib.RepresentationTheory.Intertwining + +import Mathlib.Tactic.Group + +/-! +# Stabilizers in representations + +This file defines the stabilizer of a vector in a representation and proves basic lemmas about +stabilizers of zero vectors, scalar multiplies, sums, intertwining maps, and actions by group +elements. + +## Main definitions + +* `Representation.stabilizer`: the subgroup fixing a vector in a representation. + +## Main statements + +* `Representation.mem_stabilizer` +* `Representation.stabilizer_zero` +* `Representation.stabilizer_smul` +* `Representation.stabilizer_add` +* `Representation.stabilizer_sum` +* `Representation.stabilizer_intertwining` +* `Representation.stabilizer_conj` +* `Representation.stabilizer_conj_coe` +-/ + +@[expose] public section + + +open Set +open scoped Pointwise +open MulOpposite + +namespace Representation + +variable {k G : Type*} [Group G] [Semiring k] +variable {V V' : Type*} [AddCommMonoid V] [Module k V] [AddCommMonoid V'] [Module k V'] + +/-- The stabilizer of a vector in a representation. -/ +def stabilizer (ρ : Representation k G V) (v : V) : Subgroup G where + carrier := {g : G | ρ g v = v} + mul_mem' := by + intro a b ha hb + rw [mem_setOf_eq, map_mul, Module.End.mul_apply, hb, ha] + one_mem' := by simp + inv_mem' := by + intro g hg + rw [mem_setOf_eq, ← hg, inv_self_apply, hg] + +@[simp] +lemma mem_stabilizer (ρ : Representation k G V) (v : V) (g : G) : + (g ∈ stabilizer ρ v) ↔ (ρ g v = v) := by + rfl + +lemma stabilizer_zero (ρ : Representation k G V) : stabilizer ρ 0 = ⊤ := by + ext x + simp only [mem_stabilizer, map_zero, Subgroup.mem_top] + +lemma stabilizer_smul (ρ : Representation k G V) (c : k) (v : V) : + stabilizer ρ v ≤ stabilizer ρ (c • v) := by + intro g hg_stab + rw [mem_stabilizer] at hg_stab + rw [mem_stabilizer, map_smul, hg_stab] + +lemma stabilizer_add (ρ : Representation k G V) (v1 v2 : V) : + (stabilizer ρ v1) ⊓ (stabilizer ρ v2) ≤ stabilizer ρ (v1 + v2) := by + intro g hg_stab + rw [mem_stabilizer, map_add, hg_stab.1, hg_stab.2] + +lemma stabilizer_sum (ρ : Representation k G V) (n : ℕ) (v : Fin n → V) : + ⨅ i, (stabilizer ρ (v i)) ≤ stabilizer ρ (∑ i, v i) := by + intro g hg_stab + simp only [Subgroup.mem_iInf, mem_stabilizer] at hg_stab + simp only [mem_stabilizer, map_sum, hg_stab] + +lemma stabilizer_intertwining (ρ : Representation k G V) (v : V) (ρ' : Representation k G V') + (f : ρ.IntertwiningMap ρ') : stabilizer ρ v ≤ stabilizer ρ' (f v) := by + intro x hx_stab + rw [mem_stabilizer] at hx_stab + rw [mem_stabilizer, ← IntertwiningMap.isIntertwining, hx_stab] + +/-- The stabilizer of `ρ g v` is the conjugate of the stabilizer of `v`. -/ +lemma stabilizer_conj (ρ : Representation k G V) (g : G) (v : V) : + ρ.stabilizer (ρ g v) = Subgroup.map (↑(MulAut.conj g)) (stabilizer ρ v) := by + ext x + simp only [mem_stabilizer, Subgroup.mem_map, MonoidHom.coe_coe, MulAut.conj_apply] + constructor + · intro hx_stab + refine ⟨g⁻¹ * x * g, ?_, ?_⟩ + · simp only [map_mul, Module.End.mul_apply, hx_stab, inv_self_apply] + · group + · rintro ⟨y, hy_stab, hy_conj⟩ + simp only [← hy_conj, map_mul, Module.End.mul_apply, inv_self_apply, hy_stab] + +/-- A set-level version of `stabilizer_conj`, useful for topological arguments. -/ +lemma stabilizer_conj_coe (ρ : Representation k G V) (g : G) (v : V) : + (ρ.stabilizer (ρ g v)).carrier = (op g⁻¹) • (g • (stabilizer ρ v).carrier) := by + ext x + simp only [stabilizer, mem_setOf_eq] + apply Iff.intro + · intro hx_stab + use x * g + simp only [smul_eq_mul_unop, MulOpposite.unop_op, mul_inv_cancel_right, and_true] + use g⁻¹ * x * g + constructor + · simp only [mem_setOf_eq, map_mul, Module.End.mul_apply, hx_stab, inv_self_apply] + · simp only [smul_eq_mul, ← mul_assoc, mul_inv_cancel, one_mul] + · rintro ⟨y, h, hy⟩ + obtain ⟨z, hz_stab, hz_conj⟩ := h + simp only [smul_eq_mul_unop, MulOpposite.unop_op] at hy + rw [← hy, map_mul, Module.End.mul_apply, inv_self_apply, ← hz_conj] + rw [mem_setOf_eq] at hz_stab + simp only [smul_eq_mul, map_mul, Module.End.mul_apply, hz_stab] + +end Representation From 832d2194515ccaa6827762b45ab0a7c4eed17d15 Mon Sep 17 00:00:00 2001 From: JX-Mo Date: Tue, 23 Jun 2026 18:23:10 +0800 Subject: [PATCH 2/8] add Stabilizer in RepresentationTheory --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index e172db56965dbd..8004300410c86c 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6390,6 +6390,7 @@ public import Mathlib.RepresentationTheory.Rep.Basic public import Mathlib.RepresentationTheory.Rep.Iso public import Mathlib.RepresentationTheory.Rep.Res public import Mathlib.RepresentationTheory.Semisimple +public import Mathlib.RepresentationTheory.Stabilizer public import Mathlib.RepresentationTheory.Submodule public import Mathlib.RepresentationTheory.Subrepresentation public import Mathlib.RepresentationTheory.Tannaka From cc068a084aa43d6a117cd2ac3d3719981ee1d892 Mon Sep 17 00:00:00 2001 From: JX-Mo Date: Tue, 23 Jun 2026 21:27:16 +0800 Subject: [PATCH 3/8] Update Mathlib/RepresentationTheory/Stabilizer.lean Co-authored-by: Thomas Browning --- Mathlib/RepresentationTheory/Stabilizer.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RepresentationTheory/Stabilizer.lean b/Mathlib/RepresentationTheory/Stabilizer.lean index d1d79745e22600..44f25c561b29f4 100644 --- a/Mathlib/RepresentationTheory/Stabilizer.lean +++ b/Mathlib/RepresentationTheory/Stabilizer.lean @@ -91,7 +91,7 @@ lemma stabilizer_intertwining (ρ : Representation k G V) (v : V) (ρ' : Represe /-- The stabilizer of `ρ g v` is the conjugate of the stabilizer of `v`. -/ lemma stabilizer_conj (ρ : Representation k G V) (g : G) (v : V) : - ρ.stabilizer (ρ g v) = Subgroup.map (↑(MulAut.conj g)) (stabilizer ρ v) := by + ρ.stabilizer (ρ g v) = (stabilizer ρ v).map (MulAut.conj g) := by ext x simp only [mem_stabilizer, Subgroup.mem_map, MonoidHom.coe_coe, MulAut.conj_apply] constructor From 97aab093352a74e89679110688104c2eb393636f Mon Sep 17 00:00:00 2001 From: JX-Mo Date: Wed, 24 Jun 2026 01:12:09 +0800 Subject: [PATCH 4/8] Address review comments 1. Delete the last lemma and relevant imports. 2. Fix naming conventions. 3. Delete the long list in docstring. --- Mathlib/RepresentationTheory/Stabilizer.lean | 57 +++----------------- 1 file changed, 8 insertions(+), 49 deletions(-) diff --git a/Mathlib/RepresentationTheory/Stabilizer.lean b/Mathlib/RepresentationTheory/Stabilizer.lean index 44f25c561b29f4..d5a95ad0734f43 100644 --- a/Mathlib/RepresentationTheory/Stabilizer.lean +++ b/Mathlib/RepresentationTheory/Stabilizer.lean @@ -5,8 +5,6 @@ Authors: Jiaxi Mo -/ module -public import Mathlib.Algebra.Group.Action.Pointwise.Set.Basic -public import Mathlib.Algebra.Group.Opposite public import Mathlib.RepresentationTheory.Intertwining import Mathlib.Tactic.Group @@ -15,32 +13,13 @@ import Mathlib.Tactic.Group # Stabilizers in representations This file defines the stabilizer of a vector in a representation and proves basic lemmas about -stabilizers of zero vectors, scalar multiplies, sums, intertwining maps, and actions by group +stabilizers of zero vectors, scalar multiples, sums, intertwining maps, and translates by group elements. -## Main definitions - -* `Representation.stabilizer`: the subgroup fixing a vector in a representation. - -## Main statements - -* `Representation.mem_stabilizer` -* `Representation.stabilizer_zero` -* `Representation.stabilizer_smul` -* `Representation.stabilizer_add` -* `Representation.stabilizer_sum` -* `Representation.stabilizer_intertwining` -* `Representation.stabilizer_conj` -* `Representation.stabilizer_conj_coe` -/ @[expose] public section - -open Set -open scoped Pointwise -open MulOpposite - namespace Representation variable {k G : Type*} [Group G] [Semiring k] @@ -51,11 +30,11 @@ def stabilizer (ρ : Representation k G V) (v : V) : Subgroup G where carrier := {g : G | ρ g v = v} mul_mem' := by intro a b ha hb - rw [mem_setOf_eq, map_mul, Module.End.mul_apply, hb, ha] + rw [Set.mem_setOf_eq, map_mul, Module.End.mul_apply, hb, ha] one_mem' := by simp inv_mem' := by intro g hg - rw [mem_setOf_eq, ← hg, inv_self_apply, hg] + rw [Set.mem_setOf_eq, ← hg, inv_self_apply, hg] @[simp] lemma mem_stabilizer (ρ : Representation k G V) (v : V) (g : G) : @@ -66,25 +45,25 @@ lemma stabilizer_zero (ρ : Representation k G V) : stabilizer ρ 0 = ⊤ := by ext x simp only [mem_stabilizer, map_zero, Subgroup.mem_top] -lemma stabilizer_smul (ρ : Representation k G V) (c : k) (v : V) : +lemma le_stabilizer_smul (ρ : Representation k G V) (c : k) (v : V) : stabilizer ρ v ≤ stabilizer ρ (c • v) := by intro g hg_stab rw [mem_stabilizer] at hg_stab rw [mem_stabilizer, map_smul, hg_stab] -lemma stabilizer_add (ρ : Representation k G V) (v1 v2 : V) : +lemma le_stabilizer_add (ρ : Representation k G V) (v1 v2 : V) : (stabilizer ρ v1) ⊓ (stabilizer ρ v2) ≤ stabilizer ρ (v1 + v2) := by intro g hg_stab rw [mem_stabilizer, map_add, hg_stab.1, hg_stab.2] -lemma stabilizer_sum (ρ : Representation k G V) (n : ℕ) (v : Fin n → V) : +lemma le_stabilizer_sum (ρ : Representation k G V) (n : ℕ) (v : Fin n → V) : ⨅ i, (stabilizer ρ (v i)) ≤ stabilizer ρ (∑ i, v i) := by intro g hg_stab simp only [Subgroup.mem_iInf, mem_stabilizer] at hg_stab simp only [mem_stabilizer, map_sum, hg_stab] -lemma stabilizer_intertwining (ρ : Representation k G V) (v : V) (ρ' : Representation k G V') - (f : ρ.IntertwiningMap ρ') : stabilizer ρ v ≤ stabilizer ρ' (f v) := by +lemma IntertwiningMap.stabilizer_le {ρ : Representation k G V} {ρ' : Representation k G V'} + (f : ρ.IntertwiningMap ρ') (v : V) : stabilizer ρ v ≤ stabilizer ρ' (f v) := by intro x hx_stab rw [mem_stabilizer] at hx_stab rw [mem_stabilizer, ← IntertwiningMap.isIntertwining, hx_stab] @@ -102,24 +81,4 @@ lemma stabilizer_conj (ρ : Representation k G V) (g : G) (v : V) : · rintro ⟨y, hy_stab, hy_conj⟩ simp only [← hy_conj, map_mul, Module.End.mul_apply, inv_self_apply, hy_stab] -/-- A set-level version of `stabilizer_conj`, useful for topological arguments. -/ -lemma stabilizer_conj_coe (ρ : Representation k G V) (g : G) (v : V) : - (ρ.stabilizer (ρ g v)).carrier = (op g⁻¹) • (g • (stabilizer ρ v).carrier) := by - ext x - simp only [stabilizer, mem_setOf_eq] - apply Iff.intro - · intro hx_stab - use x * g - simp only [smul_eq_mul_unop, MulOpposite.unop_op, mul_inv_cancel_right, and_true] - use g⁻¹ * x * g - constructor - · simp only [mem_setOf_eq, map_mul, Module.End.mul_apply, hx_stab, inv_self_apply] - · simp only [smul_eq_mul, ← mul_assoc, mul_inv_cancel, one_mul] - · rintro ⟨y, h, hy⟩ - obtain ⟨z, hz_stab, hz_conj⟩ := h - simp only [smul_eq_mul_unop, MulOpposite.unop_op] at hy - rw [← hy, map_mul, Module.End.mul_apply, inv_self_apply, ← hz_conj] - rw [mem_setOf_eq] at hz_stab - simp only [smul_eq_mul, map_mul, Module.End.mul_apply, hz_stab] - end Representation From 418e1da7e3e96a3f25c01c0aa07eb0d1cf1f6a85 Mon Sep 17 00:00:00 2001 From: JX-Mo Date: Wed, 24 Jun 2026 12:14:06 +0800 Subject: [PATCH 5/8] Fix lemma le_stabilizer_sum argument syntax Make {n : \Nat} implicit in le_stabilizer_sum --- Mathlib/RepresentationTheory/Stabilizer.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RepresentationTheory/Stabilizer.lean b/Mathlib/RepresentationTheory/Stabilizer.lean index d5a95ad0734f43..44c5c55628aa7a 100644 --- a/Mathlib/RepresentationTheory/Stabilizer.lean +++ b/Mathlib/RepresentationTheory/Stabilizer.lean @@ -56,7 +56,7 @@ lemma le_stabilizer_add (ρ : Representation k G V) (v1 v2 : V) : intro g hg_stab rw [mem_stabilizer, map_add, hg_stab.1, hg_stab.2] -lemma le_stabilizer_sum (ρ : Representation k G V) (n : ℕ) (v : Fin n → V) : +lemma le_stabilizer_sum {n : ℕ} (ρ : Representation k G V) (v : Fin n → V) : ⨅ i, (stabilizer ρ (v i)) ≤ stabilizer ρ (∑ i, v i) := by intro g hg_stab simp only [Subgroup.mem_iInf, mem_stabilizer] at hg_stab From abb5d00f988b3c6bf63b888414e42b5b609b44f6 Mon Sep 17 00:00:00 2001 From: JX-Mo Date: Fri, 26 Jun 2026 21:18:09 +0800 Subject: [PATCH 6/8] Address review comments Style improvements. --- Mathlib/RepresentationTheory/Stabilizer.lean | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/Mathlib/RepresentationTheory/Stabilizer.lean b/Mathlib/RepresentationTheory/Stabilizer.lean index 44c5c55628aa7a..7339ff2ae6c115 100644 --- a/Mathlib/RepresentationTheory/Stabilizer.lean +++ b/Mathlib/RepresentationTheory/Stabilizer.lean @@ -28,22 +28,19 @@ variable {V V' : Type*} [AddCommMonoid V] [Module k V] [AddCommMonoid V'] [Modul /-- The stabilizer of a vector in a representation. -/ def stabilizer (ρ : Representation k G V) (v : V) : Subgroup G where carrier := {g : G | ρ g v = v} - mul_mem' := by - intro a b ha hb + mul_mem' {a b} ha hb := by rw [Set.mem_setOf_eq, map_mul, Module.End.mul_apply, hb, ha] one_mem' := by simp - inv_mem' := by - intro g hg + inv_mem' {g} hg := by rw [Set.mem_setOf_eq, ← hg, inv_self_apply, hg] @[simp] -lemma mem_stabilizer (ρ : Representation k G V) (v : V) (g : G) : - (g ∈ stabilizer ρ v) ↔ (ρ g v = v) := by +lemma mem_stabilizer {ρ : Representation k G V} {v : V} {g : G} : + g ∈ stabilizer ρ v ↔ ρ g v = v := by rfl lemma stabilizer_zero (ρ : Representation k G V) : stabilizer ρ 0 = ⊤ := by - ext x - simp only [mem_stabilizer, map_zero, Subgroup.mem_top] + ext; simp lemma le_stabilizer_smul (ρ : Representation k G V) (c : k) (v : V) : stabilizer ρ v ≤ stabilizer ρ (c • v) := by @@ -60,7 +57,7 @@ lemma le_stabilizer_sum {n : ℕ} (ρ : Representation k G V) (v : Fin n → V) ⨅ i, (stabilizer ρ (v i)) ≤ stabilizer ρ (∑ i, v i) := by intro g hg_stab simp only [Subgroup.mem_iInf, mem_stabilizer] at hg_stab - simp only [mem_stabilizer, map_sum, hg_stab] + simp [hg_stab] lemma IntertwiningMap.stabilizer_le {ρ : Representation k G V} {ρ' : Representation k G V'} (f : ρ.IntertwiningMap ρ') (v : V) : stabilizer ρ v ≤ stabilizer ρ' (f v) := by @@ -76,9 +73,9 @@ lemma stabilizer_conj (ρ : Representation k G V) (g : G) (v : V) : constructor · intro hx_stab refine ⟨g⁻¹ * x * g, ?_, ?_⟩ - · simp only [map_mul, Module.End.mul_apply, hx_stab, inv_self_apply] + · simp [hx_stab] · group · rintro ⟨y, hy_stab, hy_conj⟩ - simp only [← hy_conj, map_mul, Module.End.mul_apply, inv_self_apply, hy_stab] + simp [← hy_conj, hy_stab] end Representation From fee692595371affcfea2e5e54b8ff676f29c4247 Mon Sep 17 00:00:00 2001 From: JX-Mo Date: Fri, 26 Jun 2026 21:37:28 +0800 Subject: [PATCH 7/8] Refactor stabilizer lemmas with simp +contextual Simplify proofs related to stabilizers using simp +contextual. --- Mathlib/RepresentationTheory/Stabilizer.lean | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/Mathlib/RepresentationTheory/Stabilizer.lean b/Mathlib/RepresentationTheory/Stabilizer.lean index 7339ff2ae6c115..519edb3bcaaac1 100644 --- a/Mathlib/RepresentationTheory/Stabilizer.lean +++ b/Mathlib/RepresentationTheory/Stabilizer.lean @@ -44,26 +44,19 @@ lemma stabilizer_zero (ρ : Representation k G V) : stabilizer ρ 0 = ⊤ := by lemma le_stabilizer_smul (ρ : Representation k G V) (c : k) (v : V) : stabilizer ρ v ≤ stabilizer ρ (c • v) := by - intro g hg_stab - rw [mem_stabilizer] at hg_stab - rw [mem_stabilizer, map_smul, hg_stab] + simp +contextual [SetLike.le_def] lemma le_stabilizer_add (ρ : Representation k G V) (v1 v2 : V) : (stabilizer ρ v1) ⊓ (stabilizer ρ v2) ≤ stabilizer ρ (v1 + v2) := by - intro g hg_stab - rw [mem_stabilizer, map_add, hg_stab.1, hg_stab.2] + simp +contextual [SetLike.le_def] lemma le_stabilizer_sum {n : ℕ} (ρ : Representation k G V) (v : Fin n → V) : ⨅ i, (stabilizer ρ (v i)) ≤ stabilizer ρ (∑ i, v i) := by - intro g hg_stab - simp only [Subgroup.mem_iInf, mem_stabilizer] at hg_stab - simp [hg_stab] + simp +contextual [SetLike.le_def] lemma IntertwiningMap.stabilizer_le {ρ : Representation k G V} {ρ' : Representation k G V'} (f : ρ.IntertwiningMap ρ') (v : V) : stabilizer ρ v ≤ stabilizer ρ' (f v) := by - intro x hx_stab - rw [mem_stabilizer] at hx_stab - rw [mem_stabilizer, ← IntertwiningMap.isIntertwining, hx_stab] + simp +contextual [SetLike.le_def, ← IntertwiningMap.isIntertwining] /-- The stabilizer of `ρ g v` is the conjugate of the stabilizer of `v`. -/ lemma stabilizer_conj (ρ : Representation k G V) (g : G) (v : V) : From 6215b7002a67a0b4df90b7109cdc5565a3703a10 Mon Sep 17 00:00:00 2001 From: JX-Mo Date: Fri, 26 Jun 2026 22:27:53 +0800 Subject: [PATCH 8/8] Refactor stabilizer_conj lemma for simplification Use the latest lemma `inv_apply_eq_iff` to shorten the proof of stabilizer_conj --- Mathlib/RepresentationTheory/Stabilizer.lean | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/Mathlib/RepresentationTheory/Stabilizer.lean b/Mathlib/RepresentationTheory/Stabilizer.lean index 519edb3bcaaac1..63a340d4383e6d 100644 --- a/Mathlib/RepresentationTheory/Stabilizer.lean +++ b/Mathlib/RepresentationTheory/Stabilizer.lean @@ -62,13 +62,8 @@ lemma IntertwiningMap.stabilizer_le {ρ : Representation k G V} {ρ' : Represent lemma stabilizer_conj (ρ : Representation k G V) (g : G) (v : V) : ρ.stabilizer (ρ g v) = (stabilizer ρ v).map (MulAut.conj g) := by ext x - simp only [mem_stabilizer, Subgroup.mem_map, MonoidHom.coe_coe, MulAut.conj_apply] - constructor - · intro hx_stab - refine ⟨g⁻¹ * x * g, ?_, ?_⟩ - · simp [hx_stab] - · group - · rintro ⟨y, hy_stab, hy_conj⟩ - simp [← hy_conj, hy_stab] + simp only [mem_stabilizer, Subgroup.mem_map, MonoidHom.coe_coe, MulAut.conj_apply, + ← Module.End.mul_apply, ← inv_apply_eq_iff, ← map_mul, ← mul_assoc] + exact ⟨fun h ↦ ⟨_, h, by simp [mul_assoc]⟩, by rintro ⟨y, hy1, rfl⟩; simp [mul_assoc, hy1]⟩ end Representation