The connecting class of a character

Let G be a finite group. A character χ : Gᵃᵇ → ℚ/ℤ is a homomorphism G → ℚ/ℤ, which is a class in H¹(G, ℚ/ℤ) for the trivial action. The connecting map of the sequence 0 → ℤ → ℚ → ℚ/ℤ → 0 of trivial G-modules sends it to a class δχ ∈ H²(G, ℤ), which is read in the Tate group of degree 2.

The character also has a canonical invariant representative in the first upward dimension shift of ℚ/ℤ, whose connecting image is its standard Tate degree-one class. This identifies δχ with the Tate connecting map of 0 → ℤ → ℚ → ℚ/ℤ → 0 applied to that class.

As elsewhere in this development, ℚ/ℤ is the rational circle AddCircle (1 : ℚ).

Main definitions

• TauCeti.TateCohomology.characterConnectingClass: the connecting class δχ ∈ H²(G, ℤ) of a character χ : Gᵃᵇ → ℚ/ℤ, in the Tate group of degree 2, as an additive map in χ.
• TauCeti.TateCohomology.characterDimensionShift: the canonical invariant in the first upward dimension shift of ℚ/ℤ attached to a character, as an additive map in the character.

Main results

• TauCeti.TateCohomology.characterConnectingClass_def: δχ is the connecting map of Rep.ratAddCircleShortComplex applied to the class of χ in H¹(G, ℚ/ℤ), read in Tate cohomology.
• TauCeti.TateCohomology.dimensionShiftUpIso_characterDimensionShift: the connecting isomorphism sends characterDimensionShift to the standard Tate degree-one class of χ.
• TauCeti.TateCohomology.characterConnectingClass_eq_tateδ: δχ is the Tate connecting map applied to the standard Tate degree-one class of χ.

References

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

noncomputable def TauCeti.TateCohomology.characterConnectingClass (G : Type) [Group G] [Fintype G] : (Additive (Abelianization G) →+ AddCircle 1) →+ ↑(tateCohomology (Rep.trivial ℤ G ℤ) 2)

The connecting class δχ ∈ H²(G, ℤ) of a character χ : Gᵃᵇ → ℚ/ℤ of a finite group G, in the Tate group of degree 2: the image of χ, as a class in H¹(G, ℚ/ℤ) for the trivial action, under the connecting map of 0 → ℤ → ℚ → ℚ/ℤ → 0. The character is read on G through the abelianization map G → Gᵃᵇ. It is additive in the character.

theorem TauCeti.TateCohomology.characterConnectingClass_def (G : Type) [Group G] [Fintype G] (χ : Additive (Abelianization G) →+ AddCircle 1) : (characterConnectingClass G) χ = (CategoryTheory.ConcreteCategory.hom ((TateCohomology.isoGroupCohomology 2).inv.app (Rep.trivial ℤ G ℤ))) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.δ ⋯ 1 2 ⋯)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1IsoOfIsTrivial (Rep.trivial ℤ G (AddCircle 1))).inv) (χ.comp (MonoidHom.toAdditive Abelianization.of))))

The connecting class of χ is the connecting map applied to the class of G → Gᵃᵇ → ℚ/ℤ in H¹(G, ℚ/ℤ), carried to Tate cohomology by the comparison of positive degrees.

noncomputable def TauCeti.TateCohomology.characterDimensionShift (G : Type) [Group G] : (Additive (Abelianization G) →+ AddCircle 1) →+ ↥(Rep.ratAddCircleShortComplex G).X₃.dimensionShiftUp.ρ.invariants

The canonical invariant in the first upward dimension shift of ℚ/ℤ attached to a character. Its image under the dimension-shift isomorphism is the Tate degree-one class obtained from the ordinary character class in H¹(G, ℚ/ℤ).

@[simp]

theorem TauCeti.TateCohomology.coe_characterDimensionShift (G : Type) [Group G] (χ : Additive (Abelianization G) →+ AddCircle 1) : ↑((characterDimensionShift G) χ) = (Rep.Hom.hom (Rep.ratAddCircleShortComplex G).X₃.dimensionShiftUpπ) ((Rep.coindBotEquivPi ℤ G (AddCircle 1)).symm fun (g : G) => χ (Additive.ofMul (Abelianization.of g)))

The underlying value of characterDimensionShift is the image in the first upward dimension shift of the coinduced function g ↦ χ(g).

theorem TauCeti.TateCohomology.dimensionShiftUpIso_characterDimensionShift (G : Type) [Group G] [Fintype G] (χ : Additive (Abelianization G) →+ AddCircle 1) : (CategoryTheory.ConcreteCategory.hom (dimensionShiftUpIso (Rep.ratAddCircleShortComplex G).X₃ 0).hom) ((CategoryTheory.ConcreteCategory.hom (H0π (Rep.ratAddCircleShortComplex G).X₃.dimensionShiftUp)) ((characterDimensionShift G) χ)) = (CategoryTheory.ConcreteCategory.hom ((Rep.ratAddCircleShortComplex G).X₃.fromGroupCohomology 1)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1IsoOfIsTrivial (Rep.ratAddCircleShortComplex G).X₃).inv) (χ.comp (MonoidHom.toAdditive Abelianization.of)))

The connecting isomorphism sends characterDimensionShift to the standard Tate degree-one class of the character.

theorem TauCeti.TateCohomology.characterConnectingClass_eq_tateδ (G : Type) [Group G] [Fintype G] (χ : Additive (Abelianization G) →+ AddCircle 1) : (characterConnectingClass G) χ = (CategoryTheory.ConcreteCategory.hom (TateCohomology.δ ⋯ 1)) ((CategoryTheory.ConcreteCategory.hom ((Rep.ratAddCircleShortComplex G).X₃.fromGroupCohomology 1)) ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1IsoOfIsTrivial (Rep.ratAddCircleShortComplex G).X₃).inv) (χ.comp (MonoidHom.toAdditive Abelianization.of))))

The connecting class of a character is the Tate connecting map applied to its canonical degree-one class. This compares the definition through ordinary group cohomology with the Tate connecting homomorphism used by the cup-product boundary formula.