Changing the transversal in the tensor-induced resolution

The comparison between two tensor inductions preserves the total grading and commutes with the slot-sum differential. It therefore compares the contracted tensor-induced resolutions over the corresponding coefficient comparison. An invariant diagonal tensor is fixed by this comparison, so its continuous cohomology class is independent of the transversal after transporting the coefficients.

References

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

theorem TauCeti.coeffMap_smoothTensorInducedDiagonalClass_changeTransversal {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] [CompactSpace ↥U] (A : SmoothDiscreteTopRep R ↥U) [Fintype (G ⧸ U)] (hA : ∀ (a : ↑A.obj), a + a = 0) {n : ℕ} (z : A.obj.gradedResolutionModule) (hz : z ∈ A.obj.gradedResolutionPiece ↑n) (hinv : ∀ (u : ↥U), (A.obj.gradedResolutionTopRep.ρ u) z = z) (hdz : A.obj.gradedResolutionDifferential z = 0) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (smoothTensorInducedChangeTransversalIso U hU s t A).hom.hom (Fintype.card (G ⧸ U) * n))) (smoothTensorInducedDiagonalClass U hU t A hA z hz hinv hdz) = smoothTensorInducedDiagonalClass U hU s A hA z hz hinv hdz

Changing the transversal transports the class of an invariant diagonal cocycle along the canonical comparison of tensor-induced coefficients. The comparison has source t and target s, as does smoothTensorInducedChangeTransversalIso U hU s t A.

theorem TauCeti.smoothTensorInducedDiagonalClass_trivialF2_changeTransversal (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : Subgroup G) (hU : IsOpen ↑U) (s t : U.LeftTransversal) [U.FiniteIndex] [CompactSpace ↥U] [Fintype (G ⧸ U)] {n : ℕ} (z : (trivialF2 ↥U).gradedResolutionModule) (hz : z ∈ (trivialF2 ↥U).gradedResolutionPiece ↑n) (hinv : ∀ (u : ↥U), ((trivialF2 ↥U).gradedResolutionTopRep.ρ u) z = z) (hdz : (trivialF2 ↥U).gradedResolutionDifferential z = 0) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (smoothTensorInducedTrivialF2Iso G U hU t).hom.hom (Fintype.card (G ⧸ U) * n))) (smoothTensorInducedDiagonalClass U hU t { obj := trivialF2 ↥U, property := ⋯ } ⋯ z hz hinv hdz) = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (smoothTensorInducedTrivialF2Iso G U hU s).hom.hom (Fintype.card (G ⧸ U) * n))) (smoothTensorInducedDiagonalClass U hU s { obj := trivialF2 ↥U, property := ⋯ } ⋯ z hz hinv hdz)

After identifying tensor-induced trivial 𝔽₂ coefficients with the ambient trivial coefficient object, the class of an invariant diagonal cocycle does not depend on the transversal.