feat(RepresentationTheory): add smooth representations for topological groups by JX-Mo · Pull Request #41199 · leanprover-community/mathlib4

JX-Mo · 2026-06-30T13:37:07Z

This PR introduces basic set up for smooth representations of a topological group. Hopefully it will serve as preliminary content for those who are interested in formalizing representation theory for p-adic reductive groups in the future. Concretely, we introduce the following in the file:

Define smoothness for representations of a topological group. It is a property for a representation to be smooth: the stabilizer of any vector is open.
Prove basic closure properties: subrepresentations, quotient representations, tensor products, direct sums of smooth representations are smooth.
Construct smoothHom and smoothDual: they are obtained by cutting out smooth vectors from the naive Hom and Dual.

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

1. Delete the last lemma and relevant imports. 2. Fix naming conventions. 3. Delete the long list in docstring.

Make {n : \Nat} implicit in le_stabilizer_sum

Style improvements.

Simplify proofs related to stabilizers using simp +contextual.

Use the latest lemma `inv_apply_eq_iff` to shorten the proof of stabilizer_conj

Add a lemma for Subrepresentation recording the inherited group action.

Add the definition of the quotient representation associated to a subrepresentation in Representation.Subrepresentation

Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>

Rename using `toRepresentation_apply_mk` and `quotient_apply_mk` Remove @[simp] above quotient_apply_mk

…l groups Introduces the concept of smooth representations for topological groups. Prove closure properties such as subrepresentations, quotient representations, direct sums, and tensor products being smooth. Construct smoothHom and smoothDual.

github-actions · 2026-06-30T13:37:17Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-06-30T13:38:36Z

PR summary ba30e4f091

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RepresentationTheory.Stabilizer` (new file)	1482
`Mathlib.RepresentationTheory.Smooth.Basic` (new file)	1610

Declarations diff (regex)

+ IntertwiningMap.isSmoothVector
+ IntertwiningMap.stabilizer_le
+ IsSmooth
+ IsSmoothVector
+ isSmoothVector_add
+ isSmoothVector_apply
+ isSmoothVector_iff
+ isSmoothVector_smul
+ isSmoothVector_sum
+ isSmoothVector_zero
+ isSmooth_directSum
+ isSmooth_iff
+ isSmooth_quotient
+ isSmooth_smoothDual
+ isSmooth_smoothHom
+ isSmooth_smoothVectors
+ isSmooth_subrepresentation
+ isSmooth_tprod
+ isSmooth_trivial
+ le_stabilizer_add
+ le_stabilizer_smul
+ le_stabilizer_sum
+ mem_smoothVectors
+ mem_stabilizer
+ quotient
+ quotient_apply_mk
+ smoothDual
+ smoothHom
+ smoothSubmodule
+ smoothVectors
+ stabilizer
+ stabilizer_conj
+ stabilizer_zero
+ toRepresentation_apply_mk

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit ba30e4f).

+40 new declarations
−0 removed declarations

+Representation.IntertwiningMap.stabilizer_le
+Representation.Smooth.IntertwiningMap.isSmoothVector
+Representation.Smooth.IsSmooth
+Representation.Smooth.IsSmooth.casesOn
+Representation.Smooth.IsSmooth.mk
+Representation.Smooth.IsSmooth.rec
+Representation.Smooth.IsSmooth.recOn
+Representation.Smooth.IsSmooth.smooth
+Representation.Smooth.IsSmoothVector
+Representation.Smooth.isSmoothVector_add
+Representation.Smooth.isSmoothVector_apply
+Representation.Smooth.isSmoothVector_iff
+Representation.Smooth.isSmoothVector_smul
+Representation.Smooth.isSmoothVector_sum
+Representation.Smooth.isSmoothVector_zero
+Representation.Smooth.isSmooth_directSum
+Representation.Smooth.isSmooth_iff
+Representation.Smooth.isSmooth_quotient
+Representation.Smooth.isSmooth_smoothDual
+Representation.Smooth.isSmooth_smoothHom
+Representation.Smooth.isSmooth_smoothVectors
+Representation.Smooth.isSmooth_subrepresentation
+Representation.Smooth.isSmooth_tprod
+Representation.Smooth.isSmooth_trivial
+Representation.Smooth.mem_smoothVectors
+Representation.Smooth.smoothDual
+Representation.Smooth.smoothHom
+Representation.Smooth.smoothSubmodule
+Representation.Smooth.smoothVectors
+Representation.Smooth.smoothVectors.congr_simp
+Representation.le_stabilizer_add
+Representation.le_stabilizer_smul
+Representation.le_stabilizer_sum
+Representation.mem_stabilizer
+Representation.stabilizer
+Representation.stabilizer_conj
+Representation.stabilizer_zero
+Subrepresentation.quotient
+Subrepresentation.quotient_apply_mk
+Subrepresentation.toRepresentation_apply_mk

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type (weak)
4997	2	exposed public sections

Current commit ba30e4f091
Reference commit 6b95510187

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mathlib-bors · 2026-06-30T13:39:33Z

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

loefflerd · 2026-06-30T20:52:02Z

I think you need to run lake exe mk_all in the mathlib root directory to add your file to Mathlib.lean. Otherwise the automatic CI tests don't run on it.

JX-Mo · 2026-07-01T04:44:42Z

Thanks for the reminder! I will fix it soon. Currently this draft depends on two smaller PR #41081 #40941

… Smooth.Basic

JX-Mo · 2026-07-01T08:24:35Z

The CI failure seems due to the warning:

Mathlib/RepresentationTheory/Smooth/Basic.lean:16:0: Modules starting with Mathlib.RepresentationTheory are not allowed to import modules starting with Mathlib.Topology. This module depends on Mathlib.Topology.Defs.Basic

When building up locally on my PC, there was a same warning, but no error reported.

loefflerd · 2026-07-01T09:11:37Z

The CI failure seems due to the warning:

Mathlib/RepresentationTheory/Smooth/Basic.lean:16:0: Modules starting with Mathlib.RepresentationTheory are not allowed to import modules starting with Mathlib.Topology. This module depends on Mathlib.Topology.Defs.Basic

When building up locally on my PC, there was a same warning, but no error reported.

You should add an allowed-import exception to Mathlib/Tactic/Linter/DirectoryDependency.lean, allowing files in Mathlib.RepresentationTheory.Smooth to import topology files.

JX-Mo · 2026-07-01T14:09:12Z

The CI failure seems due to the warning:
Mathlib/RepresentationTheory/Smooth/Basic.lean:16:0: Modules starting with Mathlib.RepresentationTheory are not allowed to import modules starting with Mathlib.Topology. This module depends on Mathlib.Topology.Defs.Basic
When building up locally on my PC, there was a same warning, but no error reported.

You should add an allowed-import exception to Mathlib/Tactic/Linter/DirectoryDependency.lean, allowing files in Mathlib.RepresentationTheory.Smooth to import topology files.

CI is green now. Thanks a lot!

JX-Mo · 2026-07-01T14:26:40Z

-awaiting-author

mathlib-merge-conflicts · 2026-07-03T00:15:03Z

This pull request has conflicts, please merge master and resolve them.

JX-Mo and others added 16 commits June 23, 2026 18:21

add Stabilizer in RepresentationTheory

03612d8

add Stabilizer in RepresentationTheory

832d219

Update Mathlib/RepresentationTheory/Stabilizer.lean

cc068a0

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

Address review comments

97aab09

1. Delete the last lemma and relevant imports. 2. Fix naming conventions. 3. Delete the long list in docstring.

Fix lemma le_stabilizer_sum argument syntax

418e1da

Make {n : \Nat} implicit in le_stabilizer_sum

Merge branch 'master' into representation-stabilizer

518dd1b

Address review comments

abb5d00

Style improvements.

Refactor stabilizer lemmas with simp +contextual

fee6925

Simplify proofs related to stabilizers using simp +contextual.

Merge branch 'master' into representation-stabilizer

8231b32

Refactor stabilizer_conj lemma for simplification

6215b70

Use the latest lemma `inv_apply_eq_iff` to shorten the proof of stabilizer_conj

Add lemma for toRepresentation application

0f0fedd

Add a lemma for Subrepresentation recording the inherited group action.

Add quotient representation for a subrepresentation

a96b6d0

Add the definition of the quotient representation associated to a subrepresentation in Representation.Subrepresentation

Update Mathlib/RepresentationTheory/Subrepresentation.lean

ff35791

Co-authored-by: Whysoserioushah <109107491+Whysoserioushah@users.noreply.github.com>

Address review comments

64f2246

Rename using `toRepresentation_apply_mk` and `quotient_apply_mk` Remove @[simp] above quotient_apply_mk

Fix formatting in toRepresentation_apply_mk lemma

be113c2

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jun 30, 2026

github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label Jun 30, 2026

JX-Mo marked this pull request as draft June 30, 2026 13:39

JX-Mo mentioned this pull request Jun 30, 2026

feat(RepresentationTheory): add stabilizers of vectors in representations #40941

Open

JX-Mo added 5 commits July 1, 2026 14:07

Merge branch 'pr-40941' into Smooth.Basic

d63b652

Merge branch 'pr-41081' into Smooth.Basic

ab47e86

Rename Basic to Basic.lean

017f810

Merge branch 'Smooth.Basic' of https://github.com/JX-Mo/mathlib4 into…

531a22a

… Smooth.Basic

Update Mathlib.lean

4ed7cbe

JX-Mo force-pushed the Smooth.Basic branch from c37e186 to 4ed7cbe Compare July 1, 2026 07:37

loefflerd added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 1, 2026

Allow smooth representations to import topology

fff9107

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 3, 2026

t pushMerge remote-tracking branch 'upstream/master' into Smooth.Basic

ba30e4f

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 3, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(RepresentationTheory): add smooth representations for topological groups#41199

feat(RepresentationTheory): add smooth representations for topological groups#41199
JX-Mo wants to merge 23 commits into
leanprover-community:masterfrom
JX-Mo:Smooth.Basic

JX-Mo commented Jun 30, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jun 30, 2026

Uh oh!

github-actions Bot commented Jun 30, 2026 •

edited

Loading

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-bors Bot commented Jun 30, 2026

Uh oh!

loefflerd commented Jun 30, 2026

Uh oh!

JX-Mo commented Jul 1, 2026 •

edited

Loading

Uh oh!

JX-Mo commented Jul 1, 2026

Uh oh!

loefflerd commented Jul 1, 2026

Uh oh!

JX-Mo commented Jul 1, 2026

Uh oh!

JX-Mo commented Jul 1, 2026 •

edited

Loading

Uh oh!

mathlib-merge-conflicts Bot commented Jul 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

JX-Mo commented Jun 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jun 30, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Jun 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ba30e4f091

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-bors Bot commented Jun 30, 2026

Uh oh!

loefflerd commented Jun 30, 2026

Uh oh!

JX-Mo commented Jul 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JX-Mo commented Jul 1, 2026

Uh oh!

loefflerd commented Jul 1, 2026

Uh oh!

JX-Mo commented Jul 1, 2026

Uh oh!

JX-Mo commented Jul 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-merge-conflicts Bot commented Jul 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

JX-Mo commented Jun 30, 2026 •

edited

Loading

github-actions Bot commented Jun 30, 2026 •

edited

Loading

JX-Mo commented Jul 1, 2026 •

edited

Loading

JX-Mo commented Jul 1, 2026 •

edited

Loading