Restriction of discrete representations along a continuous homomorphism

A continuous monoid homomorphism φ : H →* G restricts a discrete G-module with continuous G-action to a discrete H-module with continuous H-action on the same underlying module: h acts by φ h. This file packages that restriction for TauCeti.DiscreteRep and, through the dictionary TauCeti.ofSmoothDiscrete, TauCeti.toSmoothDiscrete, for smooth discrete representations.

Restriction to a subgroup along its inclusion is the special case TauCeti.smoothDiscreteResFunctor, which is stated directly through TopRep.res.

Main definitions

• TauCeti.DiscreteRep.res: restriction of a discrete representation along φ.
• TauCeti.DiscreteRep.resFunctor: restriction along φ as a functor.
• TauCeti.smoothResFunctor: restriction along φ on smooth discrete representations.

def TauCeti.DiscreteRep.res {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] {H : Type v'} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (A : DiscreteRep R G) : DiscreteRep R H

Restriction of a discrete representation along a continuous monoid homomorphism φ: the same module, on which h acts by φ h.

@[simp]

theorem TauCeti.DiscreteRep.res_V {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] {H : Type v'} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (A : DiscreteRep R G) : (res φ hφ A).V = A.V

Restriction does not change the underlying module.

@[simp]

theorem TauCeti.DiscreteRep.res_ρ_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] {H : Type v'} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (A : DiscreteRep R G) (h : H) (x : A.V) : ((res φ hφ A).ρ h) x = (A.ρ (φ h)) x

The restricted action is the original action through φ.

def TauCeti.DiscreteRep.resFunctor {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] {H : Type v'} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) : CategoryTheory.Functor (DiscreteRep R G) (DiscreteRep R H)

Restriction along a continuous monoid homomorphism, as a functor of discrete representations. A morphism keeps its underlying linear map.

@[simp]

theorem TauCeti.DiscreteRep.resFunctor_obj {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] {H : Type v'} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (A : DiscreteRep R G) : (resFunctor φ hφ).obj A = res φ hφ A

The object map of resFunctor is res.

@[simp]

theorem TauCeti.DiscreteRep.resFunctor_map_toLinearMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] {H : Type v'} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) {A B : DiscreteRep R G} (f : A ⟶ B) : ((resFunctor φ hφ).map f).toLinearMap = f.toLinearMap

Restriction keeps the underlying linear map of a morphism.

def TauCeti.smoothResFunctor (R : Type u) [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v'} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) : CategoryTheory.Functor (SmoothDiscreteTopRep R G) (SmoothDiscreteTopRep R H)

Restriction along a continuous monoid homomorphism from a topological monoid to a topological group, on smooth discrete representations.

The functor passes through the equivalent category of discrete continuous representations. The body is exposed so that smoothResFunctor_map can be stated without transports between the functor's objects and the named restricted objects.

@[simp]

theorem TauCeti.smoothResFunctor_obj (R : Type u) [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v'} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) (A : SmoothDiscreteTopRep R G) : (smoothResFunctor R φ hφ).obj A = (toSmoothDiscrete R H).obj (DiscreteRep.res φ hφ ((ofSmoothDiscrete R G).obj A))

The object map of smooth restriction is discrete restriction of the coefficient module underlying the smooth representation.

@[simp]

theorem TauCeti.smoothResFunctor_map (R : Type u) [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v'} [Monoid H] [TopologicalSpace H] (φ : H →* G) (hφ : Continuous ⇑φ) {A B : SmoothDiscreteTopRep R G} (f : A ⟶ B) : (smoothResFunctor R φ hφ).map f = (toSmoothDiscrete R H).map ((DiscreteRep.resFunctor φ hφ).map ((ofSmoothDiscrete R G).map f))

The morphism map of smooth restriction applies discrete restriction to the underlying equivariant linear map, then returns through the smooth-discrete dictionary.