The unitary and special unitary matrix groups are compact

For a finite index type n and 𝕜 = ℝ or ℂ (any RCLike field), the unitary group Matrix.unitaryGroup n 𝕜 and the special unitary group Matrix.specialUnitaryGroup n 𝕜 are compact subsets of Matrix n n 𝕜 in the entrywise topology, hence compact topological groups.

The argument is the classical one. A unitary matrix has unit rows, so all its entries lie in the closed unit ball (Mathlib's entry_norm_bound_of_unitary); the unitary group is therefore contained in the compact set of matrices with entries in that ball, and it is closed because it is cut out by the equations star A * A = 1 and A * star A = 1. The special unitary group adds the closed condition det A = 1.

Mathlib already supplies the topological group structure on unitary R for a topological star monoid R (isClosed_unitary and the IsTopologicalGroup (unitary R) instance), so for the unitary group only compactness is new. The special unitary group is a different submonoid, carrying its own Group instance in Mathlib/LinearAlgebra/UnitaryGroup.lean, so its ContinuousInv and IsTopologicalGroup instances are recorded here too. Those instances and its closedness need no RCLike hypothesis, and are stated over a topological commutative star ring instead; only compactness is RCLike-specific. Hausdorffness is not proved here: it is inherited from the ambient matrix topology whenever 𝕜 is Hausdorff.

Closedness is also recorded one level up, for TauCeti.GLSpecialUnitary, the same group seen as a subgroup of the general linear group of units: its carrier is the preimage of the matrix special unitary group under the continuous coercion Units.val. That is the form in which the closed-subgroup theorem consumes it.

This is the setup the compact-group representation theory of SU(2) runs on; see TauCeti/RepresentationTheory/SU2/Basic.lean.

Main results

• TauCeti.Matrix.isClosed_specialUnitaryGroup: the special unitary matrix group is closed.
• TauCeti.Matrix.isCompact_unitaryGroup and TauCeti.Matrix.isCompact_specialUnitaryGroup: the unitary and special unitary matrix groups over ℝ or ℂ are compact.
• TauCeti.isClosed_GLSpecialUnitary: the special unitary subgroup of the general linear group is closed.

instance TauCeti.Matrix.instContinuousInvSubtypeMatrixMemSubmonoidSpecialUnitaryGroup_tauCeti {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [CommRing 𝕜] [StarRing 𝕜] [TopologicalSpace 𝕜] [ContinuousStar 𝕜] : ContinuousInv ↥(Matrix.specialUnitaryGroup n 𝕜)

instance TauCeti.Matrix.instIsTopologicalGroupSubtypeMatrixMemSubmonoidSpecialUnitaryGroup_tauCeti {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [CommRing 𝕜] [StarRing 𝕜] [TopologicalSpace 𝕜] [ContinuousStar 𝕜] [IsTopologicalSemiring 𝕜] : IsTopologicalGroup ↥(Matrix.specialUnitaryGroup n 𝕜)

theorem TauCeti.Matrix.isClosed_specialUnitaryGroup {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [CommRing 𝕜] [StarRing 𝕜] [TopologicalSpace 𝕜] [ContinuousStar 𝕜] [IsTopologicalRing 𝕜] [T1Space 𝕜] : IsClosed ↑(Matrix.specialUnitaryGroup n 𝕜)

The special unitary group of n × n matrices is a closed subset of Matrix n n 𝕜: it is cut out of the closed unitary group by the closed condition det A = 1.

theorem TauCeti.Matrix.isCompact_unitaryGroup {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] : IsCompact ↑(Matrix.unitaryGroup n 𝕜)

The unitary group of n × n matrices over ℝ or ℂ is a compact subset of Matrix n n 𝕜.

instance TauCeti.Matrix.instCompactSpaceSubtypeMatrixMemSubmonoidUnitaryGroup_tauCeti {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] : CompactSpace ↥(Matrix.unitaryGroup n 𝕜)

theorem TauCeti.Matrix.isCompact_specialUnitaryGroup {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] : IsCompact ↑(Matrix.specialUnitaryGroup n 𝕜)

The special unitary group of n × n matrices over ℝ or ℂ is a compact subset of Matrix n n 𝕜.

instance TauCeti.Matrix.instCompactSpaceSubtypeMatrixMemSubmonoidSpecialUnitaryGroup_tauCeti {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] : CompactSpace ↥(Matrix.specialUnitaryGroup n 𝕜)

theorem TauCeti.isClosed_GLSpecialUnitary (n : Type u_1) [Fintype n] [DecidableEq n] (𝕜 : Type u_2) [CommRing 𝕜] [StarRing 𝕜] [TopologicalSpace 𝕜] [ContinuousStar 𝕜] [IsTopologicalRing 𝕜] [T1Space 𝕜] : IsClosed ↑(GLSpecialUnitary n 𝕜)

The special unitary subgroup of the general linear group is closed. Its carrier is the preimage of the closed matrix special unitary group under the continuous coercion of units. This is the hypothesis the closed-subgroup theorem needs in order to promote it to an embedded Lie subgroup.