Rational characters of the profinite integers

Evaluation at the canonical generator identifies continuous characters of zHat with the rational circle ℚ/ℤ, given the discrete topology. Every rational-circle element has finite order, so its character factors through a finite cyclic quotient of zHat. In particular, the first continuous cohomology of zHat with trivial discrete ℚ/ℤ coefficients is ℚ/ℤ.

This is the degree-one term in the long exact sequence of 0 → ℤ → ℚ → ℚ/ℤ → 0 used to calculate H²(zHat, ℤ).

References

• J.-P. Serre, Local Fields, Chapter XIII, §1, Propositions 1–2.

@[reducible, inline]

abbrev TauCeti.zHat.DiscreteRatCircle : Type

The rational circle with the discrete topology, as a continuous cohomology coefficient.

@[instance_reducible]

instance TauCeti.zHat.instAddCommGroupDiscreteRatCircle : AddCommGroup DiscreteRatCircle

@[instance_reducible]

instance TauCeti.zHat.instDistribMulActionCarrierToTopTotallyDisconnectedSpaceToProfiniteDiscreteRatCircle : DistribMulAction (↑zHat.toProfinite.toTop) DiscreteRatCircle

The trivial action of the profinite integers on the discrete rational circle.

instance TauCeti.zHat.instContinuousSMulCarrierToTopTotallyDisconnectedSpaceToProfiniteDiscreteRatCircle : ContinuousSMul (↑zHat.toProfinite.toTop) DiscreteRatCircle

def TauCeti.zHat.discreteRatCircleEquiv : DiscreteRatCircle ≃+ AddCircle 1

Forget the discrete topology on the rational circle.

theorem TauCeti.zHat.exists_ratCharacter_gen (a : DiscreteRatCircle) : ∃ (χ : ↑zHat.toProfinite.toTop →ₜ* Multiplicative DiscreteRatCircle), χ gen = Multiplicative.ofAdd a

Every element of the discrete rational circle is the value at zHat.gen of a continuous character of zHat.

noncomputable def TauCeti.zHat.ratCharacterEquiv : Additive (↑zHat.toProfinite.toTop →ₜ* Multiplicative DiscreteRatCircle) ≃+ AddCircle 1

Evaluation at the generator identifies continuous rational-circle characters of zHat with ℚ/ℤ. The target carries the discrete topology.

@[simp]

theorem TauCeti.zHat.ratCharacterEquiv_apply (χ : Additive (↑zHat.toProfinite.toTop →ₜ* Multiplicative DiscreteRatCircle)) : ratCharacterEquiv χ = discreteRatCircleEquiv (Multiplicative.toAdd ((Additive.toMul χ) gen))

A continuous rational-circle character is evaluated at the canonical generator.

@[simp]

theorem TauCeti.zHat.ratCharacterEquiv_symm_apply_gen (a : AddCircle 1) : discreteRatCircleEquiv (Multiplicative.toAdd ((Additive.toMul (ratCharacterEquiv.symm a)) gen)) = a

The unique character taking the value a at the generator is the inverse of evaluation.

noncomputable def TauCeti.zHat.h1EquivRatCircle : ↑(continuousCohomology 1 (ofDiscreteModule ℤ (↑zHat.toProfinite.toTop) DiscreteRatCircle)).toModuleCat ≃+ AddCircle 1

First continuous cohomology of the profinite integers with trivial discrete ℚ/ℤ coefficients is the rational circle, by evaluating the associated character at gen.

@[simp]

theorem TauCeti.zHat.h1EquivRatCircle_apply_mk (f : ↥(ContCohomology.Z1 (↑zHat.toProfinite.toTop) DiscreteRatCircle)) : h1EquivRatCircle ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (ofDiscreteModule ℤ (↑zHat.toProfinite.toTop) DiscreteRatCircle).homogeneousCochains 1)) ((ContCohomology.cocycleEquiv1 (↑zHat.toProfinite.toTop) DiscreteRatCircle) f)) = discreteRatCircleEquiv (↑f gen)

On a continuous one-cocycle, the cohomology equivalence returns its value at gen.

theorem TauCeti.zHat.nontrivial_continuousCohomology_one_discreteRatCircle : Nontrivial ↑(continuousCohomology 1 (ofDiscreteModule ℤ (↑zHat.toProfinite.toTop) DiscreteRatCircle)).toModuleCat

In particular, discrete ℚ/ℤ has nonzero first continuous cohomology over zHat.

theorem TauCeti.zHat.bijective_ratCircleCharacterEvaluation (C : Type v) [AddCommGroup C] [TopologicalSpace C] [DiscreteTopology C] (e : C ≃+ AddCircle 1) : Function.Bijective fun (χ : Additive (↑zHat.toProfinite.toTop →ₜ* Multiplicative C)) => e (Multiplicative.toAdd ((Additive.toMul χ) gen))

Evaluation at the generator is bijective for any discrete model of the rational circle. The coefficient universe may differ from that of the profinite integers.