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 π.

• ContIntertwiningMap.mapInvariantsOfRes φ f is the continuous linear map π.invariants →L[R] π'.invariants induced by a monoid homomorphism φ : H →* G and a continuous intertwining map f : π.restrict φ →ⁱL π'.

• ContRepresentation.coind₁ResMap φ f is the continuous intertwining map π.coind₁.restrict φ →ⁱL π'.coind₁ induced by a continuous group homomorphism φ : H →ₜ* G and a continuous intertwining map f : π.restrict φ →ⁱL π', given by F ↦ f ∘ F ∘ φ.

Tags

continuous representation, algebra

structure 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.

• ofMonoidHom :: (
• toMonoidHom : G →* V →L[R] V

  The underlying monoid homomorphism of a continuous representation.

• )

@[implicit_reducible]

instance instFunLikeContRepresentationContinuousLinearMapId (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] : FunLike (ContRepresentation R G V) G (V →L[R] V)

Equations

• instFunLikeContRepresentationContinuousLinearMapId R G V = { coe := fun (π : ContRepresentation R G V) => ⇑π.toMonoidHom, coe_injective := ⋯ }

instance instMonoidHomClassContRepresentationContinuousLinearMapId (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] : MonoidHomClass (ContRepresentation R G V) G (V →L[R] V)

theorem ContRepresentation.toMonoidHom_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) (g : G) : π.toMonoidHom g = π g

@[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 π.toMonoidHom

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' := ⋯ }

@[simp]

theorem ContIntertwiningMap.toContinuousLinearMap_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} : id.toContinuousLinearMap = ContinuousLinearMap.id R V

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.toContinuousLinearMap_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.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.toIntertwiningMap

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.id_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) : id v = v

theorem ContIntertwiningMap.toContinuousLinearMap_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} (f : ContIntertwiningMap π₁ π₂) (v : V) : f.toContinuousLinearMap v = f v

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' := ⋯ }

@[simp]

theorem ContIntertwiningMap.toContinuousLinearMap_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 π₁ π₂) : (f.comp g).toContinuousLinearMap = f.toContinuousLinearMap ∘SL g.toContinuousLinearMap

@[implicit_reducible]

instance ContIntertwiningMap.instAdd {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} : Add (ContIntertwiningMap π₁ π₂)

Equations

• ContIntertwiningMap.instAdd = { add := fun (f g : ContIntertwiningMap π₁ π₂) => { toContinuousLinearMap := f.toContinuousLinearMap + g.toContinuousLinearMap, isIntertwining' := ⋯ } }

@[simp]

theorem ContIntertwiningMap.toContinuousLinearMap_add {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).toContinuousLinearMap = f.toContinuousLinearMap + g.toContinuousLinearMap

theorem ContIntertwiningMap.add_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} (f g : ContIntertwiningMap π₁ π₂) (v : V) : (f + g) v = f v + g v

theorem ContIntertwiningMap.comp_add {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 h : ContIntertwiningMap π₁ π₂) : f.comp (g + h) = f.comp g + f.comp h

theorem ContIntertwiningMap.add_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 g : ContIntertwiningMap π₂ π₃) (h : ContIntertwiningMap π₁ π₂) : (f + g).comp h = f.comp h + g.comp h

@[implicit_reducible]

instance ContIntertwiningMap.instOne {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} : One (ContIntertwiningMap π₁ π₁)

Equations

• ContIntertwiningMap.instOne = { one := ContIntertwiningMap.id }

theorem ContIntertwiningMap.one_def {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} : 1 = id

@[simp]

theorem ContIntertwiningMap.toContinuousLinearMap_one {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} : toContinuousLinearMap 1 = 1

theorem ContIntertwiningMap.one_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) : 1 v = v

@[implicit_reducible]

instance ContIntertwiningMap.instZero {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} : Zero (ContIntertwiningMap π₁ π₂)

Equations

• ContIntertwiningMap.instZero = { zero := { toContinuousLinearMap := 0, isIntertwining' := ⋯ } }

@[simp]

theorem ContIntertwiningMap.toContinuousLinearMap_zero {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} : toContinuousLinearMap 0 = 0

theorem ContIntertwiningMap.zero_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} (v : V) : 0 v = 0

@[implicit_reducible]

instance ContIntertwiningMap.instAddZeroClass {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} : AddZeroClass (ContIntertwiningMap π₁ π₂)

Equations

• ContIntertwiningMap.instAddZeroClass = { toZero := ContIntertwiningMap.instZero, toAdd := ContIntertwiningMap.instAdd, zero_add := ⋯, add_zero := ⋯ }

@[implicit_reducible]

instance ContIntertwiningMap.instAddCommSemigroup {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} : AddCommSemigroup (ContIntertwiningMap π₁ π₂)

Equations

• ContIntertwiningMap.instAddCommSemigroup = { toAdd := ContIntertwiningMap.instAdd, add_assoc := ⋯, add_comm := ⋯ }

@[implicit_reducible]

instance ContIntertwiningMap.instNeg {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} : Neg (ContIntertwiningMap π₁ π₂)

Equations

• ContIntertwiningMap.instNeg = { neg := fun (f : ContIntertwiningMap π₁ π₂) => { toContinuousLinearMap := -f.toContinuousLinearMap, isIntertwining' := ⋯ } }

@[simp]

theorem ContIntertwiningMap.toContinuousLinearMap_neg {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 π₁ π₂) : (-f).toContinuousLinearMap = -f.toContinuousLinearMap

theorem ContIntertwiningMap.neg_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} (f : ContIntertwiningMap π₁ π₂) (v : V) : (-f) v = -f v

@[implicit_reducible]

instance ContIntertwiningMap.instSub {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} : Sub (ContIntertwiningMap π₁ π₂)

Equations

• ContIntertwiningMap.instSub = { sub := fun (f g : ContIntertwiningMap π₁ π₂) => { toContinuousLinearMap := f.toContinuousLinearMap - g.toContinuousLinearMap, isIntertwining' := ⋯ } }

@[simp]

theorem ContIntertwiningMap.toContinuousLinearMap_sub {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).toContinuousLinearMap = f.toContinuousLinearMap - g.toContinuousLinearMap

theorem ContIntertwiningMap.sub_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} (f g : ContIntertwiningMap π₁ π₂) (v : V) : (f - g) v = f v - g v

theorem ContIntertwiningMap.sub_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 g : ContIntertwiningMap π₂ π₃) (h : ContIntertwiningMap π₁ π₂) : (f - g).comp h = f.comp h - g.comp h

theorem ContIntertwiningMap.comp_sub {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 h : ContIntertwiningMap π₁ π₂) : f.comp (g - h) = f.comp g - f.comp h

@[implicit_reducible]

instance ContIntertwiningMap.instSMul {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} {S : Type u_6} [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [LinearMap.CompatibleSMul W W S R] : SMul S (ContIntertwiningMap π₁ π₂)

Equations

• ContIntertwiningMap.instSMul = { smul := fun (s : S) (f : ContIntertwiningMap π₁ π₂) => { toContinuousLinearMap := s • f.toContinuousLinearMap, isIntertwining' := ⋯ } }

@[simp]

theorem ContIntertwiningMap.toContinuousLinearMap_smul {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} {S : Type u_6} [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [LinearMap.CompatibleSMul W W S R] (s : S) (f : ContIntertwiningMap π₁ π₂) : (s • f).toContinuousLinearMap = s • f.toContinuousLinearMap

theorem ContIntertwiningMap.smul_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} {S : Type u_6} [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [LinearMap.CompatibleSMul W W S R] (s : S) (f : ContIntertwiningMap π₁ π₂) (v : V) : (s • f) v = s • f v

theorem ContIntertwiningMap.smul_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} {S : Type u_7} [Monoid S] [DistribMulAction S U] [SMulCommClass R S U] [ContinuousConstSMul S U] [LinearMap.CompatibleSMul U U S R] (s : S) (f : ContIntertwiningMap π₂ π₃) (g : ContIntertwiningMap π₁ π₂) : (s • f).comp g = s • f.comp g

theorem ContIntertwiningMap.comp_smul {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} {S : Type u_7} [Monoid S] [DistribMulAction S U] [SMulCommClass R S U] [ContinuousConstSMul S U] [LinearMap.CompatibleSMul U U S R] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [LinearMap.CompatibleSMul W W S R] [LinearMap.CompatibleSMul W U S R] (s : S) (f : ContIntertwiningMap π₂ π₃) (g : ContIntertwiningMap π₁ π₂) : f.comp (s • g) = s • f.comp g

@[implicit_reducible]

instance ContIntertwiningMap.instAddCommGroup {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} : AddCommGroup (ContIntertwiningMap π₁ π₂)

Equations

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

@[implicit_reducible]

instance ContIntertwiningMap.instDistribMulAction {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} {S : Type u_6} [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [LinearMap.CompatibleSMul W W S R] : DistribMulAction S (ContIntertwiningMap π₁ π₂)

Equations

• ContIntertwiningMap.instDistribMulAction = { toSMul := ContIntertwiningMap.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

instance ContIntertwiningMap.instModule {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} {S : Type u_7} [Ring S] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] [LinearMap.CompatibleSMul W W S R] : Module S (ContIntertwiningMap π₁ π₂)

Equations

• ContIntertwiningMap.instModule = { toDistribMulAction := ContIntertwiningMap.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

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 = { toMonoidHom := 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

@[implicit_reducible]

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 φ = { toMonoidHom := π.toMonoidHom.comp φ }

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) (h : H) : (π.restrict φ) h = π (φ h)

@[simp]

theorem ContRepresentation.restrict_apply_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) (h : H) (v : V) : ((π.restrict φ) h) v = (π (φ h)) v

def ContIntertwiningMap.restrict {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] {H : Type u_6} [Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R G W} (φ : H →* G) (f : ContIntertwiningMap π π') : ContIntertwiningMap (π.restrict φ) (π'.restrict φ)

The restriction of a continuous intertwining map along a monoid homomorphism.

Equations

• ContIntertwiningMap.restrict φ f = { toContinuousLinearMap := f.toContinuousLinearMap, isIntertwining' := ⋯ }

theorem ContIntertwiningMap.restrict_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] {H : Type u_6} [Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R G W} (φ : H →* G) (f : ContIntertwiningMap π π') : (restrict φ f).toContinuousLinearMap = f.toContinuousLinearMap

@[simp]

theorem ContIntertwiningMap.restrict_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] {H : Type u_6} [Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R G W} (φ : H →* G) (f : ContIntertwiningMap π π') (v : V) : (restrict φ f) v = f v

theorem ContIntertwiningMap.restrict_sub {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] {H : Type u_6} [Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R G W} (φ : H →* G) (f g : ContIntertwiningMap π π') : restrict φ (f - g) = restrict φ f - restrict φ g

def ContRepresentation.invariants {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) : Submodule R V

The submodule of G-invariant elements of a continuous representation.

Equations

• π.invariants = { carrier := {v : V | ∀ (g : G), (π g) v = v}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem ContRepresentation.mem_invariants {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) : v ∈ π.invariants ↔ ∀ (g : G), (π g) v = v

def ContIntertwiningMap.mapInvariants {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 π π') : ↥π.invariants →L[R] ↥π'.invariants

The map induced on G-invariant elements by a continuous intertwining map.

Equations

• f.mapInvariants = f.restrict ⋯

theorem ContIntertwiningMap.mapInvariants_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} (f : ContIntertwiningMap π π') (v : ↥π.invariants) : ↑(f.mapInvariants v) = f ↑v

@[simp]

theorem ContIntertwiningMap.mk_mapInvariants_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} (f : ContIntertwiningMap π π') (v : V) (hv : v ∈ π.invariants) : ↑(f.mapInvariants ⟨v, hv⟩) = f v

theorem ContRepresentation.invariants_le_invariants_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) : π.invariants ≤ (π.restrict φ).invariants

def ContIntertwiningMap.mapInvariantsOfRes {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] {H : Type u_6} [Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R H W} (φ : H →* G) (f : ContIntertwiningMap (π.restrict φ) π') : ↥π.invariants →L[R] ↥π'.invariants

Given a monoid homomorphism φ : H →* G, a G-representation π and an H-representation π', a continuous intertwining map f : π.restrict φ →ⁱL π' induces a continuous linear map π.invariants →L[R] π'.invariants between the invariant submodules.

Equations

• ContIntertwiningMap.mapInvariantsOfRes φ f = f.restrict ⋯

theorem ContIntertwiningMap.mapInvariantsOfRes_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] {H : Type u_6} [Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R H W} (φ : H →* G) (f : ContIntertwiningMap (π.restrict φ) π') (v : ↥π.invariants) : ↑((mapInvariantsOfRes φ f) v) = f ↑v

@[simp]

theorem ContIntertwiningMap.mk_mapInvariantsOfRes_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] {H : Type u_6} [Monoid H] {π : ContRepresentation R G V} {π' : ContRepresentation R H W} (φ : H →* G) (f : ContIntertwiningMap (π.restrict φ) π') (v : V) (hv : v ∈ π.invariants) : ↑((mapInvariantsOfRes φ f) ⟨v, hv⟩) = f v

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_7} {H : Type u_8} [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_7} {H : Type u_8} [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_7} {H : Type u_8} [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_7} {H : Type u_8} [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_7} {H : Type u_8} [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_toMonoidHom_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_7} {H : Type u_8} [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 φ π).toMonoidHom 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_7} [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_7} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [IsTopologicalGroup G] (π : ContRepresentation R G V) (g : G) (f : C(G, V)) (x : G) : ((π.coind₁ g) f) x = (π g) (f (g⁻¹ * x))

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_7} [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

• ContRepresentation.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_7} [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_7} [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_7} [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_7} [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.

def ContRepresentation.coind₁Res {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_7} {H : Type u_8} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [Group H] [TopologicalSpace H] [IsTopologicalGroup G] [IsTopologicalGroup H] (φ : H →ₜ* G) (π : ContRepresentation R G V) : ContIntertwiningMap (π.coind₁.restrict ↑φ) (π.restrict ↑φ).coind₁

Given a continuous group homomorphism φ : H →ₜ* G, precomposition with φ defines a continuous intertwining map π.coind₁.restrict φ →ⁱL (π.restrict φ).coind₁.

Equations

• ContRepresentation.coind₁Res φ π = { toContinuousLinearMap := ContinuousMap.compCLM R V φ.toContinuousMap, isIntertwining' := ⋯ }

@[simp]

theorem ContRepresentation.coind₁Res_apply {R : Type u_1} {V : Type u_3} [Ring R] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {G : Type u_7} {H : Type u_8} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [Group H] [TopologicalSpace H] [IsTopologicalGroup G] [IsTopologicalGroup H] (φ : H →ₜ* G) (π : ContRepresentation R G V) (F : C(G, V)) (x : H) : ((coind₁Res φ π) F) x = F (φ x)

def ContRepresentation.coind₁ResMap {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_7} {H : Type u_8} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [ContinuousSMul R W] [Group H] [TopologicalSpace H] {π : ContRepresentation R G V} [IsTopologicalGroup G] [IsTopologicalGroup H] {π' : ContRepresentation R H W} (φ : H →ₜ* G) (f : ContIntertwiningMap (π.restrict ↑φ) π') : ContIntertwiningMap (π.coind₁.restrict ↑φ) π'.coind₁

Given a continuous group homomorphism φ : H →ₜ* G, a continuous intertwining map f : π.restrict φ →ⁱL π' induces a continuous intertwining map π.coind₁.restrict φ →ⁱL π'.coind₁, sending F : C(G, V) to f ∘ F ∘ φ : C(H, W).

Equations

• ContRepresentation.coind₁ResMap φ f = (ContRepresentation.coind₁Map f).comp (ContRepresentation.coind₁Res φ π)

@[simp]

theorem ContRepresentation.coind₁ResMap_apply {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_7} {H : Type u_8} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [ContinuousSMul R W] [Group H] [TopologicalSpace H] {π : ContRepresentation R G V} [IsTopologicalGroup G] [IsTopologicalGroup H] {π' : ContRepresentation R H W} (φ : H →ₜ* G) (f : ContIntertwiningMap (π.restrict ↑φ) π') (F : C(G, V)) (x : H) : ((coind₁ResMap φ f) F) x = f (F (φ x))

theorem ContRepresentation.coind₁ResMap_comp_coind₁ι_restrict {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_7} {H : Type u_8} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [ContinuousSMul R W] [Group H] [TopologicalSpace H] {π : ContRepresentation R G V} [IsTopologicalGroup G] [IsTopologicalGroup H] {π' : ContRepresentation R H W} (φ : H →ₜ* G) (f : ContIntertwiningMap (π.restrict ↑φ) π') : (coind₁ResMap φ f).comp (ContIntertwiningMap.restrict (↑φ) π.coind₁ι) = π'.coind₁ι.comp f

The naturality of coind₁ι with respect to coind₁ResMap.

theorem ContRepresentation.coind₁Map_comp_coind₁ResMap {R : Type u_1} {V : Type u_3} {W : Type u_4} {U : Type u_5} [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] {G : Type u_7} {H : Type u_8} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [ContinuousSMul R W] [Group H] [TopologicalSpace H] {π : ContRepresentation R G V} [IsTopologicalGroup G] [IsTopologicalGroup H] [ContinuousSMul R U] {π' : ContRepresentation R H W} (φ : H →ₜ* G) {σ : ContRepresentation R H U} (f : ContIntertwiningMap (π.restrict ↑φ) π') (g : ContIntertwiningMap π' σ) : (coind₁Map g).comp (coind₁ResMap φ f) = coind₁ResMap φ (g.comp f)

theorem ContRepresentation.coind₁ResMap_comp_coind₁Map_restrict {R : Type u_1} {V : Type u_3} {W : Type u_4} {U : Type u_5} [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] {G : Type u_7} {H : Type u_8} [Group G] [TopologicalSpace G] [TopologicalSpace R] [ContinuousSMul R V] [ContinuousSMul R W] [Group H] [TopologicalSpace H] {π : ContRepresentation R G V} [IsTopologicalGroup G] [IsTopologicalGroup H] [ContinuousSMul R U] {π' : ContRepresentation R H W} (φ : H →ₜ* G) {ρ : ContRepresentation R G U} (g : ContIntertwiningMap ρ π) (f : ContIntertwiningMap (π.restrict ↑φ) π') : (coind₁ResMap φ f).comp (ContIntertwiningMap.restrict (↑φ) (coind₁Map g)) = coind₁ResMap φ (f.comp (ContIntertwiningMap.restrict (↑φ) g))