Classes with invariant zero, from the layers of prime degree

Let φ : A → A' be an equivariant map between the coefficient modules of two formations F and F' on G, and let σ assign to every finite normal layer L a homomorphism σ_L : H²(L, A) → ℚ/ℤ that does not change under inflation, multiplies by the relative degree under restriction, and vanishes on the classes that φ kills. For the idele classes of a number field, A is the ideles, A' the idele classes and σ the sum of the local invariants. The construction of the invariant map of F' from σ (ClassFormation.ofDescendedInv) needs the converse: σ vanishes only on the classes that φ kills. For the idele classes of a layer L/F this says that a class of H²(Gal(L/F), I_L), a family of local Brauer classes split by L, whose local invariants sum to zero comes from H²(Gal(L/F), Lˣ): the kernel of the sum of the local invariants is the image of the Brauer group.

This file reduces that converse to the layers of prime degree, provided that H¹ of every layer of F' vanishes and that φ is surjective on H² of every layer of prime degree. The reduction is by induction on the degree n of L, with Galois group Γ (NormalLayer.map_eq_zero_of_prime_degree). Let y be a class of H²(L, A) with σ(y) = 0, and x = φ(y).

• If Γ is not a p-group for any prime p, every Sylow subgroup P of Γ is proper. The restriction of y to the layer of P has σ = [Γ : P] • 0 = 0, so by induction x restricts to zero there, and corestricting back gives [Γ : P] • x = 0. The indices of the Sylow subgroups have no common prime factor, so x = 0.
• If Γ is a nontrivial p-group, it has a normal subgroup N of index p, and L refines the layer L_N of Γ ⧸ N, of degree p. The restriction of x to the layer of N vanishes by induction, so by the inflation-restriction sequence x is inflated from a class x₀ of H²(L_N, A'). That class is φ(y₀) by the surjectivity of φ in prime degree, and φ(y - infl y₀) = 0, so σ(y₀) = σ(infl y₀) = σ(y) = 0. The prime-degree case gives x₀ = φ(y₀) = 0, hence x = 0.

The prime-degree case itself is a counting statement (NormalLayer.map_eq_zero_of_natCard_H2_dvd_degree): on a layer L of degree n carrying a class z with σ(z) = 1/n, if #H²(L, A') ∣ n, then φ(z) generates H²(L, A'), so every class φ(y) is a multiple k • φ(z); then σ(y) = k • (1/n), and σ(y) = 0 forces n ∣ k, so φ(y) = 0. For the idele classes the divisibility is the second fundamental inequality, and on a layer of prime degree p a class with σ = 1/p comes from a place of local degree p.

Main statements

• TauCeti.ClassFieldTheory.NormalLayer.map_eq_zero_of_natCard_H2_dvd_degree: on a layer of degree n with #H²(L, A') ∣ n and a class with σ = 1/n, the classes with σ = 0 are killed by φ.
• TauCeti.ClassFieldTheory.NormalLayer.map_eq_zero_of_prime_degree: if the classes with σ = 0 are killed by φ on the layers of prime degree, they are killed by φ on every layer.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VIII, §4.
• J. Tate, Global class field theory, in J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Chapter VII, §11.

theorem TauCeti.ClassFieldTheory.NormalLayer.map_eq_zero_of_natCard_H2_dvd_degree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) {L : NormalLayer G} (h2 : Nat.card ↑(L.H F' 2) ∣ L.degree) (hgen : ∃ (z : ↑(L.H F 2)), (σ L) z = ↑(1 / ↑L.degree)) {y : ↑(L.H F 2)} (hy : (σ L) y = 0) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0

On a layer with a class of invariant 1/n, only the classes killed by φ have invariant zero, when the order of H²(L, A') divides the degree n of L: a class y of H²(L, A) with σ(y) = 0 has φ(y) = 0.

theorem TauCeti.ClassFieldTheory.NormalLayer.map_eq_zero_of_prime_degree {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {F F' : Formation G} (φ : F.toRep ⟶ F'.toRep) (σ : (L : NormalLayer G) → ↑(L.H F 2) →+ AddCircle 1) (hσ : ∀ {old new : NormalLayer G} (T : LayerRefinement old new) (y : ↑(old.H F 2)), (σ new) ((CategoryTheory.ConcreteCategory.hom (T.cohomologyInfl F 2)) y) = (σ old) y) (hres : ∀ {small big : NormalLayer G} (R : LayerRestriction small big) (y : ↑(big.H F 2)), (σ small) ((CategoryTheory.ConcreteCategory.hom (R.cohomologyRes F 2)) y) = R.relativeDegree • (σ big) y) (hker : ∀ (L : NormalLayer G) (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0 → (σ L) y = 0) (h1 : ∀ (L : NormalLayer G), Subsingleton ↑(L.H F' 1)) (hsurj : ∀ (L : NormalLayer G), Nat.Prime L.degree → ∀ (x : ↑(L.H F' 2)), ∃ (y : ↑(L.H F 2)), (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = x) (hprime : ∀ (L : NormalLayer G), Nat.Prime L.degree → ∀ (y : ↑(L.H F 2)), (σ L) y = 0 → (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0) (L : NormalLayer G) {y : ↑(L.H F 2)} (hy : (σ L) y = 0) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id L.Gal) (L.repMap φ) 2)) y = 0

The classes with invariant zero are killed by φ, from the layers of prime degree. Suppose that σ does not change under inflation, multiplies by the relative degree under restriction and vanishes on the classes that φ kills, and that H¹ of every layer of F' vanishes. If, on every layer of prime degree, φ is surjective on H² and kills every class with σ = 0, then on every layer L a class y of H²(L, A) with σ(y) = 0 has φ(y) = 0.