Cup product with the connecting class of a character of a cyclic group

Let G be a finite cyclic group of order n generated by g, and let χ : Gᵃᵇ → ℚ/ℤ be the character with χ(g) = 1/n. For a representation A of G and an invariant a ∈ Aᴳ, this file proves that the cup product a ∪ δχ ∈ H^2(G, A) of the degree-zero class of a with the connecting class δχ ∈ H^2(G, ℤ) of χ (TauCeti.TateCohomology.characterConnectingClass) is the periodicity class of a at g: the image of a under Rep.FiniteCyclicGroup.groupCohomologyπEven, which is represented by the carry cocycle (gⁱ, gʲ) ↦ a if i + j ≥ n and 0 otherwise, for 0 ≤ i, j < n.

This is the classical description of two-periodicity of a cyclic group as cup product with the class δχ, and the form in which the character formula χ(artinMap a) = inv(a ∪ δχ) of a class formation is evaluated on a cyclic layer: on an unramified layer of a local field, with g the arithmetic Frobenius, the periodicity class of a is the class whose local invariant is v(a)/n.

The proof computes δχ on cocycles. Lifting χ to the cochain gⁱ ↦ i/n with values in ℚ, for 0 ≤ i < n, its coboundary is (gⁱ, gʲ) ↦ (i + j - ((i + j) mod n))/n, which is the carry of i + j modulo n. So δχ is the periodicity class of 1 ∈ ℤ (TauCeti.TateCohomology.characterConnectingClass_eq_groupCohomologyπEven). Cup product with the class of a is induced by the map ℤ → A, 1 ↦ a, which carries the periodicity class of 1 to that of a.

Main results

• TauCeti.TateCohomology.δ_H1IsoOfIsTrivial_inv_eq_groupCohomologyπEven, TauCeti.TateCohomology.characterConnectingClass_eq_groupCohomologyπEven: if χ(g) = 1/n, then δχ is the periodicity class of 1 ∈ ℤ at g.
• TauCeti.TateCohomology.cup_characterConnectingClass_eq_groupCohomologyπEven: if χ(g) = 1/n, then a ∪ δχ is the periodicity class of a at g.

References

• J.-P. Serre, Local Fields, Chapter VIII, §4, and Chapter XI, §3.
• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §3.

theorem TauCeti.TateCohomology.δ_H1IsoOfIsTrivial_inv_eq_groupCohomologyπEven {G : Type} [CommGroup G] [Fintype G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (χ : Additive (Abelianization G) →+ AddCircle 1) (hχ : χ (Additive.ofMul (Abelianization.of g)) = ↑(1 / ↑(orderOf g))) (x : ↥(Rep.Hom.hom ((Rep.trivial ℤ G ℤ).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.trivial ℤ G ℤ))).ker) (hx : ↑x = 1) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.δ ⋯ 1 2 ⋯)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1IsoOfIsTrivial (Rep.trivial ℤ G (AddCircle 1))).inv) (χ.comp (MonoidHom.toAdditive Abelianization.of))) = (CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven (Rep.trivial ℤ G ℤ) g hg 2 ⋯)) x

The connecting class of the character g ↦ 1/n is the periodicity class of 1. For a finite cyclic group generated by g and a character χ with χ(g) = 1/n, the connecting map of 0 → ℤ → ℚ → ℚ/ℤ → 0 sends the class of χ in H¹(G, ℚ/ℤ) to the class in H²(G, ℤ) of the g-fixed element 1, which is represented by the carry cocycle of 1.

theorem TauCeti.TateCohomology.characterConnectingClass_eq_groupCohomologyπEven {G : Type} [CommGroup G] [Fintype G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (χ : Additive (Abelianization G) →+ AddCircle 1) (hχ : χ (Additive.ofMul (Abelianization.of g)) = ↑(1 / ↑(orderOf g))) (x : ↥(Rep.Hom.hom ((Rep.trivial ℤ G ℤ).applyAsHom g - CategoryTheory.CategoryStruct.id (Rep.trivial ℤ G ℤ))).ker) (hx : ↑x = 1) : (characterConnectingClass G) χ = (CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupCohomology 2).inv.app (Rep.trivial ℤ G ℤ))) ((CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven (Rep.trivial ℤ G ℤ) g hg 2 ⋯)) x)

The connecting class of the character g ↦ 1/n is the periodicity class of 1, in Tate cohomology: for a finite cyclic group generated by g and a character χ with χ(g) = 1/n, δχ ∈ H^2(G, ℤ) is the class of the g-fixed element 1.

theorem TauCeti.TateCohomology.cup_characterConnectingClass_eq_groupCohomologyπEven {G : Type} [CommGroup G] [Fintype G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (χ : Additive (Abelianization G) →+ AddCircle 1) (hχ : χ (Additive.ofMul (Abelianization.of g)) = ↑(1 / ↑(orderOf g))) (A : Rep.{0, 0, 0} ℤ G) (a : ↥A.ρ.invariants) (x : ↥(Rep.Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) (hx : ↑x = ↑a) : (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor 2).map (CategoryTheory.MonoidalCategoryStruct.rightUnitor A).hom)) (((cup A (Rep.trivial ℤ G ℤ) 0 2 2 ⋯) ((CategoryTheory.ConcreteCategory.hom (H0π A)) a)) ((characterConnectingClass G) χ)) = (CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupCohomology 2).inv.app A)) ((CategoryTheory.ConcreteCategory.hom (Rep.FiniteCyclicGroup.groupCohomologyπEven A g hg 2 ⋯)) x)

Cup product with δχ is two-periodicity. For a finite cyclic group generated by g, a character χ with χ(g) = 1/n and an invariant a of a representation A, the cup product a ∪ δχ ∈ H^2(G, A ⊗ ℤ) = H^2(G, A) of the degree-zero class of a with the connecting class of χ is the class of the g-fixed element a under two-periodicity, represented by the carry cocycle of a.