Cup product with the connecting class of a character, on cocycles

Let G be a finite group, χ : Gᵃᵇ → ℚ/ℤ a character and A a representation of G with an invariant a ∈ Aᴳ. Write χ'(g) ∈ [0, 1) for the representative of χ(g). This file computes the cup product a ∪ δχ ∈ H²(G, A) of the degree-zero class of a with the connecting class δχ ∈ H²(G, ℤ) of χ (TauCeti.TateCohomology.characterConnectingClass) on cocycles: it is the class of the carry cocycle

(g, h) ↦ ⌊χ'(g) + χ'(h)⌋ • a,

with the carry TauCeti.ContCohomology.characterCarry of χ.

The connecting map of 0 → ℤ → ℚ → ℚ/ℤ → 0 is computed by lifting χ to the rational cochain χ', whose coboundary (g, h) ↦ χ'(g) + χ'(h) - χ'(gh) is the carry (TauCeti.ContCohomology.intCast_characterCarry). Cup product with the class of a is induced by the map ℤ → A, 1 ↦ a, which multiplies the carry by a.

This is the cocycle description of the classes a ∪ δχ in the character formula χ(artinMap a) = inv(a ∪ δχ) of a class formation, valid for every character of every finite group. For a cyclic group of order n and a character sending a generator to 1 / n, the carry cocycle is the cocycle of two-periodicity (TauCeti.ContCohomology.characterCarry_eq_ite).

Main definitions

• TauCeti.groupCohomology.characterCarryCocycles₂: the carry cocycle (g, h) ↦ ⌊χ'(g) + χ'(h)⌋ • a of a character and an invariant, as a 2-cocycle of an integral representation.

Main results

• TauCeti.TateCohomology.characterConnectingClass_eq_H2π: δχ is the class of the integer carry cocycle of χ.
• TauCeti.TateCohomology.cup_characterConnectingClass_eq_H2π: a ∪ δχ is the class of the carry cocycle of χ and a.

References

• J.-P. Serre, Local Fields, Chapter XIV, §1.
• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VII (Tate, Global Class Field Theory), §1.

noncomputable def TauCeti.groupCohomology.characterCarryCocycles₂ {G : Type} [Group G] (χ : Additive G →+ AddCircle 1) (A : Rep.{u_1, 0, 0} ℤ G) (a : ↥A.ρ.invariants) : ↥(groupCohomology.cocycles₂ A)

The carry cocycle of a character χ : G → ℚ/ℤ and an invariant a of a representation A of G: the 2-cocycle (g, h) ↦ ⌊χ'(g) + χ'(h)⌋ • a, where χ'(x) ∈ [0, 1) represents χ(x) (characterCarryCocycles₂_apply). For a finite group its class is the cup product a ∪ δχ (TauCeti.TateCohomology.cup_characterConnectingClass_eq_H2π).

@[simp]

theorem TauCeti.groupCohomology.characterCarryCocycles₂_apply {G : Type} [Group G] (χ : Additive G →+ AddCircle 1) (A : Rep.{u_1, 0, 0} ℤ G) (a : ↥A.ρ.invariants) (g h : G) : (characterCarryCocycles₂ χ A a) (g, h) = ContCohomology.characterCarry χ g h • ↑a

The value of the carry cocycle of χ and a at (g, h) is the carry of χ times a.

theorem TauCeti.TateCohomology.characterConnectingClass_eq_H2π {G : Type} [Group G] [Fintype G] (χ : Additive (Abelianization G) →+ AddCircle 1) (c : ↥(groupCohomology.cocycles₂ (Rep.trivial ℤ G ℤ))) (hc : ∀ (g h : G), c (g, h) = ContCohomology.characterCarry (χ.comp (MonoidHom.toAdditive Abelianization.of)) g h) : (characterConnectingClass G) χ = (CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupCohomology 2).inv.app (Rep.trivial ℤ G ℤ))) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.trivial ℤ G ℤ))) c)

The connecting class of a character is its carry class. For a character χ of a finite group, δχ ∈ H²(G, ℤ) is the class of every 2-cocycle whose value at (g, h) is the carry ⌊χ'(g) + χ'(h)⌋ of χ.

theorem TauCeti.TateCohomology.cup_characterConnectingClass_eq_H2π {G : Type} [Group G] [Fintype G] (χ : Additive (Abelianization G) →+ AddCircle 1) (A : Rep.{0, 0, 0} ℤ G) (a : ↥A.ρ.invariants) : (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 (groupCohomology.H2π A)) (groupCohomology.characterCarryCocycles₂ (χ.comp (MonoidHom.toAdditive Abelianization.of)) A a))

Cup product with the connecting class of a character is the carry class. For a character χ of a finite group and an invariant a of a representation A, the cup product a ∪ δχ ∈ H²(G, A ⊗ ℤ) = H²(G, A) of the degree-zero class of a with the connecting class of χ is the class of the carry cocycle (g, h) ↦ ⌊χ'(g) + χ'(h)⌋ • a.