The low-degree Tate pairing with a character class

For a finite group G of order n, the cup product pairs its additive abelianization, identified with Ĥ⁻²(G, ℤ) (TauCeti.TateCohomology.HNegTwoAddEquivAbelianization), with the connecting class δχ ∈ Ĥ²(G, ℤ) of a character χ : Gᵃᵇ → ℚ/ℤ, landing in Ĥ⁰(G, ℤ) = ℤ/nℤ. This file computes the pairing: for σ ∈ Gᵃᵇ, the product σ ∪ δχ is the class of -k, for any integer k with k / n ≡ χ(σ) (mod 1) (TauCeti.TateCohomology.map_leftUnitor_cup_characterConnectingClass). In other words, the pairing Gᵃᵇ × Hom(Gᵃᵇ, ℚ/ℤ) → (1/n)ℤ/ℤ that it induces is (σ, χ) ↦ -χ(σ).

The computation has three steps.

• For x ∈ Ĥ⁻²(G, ℤ), the class x ∪ δχ is the Tate connecting map of the sequence 0 → ℤ → ℚ → ℚ/ℤ → 0, tensored on the left with ℤ, applied to the degree (-2, 1) product x ∪ χ with the degree-one class of χ. The sign is positive because x has even degree (TauCeti.TateCohomology.cup_characterConnectingClass_eq_tateδ).
• The degree (-2, 1) product is evaluation of the character up to sign: σ ∪ χ is the class in Ĥ⁻¹(G, ℤ ⊗ ℚ/ℤ) of 1 ⊗ (-χ(σ)) (TauCeti.TateCohomology.cup_character_eq_HNegOneπ). The product is defined by shifting χ to the invariant g ↦ χ(g) of the first upward dimension shift of ℚ/ℤ (TauCeti.TateCohomology.characterDimensionShift), so σ ∪ χ is the connecting map of the upward shifting sequence applied to the image of σ. Through first homology, the class of σ = g is the cycle [g] ⊗ (1 ⊗ (h ↦ χ(h))), whose boundary, computed with the homological differential [g] ⊗ m ↦ g⁻¹ • m - m, is the constant function h ↦ -χ(g). This is where the sign comes from.
• The connecting map Ĥ⁻¹(G, ℤ ⊗ ℚ/ℤ) → Ĥ⁰(G, ℤ ⊗ ℤ) lifts 1 ⊗ (-χ(σ)) = 1 ⊗ (-k/n) to ℤ ⊗ ℚ and takes its norm, which is 1 ⊗ (-k).

This is the low-degree normalization through which a character detects the Artin map of a class formation. Its Nakayama isomorphism is induced by cup product with the fundamental class in degree -2, and Artin reciprocity is the inverse of that isomorphism.

Main results

• TauCeti.TateCohomology.cup_characterConnectingClass_eq_tateδ: x ∪ δχ is the tensored connecting map applied to the degree (-2, 1) product x ∪ χ.
• TauCeti.TateCohomology.cup_character_eq_HNegOneπ: for σ ∈ Gᵃᵇ, the degree (-2, 1) product σ ∪ χ is the class of 1 ⊗ (-χ(σ)) in Ĥ⁻¹(G, ℤ ⊗ ℚ/ℤ).
• TauCeti.TateCohomology.map_leftUnitor_cup_characterConnectingClass: for σ ∈ Gᵃᵇ, the product σ ∪ δχ ∈ Ĥ⁰(G, ℤ) is -k times the class of 1 whenever k / |G| ≡ χ(σ) (mod 1).
• TauCeti.TateCohomology.toRatAddCircle_map_leftUnitor_cup_characterConnectingClass: under the canonical embedding Ĥ⁰(G, ℤ) = ℤ/|G|ℤ → ℚ/ℤ, this product is -χ(σ).

References

• J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter IV (Atiyah–Wall), §7.
• E. Artin and J. Tate, Class Field Theory, Chapter XIV, §3.
• J.-P. Serre, Local Fields, Chapter XI, §3.

theorem TauCeti.TateCohomology.cup_characterConnectingClass_eq_tateδ (G : Type) [Group G] [Fintype G] (x : ↑(tateCohomology (Rep.trivial ℤ G ℤ) (-2))) (χ : Additive (Abelianization G) →+ AddCircle 1) : ((cup (Rep.trivial ℤ G ℤ) (Rep.ratAddCircleShortComplex G).X₁ (-2) 2 0 cup_characterConnectingClass_eq_tateδ._proof_2) x) ((characterConnectingClass G) χ) = (CategoryTheory.ConcreteCategory.hom (TateCohomology.δ ⋯ (-1))) (((cup (Rep.trivial ℤ G ℤ) (Rep.ratAddCircleShortComplex G).X₃ (-2) 1 (-1) cup_characterConnectingClass_eq_tateδ._proof_4) x) ((CategoryTheory.ConcreteCategory.hom ((Rep.ratAddCircleShortComplex G).X₃.fromGroupCohomology 1)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1IsoOfIsTrivial (Rep.ratAddCircleShortComplex G).X₃).inv) (χ.comp (MonoidHom.toAdditive Abelianization.of)))))

Cup product with the connecting class δχ is the connecting map of the tensored sequence applied to the degree (-2, 1) cup product with the character class. The sign is positive because the left degree is even.

theorem TauCeti.TateCohomology.cup_character_eq_HNegOneπ (G : Type) [Group G] [Fintype G] (σ : Additive (Abelianization G)) (χ : Additive (Abelianization G) →+ AddCircle 1) : ((cup (Rep.trivial ℤ G ℤ) (Rep.ratAddCircleShortComplex G).X₃ (-2) 1 (-1) cup_characterConnectingClass_eq_tateδ._proof_4) (HNegTwoAddEquivAbelianization.symm σ)) ((CategoryTheory.ConcreteCategory.hom ((Rep.ratAddCircleShortComplex G).X₃.fromGroupCohomology 1)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1IsoOfIsTrivial (Rep.ratAddCircleShortComplex G).X₃).inv) (χ.comp (MonoidHom.toAdditive Abelianization.of)))) = (CategoryTheory.ConcreteCategory.hom (HNegOneπ (CategoryTheory.MonoidalCategoryStruct.tensorObj (Rep.trivial ℤ G ℤ) (Rep.ratAddCircleShortComplex G).X₃))) ⟨1 ⊗ₜ[ℤ] (-χ σ), ⋯⟩

The degree (-2, 1) cup product with a character is evaluation, up to sign. For σ ∈ Gᵃᵇ = Ĥ⁻²(G, ℤ) and a character χ : Gᵃᵇ → ℚ/ℤ, read as a class in Ĥ¹(G, ℚ/ℤ), the product σ ∪ χ is the class of the norm-zero element 1 ⊗ (-χ(σ)) in Ĥ⁻¹(G, ℤ ⊗ ℚ/ℤ).

theorem TauCeti.TateCohomology.map_leftUnitor_cup_characterConnectingClass (G : Type) [Group G] [Fintype G] (σ : Additive (Abelianization G)) (χ : Additive (Abelianization G) →+ AddCircle 1) (k : ℤ) (hk : ↑(↑k / ↑(Nat.card G)) = χ σ) : (CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor 0).map (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Rep.trivial ℤ G ℤ)).hom)) (((cup (Rep.trivial ℤ G ℤ) (Rep.trivial ℤ G ℤ) (-2) 2 0 cup_characterConnectingClass_eq_tateδ._proof_2) (HNegTwoAddEquivAbelianization.symm σ)) ((characterConnectingClass G) χ)) = -k • trivialTateHZeroOne G

The Tate pairing of Gᵃᵇ with a character class. For σ ∈ Gᵃᵇ = Ĥ⁻²(G, ℤ), a character χ : Gᵃᵇ → ℚ/ℤ and an integer k with k / |G| ≡ χ(σ) (mod 1), the cup product σ ∪ δχ, read in Ĥ⁰(G, ℤ) through the left unitor, is -k times the class of 1.

@[simp]

theorem TauCeti.TateCohomology.toRatAddCircle_map_leftUnitor_cup_characterConnectingClass (G : Type) [Group G] [Fintype G] (σ : Additive (Abelianization G)) (χ : Additive (Abelianization G) →+ AddCircle 1) : (ZMod.toRatAddCircle (Nat.card G)) ((H0LinearEquivTrivialIntZModCard G) ((CategoryTheory.ConcreteCategory.hom ((tateCohomologyFunctor 0).map (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Rep.trivial ℤ G ℤ)).hom)) (((cup (Rep.trivial ℤ G ℤ) (Rep.trivial ℤ G ℤ) (-2) 2 0 cup_characterConnectingClass_eq_tateδ._proof_2) (HNegTwoAddEquivAbelianization.symm σ)) ((characterConnectingClass G) χ)))) = -χ σ

Under the canonical embedding Ĥ⁰(G, ℤ) = ℤ/|G|ℤ → ℚ/ℤ, the Tate pairing of σ ∈ Gᵃᵇ with the connecting class of a character χ is the negative evaluation -χ(σ).