Continuous representations (algebraic + topology)

This file defines ContinuousRep R G V: a Representation R G V together with continuity of the action map G × V → V.

This file contains basic definitions and properties.

The category-theoretic packaging lives in PAdicRep.ContinuousReps.CRep.

Actions induced by a representation

For many purposes (e.g. stabilizers, orbits, group cohomology), it is convenient to view a representation ρ : Representation R G V as a G-action on V.

Mathlib provides constructions in the other direction (MulAction/DistribMulAction → Representation), but (as of the current mathlib version in this project) it does not provide Representation → MulAction/DistribMulAction.

We therefore add lightweight definitions here. These are intended to be used via local instances: letI : MulAction G V := (ρ.mulAction) or letI : DistribMulAction G V := (ρ.distribMulAction).

def Representation.toFunctionEnd {R : Type u} [CommSemiring R] {G : Type v} [Monoid G] {V : Type w} [AddCommMonoid V] [Module R V] (ρ : Representation R G V) : G →* Function.End V

Forget the linear structure of a representation, as a monoid hom to Function.End V.

Equations

• ρ.toFunctionEnd = { toFun := fun (g : G) (x : V) => (ρ g) x, map_one' := ⋯, map_mul' := ⋯ }

@[reducible, inline]

abbrev Representation.mulAction {R : Type u} [CommSemiring R] {G : Type v} [Monoid G] {V : Type w} [AddCommMonoid V] [Module R V] (ρ : Representation R G V) : MulAction G V

The MulAction of G on V induced by a representation ρ, i.e. g • v := ρ g v.

This is best used via a local instance: letI : MulAction G V := ρ.mulAction.

Equations

• ρ.mulAction = MulAction.ofEndHom ρ.toFunctionEnd

def Representation.distribMulAction {R : Type u} [CommSemiring R] {G : Type v} [Monoid G] {V : Type w} [AddCommMonoid V] [Module R V] (ρ : Representation R G V) : DistribMulAction G V

The DistribMulAction (i.e. a ℤ[G]-module structure) on V induced by ρ.

This is best used via a local instance: letI : DistribMulAction G V := ρ.distribMulAction.

Equations

• ρ.distribMulAction = { toMulAction := ρ.mulAction, smul_zero := ⋯, smul_add := ⋯ }

@[simp]

theorem Representation.mulAction_smul_def {R : Type u} [CommSemiring R] {G : Type v} [Monoid G] {V : Type w} [AddCommMonoid V] [Module R V] (ρ : Representation R G V) (g : G) (v : V) : g • v = (ρ g) v

@[simp]

theorem Representation.distribMulAction_smul_def {R : Type u} [CommSemiring R] {G : Type v} [Monoid G] {V : Type w} [AddCommMonoid V] [Module R V] (ρ : Representation R G V) (g : G) (v : V) : g • v = (ρ g) v

def Representation.stabilizer {R : Type u} [CommSemiring R] {V : Type w} [AddCommMonoid V] [Module R V] {G : Type v} [Group G] (ρ : Representation R G V) (v : V) : Subgroup G

The stabilizer subgroup of a vector v : V in the representation ρ.

This is defined using the MulAction induced by ρ, and is intended to be used without introducing a global MulAction instance.

Equations

• ρ.stabilizer v = MulAction.stabilizer G v

@[simp]

theorem Representation.mem_stabilizer_iff {R : Type u} [CommSemiring R] {V : Type w} [AddCommMonoid V] [Module R V] {G : Type v} [Group G] (ρ : Representation R G V) (v : V) (g : G) : g ∈ ρ.stabilizer v ↔ (ρ g) v = v

A topology-free fiber/coset identity for group actions

theorem MulAction.preimage_smul_eq_preimage_stabilizer {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (x b : X) (g0 : G) (hg0 : g0 • x = b) : (fun (g : G) => g • x) ⁻¹' {b} = (fun (g : G) => g0⁻¹ * g) ⁻¹' ↑(stabilizer G x)

If g0 • x = b, then the fiber of g ↦ g • x over b is a left coset of the stabilizer.

A set-theoretic decomposition for action preimages

theorem MulAction.preimage_smul_preimage_eq_iUnion_orbitMap_preimage {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] (s : Set X) : (fun (p : G × X) => p.1 • p.2) ⁻¹' s = ⋃ (x : X), ((fun (g : G) => g • x) ⁻¹' s) ×ˢ {x}

Preimage decomposition for the action map (g, x) ↦ g • x.

@[reducible, inline]

abbrev ContinuousRep (R : Type u) [CommRing R] (G : Type v) [Group G] [TopologicalSpace G] (V : Type w) [AddCommGroup V] [Module R V] [TopologicalSpace V] : Type (max 0 v w)

A continuous representation of a group G on an R-module V.

This is a Representation R G V together with the continuity of the action map (g, v) ↦ ρ g v.

We use an abbrev (rather than a new structure) so that the underlying representation is definitionally just a Representation, matching the style of Mathlib.RepresentationTheory.

Equations

• ContinuousRep R G V = { ρ : Representation R G V // Continuous fun (p : G × V) => (ρ p.1) p.2 }

instance ContinuousRep.instCoeRepresentation {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] : Coe (ContinuousRep R G V) (Representation R G V)

Equations

• ContinuousRep.instCoeRepresentation = { coe := fun (ρ : ContinuousRep R G V) => ↑ρ }

instance ContinuousRep.instCoeFunForallLinearMapId {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] : CoeFun (ContinuousRep R G V) fun (x : ContinuousRep R G V) => G → V →ₗ[R] V

Equations

• ContinuousRep.instCoeFunForallLinearMapId = { coe := fun (ρ : ContinuousRep R G V) => ⇑↑ρ }

def ContinuousRep.of {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : Representation R G V) (hcont : Continuous fun (p : G × V) => (ρ p.1) p.2) : ContinuousRep R G V

Lift a representation together with continuity of the action map to ContinuousRep.

Equations

• ContinuousRep.of ρ hcont = ⟨ρ, hcont⟩

@[simp]

theorem ContinuousRep.of_fst {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : Representation R G V) (hcont : Continuous fun (p : G × V) => (ρ p.1) p.2) : ↑(of ρ hcont) = ρ

@[simp]

theorem ContinuousRep.of_snd {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : Representation R G V) (hcont : Continuous fun (p : G × V) => (ρ p.1) p.2) : ⋯ = hcont

@[simp]

theorem ContinuousRep.coe_of {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : Representation R G V) (hcont : Continuous fun (p : G × V) => (ρ p.1) p.2) : ↑(of ρ hcont) = ρ

@[simp]

theorem ContinuousRep.of_apply {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : Representation R G V) (hcont : Continuous fun (p : G × V) => (ρ p.1) p.2) (g : G) (v : V) : (↑(of ρ hcont) g) v = (ρ g) v

@[simp]

theorem ContinuousRep.coe_apply {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (g : G) (v : V) : (↑ρ g) v = (↑ρ g) v

@[reducible, inline]

abbrev ContinuousRep.action {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) : G × V → V

The action map G × V → V associated to a continuous representation.

Equations

• ρ.action p = (↑ρ p.1) p.2

@[simp]

theorem ContinuousRep.action_apply {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (g : G) (v : V) : ρ.action (g, v) = (↑ρ g) v

theorem ContinuousRep.continuous {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) : Continuous ρ.action

Basic continuity lemmas

Realize the underlying module as a topological module

def ContinuousRep.toTopModuleCat {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] [ContinuousAdd V] [ContinuousSMul R V] (_ρ : ContinuousRep R G V) : TopModuleCat R

The underlying topological R-module of a ContinuousRep, bundled as an object of TopModuleCat R.

This is just TopModuleCat.of R V, but having it as a named abbreviation makes later constructions (e.g. in CRep) shorter.

Equations

• _ρ.toTopModuleCat = TopModuleCat.of R V

@[simp]

theorem ContinuousRep.toTopModuleCat_def {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] [ContinuousAdd V] [ContinuousSMul R V] (ρ : ContinuousRep R G V) : ρ.toTopModuleCat = TopModuleCat.of R V

Building ContinuousRep from TopModuleCat

def ContinuousRep.ofTopModuleCat {R : Type u} [CommRing R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] (M : TopModuleCat R) (ρ : Representation R G ↑M.toModuleCat) (hcont : Continuous fun (p : G × ↑M.toModuleCat) => (ρ p.1) p.2) : ContinuousRep R G ↑M.toModuleCat

Given an object M : TopModuleCat R and a continuous G-action by R-linear maps on the underlying type, produce a ContinuousRep R G M.

This is a convenience wrapper around ContinuousRep.of, specialized to the case where the representation space is already bundled as a TopModuleCat object.

Equations

• ContinuousRep.ofTopModuleCat M ρ hcont = ContinuousRep.of ρ hcont

theorem ContinuousRep.continuous_const_smul {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (g : G) : Continuous fun (v : V) => (↑ρ g) v

theorem ContinuousRep.continuous_smul_const {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (v : V) : Continuous fun (g : G) => (↑ρ g) v

theorem ContinuousRep.continuous_const_smul_add_const {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] [ContinuousAdd V] (ρ : ContinuousRep R G V) (g : G) (u : V) : Continuous fun (v : V) => (↑ρ g) v + u

theorem ContinuousRep.ext {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] {ρ σ : ContinuousRep R G V} (h : ↑ρ = ↑σ) : ρ = σ

theorem ContinuousRep.ext_iff {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] {ρ σ : ContinuousRep R G V} : ρ = σ ↔ ↑ρ = ↑σ

@[simp]

theorem ContinuousRep.toRepresentation_ext_iff {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] {ρ σ : ContinuousRep R G V} : ρ = σ ↔ ↑ρ = ↑σ

Trivial continuous representation

@[reducible, inline]

abbrev ContinuousRep.IsTrivial {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) : Prop

A predicate for continuous representations which fix every element.

Equations

• ρ.IsTrivial = (↑ρ).IsTrivial

@[simp]

theorem ContinuousRep.isTrivial_def {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) [ρ.IsTrivial] (g : G) : ↑ρ g = LinearMap.id

theorem ContinuousRep.isTrivial_apply {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) [ρ.IsTrivial] (g : G) (x : V) : (↑ρ g) x = x

def ContinuousRep.ofIsTrivial {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : Representation R G V) [ρ.IsTrivial] : ContinuousRep R G V

Bundle an (algebraically) trivial representation as a continuous representation.

Equations

• ContinuousRep.ofIsTrivial ρ = ⟨ρ, ⋯⟩

def ContinuousRep.trivial {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] : ContinuousRep R G V

The trivial continuous representation.

Equations

• ContinuousRep.trivial = ⟨Representation.trivial R G V, ⋯⟩

instance ContinuousRep.instIsTrivialTrivial {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] : trivial.IsTrivial

def ContinuousRep.restrict {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (H : Subgroup G) : ContinuousRep R (↥H) V

Restrict a continuous representation to a subgroup.

Equations

• ρ.restrict H = ⟨MonoidHom.comp (↑ρ) H.subtype, ⋯⟩

@[simp]

theorem ContinuousRep.restrict_apply {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (H : Subgroup G) (h : ↥H) (v : V) : (↑(ρ.restrict H) h) v = (↑ρ ↑h) v

Descent to a quotient group

def ContinuousRep.ofQuotient {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (N : Subgroup G) [N.Normal] [(ρ.restrict N).IsTrivial] : ContinuousRep R (G ⧸ N) V

If a continuous representation is trivial on a normal subgroup N, it factors through G ⧸ N.

Equations

• ρ.ofQuotient N = ContinuousRep.of ((↑ρ).ofQuotient N) ⋯

@[simp]

theorem ContinuousRep.ofQuotient_coe_apply {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (N : Subgroup G) [N.Normal] [(ρ.restrict N).IsTrivial] (g : G) (x : V) : (↑(ρ.ofQuotient N) ↑g) x = (↑ρ g) x

Stabilizers

@[reducible, inline]

abbrev ContinuousRep.stabilizer {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (v : V) : Subgroup G

The stabilizer subgroup of v in ρ.

Equations

• ρ.stabilizer v = (↑ρ).stabilizer v

@[simp]

theorem ContinuousRep.mem_stabilizer_iff {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (v : V) (g : G) : g ∈ ρ.stabilizer v ↔ (↑ρ g) v = v

theorem ContinuousRep.stabilizer_coe_eq_preimage_singleton {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] (ρ : ContinuousRep R G V) (v : V) : ↑(ρ.stabilizer v) = (fun (g : G) => (↑ρ g) v) ⁻¹' {v}

Discrete target spaces

Three conditions (discrete target)

Assume [DiscreteTopology V]. For an algebraic representation ρ : Representation R G V, we consider the following three conditions:

1. (Action continuity) the action map G × V → V, (g, v) ↦ ρ g v, is continuous;
2. (Orbit-map continuity) for every v : V, the orbit map G → V, g ↦ ρ g v, is continuous;
3. (Open stabilizers) for every v : V, the stabilizer subgroup ρ.stabilizer v is open in G.

We will prove the implications as three separate theorems, in the order 1 → 2 → 3 → 1. At the moment these are only stated, with proofs left as sorry.

Remark: the direction (1) → (2) is essentially just “fix v and precompose by g ↦ (g, v)”. In this file it is already available in the bundled setting as ContinuousRep.continuous_smul_const.

The implication chain 2 → 3 → 1

If a stabilizer is open, then all fibers of the corresponding orbit map are open.

theorem ContinuousRep.isOpen_orbitFiber_of_isOpen_stabilizer {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : Type w} [AddCommGroup V] [Module R V] (ρ : Representation R G V) (v b : V) (hopen : IsOpen ↑(ρ.stabilizer v)) : IsOpen ((fun (g : G) => (ρ g) v) ⁻¹' {b})

theorem ContinuousRep.discreteTopology_forall_isOpen_stabilizer_of_forall_continuous_smul_const {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] [DiscreteTopology V] (ρ : Representation R G V) (hcont : ∀ (v : V), Continuous fun (g : G) => (ρ g) v) (v : V) : IsOpen ↑(ρ.stabilizer v)

(2) → (3): continuity of all orbit maps implies openness of all stabilizers.

theorem ContinuousRep.discreteTopology_continuous_action_of_forall_isOpen_stabilizer {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] [DiscreteTopology V] (ρ : Representation R G V) (hopen : ∀ (v : V), IsOpen ↑(ρ.stabilizer v)) : Continuous fun (p : G × V) => (ρ p.1) p.2

(3) → (1): openness of all stabilizers implies continuity of the action map.

This is the nontrivial direction: for a discrete target it suffices to show that every fiber is open, and each fiber is a (possibly empty) left coset of a stabilizer, hence open.

theorem ContinuousRep.exists_discreteTopology_continuous_action_of_forall_isOpen_stabilizer {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : Type w} [AddCommGroup V] [Module R V] (ρ : Representation R G V) (hopen : ∀ (v : V), IsOpen ↑(ρ.stabilizer v)) : ∃ (t : TopologicalSpace V), DiscreteTopology V ∧ Continuous fun (p : G × V) => (ρ p.1) p.2

If every stabilizer is open, then there exists a (discrete) topology on V for which the action map G × V → V is continuous.

This is the “mathematically sound” packaging of continuous_action_discreteTopology_of_forall_isOpen_stabilizer: it does not assume a topology on V upfront.

def ContinuousRep.continuousRep_of_forall_isOpen_stabilizer_of_discreteTopology {R : Type u} [CommRing R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {V : Type w} [AddCommGroup V] [Module R V] [TopologicalSpace V] [DiscreteTopology V] (ρ₀ : Representation R G V) (hopen : ∀ (v : V), IsOpen ↑(ρ₀.stabilizer v)) : ContinuousRep R G V

If every stabilizer is open, then the same representation is a ContinuousRep once the representation space is given the discrete topology.

This packages continuous_action_discreteTopology_of_forall_isOpen_stabilizer using ContinuousRep.of.

Equations

• ContinuousRep.continuousRep_of_forall_isOpen_stabilizer_of_discreteTopology ρ₀ hopen = ContinuousRep.of ρ₀ ⋯