Change of transversal for discrete tensor induction

Tensor induction of a discrete continuous representation is independent of the chosen left transversal. This file lifts the algebraic comparison Subgroup.tensorInducedChangeTransversal to the categories of discrete and smooth discrete representations. The comparisons are natural in the coefficient representation.

For trivial 𝔽₂ coefficients, the comparison commutes with the canonical identification of the tensor-induced coefficient object with the ambient trivial coefficient object. Consequently, changing the transversal does not change the coefficient identification used by the cochain-level Evens norm.

Main definitions

• TauCeti.DiscreteRep.tensorInducedChangeTransversalIso: the comparison on discrete continuous representations.
• TauCeti.DiscreteRep.tensorInductionChangeTransversalNatIso: the comparison as a natural isomorphism of tensor-induction functors.
• TauCeti.smoothTensorInducedChangeTransversalIso: the comparison on smooth discrete representations.
• TauCeti.smoothTensorInductionChangeTransversalNatIso: its functorial form.
• TauCeti.smoothTensorInducedTrivialF2Iso_changeTransversal_hom: compatibility with the canonical trivial-𝔽₂ coefficient identification.

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.DiscreteRep.tensorInducedChangeTransversalIso {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 t : U.LeftTransversal) [U.FiniteIndex] (A : DiscreteRep R ↥U) : tensorInduced U hU t A ≅ tensorInduced U hU s A

Changing the transversal gives an isomorphism between the corresponding tensor-induced discrete continuous representations.

theorem TauCeti.DiscreteRep.tensorInducedChangeTransversalIso_hom_toLinearMap {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 t : U.LeftTransversal) [U.FiniteIndex] (A : DiscreteRep R ↥U) : (tensorInducedChangeTransversalIso U hU s t A).hom.toLinearMap = ↑(U.tensorInducedChangeTransversal s t A.ρ).toLinearEquiv

The forward map of the discrete comparison is the algebraic change-of-transversal map.

@[simp]

theorem TauCeti.DiscreteRep.tensorInducedChangeTransversalIso_hom_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 t : U.LeftTransversal) [U.FiniteIndex] (A : DiscreteRep R ↥U) (m : G ⧸ U → A.V) : (tensorInducedChangeTransversalIso U hU s t A).hom.toLinearMap ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (x : G ⧸ U) => (A.ρ ((U.monomialChangeTransversal s t).left x)) (m x)

On a pure tensor, the discrete comparison applies the difference of the two transversal representatives in every coset coordinate.

theorem TauCeti.DiscreteRep.tensorInducedChangeTransversalIso_hom_naturality {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 t : U.LeftTransversal) [U.FiniteIndex] {A B : DiscreteRep R ↥U} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp ((tensorInductionFunctor U hU t).map f) (tensorInducedChangeTransversalIso U hU s t B).hom = CategoryTheory.CategoryStruct.comp (tensorInducedChangeTransversalIso U hU s t A).hom ((tensorInductionFunctor U hU s).map f)

The discrete change-of-transversal comparison is natural in the coefficient representation.

theorem TauCeti.DiscreteRep.tensorInducedChangeTransversalIso_hom_naturality_assoc {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 t : U.LeftTransversal) [U.FiniteIndex] {A B : DiscreteRep R ↥U} (f : A ⟶ B) {Z : DiscreteRep R G} (h : tensorInduced U hU s B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((tensorInductionFunctor U hU t).map f) (tensorInducedChangeTransversalIso U hU s t B).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (tensorInducedChangeTransversalIso U hU s t A).hom ((tensorInductionFunctor U hU s).map f)) h

The discrete change-of-transversal comparison is natural in the coefficient representation.

noncomputable def TauCeti.DiscreteRep.tensorInductionChangeTransversalNatIso {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 t : U.LeftTransversal) [U.FiniteIndex] : tensorInductionFunctor U hU t ≅ tensorInductionFunctor U hU s

Tensor induction on discrete continuous representations is naturally independent of the chosen transversal.

@[simp]

theorem TauCeti.DiscreteRep.tensorInductionChangeTransversalNatIso_app {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 t : U.LeftTransversal) [U.FiniteIndex] (A : DiscreteRep R ↥U) : (tensorInductionChangeTransversalNatIso U hU s t).app A = tensorInducedChangeTransversalIso U hU s t A

The component of the natural change-of-transversal isomorphism is the named discrete comparison.

noncomputable def TauCeti.smoothTensorInducedChangeTransversalIso {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 t : U.LeftTransversal) [U.FiniteIndex] (A : SmoothDiscreteTopRep R ↥U) : (toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU t ((ofSmoothDiscrete R ↥U).obj A)) ≅ (toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj A))

Changing the transversal gives an isomorphism between the corresponding smooth tensor-induced representations.

The objects are written in the simp-normal form produced by smoothTensorInductionFunctor_obj, so that the pure-tensor computation rules below can be simp lemmas.

@[simp]

theorem TauCeti.smoothTensorInducedChangeTransversalIso_hom_apply_tprod {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 t : U.LeftTransversal) [U.FiniteIndex] (A : SmoothDiscreteTopRep R ↥U) (m : G ⧸ U → ↑A.obj) : (TopRep.Hom.hom (smoothTensorInducedChangeTransversalIso U hU s t A).hom.hom) ((PiTensorProduct.tprod R) m) = (PiTensorProduct.tprod R) fun (x : G ⧸ U) => (A.obj.ρ ((U.monomialChangeTransversal s t).left x)) (m x)

On a pure tensor, the smooth comparison applies the difference of the two transversal representatives in every coset coordinate.

@[simp]

theorem TauCeti.smoothTensorInducedChangeTransversalIso_hom_apply_trivialF2Tprod (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s t : U.LeftTransversal) [U.FiniteIndex] (m : G ⧸ U → (DiscreteRep.trivialF2 ↥U).V) : (TopRep.Hom.hom (smoothTensorInducedChangeTransversalIso U hU s t { obj := trivialF2 ↥U, property := ⋯ }).hom.hom) (smoothTensorInducedTrivialF2Tprod G U hU t m) = smoothTensorInducedTrivialF2Tprod G U hU s fun (x : G ⧸ U) => ((DiscreteRep.trivialF2 ↥U).ρ ((U.monomialChangeTransversal s t).left x)) (m x)

The smooth comparison sends the named pure tensor for trivial 𝔽₂ coefficients to the corresponding named pure tensor for the new transversal.

theorem TauCeti.smoothTensorInducedChangeTransversalIso_hom_naturality {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 t : U.LeftTransversal) [U.FiniteIndex] {A B : SmoothDiscreteTopRep R ↥U} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp ((smoothTensorInductionFunctor R G U hU t).map f) (smoothTensorInducedChangeTransversalIso U hU s t B).hom = CategoryTheory.CategoryStruct.comp (smoothTensorInducedChangeTransversalIso U hU s t A).hom ((smoothTensorInductionFunctor R G U hU s).map f)

The smooth change-of-transversal comparison is natural in the coefficient representation.

theorem TauCeti.smoothTensorInducedChangeTransversalIso_hom_naturality_assoc {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 t : U.LeftTransversal) [U.FiniteIndex] {A B : SmoothDiscreteTopRep R ↥U} (f : A ⟶ B) {Z : SmoothDiscreteTopRep R G} (h : (toSmoothDiscrete R G).obj (DiscreteRep.tensorInduced U hU s ((ofSmoothDiscrete R ↥U).obj B)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((smoothTensorInductionFunctor R G U hU t).map f) (smoothTensorInducedChangeTransversalIso U hU s t B).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (smoothTensorInducedChangeTransversalIso U hU s t A).hom ((smoothTensorInductionFunctor R G U hU s).map f)) h

The smooth change-of-transversal comparison is natural in the coefficient representation.

noncomputable def TauCeti.smoothTensorInductionChangeTransversalNatIso {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 t : U.LeftTransversal) [U.FiniteIndex] : smoothTensorInductionFunctor R G U hU t ≅ smoothTensorInductionFunctor R G U hU s

Smooth tensor induction is naturally independent of the chosen transversal.

@[simp]

theorem TauCeti.smoothTensorInductionChangeTransversalNatIso_app {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 t : U.LeftTransversal) [U.FiniteIndex] (A : SmoothDiscreteTopRep R ↥U) : (smoothTensorInductionChangeTransversalNatIso U hU s t).app A = smoothTensorInducedChangeTransversalIso U hU s t A

The component of the smooth natural isomorphism is the named change-of-transversal comparison.

theorem TauCeti.smoothTensorInducedTrivialF2Iso_changeTransversal_apply_tprod (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s t : U.LeftTransversal) [U.FiniteIndex] (m : G ⧸ U → (DiscreteRep.trivialF2 ↥U).V) : (trivialF2Equiv G) ((TopRep.Hom.hom (smoothTensorInducedTrivialF2Iso G U hU s).hom.hom) ((TopRep.Hom.hom (smoothTensorInducedChangeTransversalIso U hU s t { obj := trivialF2 ↥U, property := ⋯ }).hom.hom) (smoothTensorInducedTrivialF2Tprod G U hU t m))) = (trivialF2Equiv G) ((TopRep.Hom.hom (smoothTensorInducedTrivialF2Iso G U hU t).hom.hom) (smoothTensorInducedTrivialF2Tprod G U hU t m))

On pure tensors, changing the transversal does not change the canonical identification of tensor-induced trivial 𝔽₂ coefficients with ambient trivial 𝔽₂ coefficients.

theorem TauCeti.smoothTensorInducedTrivialF2Iso_changeTransversal_hom (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s t : U.LeftTransversal) [U.FiniteIndex] : CategoryTheory.CategoryStruct.comp (smoothTensorInducedChangeTransversalIso U hU s t { obj := trivialF2 ↥U, property := ⋯ }).hom (smoothTensorInducedTrivialF2Iso G U hU s).hom = (smoothTensorInducedTrivialF2Iso G U hU t).hom

The canonical identification of tensor-induced trivial 𝔽₂ coefficients commutes with change of transversal.

theorem TauCeti.smoothTensorInducedTrivialF2Iso_changeTransversal_hom_assoc (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s t : U.LeftTransversal) [U.FiniteIndex] {Z : SmoothDiscreteTopRep ℤ G} (h : { obj := trivialF2 G, property := ⋯ } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (smoothTensorInducedChangeTransversalIso U hU s t { obj := trivialF2 ↥U, property := ⋯ }).hom (smoothTensorInducedTrivialF2Iso G U hU s).hom) h = CategoryTheory.CategoryStruct.comp (smoothTensorInducedTrivialF2Iso G U hU t).hom h

The canonical identification of tensor-induced trivial 𝔽₂ coefficients commutes with change of transversal.