feat(RepresentationTheory): add smooth representations (draft)

Mathlib.lean

@@ -6413,6 +6413,9 @@ 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.Smooth.Basic
+public import Mathlib.RepresentationTheory.Smooth.SmRep
+public import Mathlib.RepresentationTheory.Stabilizer
 public import Mathlib.RepresentationTheory.Submodule
 public import Mathlib.RepresentationTheory.Subrepresentation
 public import Mathlib.RepresentationTheory.Tannaka

Mathlib/RepresentationTheory/Smooth/Basic.lean

@@ -0,0 +1,219 @@
+/-
+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.RepresentationTheory.Stabilizer
+public import Mathlib.Topology.Algebra.OpenSubgroup
+
+/-!
+# Smooth representations
+
+This file defines smoothness for representations of a topological group, and proves basic closure
+properties.
+
+A representation is called smooth if the stabilizer of any vector is open. We prove that
+subrepresentations, quotient representations, direct sums, and tensor products of smooth
+representations are smooth. We construct `smoothHom`, resp. `contragredient` by cutting out the
+smooth vectors from the naive `linHom`, resp. `dual`.
+
+## Main definitions
+
+* `Representation.Smooth.IsSmooth`
+* `Representation.Smooth.smoothHom`
+* `Representation.Smooth.contragredient`
+
+## Main theorems
+
+* `isSmooth_smoothVectors`
+
+-/
+
+@[expose] public section
+
+open Representation
+
+namespace Representation.Smooth
+
+section basic
+
+variable {G : Type*} [TopologicalSpace G] [Group G]
+variable {k : Type*} [Semiring k]
+variable {V : Type*} [AddCommMonoid V] [Module k V]
+
+/-- A vector is called smooth if its stabilizer is open. -/
+def IsSmoothVector (ρ : Representation k G V) (v : V) : Prop :=
+  IsOpen ((stabilizer ρ v) : Set G)
+
+lemma isSmoothVector_iff {ρ : Representation k G V} {v : V}
+    : IsSmoothVector ρ v ↔ IsOpen {g : G | ρ g v = v} := by
+  rfl
+
+/-- A representation is called smooth if every vector is smooth. -/
+class IsSmooth (ρ : Representation k G V) : Prop where
+  smooth : ∀ (v : V), IsSmoothVector ρ v
+
+lemma isSmooth_iff {ρ : Representation k G V} :
+    (IsSmooth ρ) ↔ ∀ (v : V), IsOpen {g : G | ρ g v = v} :=
+  ⟨fun h v => isSmoothVector_iff.mp (h.smooth v),
+  fun h => {smooth v := isSmoothVector_iff.mpr (h v)}⟩
+
+/-- Any trivial representation is smooth. -/
+lemma isSmooth_trivial : IsSmooth (trivial k G V) := by
+  simp [isSmooth_iff]
+
+/-- Any subrepresentation of a smooth representation is smooth. -/
+lemma isSmooth_subrepresentation {ρ : Representation k G V} (φ : Subrepresentation ρ)
+    [h : IsSmooth ρ] : IsSmooth φ.toRepresentation := by
+  simpa [isSmooth_iff, isSmoothVector_iff] using fun v _ => h.smooth v
+
+/-- An arbitrary direct sum of smooth representations is smooth. -/
+lemma isSmooth_directSum {I : Type*} {V : I → Type*} [(i : I) → AddCommMonoid (V i)]
+    [(i : I) → Module k (V i)] (ρ : (i : I) → Representation k G (V i)) (h : ∀ i, IsSmooth (ρ i)) :
+    IsSmooth (Representation.directSum ρ) := by classical
+  simp only [isSmooth_iff, directSum_apply, DirectSum.ext_iff, DirectSum.lmap_apply]
+  intro v
+  have hset : {g : G | ∀ i : I, ((ρ i) g) (v i) = v i}
+      = ⋂ i ∈ DFinsupp.support v, {g : G | ((ρ i) g) (v i) = v i} := by
+    ext g; simp only [Set.mem_setOf_eq, Set.mem_iInter]; constructor
+    · exact fun h_stab i _ => h_stab i
+    · intro h_stab i
+      by_cases h_supp : i ∈ DFinsupp.support v
+      · exact h_stab i h_supp
+      · rw [DFinsupp.notMem_support_iff] at h_supp; rw [h_supp, map_zero]
+  rw [hset]; exact isOpen_biInter_finset fun i _ => (h i).smooth (v i)
+
+end basic
+
+section quotient
+
+variable {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
+variable {k : Type*} [Ring k]
+variable {V : Type*} [AddCommGroup V] [Module k V]
+
+/-- Any quotient representation of a smooth representation is smooth. -/
+lemma isSmooth_quotient {ρ : Representation k G V} {φ : Subrepresentation ρ} [IsSmooth ρ]
+    : IsSmooth (φ.quotient) := by
+  refine ⟨fun w => Quotient.inductionOn' w fun v => ?_⟩
+  have h_sub : stabilizer ρ v ≤ stabilizer (φ.quotient) ⟦v⟧ := by
+    simp +contextual [SetLike.le_def, Subrepresentation.quotient_apply_mk]
+  exact Subgroup.isOpen_mono h_sub (IsSmooth.smooth v)
+
+end quotient
+
+section smoothVectors
+
+variable {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
+variable {k : Type*} [Semiring k]
+variable {V : Type*} [AddCommMonoid V] [Module k V]
+variable {V' : Type*} [AddCommMonoid V'] [Module k V']
+
+omit [IsTopologicalGroup G] in
+lemma isSmoothVector_zero (ρ : Representation k G V) : IsSmoothVector ρ 0 := by
+  simp [isSmoothVector_iff]
+
+lemma isSmoothVector_add {ρ : Representation k G V} {v1 v2 : V}
+    (hv1 : IsSmoothVector ρ v1) (hv2 : IsSmoothVector ρ v2)
+    : IsSmoothVector ρ (v1 + v2) :=
+  Subgroup.isOpen_mono (le_stabilizer_add ρ v1 v2) (hv1.inter hv2)
+
+lemma isSmoothVector_sum {n : ℕ} {ρ : Representation k G V} {v : Fin n → V}
+    (h : ∀ (i : Fin n), IsSmoothVector ρ (v i)) : IsSmoothVector ρ (∑ i, v i) :=
+  Subgroup.isOpen_mono (le_stabilizer_sum ρ v) (by simpa using isOpen_iInter_of_finite h)
+
+lemma isSmoothVector_smul {ρ : Representation k G V} {v : V} (c : k)
+    (h : IsSmoothVector ρ v) : IsSmoothVector ρ (c • v) :=
+  Subgroup.isOpen_mono (le_stabilizer_smul ρ c v) h
+
+open scoped Pointwise
+
+lemma isSmoothVector_apply {ρ : Representation k G V} {v : V} (g : G) (hv : IsSmoothVector ρ v)
+    : IsSmoothVector ρ (ρ g v) := by
+  rw [IsSmoothVector, stabilizer_conj]
+  convert isOpenMap_mul_right g⁻¹ (g • (ρ.stabilizer v)) (isOpenMap_mul_left g (ρ.stabilizer v) hv)
+  ext x; rw[Set.mem_image]; simp [Set.mem_smul_set]
+
+/-- `IntertwiningMap` sends smooth vectors to smooth vectors. -/
+lemma IntertwiningMap.isSmoothVector {ρ : Representation k G V} {ρ' : Representation k G V'}
+    {v : V} (f : ρ.IntertwiningMap ρ') (h : IsSmoothVector ρ v) : IsSmoothVector ρ' (f v) :=
+  Subgroup.isOpen_mono (IntertwiningMap.stabilizer_le f v) h
+
+/-- The submodule of smooth vectors of a representation. -/
+def smoothSubmodule (ρ : Representation k G V) : Submodule k V where
+  carrier := {v : V | IsSmoothVector ρ v}
+  add_mem' h1 h2 := isSmoothVector_add h1 h2
+  zero_mem' := isSmoothVector_zero ρ
+  smul_mem' c _ h := isSmoothVector_smul c h
+
+/-- Smooth vectors of a representation form a `Subrepresentation`. -/
+def smoothVectors (ρ : Representation k G V) : Subrepresentation ρ where
+  toSubmodule := smoothSubmodule ρ
+  apply_mem_toSubmodule g _ h := isSmoothVector_apply g h
+
+@[simp]
+lemma mem_smoothSubmodule {ρ : Representation k G V} {v : V} :
+    v ∈ (smoothVectors ρ).toSubmodule ↔ IsSmoothVector ρ v := by
+  rfl
+
+/-- Taking smooth vectors gives a smooth representation. -/
+theorem isSmooth_smoothVectors {ρ : Representation k G V} :
+    IsSmooth ((smoothVectors ρ).toRepresentation) := by
+  simp [isSmooth_iff, isSmoothVector_iff]
+
+/-- `IntertwiningMap` descends to maximal smooth subrepresentations. -/
+def IntertwiningMap.smoothVectors {ρ : Representation k G V} {ρ' : Representation k G V'}
+    (f : ρ.IntertwiningMap ρ')
+    : ((smoothVectors ρ).toRepresentation).IntertwiningMap (smoothVectors ρ').toRepresentation where
+  toFun v := ⟨f v.1, IntertwiningMap.isSmoothVector f v.2⟩
+  map_add' := by simp [Subtype.ext_iff]
+  map_smul' := by simp [Subtype.ext_iff]
+  isIntertwining' g := by ext x; apply IntertwiningMap.isIntertwining
+
+end smoothVectors
+
+section tensorHomContragredient
+
+variable {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
+variable {k : Type*} [CommSemiring k]
+variable {V : Type*} [AddCommMonoid V] [Module k V]
+variable {V' : Type*} [AddCommMonoid V'] [Module k V']
+
+lemma isSmoothVector_tmul {ρ : Representation k G V} {ρ' : Representation k G V'} {v : V} {v' : V'}
+    (h : IsSmoothVector ρ v) (h' : IsSmoothVector ρ' v')
+    : IsSmoothVector (ρ.tprod ρ') (v ⊗ₜ[k] v') := by
+  have h_sub : (stabilizer ρ v) ⊓ (stabilizer ρ' v') ≤ (stabilizer (ρ.tprod ρ') (v ⊗ₜ[k] v')) := by
+    simp +contextual [SetLike.le_def]
+  exact Subgroup.isOpen_mono h_sub (h.inter h')
+
+/-- The tensor product of two smooth representations is smooth. -/
+lemma isSmooth_tprod {ρ : Representation k G V} {ρ' : Representation k G V'}
+    [h : IsSmooth ρ] [h' : IsSmooth ρ'] : IsSmooth (tprod ρ ρ') := by
+  refine ⟨fun v => ?_⟩
+  induction v with
+  | zero => exact isSmoothVector_zero _
+  | tmul v v' => exact isSmoothVector_tmul (h.smooth v) (h'.smooth v')
+  | add _ _ h1 h2 => exact isSmoothVector_add h1 h2
+
+/-- The maximal smooth subrepresentation of the `linHom` representation. -/
+def smoothHom (ρ : Representation k G V) (ρ' : Representation k G V') :
+    Representation k G (smoothVectors (linHom ρ ρ')).toSubmodule :=
+  (smoothVectors (linHom ρ ρ')).toRepresentation
+
+lemma isSmooth_smoothHom {ρ : Representation k G V} {ρ' : Representation k G V'}
+    : IsSmooth (smoothHom ρ ρ') := by
+  apply isSmooth_smoothVectors
+
+/-- The maximal smooth subrepresentation of the dual representation. -/
+def contragredient (ρ : Representation k G V) :
+    Representation k G (smoothVectors ρ.dual).toSubmodule :=
+  (smoothVectors ρ.dual).toRepresentation
+
+lemma isSmooth_contragredient {ρ : Representation k G V}
+    : IsSmooth (contragredient ρ) := by
+  apply isSmooth_smoothVectors
+
+end tensorHomContragredient
+
+end Representation.Smooth