Tensor induction of smooth discrete representations

Tensor induction along an open finite-index subgroup acts on smooth discrete representations by passing through the equivalent category of discrete continuous representations, where the tensor power has the discrete topology and continuity of the induced action is available.

Main definitions

• TauCeti.smoothTensorInductionFunctor: tensor induction on smooth discrete coefficients.
• TauCeti.TopPairing.smoothTensorInduced: the tensor induction of a coefficient pairing, which applies it in every coset factor.

Main results

• TauCeti.smoothTensorInductionFunctor_map_hom_hom_apply: smooth tensor induction of a morphism acts factorwise.

References

• L. Evens, "A generalization of the transfer map in the cohomology of groups", Transactions of the American Mathematical Society 108 (1963), §§2–5.

noncomputable def TauCeti.smoothTensorInductionFunctor (R : Type u) [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] : CategoryTheory.Functor (SmoothDiscreteTopRep R ↥U) (SmoothDiscreteTopRep R G)

Tensor induction on smooth discrete representations along an open finite-index subgroup.

The functor passes through the equivalent category of discrete continuous representations, where the tensor power has the discrete topology and continuity of the induced action is available. The body is exposed so that the morphism formula smoothTensorInductionFunctor_map can be stated without transports between the functor's objects and the named tensor-induced objects.

@[simp]

theorem TauCeti.smoothTensorInductionFunctor_obj (R : Type u) [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] (A : SmoothDiscreteTopRep R ↥U) : (smoothTensorInductionFunctor R G U hU s).obj A = (toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))

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

@[simp]

theorem TauCeti.smoothTensorInductionFunctor_map (R : Type u) [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] {A B : SmoothDiscreteTopRep R ↥U} (f : A ⟶ B) : (smoothTensorInductionFunctor R G U hU s).map f = (toSmoothDiscrete R G).map ((DiscreteRep.tensorInductionFunctor U hU s).map ((ofSmoothDiscrete R ↥U).map f))

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

theorem TauCeti.smoothTensorInductionFunctor_map_hom_hom_apply (R : Type u) [CommRing R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] {A B : SmoothDiscreteTopRep R ↥U} (f : A ⟶ B) (x : PiTensorProduct R fun (x : G ⧸ U) => ↑A.obj) : (TopRep.Hom.hom ((smoothTensorInductionFunctor R G U hU s).map f).hom) x = (PiTensorProduct.map fun (x : G ⧸ U) => ↑(TopRep.Hom.hom f.hom).toContinuousLinearMap) x

Smooth tensor induction of a morphism applies its underlying linear map in every coset factor.

This is not a simp lemma: smoothTensorInductionFunctor_map rewrites its left-hand side.

noncomputable def TauCeti.TopPairing.smoothTensorInduced {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] {A B C : SmoothDiscreteTopRep R ↥U} (P : TopPairing A.obj B.obj C.obj) : TopPairing ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))).obj ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj B))).obj ((toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj C))).obj

The tensor induction of a coefficient pairing: applying a pairing of smooth discrete U-representations in every coset factor gives a coefficient pairing of their tensor inductions to G.

@[simp]

theorem TauCeti.TopPairing.smoothTensorInduced_bil {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] {A B C : SmoothDiscreteTopRep R ↥U} (P : TopPairing A.obj B.obj C.obj) : (smoothTensorInduced U hU s P).bil = PiTensorProduct.map₂ fun (x : G ⧸ U) => P.bil

The tensor induction of a coefficient pairing applies it in every coset factor.