The local invariant on roots-of-unity cohomology

For a nonarchimedean local field F and an exponent n invertible in F, the Kummer coefficient map identifies H²(F, μₙ) with the n-torsion of the Brauer group. The local invariant invMap F, normalized by arithmetic Frobenius, therefore identifies it with the n-torsion of ℚ/ℤ. The class of invariant 1/n determines the normalized equivalence h2MuEquivZMod F hn : H²(F, μₙ) ≃+ ZMod n.

The normalization is characterized by toRatAddCircle_h2MuEquivZMod: a class whose image in the Brauer group has invariant k/n maps to k. In particular, the inverse image of 1 has Brauer invariant 1/n. This is the degree-two identification used after taking the cup product of two Kummer classes in the cohomological local symbol.

Only invertibility in the field is required, not in its valuation ring. Thus in characteristic zero the construction works for every nonzero n, including exponents divisible by the residue characteristic (h2MuEquivZMod_mixed).

An isomorphism of coefficient objects e : μₙ ≅ T transports the invariant to h2EquivZModOfMuNRepIso F hn e : H²(F, T) ≃+ ZMod n. When F contains a primitive nth root of unity ζ, the root identifies the trivial coefficients ℤ/n with μₙ, and h2FpEquivZMod hζ : H²(F, ℤ/n) ≃+ ZMod n is the transported invariant. In particular H²(F, ℤ/n) then has exactly n elements.

Main definitions

• h2MuEquivZMod: the normalized identification H²(F, μₙ) ≃+ ZMod n.
• h2EquivZModOfMuNRepIso: its transport H²(F, T) ≃+ ZMod n along a coefficient isomorphism μₙ ≅ T.
• h2FpEquivZMod: the normalized identification H²(F, ℤ/n) ≃+ ZMod n with trivial coefficients, given a primitive nth root of unity in F.

Main results

• range_invMap_comp_h2MuToBr: the Kummer classes have precisely the n-torsion invariants.
• toRatAddCircle_h2MuEquivZMod: the forward identification respects the Brauer invariant.
• invMap_h2MuToBr_h2MuEquivZMod_symm: the inverse has the prescribed Brauer invariant.
• h2MuEquivZMod_eq_iff: the invariant characterizes each residue.
• h2MuEquivZMod_mixed: the identification exists for every nonzero exponent in characteristic zero.
• toRatAddCircle_h2FpEquivZMod, h2FpEquivZMod_eq_iff: the normalization with trivial coefficients.
• natCard_cohomFp_two_absoluteGaloisGroup_of_isPrimitiveRoot: H²(F, ℤ/n) has n elements.
• finrank_cohomFp_two_absoluteGaloisGroup_of_isPrimitiveRoot: H²(F, ℤ/n) has rank one over ℤ/n when 1 < n.

References

• J.-P. Serre, Local Fields, Chapter XIII, §3 and Chapter XIV, §2.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (6.2.1).

theorem TauCeti.ClassFieldTheory.range_invMap_comp_h2MuToBr (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : IsUnit ↑n) : ((invMap F).toAddMonoidHom.comp (h2MuToBr n F)).range = AddSubgroup.torsionBy (AddCircle 1) ↑n

The local invariants of roots-of-unity cohomology are exactly the n-torsion of ℚ/ℤ, when n is invertible in the field.

noncomputable def TauCeti.ClassFieldTheory.h2MuEquivZMod (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : IsUnit ↑n) : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n

The normalized local invariant H²(F, μₙ) ≃+ ℤ/n, for n invertible in the field. It sends a class of Brauer invariant k/n to k.

@[simp]

theorem TauCeti.ClassFieldTheory.toRatAddCircle_h2MuEquivZMod (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : IsUnit ↑n) (x : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat) : (ZMod.toRatAddCircle n) ((h2MuEquivZMod F hn) x) = (invMap F) ((h2MuToBr n F) x)

The degree-two invariant followed by k ↦ k/n is the Brauer invariant of the Kummer coefficient image. This characterizes its arithmetic normalization.

@[simp]

theorem TauCeti.ClassFieldTheory.invMap_h2MuToBr_h2MuEquivZMod_symm (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : IsUnit ↑n) (z : ZMod n) : (invMap F) ((h2MuToBr n F) ((h2MuEquivZMod F hn).symm z)) = (ZMod.toRatAddCircle n) z

The inverse degree-two identification has the prescribed Brauer invariant. For an integer residue k, the right side is the class of k/n in ℚ/ℤ.

theorem TauCeti.ClassFieldTheory.h2MuEquivZMod_eq_iff (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : IsUnit ↑n) (x : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat) (z : ZMod n) : (h2MuEquivZMod F hn) x = z ↔ (invMap F) ((h2MuToBr n F) x) = (ZMod.toRatAddCircle n) z

A roots-of-unity cohomology class maps to a residue exactly when its Brauer invariant is that residue's rational-circle image.

theorem TauCeti.ClassFieldTheory.h2MuEquivZMod_mixed (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [CharZero F] (n : ℕ) (hn : n ≠ 0) : Nonempty (↑(continuousCohomology 2 (muNRep n F)).toModuleCat ≃+ ZMod n)

Roots-of-unity cohomology in degree two is ℤ/n in characteristic zero, for every nonzero exponent. In particular this applies to finite extensions of ℚ_p, including n divisible by p. The witness is the normalized equivalence h2MuEquivZMod.

Coefficients identified with roots of unity

noncomputable def TauCeti.ClassFieldTheory.h2EquivZModOfMuNRepIso (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : IsUnit ↑n) {T : GalRep n F} (e : muNRep n F ≅ T) : ↑(continuousCohomology 2 T).toModuleCat ≃+ ZMod n

The local invariant on H² with coefficients identified with μₙ: an isomorphism of coefficient objects e : μₙ ≅ T transports h2MuEquivZMod to H²(F, T). The identification of coefficients is essential: an arbitrary coefficient object, such as the zero module, need not have H² isomorphic to ℤ/n.

@[simp]

theorem TauCeti.ClassFieldTheory.h2EquivZModOfMuNRepIso_coeffMap (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : IsUnit ↑n) {T : GalRep n F} (e : muNRep n F ≅ T) (x : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat) : (h2EquivZModOfMuNRepIso F hn e) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap e.hom 2)) x) = (h2MuEquivZMod F hn) x

The transported invariant of the image of a roots-of-unity class under the coefficient isomorphism is its roots-of-unity invariant.

@[simp]

theorem TauCeti.ClassFieldTheory.h2EquivZModOfMuNRepIso_symm_apply (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} (hn : IsUnit ↑n) {T : GalRep n F} (e : muNRep n F ≅ T) (z : ZMod n) : (h2EquivZModOfMuNRepIso F hn e).symm z = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap e.hom 2)) ((h2MuEquivZMod F hn).symm z)

The inverse transported invariant is the image under the coefficient isomorphism of the inverse roots-of-unity invariant.

Trivial coefficients

noncomputable def TauCeti.ClassFieldTheory.h2FpEquivZMod {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) : ↑(cohomFp n (Field.absoluteGaloisGroup F) 2).toModuleCat ≃+ ZMod n

The local invariant on H²(F, ℤ/n) with trivial coefficients, for F containing a primitive nth root of unity ζ. The root identifies the trivial coefficients ℤ/n with μₙ (muNRepIsoTrivialFp), and h2FpEquivZMod is the specialization of h2EquivZModOfMuNRepIso to that identification.

@[simp]

theorem TauCeti.ClassFieldTheory.h2FpEquivZMod_muNRepCohomologyEquivTrivialFp {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (x : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat) : (h2FpEquivZMod hζ) ((muNRepCohomologyEquivTrivialFp n F hζ 2) x) = (h2MuEquivZMod F ⋯) x

The trivial-coefficient invariant of the transport of a roots-of-unity class is its roots-of-unity invariant.

@[simp]

theorem TauCeti.ClassFieldTheory.h2FpEquivZMod_symm_apply {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (z : ZMod n) : (h2FpEquivZMod hζ).symm z = (muNRepCohomologyEquivTrivialFp n F hζ 2) ((h2MuEquivZMod F ⋯).symm z)

The inverse trivial-coefficient invariant is the transport of the inverse roots-of-unity invariant.

@[simp]

theorem TauCeti.ClassFieldTheory.toRatAddCircle_h2FpEquivZMod {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (x : ↑(cohomFp n (Field.absoluteGaloisGroup F) 2).toModuleCat) : (ZMod.toRatAddCircle n) ((h2FpEquivZMod hζ) x) = (invMap F) ((h2MuToBr n F) ((muNRepCohomologyEquivTrivialFp n F hζ 2).symm x))

The arithmetic normalization with trivial coefficients: a class of H²(F, ℤ/n) maps to k exactly when the corresponding class of H²(F, μₙ) has Brauer invariant k/n.

theorem TauCeti.ClassFieldTheory.h2FpEquivZMod_eq_iff {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) (x : ↑(cohomFp n (Field.absoluteGaloisGroup F) 2).toModuleCat) (z : ZMod n) : (h2FpEquivZMod hζ) x = z ↔ (invMap F) ((h2MuToBr n F) ((muNRepCohomologyEquivTrivialFp n F hζ 2).symm x)) = (ZMod.toRatAddCircle n) z

A class of H²(F, ℤ/n) maps to a residue exactly when the Brauer invariant of the corresponding class of H²(F, μₙ) is that residue's rational-circle image.

theorem TauCeti.ClassFieldTheory.natCard_cohomFp_two_absoluteGaloisGroup_of_isPrimitiveRoot {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} [NeZero n] {ζ : F} (hζ : IsPrimitiveRoot ζ n) : Nat.card ↑(cohomFp n (Field.absoluteGaloisGroup F) 2).toModuleCat = n

If F contains a primitive nth root of unity, then H²(F, ℤ/n) with trivial coefficients has exactly n elements.

theorem TauCeti.ClassFieldTheory.finrank_cohomFp_two_absoluteGaloisGroup_of_isPrimitiveRoot {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {n : ℕ} [Fact (1 < n)] {ζ : F} (hζ : IsPrimitiveRoot ζ n) : Module.finrank (ZMod n) ↑(cohomFp n (Field.absoluteGaloisGroup F) 2).toModuleCat = 1

If F contains a primitive nth root of unity with 1 < n, then H²(F, ℤ/n) with trivial coefficients is free of rank one over ℤ/n.