The prescription property of a character

Let G be a topological group and χ : G →ₜ* ℤ_pˣ a continuous character, with twisted coefficient modules I(χ)/pⁱ = TauCeti.ZModTwist χ i, on which G acts by g • x = χ(g) x. The equivariant reductions I(χ)/pⁱ → I(χ)/pʲ for j ≤ i induce maps on continuous cohomology.

A character has the prescription property when every reduction H¹(G, I(χ)/pⁱ) → H¹(G, I(χ)/p) is surjective: every continuous crossed homomorphism to I(χ)/p lifts, modulo principal ones, to a continuous crossed homomorphism to I(χ)/pⁱ. This is Labute's condition on the orientation of a Demushkin group: such a group has exactly one continuous character with the prescription property, its canonical character (Labute, Thm 4). Here the property is defined, against the explicit model of continuous cohomology; it holds for every continuous character of a free pro-p group (TauCeti.freeProP.hasPrescriptionProperty, in TauCeti.Topology.Algebra.Group.Profinite.Free.Prescription). I(χ)/p is ZModTwist χ 1, the module at i = 1, with carrier ZMod (p ^ 1).

The property has two cohomological reformulations (Labute, Prop. 6), both read off the long exact sequences of the short exact sequences 0 → I(χ)/pⁱ → I(χ)/pⁱ⁺¹ → I(χ)/p → 0: it says that every connecting map δ¹ : H¹(G, I(χ)/p) → H²(G, I(χ)/pⁱ) vanishes, and that multiplication by p is injective on H²(G, I(χ)/pⁱ) → H²(G, I(χ)/pⁱ⁺¹) for every i. Once it holds, every reduction H¹(G, I(χ)/pⁿ) → H¹(G, I(χ)/pʲ) between two levels is surjective, not only those onto the bottom level, so that a class at one level lifts through the whole tower of coefficients; this is the form in which compatible systems of crossed homomorphisms are built.

Main definitions

• TauCeti.HasPrescriptionProperty: surjectivity of every H¹(G, I(χ)/pⁱ) → H¹(G, I(χ)/p).

Main results

• TauCeti.HasPrescriptionProperty.surjective_explicitCoeff1_reduce: every reduction H¹(G, I(χ)/pⁿ) → H¹(G, I(χ)/pʲ), j ≤ n, is surjective.
• TauCeti.HasPrescriptionProperty.exists_forall_reduce_eq: under the prescription property a continuous 1-cocycle with values in I(χ)/pʲ is the pointwise reduction of one with values in I(χ)/pⁿ, for j ≤ n, exactly and not only up to a coboundary.
• TauCeti.hasPrescriptionProperty_iff_forall_explicitDelta1_eq_zero: the property is the vanishing of the connecting maps H¹(G, I(χ)/p) → H²(G, I(χ)/pⁱ).
• TauCeti.hasPrescriptionProperty_iff_forall_injective_explicitCoeff2_mulPow: the property is the injectivity of multiplication by p on H²(G, I(χ)/pⁱ) → H²(G, I(χ)/pⁱ⁺¹).

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §2, Proposition 6 and Theorem 4.

def TauCeti.HasPrescriptionProperty {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) : Prop

The prescription property of a continuous character χ : G →ₜ* ℤ_pˣ (Labute's condition on the orientation of a Demushkin group): every reduction H¹(G, I(χ)/pⁱ) → H¹(G, I(χ)/p), for i ≥ 1, is surjective. In cocycle terms, every continuous crossed homomorphism G → I(χ)/p is, modulo principal ones, the reduction of a continuous crossed homomorphism G → I(χ)/pⁱ.

Equations

• TauCeti.HasPrescriptionProperty χ = ∀ (i : ℕ) (hi : 1 ≤ i), Function.Surjective ⇑(TauCeti.ContCohomology.explicitCoeff1 G (TauCeti.ZModTwist χ i) (TauCeti.ZModTwist.reduce χ hi) ⋯)

theorem TauCeti.hasPrescriptionProperty_iff {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] (χ : G →ₜ* ℤ_[p]ˣ) : HasPrescriptionProperty χ ↔ ∀ (i : ℕ) (hi : 1 ≤ i), Function.Surjective ⇑(ContCohomology.explicitCoeff1 G (ZModTwist χ i) (ZModTwist.reduce χ hi) ⋯)

The defining property of HasPrescriptionProperty, available to modules that only see the declaration and not its body.

Lifting through the whole tower of coefficients

The defining property lifts classes from the bottom level I(χ)/p; by exactness at H¹(G, I(χ)/pʲ⁺¹) of the sequence 0 → I(χ)/p → I(χ)/pʲ⁺¹ → I(χ)/pʲ → 0 and induction on j, classes lift between any two levels.

theorem TauCeti.HasPrescriptionProperty.surjective_explicitCoeff1_reduce {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {χ : G →ₜ* ℤ_[p]ˣ} (hχ : HasPrescriptionProperty χ) {j n : ℕ} (h : j ≤ n) : Function.Surjective ⇑(ContCohomology.explicitCoeff1 G (ZModTwist χ n) (ZModTwist.reduce χ h) ⋯)

Every reduction H¹(G, I(χ)/pⁿ) → H¹(G, I(χ)/pʲ) is surjective under the prescription property, not only the reductions onto the bottom level I(χ)/p.

theorem TauCeti.HasPrescriptionProperty.exists_forall_reduce_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {χ : G →ₜ* ℤ_[p]ˣ} (hχ : HasPrescriptionProperty χ) {j n : ℕ} (h : j ≤ n) (f : ↥(ContCohomology.Z1 G (ZModTwist χ j))) : ∃ (f' : ↥(ContCohomology.Z1 G (ZModTwist χ n))), ∀ (x : G), (ZModTwist.reduce χ h) (↑f' x) = ↑f x

Cocycles lift exactly under the prescription property. A continuous 1-cocycle f : G → I(χ)/pʲ is the pointwise reduction of a continuous 1-cocycle G → I(χ)/pⁿ, j ≤ n, exactly and not only up to a coboundary, which is all that the surjectivity on H¹ defining the prescription property provides.

theorem TauCeti.HasPrescriptionProperty.explicitDelta1_shortExact_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {χ : G →ₜ* ℤ_[p]ˣ} (hχ : HasPrescriptionProperty χ) [ContinuousMul G] {i j n : ℕ} (h : i + j = n) : (ZModTwist.shortExact χ h).explicitDelta1 = 0

Under the prescription property every connecting map δ¹ : H¹(G, I(χ)/pʲ) → H²(G, I(χ)/pⁱ) of a sequence 0 → I(χ)/pⁱ → I(χ)/pⁱ⁺ʲ → I(χ)/pʲ → 0 vanishes.

theorem TauCeti.HasPrescriptionProperty.injective_explicitCoeff2_mulPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {χ : G →ₜ* ℤ_[p]ˣ} (hχ : HasPrescriptionProperty χ) [ContinuousMul G] {i j n : ℕ} (h : i + j = n) : Function.Injective ⇑(ContCohomology.explicitCoeff2 G (ZModTwist χ i) (ZModTwist.mulPow χ h) ⋯)

Under the prescription property multiplication by pʲ is injective on H²(G, I(χ)/pⁱ) → H²(G, I(χ)/pⁱ⁺ʲ).

The cohomological reformulations (Labute, Prop. 6)

theorem TauCeti.hasPrescriptionProperty_iff_forall_explicitDelta1_eq_zero {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (χ : G →ₜ* ℤ_[p]ˣ) : HasPrescriptionProperty χ ↔ ∀ (i n : ℕ) (h : i + 1 = n), (ZModTwist.shortExact χ h).explicitDelta1 = 0

The prescription property is the vanishing of the connecting maps δ¹ : H¹(G, I(χ)/p) → H²(G, I(χ)/pⁱ) of the sequences 0 → I(χ)/pⁱ → I(χ)/pⁱ⁺¹ → I(χ)/p → 0, for every i (Labute, Prop. 6).

theorem TauCeti.hasPrescriptionProperty_iff_forall_injective_explicitCoeff2_mulPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] (χ : G →ₜ* ℤ_[p]ˣ) : HasPrescriptionProperty χ ↔ ∀ (i n : ℕ) (h : i + 1 = n), Function.Injective ⇑(ContCohomology.explicitCoeff2 G (ZModTwist χ i) (ZModTwist.mulPow χ h) ⋯)

The prescription property is the injectivity of multiplication by p on H², H²(G, I(χ)/pⁱ) → H²(G, I(χ)/pⁱ⁺¹), for every i (Labute, Prop. 6).