diff --git a/Mathlib.lean b/Mathlib.lean
index ae8a93fa6b2aba..e888617eabe737 100644
--- a/Mathlib.lean
+++ b/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
diff --git a/Mathlib/RepresentationTheory/Smooth/Basic.lean b/Mathlib/RepresentationTheory/Smooth/Basic.lean
new file mode 100644
index 00000000000000..9306bd40da1362
--- /dev/null
+++ b/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
diff --git a/Mathlib/RepresentationTheory/Smooth/SmRep.lean b/Mathlib/RepresentationTheory/Smooth/SmRep.lean
new file mode 100644
index 00000000000000..d5c0c148c9e945
--- /dev/null
+++ b/Mathlib/RepresentationTheory/Smooth/SmRep.lean
@@ -0,0 +1,183 @@
+/-
+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.Smooth.Basic
+public import Mathlib.RepresentationTheory.Rep.Basic
+public import Mathlib.CategoryTheory.Adjunction.FullyFaithful
+public import Mathlib.CategoryTheory.Adjunction.Restrict
+public import Mathlib.CategoryTheory.Monoidal.Subcategory
+public import Mathlib.CategoryTheory.Monoidal.Closed.Basic
+
+/-!
+# Smooth representations
+
+This file defines the category `SmRep k G` of smooth representations of a topological group `G`
+and proves that it is a full, coreflexive, braided, closed, monoidal subcategory of `Rep k G`.
+
+## Main definitions
+
+* `Representation.Smooth.SmRep.SmRep`
+* `Representation.Smooth.SmRep.smVec`
+* `Representation.Smooth.SmRep.ihom`
+* `Representation.Smooth.SmRep.dual`
+
+## Main theorems
+
+* `Representation.Smooth.SmRep.tensorHomAdjunction`
+
+## Implementation notes
+
+We use `ObjectProperty.FullSubcategory` to define the category of smooth representations.
+
+To obtain the monoidal structure, we first show that taking smooth vectors `smVec` is right adjoint
+to the canonical inclusion `ι`, and then we employ the categorical machinery to obtain the desired
+categorical structures by restricting those structures in `Rep` along the fully faithful inclusion.
+
+-/
+
+@[expose] public section
+
+open CategoryTheory Representation
+
+namespace Representation.Smooth
+
+universe w u v
+
+variable (k : Type u) [Ring k]
+variable (G : Type v) [TopologicalSpace G] [Group G]
+
+/-- Smoothness is an `ObjectProperty` of `Rep k G`. -/
+def smoothProperty : ObjectProperty (Rep.{w} k G) := fun A ↦ (Smooth.IsSmooth A.ρ)
+
+/-- `SmRep k G` is the full subcategory of `Rep k G` consisting of smooth representations. -/
+abbrev SmRep := (smoothProperty.{w} k G).FullSubcategory
+
+variable {k G}
+
+@[simp]
+lemma smoothProperty_iff {A : Rep.{w} k G}
+    : smoothProperty k G A ↔ Smooth.IsSmooth A.ρ := by
+  rfl
+
+namespace SmRep
+
+variable {V : Type w} [AddCommGroup V] [Module k V]
+
+/-- The object in `SmRep k G` associated to a smooth representation. -/
+abbrev of (ρ : Representation k G V) [h : IsSmooth ρ] : SmRep.{w} k G := ⟨Rep.of.{w} ρ, h⟩
+
+/-- The zero representation is smooth. -/
+instance : Inhabited (SmRep k G) := ⟨(default : Rep k G), isSmooth_trivial⟩
+
+/-- Smoothness is stable under isomorphisms. -/
+lemma isSmooth_of_iso {A B : Rep.{w} k G} (f : A ≅ B) (h : IsSmooth A.ρ) : IsSmooth B.ρ := by
+  simp_all only [isSmooth_iff]
+  intro v
+  specialize h (f.inv.hom v)
+  simp only [← f.inv.hom.isIntertwining] at h
+  have heq (g : G) : (Rep.Hom.hom f.inv) ((B.ρ g) v) = (Rep.Hom.hom f.inv) v ↔ (B.ρ g) v = v :=
+  ⟨fun hv => by simpa [Rep.hom_inv_apply] using congrArg (Rep.Hom.hom f.hom) hv,
+  fun hv => by rw [hv]⟩
+  simpa [heq] using h
+
+instance : (smoothProperty.{w} k G).IsClosedUnderIsomorphisms := ⟨by
+  simp only [smoothProperty_iff]; exact fun f h => (isSmooth_of_iso f h)⟩
+
+variable [IsTopologicalGroup G]
+
+/-- The canonical inclusion functor from `SmRep` to `Rep`. -/
+abbrev ι : SmRep.{w} k G ⥤ Rep.{w} k G := (smoothProperty.{w} k G).ι
+
+/-- The functor of taking the maximal smooth subrepresentation. -/
+def smVec : Rep.{w} k G ⥤ SmRep.{w} k G where
+  obj := fun A ↦ ⟨Rep.of ((smoothVectors A.ρ).toRepresentation), by simp [isSmooth_smoothVectors]⟩
+  map := fun f ↦ ObjectProperty.homMk (Rep.ofHom (IntertwiningMap.smoothVectors f.hom))
+
+/-- `ι` is left adjoint to `smVec`. -/
+def smVecAdjunction : ι ⊣ smVec.{w} (k := k) (G := G) where
+  unit := { app A := ObjectProperty.homMk <| Rep.ofHom {
+    toFun v := ⟨v, A.property.smooth v⟩
+    map_add' x y := by rfl, map_smul' m x := by rfl, isIntertwining' g := by rfl }}
+  counit := { app A := Rep.ofHom {
+    toFun v := v.1
+    map_add' x y := by rfl, map_smul' m x := by rfl, isIntertwining' g :=  by rfl }}
+
+/-- `SmRep` is a coreflexive full subcategory of `Rep`. -/
+lemma isIso_smVecAdjunction_unit : IsIso (smVecAdjunction.{w} (k := k) (G := G)).unit :=
+  smVecAdjunction.unit_isIso_of_L_fully_faithful
+
+section monoidal
+
+variable {k : Type u} [CommRing k]
+
+open MonoidalCategory
+
+/-- `SmRep` is a full monoidal subcategory of `Rep`. -/
+instance : ObjectProperty.IsMonoidal (smoothProperty.{u} k G) where
+  prop_unit := by simp [isSmooth_trivial]
+  prop_tensor := by simp_all [isSmooth_tprod]
+
+/-- The definition of internal `Hom` in the category of smooth representations. -/
+noncomputable def ihom (A : SmRep.{w} k G) := ι ⋙ (ι.obj A).ihom ⋙ smVec
+
+/-- The underlying representation of `ihom` is `smoothHom`. -/
+lemma ihom_eq_RepOfSmoothHom (A B : SmRep.{w} k G)
+    : ((ihom A).obj B).obj = Rep.of (smoothHom A.obj.ρ B.obj.ρ) := by
+  rfl
+
+/-- An auxiliary form of `tensorHomAdjunction`. -/
+noncomputable def tensorHomAdjunction' (A : SmRep.{u} k G)
+    : ι ⋙ (tensorLeft (ι.obj A)) ⊣ (Rep.ihom (ι.obj A)) ⋙ smVec :=
+  smVecAdjunction.comp (ihom.adjunction (ι.obj A))
+
+/-- The adjunction between `A ⨂ _` and `ihom (A, _)` in the category `SmRep`. -/
+noncomputable def tensorHomAdjunction (A : SmRep.{u} k G) : tensorLeft A ⊣ ihom A :=
+  Adjunction.restrictFullyFaithful
+  (adj := tensorHomAdjunction' A)
+  (hiC := Functor.FullyFaithful.id (SmRep k G))
+  (hiD := (smoothProperty k G).fullyFaithfulι)
+  (comm1 := Functor.Monoidal.commTensorLeft ι A)
+  (comm2 := (Functor.rightUnitor (ihom A)).symm)
+
+/-- The explicit isomorphism between `A ⊗ B ⟶ C` and `B ⟶ ihom (A, C)`. -/
+noncomputable def tensorHomEquiv (A B C : SmRep.{u} k G) : (A ⊗ B ⟶ C) ≃ (B ⟶ (SmRep.ihom A).obj C)
+  := ((smoothProperty k G).fullyFaithfulι.homEquiv).trans <|
+  (Rep.tensorHomEquiv (ι.obj A) (ι.obj B) (ι.obj C)).trans <|
+  smVecAdjunction.homEquiv B ((Rep.ihom (ι.obj A)).obj (ι.obj C))
+
+lemma tensorHomAdjunction_homEquiv_eq_tensorHomEquiv (A : SmRep.{u} k G)
+    : (tensorHomAdjunction A).homEquiv = tensorHomEquiv A := by
+  ext; rfl
+
+/-- `SmRep` is a full closed monoidal subcategory of `Rep`. -/
+noncomputable instance : MonoidalClosed (SmRep.{u} k G) where
+  closed A := { rightAdj := ihom A, adj := tensorHomAdjunction A }
+
+/-- `SmRep` is a full braided subcategory of `Rep`. -/
+noncomputable instance : BraidedCategory (SmRep.{u} k G) := by
+  infer_instance
+
+open Opposite
+
+/-- The dualizing functor in `SmRep`. -/
+noncomputable def dualFunctor : SmRep.{u} k G ⥤ (SmRep.{u} k G)ᵒᵖ where
+  obj A := op ((ihom A).obj (𝟙_ (SmRep.{u} k G)))
+  map {A B} f := op ((MonoidalClosed.pre (C := SmRep.{u} k G) f).app (𝟙_ (SmRep.{u} k G)))
+
+/-- The smooth dual representation. -/
+noncomputable abbrev dual (A : SmRep.{u} k G) := unop (dualFunctor.obj A)
+
+/-- The underlying construction of the dualizing functor is given by `contragredient`. -/
+lemma unop_dualObj_eq_contragredient (A : SmRep.{u} k G)
+    : (dual A).obj.ρ = contragredient A.obj.ρ := by
+  rfl
+
+end monoidal
+
+end SmRep
+
+end Representation.Smooth
diff --git a/Mathlib/RepresentationTheory/Stabilizer.lean b/Mathlib/RepresentationTheory/Stabilizer.lean
new file mode 100644
index 00000000000000..63a340d4383e6d
--- /dev/null
+++ b/Mathlib/RepresentationTheory/Stabilizer.lean
@@ -0,0 +1,69 @@
+/-
+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.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 multiples, sums, intertwining maps, and translates by group
+elements.
+
+-/
+
+@[expose] public section
+
+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' {a b} ha hb := by
+    rw [Set.mem_setOf_eq, map_mul, Module.End.mul_apply, hb, ha]
+  one_mem' := by simp
+  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
+  rfl
+
+lemma stabilizer_zero (ρ : Representation k G V) : stabilizer ρ 0 = ⊤ := by
+  ext; simp
+
+lemma le_stabilizer_smul (ρ : Representation k G V) (c : k) (v : V) :
+    stabilizer ρ v ≤ stabilizer ρ (c • v) := by
+  simp +contextual [SetLike.le_def]
+
+lemma le_stabilizer_add (ρ : Representation k G V) (v1 v2 : V) :
+    (stabilizer ρ v1) ⊓ (stabilizer ρ v2) ≤ stabilizer ρ (v1 + v2) := by
+  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
+  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
+  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) :
+    ρ.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,
+    ← 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
diff --git a/Mathlib/RepresentationTheory/Subrepresentation.lean b/Mathlib/RepresentationTheory/Subrepresentation.lean
index f69a7d13d6d269..9d606d9f4388f7 100644
--- a/Mathlib/RepresentationTheory/Subrepresentation.lean
+++ b/Mathlib/RepresentationTheory/Subrepresentation.lean
@@ -57,6 +57,16 @@ def toRepresentation (ρ' : Subrepresentation ρ) : Representation A G ρ'.toSub
   map_one' := by ext; simp
   map_mul' x y := by ext; simp
 
+@[simp]
+lemma toRepresentation_apply_mk {ρ' : Subrepresentation ρ} {g : G} {v w : W} {hv : v ∈ ρ'}
+    {hw : w ∈ ρ'}
+    : ρ'.toRepresentation g ⟨v, hv⟩ = ⟨w, hw⟩ ↔ ρ g v = w := by
+  rw [Subtype.ext_iff]; rfl
+
+lemma toRepresentation_apply_coe {ρ' : Subrepresentation ρ} {g : G} {v w : ρ'.toSubmodule}
+    : ρ'.toRepresentation g v = w ↔ ρ g v.1 = w.1 := by
+  rw [Subtype.ext_iff]; rfl
+
 instance : Max (Subrepresentation ρ) where
   max ρ₁ ρ₂ := .mk (ρ₁.toSubmodule ⊔ ρ₂.toSubmodule) <| by
       simp only [Submodule.forall_mem_sup, map_add]
@@ -97,6 +107,22 @@ instance : BoundedOrder (Subrepresentation ρ) where
 
 end non_comm
 
+section quotient
+
+variable {A G W : Type*} [Ring A] [Group G] [AddCommGroup W] [Module A W]
+
+/-- The quotient representation associated to a subrepresentation. -/
+def quotient {ρ : Representation A G W} (ρ' : Subrepresentation ρ) :
+    Representation A G (W ⧸ ρ'.toSubmodule) :=
+  ρ.quotient ρ'.toSubmodule (fun g _ hw => ρ'.apply_mem_toSubmodule g hw)
+
+lemma quotient_apply_mk {ρ : Representation A G W} (ρ' : Subrepresentation ρ)
+    (g : G) (w : W) :
+    ρ'.quotient g ⟦w⟧ = ⟦ρ g w⟧ := by
+  rfl
+
+end quotient
+
 variable [CommSemiring A] [Monoid G] [AddCommMonoid W] [Module A W]
   {ρ : Representation A G W} [AddCommMonoid M] [Module A[G] M]
 
diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean
index 9e9bd3ca160442..58f8c5a2801b5e 100644
--- a/Mathlib/Tactic/Linter/DirectoryDependency.lean
+++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean
@@ -618,6 +618,7 @@ def overrideAllowedImportDirs : NamePrefixRel := .ofArray #[
   (`Mathlib.Probability.Kernel.Category, `Mathlib.CategoryTheory), -- For the category of s-finite/Markov kernels
   (`Mathlib.RepresentationTheory.Continuous, `Mathlib.Topology), -- For continuous representations
   (`Mathlib.RepresentationTheory.Homological.ContCohomology, `Mathlib.Topology),  -- For continuous cohomology
+  (`Mathlib.RepresentationTheory.Smooth, `Mathlib.Topology), -- For smooth representations
   -- TODO: think about the role of Analysis and Algebra, and perhaps further separation
   (`Mathlib.Algebra.Order.Archimedean.Real, `Mathlib.Analysis),
   (`Mathlib.Algebra.Star.CHSH, `Mathlib.Analysis),