Tensor induction of discrete continuous representations

For an open finite-index subgroup U ≤ G, tensor induction of a discrete continuous U-module is again a discrete continuous G-module. The tensor power is given the discrete topology, not a topology inferred from an algebraic tensor product. Continuity follows because a pure tensor involves finitely many continuous coordinate actions; sums of pure tensors then exhaust the tensor power.

TauCeti.DiscreteRep.tensorInductionFunctor is the continuous-coefficient version of Subgroup.tensorInductionFunctor. Composing it with TauCeti.toSmoothDiscrete supplies coefficients for Mathlib's continuous cohomology. In particular this makes the tensor induction used in the general Evens norm available on discrete coefficients, rather than only in Rep. The scalar ring is discrete; this includes both ℤ and ZMod 2. No compactness of G is needed: openness and finite index are separate hypotheses.

References

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

theorem Representation.continuous_wreathTensor_apply {R : Type u} {D : Type v} {M : Type w} {ι : Type x} [CommSemiring R] [Group D] [TopologicalSpace D] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [Finite ι] [TopologicalSpace ι] [DiscreteTopology ι] [TopologicalSpace (PiTensorProduct R fun (x : ι) => M)] [DiscreteTopology (PiTensorProduct R fun (x : ι) => M)] (ρ : Representation R D M) (hρ : Continuous fun (p : D × M) => (ρ p.1) p.2) (z : PiTensorProduct R fun (x : ι) => M) : Continuous fun (a : TauCeti.WreathProduct D ι) => ((ρ.wreathTensor ι) a) z

A wreath tensor representation has continuous orbit maps on its discrete tensor power if its base representation has a continuous action and there are finitely many tensor factors.

noncomputable def TauCeti.DiscreteRep.tensorInduced {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] (A : DiscreteRep R ↥U) : DiscreteRep R G

Tensor induction on discrete continuous modules. The underlying tensor power has the discrete topology and the action is the existing algebraic tensor-induced representation.

The body is exposed so that the carrier and its module and action instances can be used in formulas on pure tensors.

@[simp]

theorem TauCeti.DiscreteRep.tensorInduced_V {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] (A : DiscreteRep R ↥U) : (tensorInduced U hU s A).V = PiTensorProduct R fun (x : G ⧸ U) => A.V

The underlying module of discrete tensor induction is the tensor power over the cosets.

theorem TauCeti.DiscreteRep.tensorInduced_ρ_apply {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] (A : DiscreteRep R ↥U) (g : G) (z : PiTensorProduct R fun (x : G ⧸ U) => A.V) : ((tensorInduced U hU s A).ρ g) z = ((U.tensorInducedRepresentation s A.ρ) g) z

Discrete tensor induction uses the algebraic tensor-induced action.

@[simp]

theorem TauCeti.DiscreteRep.tensorInduced_ρ_apply_tprod {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] (A : DiscreteRep R ↥U) (g : G) (m : G ⧸ U → A.V) : ((tensorInduced U hU s A).ρ g) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (i : G ⧸ U) => ((U.monomialHom s) g).left i • m (g⁻¹ • i)

On a pure tensor, the coordinate at a coset is acted on by its transversal word and the coordinates are translated by g⁻¹.

noncomputable def TauCeti.DiscreteRep.tensorInductionFunctor {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] : CategoryTheory.Functor (DiscreteRep R ↥U) (DiscreteRep R G)

Tensor induction for discrete continuous representations along an open finite-index subgroup. Composing with toSmoothDiscrete gives smooth discrete coefficients for continuous cohomology. The object map is exposed so the morphism formula can be stated without transports between the opaque functor's objects and the named tensor-induced objects.

@[simp]

theorem TauCeti.DiscreteRep.tensorInductionFunctor_obj {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] (A : DiscreteRep R ↥U) : (tensorInductionFunctor U hU s).obj A = tensorInduced U hU s A

The tensor induction functor has the named tensor-induced object map.

@[simp]

theorem TauCeti.DiscreteRep.tensorInductionFunctor_map {R : Type u} [CommRing R] [TopologicalSpace R] [DiscreteTopology R] {G : Type v} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) (hU : IsOpen ↑U) (s : U.LeftTransversal) [U.FiniteIndex] {A B : DiscreteRep R ↥U} (f : A ⟶ B) : (tensorInductionFunctor U hU s).map f = Representation.IntertwiningMap.tensorInduced f s

The tensor induction functor has the factorwise tensor-induced morphism map.