feat(Analysis/CStarAlgebra/Matrix): CompactSpace instances for unitaryGroup and specialUnitaryGroup by anovickis · Pull Request #39146 · leanprover-community/mathlib4

anovickis · 2026-05-10T18:42:57Z

Adds CompactSpace instances (and supporting IsClosed / IsCompact lemmas) for the matrix unitary and special unitary groups.

The compactness follows from Heine-Borel applied to the entrywise sup norm: every unitary matrix has all entries bounded by 1 (via the existing entry_norm_bound_of_unitary lemma), and Matrix n n 𝕜 is finite-dimensional, so closed + bounded ⇒ compact.

New declarations

isClosed_unitaryGroup, isCompact_unitaryGroup
instance Matrix.unitaryGroup.instCompactSpace
isClosed_specialUnitaryGroup, isCompact_specialUnitaryGroup
instance Matrix.specialUnitaryGroup.instCompactSpace

All placed inside the existing EntrywiseSupNorm section in Mathlib/Analysis/CStarAlgebra/Matrix.lean, so the Matrix.Norms.Elementwise scope used for the bound is already in scope.

Motivation

These instances enable downstream constructions of compact matrix Lie groups such as flag manifolds (e.g. SU(3)/T = F₂), where the quotient inherits compactness for free via Quotient.compactSpace. They also fill an obvious gap in the matrix-group API: unitary R is known to be closed, but compactness for Matrix.unitaryGroup was not previously available as an instance.

…aryGroup Adds: - isClosed_unitaryGroup, isClosed_specialUnitaryGroup - isCompact_unitaryGroup, isCompact_specialUnitaryGroup - CompactSpace instances on both groups The compactness follows from Heine-Borel applied to the entrywise sup norm: each unitary matrix has all entries bounded by 1 (via the existing entry_norm_bound_of_unitary lemma), and the matrix space is finite- dimensional, so closed + bounded suffices for compactness.

github-actions · 2026-05-10T18:43:08Z

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-05-10T18:44:13Z

PR summary 706bea155c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Matrix.specialUnitaryGroup.instCompactSpace
+ Matrix.unitaryGroup.instCompactSpace
+ isClosed_specialUnitaryGroup
+ isClosed_unitaryGroup
+ isCompact_specialUnitaryGroup
+ isCompact_unitaryGroup

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.

No changes to strong technical debt.

No changes to weak technical debt.

wwylele

If you used AI, could you disclose it according to the guideline? In particular, writing comments on github using LLM is not allowed.

wwylele · 2026-05-10T18:55:37Z


+section Compact
+
+set_option backward.isDefEq.respectTransparency false


I did a quick test on Lean web and it doesn't look like this is necessary

wwylele · 2026-05-10T18:57:03Z

+section Compact
+
+set_option backward.isDefEq.respectTransparency false
+open scoped Matrix.Norms.Elementwise


This is only used internally by isCompact_unitaryGroup. To emphasize the fact that the public statement doesn't rely on any particular norm, you can put open scoped Matrix.Norms.Elementwise in as the first line after by

j-loreaux

Did you use AI for this PR? You must disclose this.

One thing that this approach fails to capture is that the unitary group of a C⋆-algebra which is also a proper space (i.e., finite dimensional) is compact as well. It would be possible to prove that instead, and then use the C⋆-norm instead of the sup norm to get these results. However, given that they are short enough, I won't require it for this PR.

j-loreaux · 2026-05-10T20:19:10Z

+/-- The unitary group `Matrix.unitaryGroup n 𝕜` is closed inside `Matrix n n 𝕜`. -/
+theorem isClosed_unitaryGroup :
+    IsClosed (Matrix.unitaryGroup n 𝕜 : Set (Matrix n n 𝕜)) := by
+  have h_eq : (Matrix.unitaryGroup n 𝕜 : Set (Matrix n n 𝕜)) = { U | U * star U = 1 } := by
+    ext U; simp [Matrix.mem_unitaryGroup_iff]
+  rw [h_eq]
+  exact isClosed_singleton.preimage (by fun_prop)


This already exists as isClosed_unitary (and it works for Matrix.unitaryGroup since that is an abbrev).

j-loreaux · 2026-05-10T20:21:01Z

+  rw [Metric.isCompact_iff_isClosed_bounded]
+  refine ⟨isClosed_unitaryGroup, ?_⟩
+  refine (Metric.isBounded_closedBall (x := (0 : Matrix n n 𝕜)) (r := 1)).subset ?_
+  intro U hU
+  rw [Metric.mem_closedBall, dist_zero_right]
+  exact entrywise_sup_norm_bound_of_unitary hU


The metric structure is only needed for the proof, so I would instead only open the scope within the proof. Also, it can be golfed using dedicated lemmas like so:

Suggested change

rw [Metric.isCompact_iff_isClosed_bounded]

refine ⟨isClosed_unitaryGroup, ?_⟩

refine (Metric.isBounded_closedBall (x := (0 : Matrix n n 𝕜)) (r := 1)).subset ?_

intro U hU

rw [Metric.mem_closedBall, dist_zero_right]

exact entrywise_sup_norm_bound_of_unitary hU

open scoped Matrix.Norms.Elementwise in

exact Metric.isCompact_of_isClosed_isBounded isClosed_unitary <|

isBounded_iff_forall_norm_le.mpr ⟨1, fun _ ↦ entrywise_sup_norm_bound_of_unitary⟩

Note you need to import Mathlib.Topology.Algebra.Star.Unitary to get the isClosed_unitary lemma.

j-loreaux · 2026-05-10T20:22:10Z

+/-- The special unitary group `Matrix.specialUnitaryGroup n 𝕜` is closed inside
+`Matrix n n 𝕜`. -/
+theorem isClosed_specialUnitaryGroup :
+    IsClosed (Matrix.specialUnitaryGroup n 𝕜 : Set (Matrix n n 𝕜)) := by
+  have h_inter : (Matrix.specialUnitaryGroup n 𝕜 : Set (Matrix n n 𝕜))
+      = (Matrix.unitaryGroup n 𝕜 : Set (Matrix n n 𝕜)) ∩ { U | U.det = 1 } := by
+    ext U
+    simp [Matrix.specialUnitaryGroup, Set.mem_inter_iff]
+  rw [h_inter]
+  exact isClosed_unitaryGroup.inter (isClosed_singleton.preimage (by fun_prop))


I would remove this an go directly for compactness.

j-loreaux · 2026-05-10T20:38:07Z

+  isCompact_unitaryGroup.of_isClosed_subset isClosed_specialUnitaryGroup
+    Matrix.specialUnitaryGroup_le_unitaryGroup


This doesn't need the previous result.

Suggested change

isCompact_unitaryGroup.of_isClosed_subset isClosed_specialUnitaryGroup

Matrix.specialUnitaryGroup_le_unitaryGroup

isCompact_unitaryGroup.inter_right <| isClosed_singleton.preimage (by dsimp; fun_prop)

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 May 10, 2026

github-actions Bot added the t-analysis Analysis (normed *, calculus) label May 10, 2026

wwylele reviewed May 10, 2026

View reviewed changes

anovickis mentioned this pull request May 10, 2026

feat(Analysis/CStarAlgebra/Matrix): IsTopologicalGroup for specialUnitaryGroup #39151

Open

j-loreaux reviewed May 10, 2026

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label May 10, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Analysis/CStarAlgebra/Matrix): CompactSpace instances for unitaryGroup and specialUnitaryGroup#39146

feat(Analysis/CStarAlgebra/Matrix): CompactSpace instances for unitaryGroup and specialUnitaryGroup#39146
anovickis wants to merge 1 commit into
leanprover-community:masterfrom
anovickis:feat-compact-unitary-group

anovickis commented May 10, 2026

Uh oh!

github-actions Bot commented May 10, 2026

Uh oh!

github-actions Bot commented May 10, 2026

Declarations diff

Uh oh!

wwylele left a comment

Uh oh!

wwylele May 10, 2026

Uh oh!

wwylele May 10, 2026

Uh oh!

j-loreaux left a comment

Uh oh!

j-loreaux May 10, 2026

Uh oh!

j-loreaux May 10, 2026

Uh oh!

j-loreaux May 10, 2026

Uh oh!

j-loreaux May 10, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants


		section Compact

		set_option backward.isDefEq.respectTransparency false

		isCompact_unitaryGroup.of_isClosed_subset isClosed_specialUnitaryGroup
		Matrix.specialUnitaryGroup_le_unitaryGroup

	isCompact_unitaryGroup.of_isClosed_subset isClosed_specialUnitaryGroup
	Matrix.specialUnitaryGroup_le_unitaryGroup
	isCompact_unitaryGroup.inter_right <\| isClosed_singleton.preimage (by dsimp; fun_prop)

Conversation

anovickis commented May 10, 2026

New declarations

Motivation

Uh oh!

github-actions Bot commented May 10, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented May 10, 2026

PR summary 706bea155c

Import changes for modified files

Declarations diff

Uh oh!

wwylele left a comment

Choose a reason for hiding this comment

Uh oh!

wwylele May 10, 2026

Choose a reason for hiding this comment

Uh oh!

wwylele May 10, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

j-loreaux May 10, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux May 10, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux May 10, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux May 10, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants