The degree-zero case of the Tate isomorphism

Cup product with a degree-two class sends the canonical generator of degree-zero Tate cohomology with trivial integral coefficients to that class. Consequently, if the class generates second cohomology and that group has the order of the Galois group, the degree-zero cup-product map is an isomorphism. In a class formation these conditions hold for the fundamental class. This is the degree-zero input to Tate's cup-product criterion.

The cup-product normalization follows Artin and Tate, Class Field Theory, Preliminaries §2 and Chapter XIV §4.

theorem TauCeti.ClassFieldTheory.cupClass_degree_zero_eq_cupTrivialInt {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (u : ↑(L.H F 2)) : cupClass F L u 0 = TateCohomology.cupTrivialInt (L.rep F) ((CategoryTheory.ConcreteCategory.hom (L.tateHIsoH F 2).inv) u)

At degree zero, the class-formation cup map is the generic cup map with trivial integral coefficients. The target degrees 0 + 2 and 2 agree by normalization.

@[simp]

theorem TauCeti.ClassFieldTheory.cupClass_trivialTateHZeroOne {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (u : ↑(L.H F 2)) : (cupClass F L u 0) (TateCohomology.trivialTateHZeroOne L.Gal) = (CategoryTheory.ConcreteCategory.hom (L.tateHIsoH F 2).inv) u

In degree zero, cup product with u sends the canonical trivial-coefficient class of 1 to u in Tate degree two. This fixes the orientation of the degree-zero Tate isomorphism.

theorem TauCeti.ClassFieldTheory.cupClass_degree_zero_bijective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (u : ↑(L.H F 2)) (hgen : ∀ (y : ↑(L.H F 2)), ∃ (m : ℤ), m • u = y) (hcardH : Nat.card ↑(L.H F 2) = L.degree) : Function.Bijective ⇑(cupClass F L u 0)

Degree-zero case of Tate's cup-product criterion: if a degree-two class generates H²(U/V, A^V) and this group has order [U : V], cupping with it is an equivalence from degree-zero Tate cohomology with trivial integral coefficients to Tate degree two.

theorem TauCeti.ClassFieldTheory.ClassFormation.cupFundamentalClass_zero_bijective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : Function.Bijective ⇑(cf.cupFundamentalClass L 0)

In degree zero, cup product with the fundamental class is bijective. This is the degree-zero case of Tate's theorem for a class formation.

noncomputable def TauCeti.ClassFieldTheory.ClassFormation.cupFundamentalClassZeroEquiv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : ↑(L.TrivialTateH 0) ≃+ ↑(L.TateH F 2)

The degree-zero Tate isomorphism of a class formation, with underlying map cup product by the fundamental class.

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.cupFundamentalClassZeroEquiv_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (x : ↑(L.TrivialTateH 0)) : (cf.cupFundamentalClassZeroEquiv L) x = (cf.cupFundamentalClass L 0) x

The degree-zero equivalence acts by cup product with the fundamental class.

theorem TauCeti.ClassFieldTheory.ClassFormation.cupFundamentalClassZeroEquiv_toAddMonoidHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : (cf.cupFundamentalClassZeroEquiv L).toAddMonoidHom = cf.cupFundamentalClass L 0

The underlying homomorphism of the degree-zero equivalence is cup product with the fundamental class.