Documentation

TauCeti.NumberTheory.ClassFieldTheory.Formation.PrimeDegree

H¹ = 0 and #H² ∣ [U : V] from the layers of prime degree #

Let F be a formation on a profinite group G and V ◁ U a finite normal layer, K/F in field notation. This file proves that the vanishing of H¹(U/V, A^V) and the divisibility #H²(U/V, A^V) ∣ [U : V] follow from the same two statements for the layers V' ◁ U' of prime degree with U' ≤ U and V ≤ V', the cyclic extensions of prime degree inside K/F (NormalLayer.subsingleton_h1_of_prime_degree, NormalLayer.natCard_H2_dvd_degree_of_prime_degree). This is the generic finite-group reduction TauCeti.groupCohomology.isZero_groupCohomology_one_of_prime_index, read on the formation: the subquotient H/N of the Galois group U/V given by a subgroup H and a normal subgroup N of H is the Galois group of the layer cut out by the preimages of N and H, and its action on the invariants (A^V)^N is the coefficient module of that layer.

For a cyclic layer the two statements are equivalent to numerical ones. If the Herbrand quotient h(A^V) of a cyclic layer is its degree n, then its norm quotient A^U / N(A^V) has at least n elements (NormalLayer.degree_le_natCard_normQuotient_of_herbrandQuotient_eq); if moreover the order of the norm quotient divides n, then H¹ vanishes and H² has exactly n elements (NormalLayer.subsingleton_h1_of_herbrandQuotient_eq_of_natCard_normQuotient_dvd, NormalLayer.natCard_H2_eq_degree_of_herbrandQuotient_eq_of_natCard_normQuotient_dvd). Together: if every layer of prime degree inside K/F has Herbrand quotient its degree and a norm quotient whose order divides its degree, then H¹(U/V, A^V) = 0 and #H²(U/V, A^V) ∣ [U : V] (NormalLayer.subsingleton_h1_of_herbrandQuotient_of_prime_degree, NormalLayer.natCard_H2_dvd_degree_of_herbrandQuotient_of_prime_degree).

For the idele classes of a number field these hypotheses are the two fundamental inequalities for cyclic extensions of prime degree, h(C_L) = [L : K] and [C_K : N_{L/K} C_L] ∣ [L : K], and the conclusions are the vanishing of H¹(Gal(L/K), C_L) and the second inequality in its cohomological form #H²(Gal(L/K), C_L) ∣ [L : K] for every finite Galois extension L/K.

Main statements #

References #

The layer of a subquotient of the Galois group #

The reduction to layers of prime degree #

source
theorem TauCeti.ClassFieldTheory.NormalLayer.subsingleton_h1_of_prime_degree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (h1 : ∀ (L' : NormalLayer G), L'.ground ≤ L.ground → L.top ≤ L'.top → Nat.Prime L'.degree → Subsingleton ↑(L'.H F 1)) :
Subsingleton ↑(L.H F 1)

H¹ of a layer vanishes if it vanishes on the layers of prime degree inside it. If H¹(U'/V', A^{V'}) = 0 for every layer V' ◁ U' of prime degree with U' ≤ U and V ≤ V', then H¹(U/V, A^V) = 0.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.natCard_H2_dvd_degree_of_prime_degree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (h1 : ∀ (L' : NormalLayer G), L'.ground ≤ L.ground → L.top ≤ L'.top → Nat.Prime L'.degree → Subsingleton ↑(L'.H F 1)) (h2 : ∀ (L' : NormalLayer G), L'.ground ≤ L.ground → L.top ≤ L'.top → Nat.Prime L'.degree → Nat.card ↑(L'.H F 2) ∣ L'.degree) :
Nat.card ↑(L.H F 2) ∣ L.degree

The order of H² of a layer divides its degree if it does on the layers of prime degree inside it. If, for every layer V' ◁ U' of prime degree with U' ≤ U and V ≤ V', H¹(U'/V', A^{V'}) = 0 and #H²(U'/V', A^{V'}) ∣ [U' : V'], then #H²(U/V, A^V) ∣ [U : V].

Cyclic layers #

source
theorem TauCeti.ClassFieldTheory.NormalLayer.natCard_normQuotient_eq_natCard_H2 {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) [IsCyclic L.Gal] :
Nat.card (L.NormQuotient F) = Nat.card ↑(L.H F 2)

The norm quotient of a cyclic layer has as many elements as its second cohomology: A^U / N(A^V) ≃ \hat{H}^0 ≅ \hat{H}^2 ≅ H².

source
theorem TauCeti.ClassFieldTheory.NormalLayer.degree_le_natCard_normQuotient_of_herbrandQuotient_eq {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) [IsCyclic L.Gal] (h : TateCohomology.herbrandQuotient (L.rep F) = ↑L.degree) :
L.degree ≤ Nat.card (L.NormQuotient F)

The first inequality from the Herbrand quotient. If the Herbrand quotient h(A^V) of a cyclic layer is its degree, then its norm quotient A^U / N(A^V) has at least [U : V] elements.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.subsingleton_h1_of_herbrandQuotient_eq_of_natCard_normQuotient_dvd {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) [IsCyclic L.Gal] (h : TateCohomology.herbrandQuotient (L.rep F) = ↑L.degree) (hN : Nat.card (L.NormQuotient F) ∣ L.degree) :
Subsingleton ↑(L.H F 1)

H¹ of a cyclic layer from the two inequalities. If the Herbrand quotient of a cyclic layer is its degree and the order of its norm quotient divides its degree, then H¹(U/V, A^V) = 0.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.natCard_H2_eq_degree_of_herbrandQuotient_eq_of_natCard_normQuotient_dvd {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) [IsCyclic L.Gal] (h : TateCohomology.herbrandQuotient (L.rep F) = ↑L.degree) (hN : Nat.card (L.NormQuotient F) ∣ L.degree) :
Nat.card ↑(L.H F 2) = L.degree

H² of a cyclic layer from the two inequalities. If the Herbrand quotient of a cyclic layer is its degree and the order of its norm quotient divides its degree, then H²(U/V, A^V) has exactly [U : V] elements.

The reduction in terms of the two inequalities #

source
theorem TauCeti.ClassFieldTheory.NormalLayer.isCyclic_gal_of_prime_degree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {L : NormalLayer G} (hp : Nat.Prime L.degree) :
IsCyclic L.Gal

A layer of prime degree has a cyclic Galois group.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.subsingleton_h1_of_herbrandQuotient_of_prime_degree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (h : ∀ (L' : NormalLayer G), L'.ground ≤ L.ground → L.top ≤ L'.top → Nat.Prime L'.degree → TateCohomology.herbrandQuotient (L'.rep F) = ↑L'.degree ∧ Nat.card (L'.NormQuotient F) ∣ L'.degree) :
Subsingleton ↑(L.H F 1)

H¹ of a layer vanishes if the two inequalities hold for the layers of prime degree inside it. If every layer V' ◁ U' of prime degree with U' ≤ U and V ≤ V' has Herbrand quotient its degree and a norm quotient whose order divides its degree, then H¹(U/V, A^V) = 0.

source
theorem TauCeti.ClassFieldTheory.NormalLayer.natCard_H2_dvd_degree_of_herbrandQuotient_of_prime_degree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (F : Formation G) (L : NormalLayer G) (h : ∀ (L' : NormalLayer G), L'.ground ≤ L.ground → L.top ≤ L'.top → Nat.Prime L'.degree → TateCohomology.herbrandQuotient (L'.rep F) = ↑L'.degree ∧ Nat.card (L'.NormQuotient F) ∣ L'.degree) :
Nat.card ↑(L.H F 2) ∣ L.degree

The order of H² of a layer divides its degree if the two inequalities hold for the layers of prime degree inside it. If every layer V' ◁ U' of prime degree with U' ≤ U and V ≤ V' has Herbrand quotient its degree and a norm quotient whose order divides its degree, then #H²(U/V, A^V) ∣ [U : V].