Continuous representations

This file defines continuous representations of a monoid G on a R-module V and related basic results.

Main Results

• ContRepresentation R G V is the type of continuous representations of a monoid G on a R-module V which is a topological addgroup (where the action of G on V is not assumed to be continuous). The reason for this more general definition is that it allows us to define the coinduced representation of a continuous representation as also a continuous representation without any restriction on the topology on G.

• ContIntertwiningMap π₁ π₂ is the type of continuous intertwining maps between two continuous representations π₁ and π₂.

• ContRepresentation.coind₁ π is the coinduced continuous representation on the space of continuous functions from G to V for a continuous representation π.

Tags

continuous representation, algebra

@[reducible, inline]

abbrev ContRepresentation (R : Type u_1) (G : Type u_2) (V : Type u_3) [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] : Type (max u_2 u_3)

A continuous representation of a group G on a R-module V which is a topological addgroup is a homomorphism G →* V →L[R] V.

Equations

• ContRepresentation R G V = (G →* V →L[R] V)

@[reducible, inline]

abbrev ContRepresentation.toRepresentation (R : Type u_1) (G : Type u_2) (V : Type u_3) [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) : Representation R G V

Every continuous representation "is" a representation.

Equations

• ContRepresentation.toRepresentation R G V π = (↑ContinuousLinearMap.toLinearMapRingHom).comp π

structure ContIntertwiningMap {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] (π₁ : ContRepresentation R G V) (π₂ : ContRepresentation R G W) extends V →L[R] W : Type (max u_3 u_4)

A continuous intertwining map between two continuous representations is an intertwining map which is also continuous.

• toFun : V → W
• map_add' (x y : V) : (↑self.toContinuousLinearMap).toFun (x + y) = (↑self.toContinuousLinearMap).toFun x + (↑self.toContinuousLinearMap).toFun y
• map_smul' (m : R) (x : V) : (↑self.toContinuousLinearMap).toFun (m • x) = (RingHom.id R) m • (↑self.toContinuousLinearMap).toFun x
• cont : Continuous (↑self.toContinuousLinearMap).toFun
• isIntertwining' (g : G) : self.toContinuousLinearMap ∘SL π₁ g = π₂ g ∘SL self.toContinuousLinearMap

def ContRepresentation.«term_→ⁱL_» : Lean.TrailingParserDescr

notation for continuous intertwining maps

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev ContIntertwiningMap.toIntertwiningMap {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (f : ContIntertwiningMap π₁ π₂) : (ContRepresentation.toRepresentation R G V π₁).IntertwiningMap (ContRepresentation.toRepresentation R G W π₂)

Any continuous intertwining map is an intertwining map.

Equations

• f.toIntertwiningMap = { toLinearMap := ↑f.toContinuousLinearMap, isIntertwining' := ⋯ }

def ContIntertwiningMap.id {R : Type u_1} {G : Type u_2} {V : Type u_3} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {π₁ : ContRepresentation R G V} : ContIntertwiningMap π₁ π₁

The identity continuous intertwining map.

Equations

• ContIntertwiningMap.id = { toContinuousLinearMap := ContinuousLinearMap.id R V, isIntertwining' := ⋯ }

theorem ContIntertwiningMap.ext {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {f g : ContIntertwiningMap π₁ π₂} (h : f.toContinuousLinearMap = g.toContinuousLinearMap) : f = g

theorem ContIntertwiningMap.ext_iff {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {f g : ContIntertwiningMap π₁ π₂} : f = g ↔ f.toContinuousLinearMap = g.toContinuousLinearMap

theorem ContIntertwiningMap.toIntertwiningMap_injective {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} : Function.Injective fun (f : ContIntertwiningMap π₁ π₂) => f.toContinuousLinearMap

theorem ContIntertwiningMap.toFun_injective {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} : Function.Injective fun (f : ContIntertwiningMap π₁ π₂) => (↑f.toContinuousLinearMap).toFun

@[implicit_reducible]

instance ContIntertwiningMap.instFunLike {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} : FunLike (ContIntertwiningMap π₁ π₂) V W

Equations

• ContIntertwiningMap.instFunLike = { coe := fun (f : ContIntertwiningMap π₁ π₂) => (↑f.toContinuousLinearMap).toFun, coe_injective' := ⋯ }

theorem ContIntertwiningMap.isIntertwining {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (f : ContIntertwiningMap π₁ π₂) (g : G) (v : V) : f ((π₁ g) v) = (π₂ g) (f v)

instance ContIntertwiningMap.instContinuousLinearMapClass {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} : ContinuousLinearMapClass (ContIntertwiningMap π₁ π₂) R V W

def ContIntertwiningMap.comp {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] [AddCommGroup U] [Module R U] [TopologicalSpace U] [IsTopologicalAddGroup U] {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {π₃ : ContRepresentation R G U} (f : ContIntertwiningMap π₂ π₃) (g : ContIntertwiningMap π₁ π₂) : ContIntertwiningMap π₁ π₃

The composition of two continuous intertwining maps is a continuous intertwining map.

Equations

• f.comp g = { toContinuousLinearMap := f.toContinuousLinearMap ∘SL g.toContinuousLinearMap, isIntertwining' := ⋯ }

structure ContRepresentation.Equiv {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] (π₁ : ContRepresentation R G V) (π₂ : ContRepresentation R G W) extends V ≃L[R] W, ContIntertwiningMap π₁ π₂ : Type (max u_3 u_4)

The equivalence between continuous representations.

• mk'' :: (
• toFun : V → W
• map_add' (x y : V) : (↑↑self.toContinuousLinearEquiv).toFun (x + y) = (↑↑self.toContinuousLinearEquiv).toFun x + (↑↑self.toContinuousLinearEquiv).toFun y
• map_smul' (m : R) (x : V) : (↑↑self.toContinuousLinearEquiv).toFun (m • x) = (RingHom.id R) m • (↑↑self.toContinuousLinearEquiv).toFun x
• invFun : W → V
• left_inv : Function.LeftInverse (↑self.toContinuousLinearEquiv).invFun (↑↑self.toContinuousLinearEquiv).toFun
• right_inv : Function.RightInverse (↑self.toContinuousLinearEquiv).invFun (↑↑self.toContinuousLinearEquiv).toFun
• continuous_toFun : Continuous (↑↑self.toContinuousLinearEquiv).toFun
• continuous_invFun : Continuous (↑self.toContinuousLinearEquiv).invFun
• cont : Continuous (↑↑self.toContinuousLinearEquiv).toFun
• isIntertwining' (g : G) : { toLinearMap := ↑↑self.toContinuousLinearEquiv, cont := ⋯ } ∘SL π₁ g = π₂ g ∘SL { toLinearMap := ↑↑self.toContinuousLinearEquiv, cont := ⋯ }
• )

theorem ContRepresentation.Equiv.isIntertwining {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) (g : G) : ↑φ.toContinuousLinearEquiv ∘SL ρ g = σ g ∘SL ↑φ.toContinuousLinearEquiv

def ContRepresentation.Equiv.mk {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (e : V ≃L[R] W) (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e) : ρ.Equiv σ

An Equiv between representations could be built from a LinearEquiv and an assumption proving the G-equivariance.

Equations

• ContRepresentation.Equiv.mk e he = { toContinuousLinearEquiv := e, cont := ⋯, isIntertwining' := he }

theorem ContRepresentation.Equiv.toContinuousLinearEquiv_mk' {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {e : V ≃L[R] W} (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e) : (mk e he).toContinuousLinearEquiv = e

theorem ContRepresentation.Equiv.toContIntertwiningMap_mk' {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (e : V ≃L[R] W) (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e) : ↑(mk e he) = { toContinuousLinearMap := ↑e, isIntertwining' := he }

@[simp]

theorem ContRepresentation.Equiv.toContinuousLinearMap_mk' {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (e : V ≃L[R] W) (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e) : ↑(mk e he).toContinuousLinearEquiv = ↑e

theorem ContRepresentation.Equiv.toContinuousLinearEquiv_injective {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} : Function.Injective toContinuousLinearEquiv

theorem ContRepresentation.Equiv.toContinuousLinearEquiv_inj {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ ψ : σ.Equiv ρ) : φ.toContinuousLinearEquiv = ψ.toContinuousLinearEquiv ↔ φ = ψ

@[implicit_reducible]

instance ContRepresentation.Equiv.instEquivLike {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} : EquivLike (ρ.Equiv σ) V W

Equations

• One or more equations did not get rendered due to their size.

instance ContRepresentation.Equiv.instContinuousLinearEquivClass {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} : ContinuousLinearEquivClass (σ.Equiv ρ) R W V

@[simp]

theorem ContRepresentation.Equiv.mk_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {e : V ≃L[R] W} (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e) (v : V) : (mk e he) v = e v

theorem ContRepresentation.Equiv.ext {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {φ ψ : ρ.Equiv σ} (h : ⇑φ = ⇑ψ) : φ = ψ

theorem ContRepresentation.Equiv.ext_iff {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {φ ψ : ρ.Equiv σ} : φ = ψ ↔ ⇑φ = ⇑ψ

def ContRepresentation.Equiv.refl {R : Type u_1} {G : Type u_2} {V : Type u_3} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (ρ : ContRepresentation R G V) : ρ.Equiv ρ

Any continuous representation is equivalent to itself.

Equations

• ContRepresentation.Equiv.refl ρ = ContRepresentation.Equiv.mk (ContinuousLinearEquiv.refl R V) ⋯

@[simp]

theorem ContRepresentation.Equiv.toContIntertwiningMap_refl {R : Type u_1} {G : Type u_2} {V : Type u_3} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {ρ : ContRepresentation R G V} : ↑(refl ρ) = ContIntertwiningMap.id

@[simp]

theorem ContRepresentation.Equiv.toContinuousLinearMap_refl {R : Type u_1} {G : Type u_2} {V : Type u_3} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {ρ : ContRepresentation R G V} : ↑(refl ρ).toContinuousLinearEquiv = ContinuousLinearMap.id R V

@[simp]

theorem ContRepresentation.Equiv.refl_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {ρ : ContRepresentation R G V} (v : V) : (refl ρ) v = v

@[simp]

theorem ContRepresentation.Equiv.coe_toContIntertwiningMap {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) : ⇑↑φ = ⇑φ

theorem ContRepresentation.Equiv.coe_toContinuousLinearMap {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) : ⇑↑φ.toContinuousLinearEquiv = ⇑φ

theorem ContRepresentation.Equiv.coe_invFun {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) : (↑φ.toContinuousLinearEquiv).invFun = ⇑φ.symm

theorem ContRepresentation.Equiv.toContinuousLinearEquiv_toContinuousLinearMap {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) : ↑φ.toContinuousLinearEquiv = (↑φ).toContinuousLinearMap

theorem ContRepresentation.Equiv.toContinuousLinearEquiv_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) (v : V) : φ.toContinuousLinearEquiv v = ↑φ v

def ContRepresentation.Equiv.symm {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) : σ.Equiv ρ

The equiv between continuous representations are symmetric.

Equations

• φ.symm = ContRepresentation.Equiv.mk φ.symm ⋯

theorem ContinuousLinearEquiv.isIntertwining_symm_isIntertwining {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {e : V ≃L[R] W} (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e) (g : G) : ↑e.symm ∘SL σ g = ρ g ∘SL ↑e.symm

@[simp]

theorem ContRepresentation.Equiv.mk_symm {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {e : V ≃L[R] W} (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e) : (mk e he).symm = mk e.symm ⋯

theorem ContRepresentation.Equiv.toLinearMap_symm {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) : ↑↑φ.symm.toContinuousLinearEquiv = ↑(↑φ.toContinuousLinearEquiv).symm

theorem ContRepresentation.Equiv.coe_symm {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) : ⇑(↑φ.toContinuousLinearEquiv).symm = ⇑φ.symm

def ContRepresentation.Equiv.trans {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] [AddCommGroup U] [Module R U] [TopologicalSpace U] [IsTopologicalAddGroup U] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {τ : ContRepresentation R G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) : ρ.Equiv τ

Composition of two Equivs.

Equations

• φ.trans ψ = ContRepresentation.Equiv.mk (φ.trans ψ.toContinuousLinearEquiv) ⋯

@[simp]

theorem ContRepresentation.Equiv.toContIntertwiningMap_trans {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] [AddCommGroup U] [Module R U] [TopologicalSpace U] [IsTopologicalAddGroup U] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {τ : ContRepresentation R G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) : ↑(φ.trans ψ) = (↑ψ).comp ↑φ

@[simp]

theorem ContRepresentation.Equiv.toContinuousLinearMap_trans {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] [AddCommGroup U] [Module R U] [TopologicalSpace U] [IsTopologicalAddGroup U] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {τ : ContRepresentation R G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) : ↑(φ.trans ψ).toContinuousLinearEquiv = ↑ψ.toContinuousLinearEquiv ∘SL ↑φ.toContinuousLinearEquiv

@[simp]

theorem ContRepresentation.Equiv.trans_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] [AddCommGroup U] [Module R U] [TopologicalSpace U] [IsTopologicalAddGroup U] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {τ : ContRepresentation R G U} (φ : ρ.Equiv σ) (ψ : σ.Equiv τ) (v : V) : (φ.trans ψ) v = ψ (φ v)

@[simp]

theorem ContRepresentation.Equiv.apply_symm_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) (v : W) : φ (φ.symm v) = v

@[simp]

theorem ContRepresentation.Equiv.symm_apply_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) (v : V) : φ.symm (φ v) = v

@[simp]

theorem ContRepresentation.Equiv.trans_symm {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) : φ.trans φ.symm = refl ρ

@[simp]

theorem ContRepresentation.Equiv.symm_trans {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (φ : ρ.Equiv σ) : φ.symm.trans φ = refl σ

def ContRepresentation.trivial (R : Type u_1) (G : Type u_2) (V : Type u_3) [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] : ContRepresentation R G V

The trivial continuous representation of a group G on a R-module V.

Equations

• ContRepresentation.trivial R G V = 1

@[simp]

theorem ContRepresentation.trivial_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (g : G) (v : V) : ((trivial R G V) g) v = v

def ContRepresentation.restrict {R : Type u_1} {G : Type u_2} {V : Type u_3} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {H : Type u_6} [Monoid H] (π : ContRepresentation R G V) (φ : H →* G) : ContRepresentation R H V

The restriction of a continuous representation along a monoid homomorphism.

Equations

• π.restrict φ = MonoidHom.comp π φ

@[simp]

theorem ContRepresentation.restrict_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Monoid G] [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {H : Type u_6} [Monoid H] (π : ContRepresentation R G V) (φ : H →* G) (x : H) : (π.restrict φ) x = π (φ x)

def ContRepresentation.coindV {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} {H : Type u_7} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [Group H] [TopologicalSpace H] (φ : G →ₜ* H) (π : ContRepresentation R G V) : Submodule R C(H, V)

The underlying module of the coinduced continuous representation.

Equations

• ContRepresentation.coindV φ π = { carrier := {f : C(H, V) | ∀ (g : G) (h : H), f (φ g * h) = (π g) (f h)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem ContRepresentation.coe_coindV {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} {H : Type u_7} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [Group H] [TopologicalSpace H] (φ : G →ₜ* H) (π : ContRepresentation R G V) : ↑(coindV φ π) = {f : C(H, V) | ∀ (g : G) (h : H), f (φ g * h) = (π g) (f h)}

@[simp]

theorem ContRepresentation.mem_coindV {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} {H : Type u_7} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [Group H] [TopologicalSpace H] (φ : G →ₜ* H) (π : ContRepresentation R G V) (f : C(H, V)) : f ∈ coindV φ π ↔ ∀ (g : G) (h : H), f (φ g * h) = (π g) (f h)

instance ContRepresentation.instContinuousSMulSubtypeContinuousMapMemSubmoduleCoindV {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} {H : Type u_7} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [Group H] [TopologicalSpace H] (φ : G →ₜ* H) (π : ContRepresentation R G V) : ContinuousSMul R ↥(coindV φ π)

def ContRepresentation.coind {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} {H : Type u_7} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [Group H] [TopologicalSpace H] (φ : G →ₜ* H) [IsTopologicalGroup H] (π : ContRepresentation R G V) : ContRepresentation R H ↥(coindV φ π)

The coinduced continuous representation where the action of H is defined by h ↦ f ↦ f ∘ (· * h).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContRepresentation.coind_apply_apply_coe {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} {H : Type u_7} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [Group H] [TopologicalSpace H] (φ : G →ₜ* H) [IsTopologicalGroup H] (π : ContRepresentation R G V) (h : H) (x✝ : ↥(coindV φ π)) : ↑(((coind φ π) h) x✝) = (↑x✝).comp (ContinuousMap.mulRight h)

def ContRepresentation.coind₁ {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [IsTopologicalGroup G] (π : ContRepresentation R G V) : ContRepresentation R G C(G, V)

Given a continuous representation π of G on V, this defines a Continuous representation π.coind₁ of G on the function space C(G,V). The action of an element g : G is defined by f ↦ (x ↦ π g (f (g⁻¹ * x))). This new representation of G is isomorphic to the continuous coinduction of the trivial representation of the trivial subgroup of G, but the action has been twisted so that the map const : V → C(G,V) is an intertwining map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContRepresentation.coind₁_apply_apply {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [IsTopologicalGroup G] (π : ContRepresentation R G V) (g : G) (f : C(G, V)) : (π.coind₁ g) f = (↑(π g)).comp (f.comp (ContinuousMap.mulLeft g⁻¹))

def ContRepresentation.coind₁_map {R : Type u_1} {V : Type u_3} {W : Type u_4} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {G : Type u_6} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [ContinuousSMul R W] [IsTopologicalGroup G] (π₁ : ContRepresentation R G V) (π₂ : ContRepresentation R G W) (f : ContIntertwiningMap π₁ π₂) : ContIntertwiningMap π₁.coind₁ π₂.coind₁

The functoriality of coind₁.

Equations

• π₁.coind₁_map π₂ f = { toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯, isIntertwining' := ⋯ }

@[simp]

theorem ContRepresentation.coind₁_map_toFun {R : Type u_1} {V : Type u_3} {W : Type u_4} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W] {G : Type u_6} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [ContinuousSMul R W] [IsTopologicalGroup G] (π₁ : ContRepresentation R G V) (π₂ : ContRepresentation R G W) (f : ContIntertwiningMap π₁ π₂) (g : C(G, V)) : (π₁.coind₁_map π₂ f) g = (↑f).comp g

def ContRepresentation.coind₁_ι {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [IsTopologicalGroup G] (π : ContRepresentation R G V) : ContIntertwiningMap π π.coind₁

The naturality of the transformation from 𝟭 ⟶ coind₁.

Equations

• π.coind₁_ι = { toFun := ContinuousMap.const G, map_add' := ⋯, map_smul' := ⋯, cont := ⋯, isIntertwining' := ⋯ }

@[simp]

theorem ContRepresentation.coind₁_ι_toFun {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [IsTopologicalGroup G] (π : ContRepresentation R G V) (b : V) : π.coind₁_ι b = ContinuousMap.const G b

def ContRepresentation.coind₁Equivcoind {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_6} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [IsTopologicalGroup G] : (trivial R (↥⊥) V).coind₁.Equiv (coind 1 (trivial R G V))

The equivalence between coind₁ and coind of the trivial representation of trivial subgroup of G.

Equations

• One or more equations did not get rendered due to their size.