Documentation

TauCeti.RepresentationTheory.Homological.ContCohomology.Evens.TensorInduction

The tensor-induced character class and the index-two graph cocycle #

For an index-two compact open subgroup, the diagonal tensor of the homogeneous cocycle of a continuous character has the class of the two-point graph cocycle. This identifies the resolution-level multiplicative transfer on character representatives with the explicit index-two Evens norm.

The calculation uses the transversal with representatives 1 and an element s outside the subgroup, ordered with 1 first. The ordered tensor homotopy first sends z ⊗ z to h z ⊗ z. The explicit cocycle of the contracted complex then has the two branches of the graph formula.

References #

theorem TauCeti.ContCohomology.smoothTensorInducedDiagonalClass_eq_graphClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (s : G) (hs : s ∉ U) (α : ↥↑U →* Multiplicative (ZMod 2)) (hα : Continuous ⇑α) [Fintype (G ⧸ ↑U)] [CompactSpace ↥↑U] (z : (trivialF2 ↥↑U).gradedResolutionModule) (hz : z ∈ (trivialF2 ↥↑U).gradedResolutionPiece 1) (hinv : ∀ (x : ↥↑U), ((trivialF2 ↥↑U).gradedResolutionTopRep.ρ x) z = z) (hdz : (trivialF2 ↥↑U).gradedResolutionDifferential z = 0) (hzα : z = (DirectSum.lof ℤ ℕ (fun (n : ℕ) => ↑((trivialF2 ↥↑U).resolutionX (n + 1))) 1) ↑(inhomogeneousCochain1 (fun (x : ↥↑U) => Multiplicative.toAdd (α x)) ⋯)) :
have t := ⟨Set.range ((↑U).indexTwoTransversal s), ⋯⟩; let A := { obj := trivialF2 ↥↑U, property := ⋯ }; (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (smoothTensorInducedTrivialF2Iso G ↑U ⋯ t).hom.hom (Fintype.card (G ⧸ ↑U) * 1))) (smoothTensorInducedDiagonalClass ↑U ⋯ t A ⋯ z hz hinv hdz) = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) (graphClass U hU α hα)

The tensor-induced class of the homogeneous degree-one cocycle of a continuous character is the index-two graph class. The transversal has representatives 1 and s, and the coefficient identification multiplies the two tensor factors. The equality includes only the transport of degrees from 2 to card (G ⧸ U) * 1.

The quotient Fintype is a caller parameter: the diagonal class and its graded contraction use that enumeration. The input z and its cocycle data are exactly the inputs of smoothTensorInducedDiagonalClass; hzα identifies their explicit homogeneous representative. The theorem compares the classes associated to this explicit homogeneous representative. The statement installs local compactness from the compact open subgroup because the existing graphClass requires it.