The prescription property for free pro-p groups

Every continuous character χ : F →ₜ* ℤ_pˣ of a free pro-p group F = freeProP p X has the prescription property (TauCeti.HasPrescriptionProperty): every reduction H¹(F, I(χ)/pⁱ) → H¹(F, I(χ)/p) is surjective. This is the free case of Labute's condition on the orientation of a Demushkin group. It is an instance of the general fact that a surjective coefficient map induces a surjection on H¹ of a free pro-p group (TauCeti.freeProP.explicitCoeff1_surjective): a continuous 1-cocycle on F is determined by its values on the generators and takes any prescribed values there, so lifting a cocycle is lifting its values on the generators.

Read through Labute's third formulation of the property, this says that for a free pro-p group of finite rank and any continuous character χ, every tuple of p-adic integers is the tuple of values on the generators of a continuous crossed homomorphism F → ℤ_p for χ, a continuous F with F (x * y) = χ x * F y + F x (TauCeti.IsCrossedHom).

Main results

• TauCeti.freeProP.hasPrescriptionProperty: every continuous character of a free pro-p group has the prescription property.
• TauCeti.freeProP.exists_continuous_isCrossedHom_forall_apply_of_eq: on a free pro-p group of finite rank, a continuous crossed homomorphism to ℤ_p for any continuous character takes any prescribed values on the generators.
• TauCeti.freeProP.crossedHom: that crossed homomorphism, with TauCeti.IsCrossedHom.eq_crossedHom its uniqueness and TauCeti.freeProP.crossedHom_apply_eq_sum the linearity of its values in the prescribed values on the generators.
• TauCeti.IsCrossedHom.pow_dvd_sub_of_forall_of_eq: two continuous crossed homomorphisms with the same values on the generators, for characters congruent modulo p ^ k, are congruent modulo p ^ k.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §2 and Theorem 4.
• J.-P. Serre, Structure de certains pro-p-groupes, Séminaire Bourbaki 252 (1962/63).

theorem TauCeti.freeProP.hasPrescriptionProperty {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} (χ : freeProP p X →ₜ* ℤ_[p]ˣ) : HasPrescriptionProperty χ

Every continuous character of a free pro-p group has the prescription property. The reductions I(χ)/pⁱ → I(χ)/p are surjective, and a surjective coefficient map induces a surjection on H¹ of a free pro-p group.

theorem TauCeti.freeProP.exists_continuous_isCrossedHom_forall_apply_of_eq {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] (χ : freeProP p X →ₜ* ℤ_[p]ˣ) (c : X → ℤ_[p]) : ∃ (F : freeProP p X → ℤ_[p]), Continuous F ∧ IsCrossedHom (⇑χ) F ∧ ∀ (x : X), F (of x) = c x

Continuous crossed homomorphisms of a free pro-p group of finite rank take prescribed values on the generators. For F = freeProP p X with X finite, a continuous character χ : F →ₜ* ℤ_pˣ and any c : X → ℤ_p, there is a continuous F : freeProP p X → ℤ_p with F (x * y) = χ x * F y + F x and F (of x) = c x.

noncomputable def TauCeti.freeProP.crossedHom {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] (χ : freeProP p X →ₜ* ℤ_[p]ˣ) (c : X → ℤ_[p]) : freeProP p X → ℤ_[p]

The continuous crossed homomorphism with prescribed values on the generators. For a continuous character χ of the free pro-p group on a finite type X and c : X → ℤ_p, the continuous crossed homomorphism F : freeProP p X → ℤ_p for χ with F (of x) = c x. It is the only one (TauCeti.IsCrossedHom.eq_crossedHom), and its value at a fixed element is ℤ_p-linear in c (TauCeti.freeProP.crossedHom_apply_eq_sum).

Equations

• TauCeti.freeProP.crossedHom χ c = ⋯.choose

theorem TauCeti.freeProP.continuous_crossedHom {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] (χ : freeProP p X →ₜ* ℤ_[p]ˣ) (c : X → ℤ_[p]) : Continuous (crossedHom χ c)

theorem TauCeti.freeProP.isCrossedHom_crossedHom {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] (χ : freeProP p X →ₜ* ℤ_[p]ˣ) (c : X → ℤ_[p]) : IsCrossedHom (⇑χ) (crossedHom χ c)

@[simp]

theorem TauCeti.freeProP.crossedHom_of {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] (χ : freeProP p X →ₜ* ℤ_[p]ˣ) (c : X → ℤ_[p]) (x : X) : crossedHom χ c (of x) = c x

theorem TauCeti.IsCrossedHom.eq_crossedHom {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Finite X] {χ : freeProP p X →ₜ* ℤ_[p]ˣ} {F : freeProP p X → ℤ_[p]} (hF : IsCrossedHom (⇑χ) F) (hFc : Continuous F) : F = freeProP.crossedHom χ fun (x : X) => F (freeProP.of x)

A continuous crossed homomorphism is determined by its values on the generators: it is crossedHom χ of those values.

@[simp]

theorem TauCeti.freeProP.crossedHom_single_freeProPGen {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (χ : freeProP p (Fin n) →ₜ* ℤ_[p]ˣ) (k : Fin n) (m : ℕ) : crossedHom χ (Pi.single k 1) (freeProPGen p n m) = if m = ↑k then 1 else 0

The Kronecker crossed homomorphism D_k, with D_k(x_j) = δ_{kj}, on the ℕ-indexed generators.

theorem TauCeti.IsCrossedHom.pow_dvd_sub_of_forall_of_eq {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} {χ χ' : freeProP p X →ₜ* ℤ_[p]ˣ} {k : ℕ} (hχ : ∀ (x : X), ↑p ^ k ∣ ↑(χ' (freeProP.of x)) - ↑(χ (freeProP.of x))) {f f' : freeProP p X → ℤ_[p]} (hf : IsCrossedHom (⇑χ) f) (hf' : IsCrossedHom (⇑χ') f') (hfc : Continuous f) (hf'c : Continuous f') (hff' : ∀ (x : X), f (freeProP.of x) = f' (freeProP.of x)) (g : freeProP p X) : ↑p ^ k ∣ f' g - f g

Crossed homomorphisms with the same values on the generators, for characters congruent modulo p ^ k, are congruent modulo p ^ k: their truncations modulo p ^ k are continuous crossed homomorphisms for the same character of F agreeing on the generators.

theorem TauCeti.freeProP.crossedHom_apply_eq_sum {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Fintype X] [DecidableEq X] (χ : freeProP p X →ₜ* ℤ_[p]ˣ) (c : X → ℤ_[p]) (g : freeProP p X) : crossedHom χ c g = ∑ x : X, c x * crossedHom χ (Pi.single x 1) g

The value of a crossed homomorphism is linear in its values on the generators: crossedHom χ c is the ℤ_p-combination, with coefficients c x, of the Kronecker crossed homomorphisms taking the value 1 at one generator and 0 at the others.