Compact

Results named in Tau Ceti's TauCeti.RepresentationTheory.Compact modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Frobenius-Schur reality trichotomy for compact groups#

The indicator of an irreducible unitary representation of a compact group on a finite-dimensional complex inner product space is 1, 0 or -1.

The indicator is the difference dim (Sym²V)ᴳ - dim (Λ²V)ᴳ (ContRepresentation.frobeniusSchurIndicator_eq_sub_finrank_invariants) and those two dimensions add up to at most 1 (ContRepresentation.finrank_invariants_squares_le_one), so the difference is one of the three values.

ContRepresentation.frobeniusSchurIndicator_trichotomy.{u_1, u_2} {G : Type u_1} {V : Type u_2}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [MeasurableSpace G]
  [BorelSpace G] [NormedAddCommGroup V] [InnerProductSpace ℂ V] [FiniteDimensional ℂ V]
  (π : ContRepresentation ℂ G V) (hπ : Continuous ⇑π) (hunitary : π.IsUnitary)
  (hirr : (ContRepresentation.toRepresentation ℂ G V π).IsIrreducible) :
  π.frobeniusSchurIndicator hπ = 1 ∨
    π.frobeniusSchurIndicator hπ = 0 ∨ π.frobeniusSchurIndicator hπ = -1
Lean

Formalized in Tau Ceti as ContRepresentation.frobeniusSchurIndicator_trichotomy.

Sources
LeanContRepresentation.frobeniusSchurIndicator_trichotomy

TheoremMaschke's theorem in orthogonal form#

A finite-dimensional representation π of a finite group on an inner product space is an internal direct sum of finitely many irreducible subrepresentations, of dimensions adding up to dim V, which are moreover pairwise orthogonal for an invariant inner product ⟪e ·, e ·⟫ obtained from the given one by a continuous linear automorphism e of the carrier.

This is the finite shadow of complete reducibility, and all that is finite about it is the production of e: unitarity is not assumed but produced, by the finite unitarian trick ContRepresentation.exists_isUnitary_congr_of_finite, and the decomposition of π itself is then ContRepresentation.IsUnitary.exists_orthogonal_irreducible_decomposition_of_congr, which decomposes the unitary model and carries every block back along the equivalence of representations ContRepresentation.congrEquiv : π.Equiv (congr e π) for an arbitrary group. The blocks are therefore subrepresentations of π itself.

Distorting the inner product by e is unavoidable and is what "Maschke" costs here: Lean fixes one inner product on V, and a representation of a finite group need not preserve it, only the average |G|⁻¹ ∑ g, ⟪π g ·, π g ·⟫ of its translates. So the blocks need not be orthogonal for ⟪·, ·⟫, and orthogonality is stated for the invariant form ⟪e ·, e ·⟫ that the unitarian trick produces — equivalently, their images under e are the orthogonal family decomposing the unitary model congr e π. It is that orthogonality which the compact theory contributes over Mathlib's Maschke, which produces complements but no inner product; the plain semisimplicity is not restated here, being already a Mathlib instance for every field in which |G| is invertible.

ContRepresentation.exists_orthogonal_irreducible_decomposition_of_finite.{u_1, u_2, u_3}
  {𝕜 : Type u_1} {G : Type u_2} {V : Type u_3} [RCLike 𝕜] [Group G] [Finite G]
  [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [FiniteDimensional 𝕜 V]
  (π : ContRepresentation 𝕜 G V) :
  ∃ e n U,
    (e.congr π).IsUnitary ∧
      (∀ (i : Fin n), (U i).toRepresentation.IsIrreducible) ∧
        (Pairwise fun i j =>
            ∀ v ∈ (U i).toSubmodule, ∀ w ∈ (U j).toSubmodule, inner 𝕜 (e v) (e w) = 0) ∧
          (DirectSum.IsInternal fun i => (U i).toSubmodule) ∧
            Module.finrank 𝕜 V = ∑ i, Module.finrank 𝕜 ↥(U i).toSubmodule
Lean

Formalized in Tau Ceti as ContRepresentation.exists_orthogonal_irreducible_decomposition_of_finite.

Sources
LeanContRepresentation.exists_orthogonal_irreducible_decomposition_of_finite

TheoremThe spectral theorem for a symmetric convolution operator#

its eigenspaces span a dense subspace of L²(G), in the sense that their supremum has trivial orthogonal complement. Together with finiteDimensional_eigenspace_convolutionOperator this says that L²(G) is exhausted, up to the kernel of the operator, by finite-dimensional translation-invariant subspaces.

TauCeti.orthogonalComplement_iSup_eigenspaces_convolutionOperator_eq_bot.{u_1, u_2} {𝕜 : Type u_1}
  {G : Type u_2} [RCLike 𝕜] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
  [MeasurableSpace G] [BorelSpace G] (k : C(G, 𝕜)) (hk : ∀ (g : G), k g⁻¹ = (starRingEnd 𝕜) (k g)) :
  (⨆ μ, Module.End.eigenspace (↑(TauCeti.convolutionOperator k)) μ)ᗮ = ⊥
Lean

Formalized in Tau Ceti as TauCeti.orthogonalComplement_iSup_eigenspaces_convolutionOperator_eq_bot.

Sources
LeanTauCeti.orthogonalComplement_iSup_eigenspaces_convolutionOperator_eq_bot
Used by 1
Used byThe Peter-Weyl theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.