Tate's theorem for a finite normal layer

Let V ◁ U be a finite normal layer of a formation with coefficient module A, and let u ∈ H²(U/V, A^V). Tate's theorem says that if, for every subgroup H of U/V,

• H¹(H, A^V) = 0,
• H²(H, A^V) has exactly #H elements,
• the restriction of u to H generates H²(H, A^V),

then cup product with u is an isomorphism H^r(U/V, ℤ) ≃ H^{r+2}(U/V, A^V) in every integer degree r (TauCeti.ClassFieldTheory.tateTheorem). The three hypotheses are separate explicit arguments, quantified over the finite quotient system H ↦ subgroupLayer H of the layer, and the underlying homomorphism of the isomorphism is the cup-product map cupClass (tateTheorem_toAddMonoidHom). For a class formation the hypotheses hold for the fundamental class, which gives the Tate isomorphisms ClassFormation.tateIso of Artin–Tate's Main Theorem.

The generic content is TauCeti.TateCohomology.cup_bijective_of_cupTrivialInt_injective. This file connects it to the finite-layer language: Tate cohomology of the layer of a subgroup H is Tate cohomology of H with coefficients in the restricted module (TauCeti.ClassFieldTheory.NormalLayer.subgroupLayerTateIso), and the generation hypothesis together with the order of H²(U/V, A^V) gives the degree-zero bijection on the whole Galois group. The generic theorem needs the vanishing and order hypotheses only on subgroups of prime-power order, and cupClass_bijective is stated in that form; tateTheorem is the roadmap's statement with all three hypotheses over every subgroup.

Main definitions

• TauCeti.ClassFieldTheory.tateTheorem: Tate's theorem for a finite normal layer, as an additive equivalence.
• TauCeti.ClassFieldTheory.ClassFormation.tateIso: Tate's theorem for a class formation, applied to the fundamental class.

Main statements

• TauCeti.ClassFieldTheory.cupClass_bijective: cup product with u is bijective in every degree, with the vanishing and order hypotheses on subgroups of prime-power order and the generation hypothesis on the whole Galois group only.
• TauCeti.ClassFieldTheory.tateTheorem_toAddMonoidHom, TauCeti.ClassFieldTheory.ClassFormation.tateIso_toAddMonoidHom: the isomorphisms are the cup-product maps.

References

• J. Tate, The higher dimensional cohomology groups of class field theory, Ann. of Math. 56 (1952), 294–297.
• E. Artin and J. Tate, Class Field Theory, Chapter XIV §4, Theorem 1.

theorem TauCeti.ClassFieldTheory.cupClass_bijective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (u : ↑(L.H F 2)) (h1 : ∀ (p : ℕ) [Fact (Nat.Prime p)] (H : Subgroup L.Gal), IsPGroup p ↥H → Subsingleton ↑((L.subgroupLayer H).H F 1)) (hcard : ∀ (p : ℕ) [Fact (Nat.Prime p)] (H : Subgroup L.Gal), IsPGroup p ↥H → Nat.card ↑((L.subgroupLayer H).H F 2) = Nat.card ↥H) (hcardG : Nat.card ↑(L.H F 2) = L.degree) (hgen : ∀ (y : ↑(L.H F 2)), ∃ (m : ℤ), m • u = y) (r : ℤ) : Function.Bijective ⇑(cupClass F L u r)

Cup product with a class u generating H²(U/V, A^V), a group of order [U : V], is bijective from H^r(U/V, ℤ) to H^{r+2}(U/V, A^V) in every integer degree r, provided H¹(H, A^V) = 0 and H²(H, A^V) has exactly #H elements for every subgroup H of U/V of prime-power order. This is Tate's theorem with the vanishing and order hypotheses on prime-power subgroups only and the generation hypothesis on the whole Galois group only; its forms on all subgroups follow.

noncomputable def TauCeti.ClassFieldTheory.tateTheorem {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (u : ↑(L.H F 2)) (h1 : ∀ (H : Subgroup L.Gal), Subsingleton ↑((L.subgroupLayer H).H F 1)) (hcard : ∀ (H : Subgroup L.Gal), Nat.card ↑((L.subgroupLayer H).H F 2) = Nat.card ↥H) (hgen : ∀ (H : Subgroup L.Gal) (x : ↑((L.subgroupLayer H).H F 2)), ∃ (m : ℤ), x = m • (CategoryTheory.ConcreteCategory.hom (⋯.cohomologyRes F 2)) u) (r : ℤ) : ↑(L.TrivialTateH r) ≃+ ↑(L.TateH F (r + 2))

Tate's theorem (J. Tate, The higher dimensional cohomology groups of class field theory, Ann. of Math. 56 (1952); Artin–Tate, Chapter XIV §4), with its hypotheses stated one by one over the finite quotient system H ↦ L.subgroupLayer H:

• h1: H¹(H, A^V) = 0 for every subgroup H ≤ U/V;
• hcard: H²(H, A^V) has exactly #H elements;
• hgen: the restriction of u to the layer of H generates that layer's H².

Then cup product with u is an isomorphism H^r(U/V, ℤ) ≃ H^{r+2}(U/V, A^V) in every integer degree r; its underlying homomorphism is cupClass F L u r (tateTheorem_toAddMonoidHom).

@[simp]

theorem TauCeti.ClassFieldTheory.tateTheorem_apply {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (u : ↑(L.H F 2)) (h1 : ∀ (H : Subgroup L.Gal), Subsingleton ↑((L.subgroupLayer H).H F 1)) (hcard : ∀ (H : Subgroup L.Gal), Nat.card ↑((L.subgroupLayer H).H F 2) = Nat.card ↥H) (hgen : ∀ (H : Subgroup L.Gal) (x : ↑((L.subgroupLayer H).H F 2)), ∃ (m : ℤ), x = m • (CategoryTheory.ConcreteCategory.hom (⋯.cohomologyRes F 2)) u) (r : ℤ) (x : ↑(L.TrivialTateH r)) : (tateTheorem F L u h1 hcard hgen r) x = (cupClass F L u r) x

The isomorphism of Tate's theorem acts by cup product with u.

theorem TauCeti.ClassFieldTheory.tateTheorem_toAddMonoidHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (u : ↑(L.H F 2)) (h1 : ∀ (H : Subgroup L.Gal), Subsingleton ↑((L.subgroupLayer H).H F 1)) (hcard : ∀ (H : Subgroup L.Gal), Nat.card ↑((L.subgroupLayer H).H F 2) = Nat.card ↥H) (hgen : ∀ (H : Subgroup L.Gal) (x : ↑((L.subgroupLayer H).H F 2)), ∃ (m : ℤ), x = m • (CategoryTheory.ConcreteCategory.hom (⋯.cohomologyRes F 2)) u) (r : ℤ) : (tateTheorem F L u h1 hcard hgen r).toAddMonoidHom = cupClass F L u r

The isomorphism of Tate's theorem is cup product with u, not an unrelated equivalence between two groups of the same cardinality.

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

Tate's theorem for a class formation, in every integer degree: the generic theorem applied to the fundamental class, with the three hypotheses discharged by the three individually named consequences of the axioms. This is Artin–Tate's Main Theorem (Chapter XIV §4, Theorem 1).

@[simp]

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

The Tate isomorphism of a class formation acts by cup product with the fundamental class.

theorem TauCeti.ClassFieldTheory.ClassFormation.tateIso_toAddMonoidHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (r : ℤ) : (cf.tateIso L r).toAddMonoidHom = cf.cupFundamentalClass L r

The Tate isomorphism of a class formation is the cup-product map with the fundamental class, not an unrelated equivalence between groups of the same cardinality.