Class formations and fundamental classes

A class formation in the sense of Artin–Tate is a formation whose finite normal layers K/F (with Galois group Γ = U ⧸ V and coefficient module C = A^V) satisfy

1. H¹(Γ, C) = 0;
2. there is an injective invariant map inv_{K/F} : H²(Γ, C) → ℚ/ℤ;
3. whose image is the unique subgroup of ℚ/ℤ of order [K : F];
4. restriction to an intermediate ground field E multiplies invariants by [E : F];
5. inflation to a larger top field does not change invariants;
6. conjugation carries the invariant map of a layer to that of the conjugate layer.

The target ℚ/ℤ is the rational circle AddCircle (1 : ℚ), and its subgroup of order n is the n-torsion AddSubgroup.torsionBy (AddCircle (1 : ℚ)) n, which AddCircle.eq_torsionBy_of_natCard_eq shows is the only subgroup of that order.

The invariant map is data of the structure. The fundamental class is not: it is derived below as the unique class u_{K/F} of invariant 1 / [K : F] (ClassFormation.fundamentalClass, ClassFormation.inv_fundamentalClass, ClassFormation.eq_fundamentalClass_iff). The axioms force H²(Γ, C) to be cyclic of order [K : F], generated by u_{K/F}. Its image in Tate degree 2 under the canonical comparison of positive-degree Tate cohomology with ordinary cohomology is ClassFormation.tateFundamentalClass, which in turn generates the Tate group in degree 2 (ClassFormation.zmultiples_tateFundamentalClass).

The compatibilities of the fundamental class have three different shapes, and each is stated separately:

• restriction to an intermediate ground field carries u_{K/F} to u_{K/E} (ClassFormation.fundamentalClass_restrict);
• inflation to a larger top field L is scaled: inf u_{K/F} = [L : K] • u_{L/F} (ClassFormation.fundamentalClass_infl);
• corestriction preserves invariants (ClassFormation.inv_cor, a theorem, not an axiom) and is scaled the other way: cor u_{K/E} = [E : F] • u_{K/F} (ClassFormation.fundamentalClass_cor);

and conjugation carries fundamental classes to fundamental classes (ClassFormation.fundamentalClass_conj).

Finally, the three hypotheses of Tate's theorem are verified, one by one, for the finite quotient system H ↦ subgroupLayer H of a layer: H¹ of each of its layers vanishes (ClassFormation.h1_subgroupLayer), H² of the layer of H has #H elements (ClassFormation.card_H2_subgroupLayer), and it is generated by the restriction of the fundamental class (ClassFormation.fundamentalClass_restrict_generates).

In a layer with cyclic Galois group, two-periodicity of Tate cohomology carries the count of H² to degree zero: the norm quotient A^U / N_{U/V}(A^V) has exactly [U : V] elements (ClassFormation.natCard_normQuotient).

Main definitions

• TauCeti.ClassFieldTheory.ClassFormation: the class-formation axioms on a formation, with the invariant map as data.
• TauCeti.ClassFieldTheory.ClassFormation.fundamentalClass: the fundamental class of a finite normal layer.
• TauCeti.ClassFieldTheory.ClassFormation.tateFundamentalClass: the fundamental class in Tate degree 2.

References

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

structure TauCeti.ClassFieldTheory.ClassFormation {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) : Type

A class formation in the finite-layer form of Artin–Tate: the first cohomology of every finite normal layer vanishes, and its second cohomology carries an injective invariant map onto the subgroup of ℚ/ℤ of order the degree of the layer, compatible with restriction, inflation and conjugation.

The invariant map is data. The fundamental class is not a field: it is derived as ClassFormation.fundamentalClass. Since every other field is a proposition, a class formation is determined by its invariant maps (ClassFormation.ext).

• subsingleton_h1 (L : NormalLayer G) : Subsingleton ↑(L.H F 1)

  H¹ of every finite normal layer vanishes.

• inv (L : NormalLayer G) : ↑(L.H F 2) →+ AddCircle 1

  The invariant map inv_{K/F} : H²(Gal(K/F), A^V) → ℚ/ℤ of a layer.

• inv_injective (L : NormalLayer G) : Function.Injective ⇑(self.inv L)

  The invariant map is injective.

• range_inv (L : NormalLayer G) : Set.range ⇑(self.inv L) = ↑(AddSubgroup.torsionBy (AddCircle 1) ↑L.degree)

  The image of the invariant map is the subgroup of ℚ/ℤ of order [K : F].

• inv_restrict {small big : NormalLayer G} (T : LayerRestriction small big) (x : ↑(big.H F 2)) : (self.inv small) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyRes F 2)) x) = T.relativeDegree • (self.inv big) x

  Restriction to an intermediate ground field E multiplies invariants by [E : F].

• inv_infl {old new : NormalLayer G} (T : LayerRefinement old new) (x : ↑(old.H F 2)) : (self.inv new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) x) = (self.inv old) x

  Inflation to a larger top field does not change invariants.

• inv_conj (L : NormalLayer G) (g : G) (x : ↑(L.H F 2)) : (self.inv (L.conjugate g)) ((CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F g 2).hom) x) = (self.inv L) x

  Conjugation carries the invariant map of a layer to that of the conjugate layer.

theorem TauCeti.ClassFieldTheory.ClassFormation.ext {G : Type} {inst✝ : Group G} {inst✝¹ : TopologicalSpace G} {inst✝² : IsTopologicalGroup G} {inst✝³ : CompactSpace G} {inst✝⁴ : TotallyDisconnectedSpace G} {F : Formation G} {x y : ClassFormation F} (inv : x.inv = y.inv) : x = y

theorem TauCeti.ClassFieldTheory.ClassFormation.ext_iff {G : Type} {inst✝ : Group G} {inst✝¹ : TopologicalSpace G} {inst✝² : IsTopologicalGroup G} {inst✝³ : CompactSpace G} {inst✝⁴ : TotallyDisconnectedSpace G} {F : Formation G} {x y : ClassFormation F} : x = y ↔ x.inv = y.inv

The second cohomology of a layer

theorem TauCeti.ClassFieldTheory.ClassFormation.natCard_H2 {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : Nat.card ↑(L.H F 2) = L.degree

H² of a finite normal layer of a class formation has exactly [K : F] elements.

theorem TauCeti.ClassFieldTheory.ClassFormation.existsUnique_inv_eq {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : ∃! u : ↑(L.H F 2), (cf.inv L) u = ↑(1 / ↑L.degree)

There is exactly one class of invariant 1 / [K : F].

noncomputable def TauCeti.ClassFieldTheory.ClassFormation.fundamentalClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : ↑(L.H F 2)

The fundamental class u_{K/F} of a finite normal layer: the unique class of invariant 1 / [K : F].

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.inv_fundamentalClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : (cf.inv L) (cf.fundamentalClass L) = ↑(1 / ↑L.degree)

The fundamental class has invariant 1 / [K : F].

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.eq_fundamentalClass_iff {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {L : NormalLayer G} (x : ↑(L.H F 2)) : x = cf.fundamentalClass L ↔ (cf.inv L) x = ↑(1 / ↑L.degree)

The fundamental class is characterized by its invariant.

theorem TauCeti.ClassFieldTheory.ClassFormation.fundamentalClass_generates {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (x : ↑(L.H F 2)) : ∃ (m : ℤ), x = m • cf.fundamentalClass L

Every class in H² of a layer is an integer multiple of the fundamental class.

theorem TauCeti.ClassFieldTheory.ClassFormation.zmultiples_fundamentalClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : AddSubgroup.zmultiples (cf.fundamentalClass L) = ⊤

The fundamental class generates H² of its layer.

theorem TauCeti.ClassFieldTheory.ClassFormation.isAddCyclic_H2 {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : IsAddCyclic ↑(L.H F 2)

H² of a finite normal layer of a class formation is cyclic; by ClassFormation.natCard_H2 it is cyclic of order [K : F].

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.addOrderOf_fundamentalClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : addOrderOf (cf.fundamentalClass L) = L.degree

The fundamental class has order exactly [K : F].

The fundamental class in Tate degree two

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

The Tate fundamental class of a finite normal layer: the fundamental class u_{K/F} transported from ordinary H²(Γ, C) to Tate cohomology in degree 2 along the canonical identification NormalLayer.tateHIsoH of positive-degree Tate cohomology with ordinary cohomology.

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.tateHIsoH_hom_tateFundamentalClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : (CategoryTheory.ConcreteCategory.hom (L.tateHIsoH F 2).hom) (cf.tateFundamentalClass L) = cf.fundamentalClass L

The Tate fundamental class corresponds to the fundamental class under the identification of Tate degree 2 with ordinary H².

theorem TauCeti.ClassFieldTheory.ClassFormation.zmultiples_tateFundamentalClass {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) : AddSubgroup.zmultiples (cf.tateFundamentalClass L) = ⊤

The Tate fundamental class generates the degree-2 Tate cohomology of its layer.

Restriction, inflation and conjugation of fundamental classes

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.fundamentalClass_restrict {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {small big : NormalLayer G} (T : LayerRestriction small big) : (CategoryTheory.ConcreteCategory.hom (T.cohomologyRes F 2)) (cf.fundamentalClass big) = cf.fundamentalClass small

Restriction of the fundamental class: restricting u_{K/F} to an intermediate ground field E gives u_{K/E}.

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.fundamentalClass_infl {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {old new : NormalLayer G} (T : LayerRefinement old new) : (CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) (cf.fundamentalClass old) = T.relativeDegree • cf.fundamentalClass new

Inflation of the fundamental class is scaled: under a refinement of the top field from K to L, inf u_{K/F} = [L : K] • u_{L/F}.

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.fundamentalClass_conj {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (g : G) : (CategoryTheory.ConcreteCategory.hom (L.conjugateCohomologyIso F g 2).hom) (cf.fundamentalClass L) = cf.fundamentalClass (L.conjugate g)

Conjugation of the fundamental class: conjugation by g carries u_{K/F} to the fundamental class of the conjugate layer.

Corestriction

theorem TauCeti.ClassFieldTheory.ClassFormation.cohomologyRes_surjective {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {small big : NormalLayer G} (T : LayerRestriction small big) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (T.cohomologyRes F 2))

In a class formation, restriction to an intermediate ground field is surjective on H²: every class of the smaller layer is the restriction of an integer multiple of the fundamental class of the larger one.

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.inv_cor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {small big : NormalLayer G} (T : LayerRestriction small big) (x : ↑(small.H F 2)) : (cf.inv big) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyCor F 2)) x) = (cf.inv small) x

Corestriction preserves invariants: inv_{K/F} (cor x) = inv_{K/E} x for an intermediate ground field E.

@[simp]

theorem TauCeti.ClassFieldTheory.ClassFormation.fundamentalClass_cor {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) {small big : NormalLayer G} (T : LayerRestriction small big) : (CategoryTheory.ConcreteCategory.hom (T.cohomologyCor F 2)) (cf.fundamentalClass small) = T.relativeDegree • cf.fundamentalClass big

Corestriction of the fundamental class is scaled: cor u_{K/E} = [E : F] • u_{K/F} for an intermediate ground field E.

The hypotheses of Tate's theorem

For the finite quotient system H ↦ subgroupLayer H of a layer, these are the three hypotheses of Tate's theorem, stated individually because they are consumed separately downstream.

theorem TauCeti.ClassFieldTheory.ClassFormation.h1_subgroupLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (H : Subgroup L.Gal) : Subsingleton ↑((L.subgroupLayer H).H F 1)

H¹ vanishes on the layer cut out by every subgroup of the Galois group.

theorem TauCeti.ClassFieldTheory.ClassFormation.card_H2_subgroupLayer {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (H : Subgroup L.Gal) : Nat.card ↑((L.subgroupLayer H).H F 2) = Nat.card ↥H

H² of the layer cut out by a subgroup H of the Galois group has exactly #H elements.

theorem TauCeti.ClassFieldTheory.ClassFormation.fundamentalClass_restrict_generates {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) (H : Subgroup L.Gal) (x : ↑((L.subgroupLayer H).H F 2)) : ∃ (m : ℤ), x = m • (CategoryTheory.ConcreteCategory.hom (⋯.cohomologyRes F 2)) (cf.fundamentalClass L)

The restriction of the fundamental class to the layer cut out by a subgroup H generates that layer's H².

The norm quotient of a cyclic layer

theorem TauCeti.ClassFieldTheory.ClassFormation.natCard_normQuotient {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F : Formation G} (cf : ClassFormation F) (L : NormalLayer G) [IsCyclic L.Gal] : Nat.card (L.NormQuotient F) = L.degree

Norm index of a cyclic layer. In a cyclic layer the norm quotient A^U / N_{U/V}(A^V) has exactly [U : V] elements. See E. Artin and J. Tate, Class Field Theory, Chapter XIV, §1, and J.-P. Serre, Local Fields, Chapter XI, §3.