Representations of topological and Lie groups

Representations of infinite groups and Lie algebras: continuous and unitary representations of compact and topological groups (Peter–Weyl theorem, complete reducibility), continuous representations over topological rings, representations of Lie algebras and of general linear groups (Schur–Weyl duality), and groups characterized by their irreducible representations.

• Groups with one irreducible representation in each dimension
• Representations of compact groups
• Schur–Weyl duality
• Tensor squares of exceptional Lie algebra representations

ClassContinuous semilinear representation#✓fully proved

Let \(G\) be a topological group, \(R\) a topological ring and \(M\) a topological abelian group that is a finite free \(R\)-module. Suppose that \(G\) acts on \(R\) by ring automorphisms and on \(M\) by additive automorphisms, and that the actions of \(G\) on \(R\), of \(G\) on \(M\) and of \(R\) on \(M\) are jointly continuous. This is a continuous semilinear representation of \(G\) on \(M\) when \(g \cdot (r x) = (g \cdot r)(g \cdot x)\) for all \(g \in G\), \(r \in R\) and \(x \in M\), and the coordinate map \(M \to R^n\) of a fixed basis of \(M\) over \(R\), where \(n\) is the size of the basis, is a homeomorphism onto \(R^n\) with the product topology.

class IsContinuousSemilinearRepresentation (G R M : Type*)
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [Ring R] [TopologicalSpace R] [IsTopologicalRing R]
    [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
    [Module R M] [Module.Free R M] [Module.Finite R M]
    [MulSemiringAction G R] [DistribMulAction G M]
    [ContinuousSMul G R] [ContinuousSMul G M] [ContinuousSMul R M] : Prop
    extends SMulDistribClass G R M where
  /-- The topology on `M` is the product topology transported through coordinates in a finite
  `R`-basis. -/
  isHomeomorph_equivFun : IsHomeomorph (Module.Free.chooseBasis R M).equivFun

Sources

• arXiv:2608.00845, Definition defsemilinrep (lines 1947–1950); this class records its object-level content.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.