Cohomological dimension of the profinite integers

The profinite integers TauCeti.zHat are topologically generated by TauCeti.zHat.gen. Consequently, when n ≠ 0, a continuous character zHat → ZMod n is determined by its value at the generator, and every value occurs. This gives a linear equivalence continuousZModDual n zHat ≃ₗ[ZMod n] ZMod n.

For trivial coefficients, continuous H¹ is the continuous character group. Composing with evaluation at the generator computes H¹(zHat, ZMod n) ≃ₗ[ZMod n] ZMod n. For prime p, the same calculation on Mathlib's canonical continuous-cohomology carrier shows that H¹(zHat, 𝔽_p) is nonzero. Thus the p-cohomological dimension of zHat is at least one.

In degree two, every profinite extension of zHat splits, so the explicit H²(zHat, M) vanishes for every profinite coefficient module M (TauCeti.zHat.subsingleton_H2_additive). A finite discrete module is profinite, and every class of the canonical H²(zHat, M) of a discrete torsion module M comes from a finite zHat-stable subgroup, so the canonical H²(zHat, M) vanishes for every discrete torsion M. Since the p-cohomological dimension of a compact group is detected in a single degree on finite p-primary coefficients, cd_p(zHat) ≤ 1, and hence cd_p(zHat) = 1 for every prime p and cd(zHat) = 1.

Main results

• TauCeti.zHat.continuousZModDualEquivZMod: evaluation at the generator identifies the continuous ZMod n-dual of zHat with ZMod n.
• TauCeti.zHat.h1EquivZMod: H¹(zHat, ZMod n) ≃ₗ[ZMod n] ZMod n for a trivial action.
• TauCeti.zHat.cohomFpOneEquivZMod: the corresponding equivalence on canonical continuous cohomology with 𝔽_p coefficients.
• TauCeti.zHat.one_le_cohomologicalDimensionAt: 1 ≤ cd_p(zHat) for prime p.
• TauCeti.zHat.subsingleton_continuousCohomology_two_of_isAddTorsion: the canonical H²(zHat, M) vanishes for every discrete torsion zHat-module M, in particular for every finite one.
• TauCeti.zHat.cohomologicalDimensionAt_le_one, TauCeti.zHat.cohomologicalDimensionAt_eq_one: cd_p(zHat) = 1 for every prime p, the upper bound holding for every p ≠ 0.
• TauCeti.zHat.cohomologicalDimension_eq_one: cd(zHat) = 1.

References

• J.-P. Serre, Local Fields, Chapter XIII, §1, Propositions 1–2.
• J.-P. Serre, Galois Cohomology, Ch. I, §3.4.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.7.7) and Ch. III, §3.

noncomputable def TauCeti.zHat.continuousZModDualEquivZMod (n : ℕ) [NeZero n] : continuousZModDual n ↑zHat.toProfinite.toTop ≃ₗ[ZMod n] ZMod n

Evaluation at the canonical generator identifies the continuous ZMod n-dual of zHat with ZMod n. The inverse sends a to the unique continuous character taking gen to a.

@[simp]

theorem TauCeti.zHat.continuousZModDualEquivZMod_apply (n : ℕ) [NeZero n] (χ : continuousZModDual n ↑zHat.toProfinite.toTop) : (continuousZModDualEquivZMod n) χ = Multiplicative.toAdd ((Additive.toMul χ) gen)

Evaluation under continuousZModDualEquivZMod is evaluation at zHat.gen.

@[simp]

theorem TauCeti.zHat.continuousZModDualEquivZMod_symm_apply (n : ℕ) [NeZero n] (a : ZMod n) : (continuousZModDualEquivZMod n).symm a = Additive.ofMul (lift (Multiplicative.ofAdd a))

The inverse of evaluation sends a : ZMod n to the lift taking zHat.gen to a.

noncomputable def TauCeti.zHat.h1EquivZMod (n : ℕ) [NeZero n] [DistribMulAction (↑zHat.toProfinite.toTop) (ZMod n)] [ContinuousSMul (↑zHat.toProfinite.toTop) (ZMod n)] (htriv : ∀ (g : ↑zHat.toProfinite.toTop) (a : ZMod n), g • a = a) : ContCohomology.H1 (↑zHat.toProfinite.toTop) (ZMod n) ≃ₗ[ZMod n] ZMod n

H¹(zHat, ZMod n) ≃ ZMod n for trivial coefficients, by evaluating the character represented by a cocycle at the canonical generator of zHat.

@[simp]

theorem TauCeti.zHat.h1EquivZMod_apply_mk (n : ℕ) [NeZero n] [DistribMulAction (↑zHat.toProfinite.toTop) (ZMod n)] [ContinuousSMul (↑zHat.toProfinite.toTop) (ZMod n)] (htriv : ∀ (g : ↑zHat.toProfinite.toTop) (a : ZMod n), g • a = a) (f : ↥(ContCohomology.Z1 (↑zHat.toProfinite.toTop) (ZMod n))) : (h1EquivZMod n htriv) ↑f = ↑f gen

The equivalence h1EquivZMod sends the class of a cocycle to its value at zHat.gen.

@[simp]

theorem TauCeti.zHat.h1EquivZMod_symm_apply (n : ℕ) [NeZero n] [DistribMulAction (↑zHat.toProfinite.toTop) (ZMod n)] [ContinuousSMul (↑zHat.toProfinite.toTop) (ZMod n)] (htriv : ∀ (g : ↑zHat.toProfinite.toTop) (a : ZMod n), g • a = a) (a : ZMod n) : (h1EquivZMod n htriv).symm a = ↑((ContCohomology.Z1EquivOfSmulEqSelf htriv).symm (Additive.ofMul (lift (Multiplicative.ofAdd a))))

The inverse of h1EquivZMod sends a to the class of the unique continuous character of zHat taking the canonical generator to a.

noncomputable def TauCeti.zHat.cohomFpOneEquivZMod (p : ℕ) [NeZero p] : ↑(cohomFp p (↑zHat.toProfinite.toTop) 1).toModuleCat ≃ₗ[ZMod p] ZMod p

Canonical continuous H¹(zHat, 𝔽_p) is one-dimensional. More precisely, evaluation of the corresponding continuous character at zHat.gen gives a linear equivalence with ZMod p.

@[simp]

theorem TauCeti.zHat.cohomFpOneEquivZMod_apply (p : ℕ) [NeZero p] (x : ↑(cohomFp p (↑zHat.toProfinite.toTop) 1).toModuleCat) : (cohomFpOneEquivZMod p) x = Multiplicative.toAdd ((Additive.toMul ((cohomFpLinearEquivContinuousZModDual p ↑zHat.toProfinite.toTop) x)) gen)

The canonical equivalence evaluates the continuous character attached to a cohomology class at zHat.gen.

@[simp]

theorem TauCeti.zHat.cohomFpOneEquivZMod_symm_apply (p : ℕ) [NeZero p] (a : ZMod p) : (cohomFpOneEquivZMod p).symm a = (cohomFpLinearEquivContinuousZModDual p ↑zHat.toProfinite.toTop).symm (Additive.ofMul (lift (Multiplicative.ofAdd a)))

The inverse of cohomFpOneEquivZMod sends a to the class attached to the unique continuous character of zHat taking the canonical generator to a.

@[simp]

theorem TauCeti.zHat.finrank_cohomFp_one (p : ℕ) [Fact (Nat.Prime p)] : Module.finrank (ZMod p) ↑(cohomFp p (↑zHat.toProfinite.toTop) 1).toModuleCat = 1

Canonical continuous H¹(zHat, 𝔽_p) has dimension one for prime p.

theorem TauCeti.zHat.nontrivial_cohomFp_one (p : ℕ) [Fact (Nat.Prime p)] : Nontrivial ↑(cohomFp p (↑zHat.toProfinite.toTop) 1).toModuleCat

Canonical continuous H¹(zHat, 𝔽_p) is nontrivial for prime p.

theorem TauCeti.zHat.one_le_cohomologicalDimensionAt (p : ℕ) [Fact (Nat.Prime p)] : 1 ≤ cohomologicalDimensionAt p ↑zHat.toProfinite.toTop

The p-cohomological dimension of the profinite integers is at least one. The nonzero class in H¹(zHat, 𝔽_p) is detected by evaluation at the canonical generator.

theorem TauCeti.zHat.subsingleton_continuousCohomology_two_of_isAddTorsion (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction (↑zHat.toProfinite.toTop) M] [ContinuousSMul (↑zHat.toProfinite.toTop) M] (hM : IsAddTorsion M) : Subsingleton ↑(continuousCohomology 2 (ofDiscreteModule ℤ (↑zHat.toProfinite.toTop) M)).toModuleCat

The canonical H²(zHat, M) vanishes for every discrete torsion module M, in particular for every finite discrete zHat-module. Each class comes from a finite zHat-stable subgroup N ≤ M, and the explicit H²(zHat, N) vanishes because N is profinite.

theorem TauCeti.zHat.cohomologicalDimensionAt_le_one {p : ℕ} (hp : p ≠ 0) : cohomologicalDimensionAt p ↑zHat.toProfinite.toTop ≤ 1

The p-cohomological dimension of the profinite integers is at most one, for every p ≠ 0.

@[simp]

theorem TauCeti.zHat.cohomologicalDimensionAt_eq_one (p : ℕ) [Fact (Nat.Prime p)] : cohomologicalDimensionAt p ↑zHat.toProfinite.toTop = 1

The p-cohomological dimension of the profinite integers is one, for every prime p.

@[simp]

theorem TauCeti.zHat.cohomologicalDimension_eq_one : cohomologicalDimension ↑zHat.toProfinite.toTop = 1

The cohomological dimension of the profinite integers is one.