The prescription property as prescribed values of crossed homomorphisms

Let G be a pro-p group, χ : G →ₜ* ℤ_pˣ a continuous character and I(χ)/pⁱ = ZModTwist χ i the twisted coefficients ℤ/pⁱ with g acting by χ(g). Labute's prescription property of χ (TauCeti.HasPrescriptionProperty) asks that every reduction H¹(G, I(χ)/pⁱ) → H¹(G, I(χ)/p) be surjective. This file proves its third formulation (Labute, Prop. 6, condition (iii)): for a topologically finitely generated pro-p group and a minimal generating tuple g₁, …, gₙ, the property holds exactly when every tuple c₁, …, cₙ of p-adic integers is the tuple of values of a compatible system of continuous crossed homomorphisms fᵢ : G → I(χ)/pⁱ, fᵢ(gⱼ) = cⱼ mod pⁱ. Such a compatible system is the same thing as a continuous crossed homomorphism F : G → ℤ_p, F(xy) = χ(x) F(y) + F(x), with values F(gⱼ) = cⱼ, since ℤ_p is the inverse limit of the ℤ/pⁱ; both forms are proved, and the second is the one downstream applications read: it converts Kummer-compatible finite-level data into prescribed values F(gⱼ) of a continuous crossed homomorphism F : G → ℤ_p for χ.

The bottom level I(χ)/p is special: a pro-p group acts trivially on it, because a continuous character of a pro-p group takes values in the principal units 1 + pℤ_p (TauCeti.IsProP.charScalar_one_eq_one), so the continuous 1-cocycles with values in I(χ)/p are the continuous homomorphisms G → 𝔽_p. These are determined by their values on a topological generating set, and take any prescribed values on a family that is linearly independent in the Frattini quotient (TauCeti.IsTopologicallyFinitelyGenerated.exists_continuousMonoidHom_apply_eq). This is why the hypotheses of the two directions differ: the construction of a compatible system with prescribed values needs linear independence of the Frattini classes of g, while the converse needs only that g generates G topologically.

Main results

• TauCeti.HasPrescriptionProperty.exists_forall_reduce_eq_and_val_eq: under the prescription property, every tuple c : ι → ℤ_p is realized on a family g with linearly independent Frattini classes by a compatible system of continuous 1-cocycles fᵢ : G → I(χ)/pⁱ.
• TauCeti.hasPrescriptionProperty_of_forall_exists_forall_reduce_eq_and_val_eq: conversely, if every tuple is so realized on a topological generating family, the character has the prescription property.
• TauCeti.IsProP.hasPrescriptionProperty_iff_forall_exists_forall_reduce_eq_and_val_eq: the equivalence, for the lifts of a basis of the Frattini quotient, that is for a minimal generating tuple.
• TauCeti.exists_continuous_forall_mul_eq_and_forall_toZModPow_eq_val and TauCeti.exists_forall_reduce_eq_and_forall_val_eq_toZModPow: a compatible system of continuous 1-cocycles with values in the I(χ)/pⁱ is the family of reductions of a continuous crossed homomorphism G → ℤ_p, and conversely.
• TauCeti.IsProP.hasPrescriptionProperty_iff_forall_exists_continuous_forall_mul_eq_and_apply_eq: the prescription property is the existence, for every tuple c, of a continuous crossed homomorphism F : G → ℤ_p for χ with F(gⱼ) = cⱼ on a minimal generating tuple.

References

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

Compatible systems with prescribed values

theorem TauCeti.HasPrescriptionProperty.exists_succ_forall_reduce_eq_and_val_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {χ : G →ₜ* ℤ_[p]ˣ} (hχ : HasPrescriptionProperty χ) (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) {ι : Type u_1} {g : ι → G} (hg : LinearIndependent (ZMod p) fun (k : ι) => Additive.ofMul ((QuotientGroup.mk' (proPFrattini p G)) (g k))) (c : ι → ℤ_[p]) {i : ℕ} (f : ↥(ContCohomology.Z1 G (ZModTwist χ i))) (hf : ∀ (k : ι), (↑f (g k)).val = (PadicInt.toZModPow i) (c k)) : ∃ (f' : ↥(ContCohomology.Z1 G (ZModTwist χ (i + 1)))), (∀ (x : G), (ZModTwist.reduce χ ⋯) (↑f' x) = ↑f x) ∧ ∀ (k : ι), (↑f' (g k)).val = (PadicInt.toZModPow (i + 1)) (c k)

One step of the compatible system. Under the prescription property, a continuous 1-cocycle f : G → I(χ)/pⁱ with values c k mod pⁱ on a family g with linearly independent Frattini classes is the reduction of a continuous 1-cocycle G → I(χ)/pⁱ⁺¹ with values c k mod pⁱ⁺¹.

theorem TauCeti.HasPrescriptionProperty.exists_forall_reduce_eq_and_val_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {χ : G →ₜ* ℤ_[p]ˣ} (hχ : HasPrescriptionProperty χ) (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) {ι : Type u_1} {g : ι → G} (hg : LinearIndependent (ZMod p) fun (k : ι) => Additive.ofMul ((QuotientGroup.mk' (proPFrattini p G)) (g k))) (c : ι → ℤ_[p]) : ∃ (f : (i : ℕ) → ↥(ContCohomology.Z1 G (ZModTwist χ i))), (∀ ⦃i j : ℕ⦄ (h : j ≤ i) (x : G), (ZModTwist.reduce χ h) (↑(f i) x) = ↑(f j) x) ∧ ∀ (i : ℕ) (k : ι), (↑(f i) (g k)).val = (PadicInt.toZModPow i) (c k)

The prescription property gives compatible systems of crossed homomorphisms with prescribed values (Labute, Prop. 6, (i) ⇒ (iii)). Let G be a topologically finitely generated pro-p group, χ a continuous character with the prescription property and g : ι → G a family whose classes in the Frattini quotient are linearly independent over 𝔽_p. Then for every c : ι → ℤ_p there are continuous 1-cocycles fᵢ : G → I(χ)/pⁱ, compatible under the reductions I(χ)/pⁱ → I(χ)/pʲ, with fᵢ (g k) = c k mod pⁱ for every i and k.

Prescribed values give the prescription property

theorem TauCeti.hasPrescriptionProperty_of_forall_exists_forall_reduce_eq_and_val_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {χ : G →ₜ* ℤ_[p]ˣ} {ι : Type u_1} {g : ι → G} (hg : (Subgroup.closure (Set.range g)).topologicalClosure = ⊤) (h : ∀ (c : ι → ℤ_[p]), ∃ (f : (i : ℕ) → ↥(ContCohomology.Z1 G (ZModTwist χ i))), (∀ ⦃i j : ℕ⦄ (h : j ≤ i) (x : G), (ZModTwist.reduce χ h) (↑(f i) x) = ↑(f j) x) ∧ ∀ (i : ℕ) (k : ι), (↑(f i) (g k)).val = (PadicInt.toZModPow i) (c k)) : HasPrescriptionProperty χ

Compatible systems with prescribed values give the prescription property (Labute, Prop. 6, (iii) ⇒ (i)). If g generates G topologically and every c : ι → ℤ_p is the tuple of values on g of a compatible system of continuous 1-cocycles fᵢ : G → I(χ)/pⁱ, then χ has the prescription property. No pro-p or finite-generation hypothesis on G is needed.

theorem TauCeti.IsProP.hasPrescriptionProperty_iff_forall_exists_forall_reduce_eq_and_val_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) {ι : Type u_1} (b : Module.Basis ι (ZMod p) (Additive (G ⧸ proPFrattini p G))) {g : ι → G} (hgb : ∀ (k : ι), Additive.ofMul ((QuotientGroup.mk' (proPFrattini p G)) (g k)) = b k) (χ : G →ₜ* ℤ_[p]ˣ) : HasPrescriptionProperty χ ↔ ∀ (c : ι → ℤ_[p]), ∃ (f : (i : ℕ) → ↥(ContCohomology.Z1 G (ZModTwist χ i))), (∀ ⦃i j : ℕ⦄ (h : j ≤ i) (x : G), (ZModTwist.reduce χ h) (↑(f i) x) = ↑(f j) x) ∧ ∀ (i : ℕ) (k : ι), (↑(f i) (g k)).val = (PadicInt.toZModPow i) (c k)

Labute's third formulation of the prescription property (Labute, Prop. 6, (i) ⇔ (iii)). Let G be a topologically finitely generated pro-p group and g : ι → G a minimal generating tuple, that is a family of lifts of a basis b of the Frattini quotient over 𝔽_p. A continuous character χ has the prescription property exactly when every c : ι → ℤ_p is the tuple of values on g of a compatible system of continuous 1-cocycles fᵢ : G → I(χ)/pⁱ.

Crossed homomorphisms with values in ℤ_p

A compatible system of continuous 1-cocycles fᵢ : G → I(χ)/pⁱ is the family of reductions of a single continuous map F : G → ℤ_p satisfying the crossed-homomorphism identity F (x * y) = χ x * F y + F x for the action of G on ℤ_p through χ, and conversely. The identity is written out rather than expressed through a module structure on ℤ_p, which would install a second action on a Mathlib type.

theorem TauCeti.exists_continuous_forall_mul_eq_and_forall_toZModPow_eq_val {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {χ : G →ₜ* ℤ_[p]ˣ} (f : (i : ℕ) → ↥(ContCohomology.Z1 G (ZModTwist χ i))) (hf : ∀ ⦃i j : ℕ⦄ (h : j ≤ i) (x : G), (ZModTwist.reduce χ h) (↑(f i) x) = ↑(f j) x) : ∃ (F : G → ℤ_[p]), Continuous F ∧ (∀ (x y : G), F (x * y) = ↑(χ x) * F y + F x) ∧ ∀ (i : ℕ) (x : G), (PadicInt.toZModPow i) (F x) = (↑(f i) x).val

A compatible system of crossed homomorphisms assembles into a p-adic one. Continuous 1-cocycles fᵢ : G → I(χ)/pⁱ compatible under the reductions are the reductions modulo pⁱ of a continuous map F : G → ℤ_p with F (x * y) = χ x * F y + F x.

theorem TauCeti.exists_forall_reduce_eq_and_forall_val_eq_toZModPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {χ : G →ₜ* ℤ_[p]ˣ} (F : G → ℤ_[p]) (hFc : Continuous F) (hF : ∀ (x y : G), F (x * y) = ↑(χ x) * F y + F x) : ∃ (f : (i : ℕ) → ↥(ContCohomology.Z1 G (ZModTwist χ i))), (∀ ⦃i j : ℕ⦄ (h : j ≤ i) (x : G), (ZModTwist.reduce χ h) (↑(f i) x) = ↑(f j) x) ∧ ∀ (i : ℕ) (x : G), (↑(f i) x).val = (PadicInt.toZModPow i) (F x)

A p-adic crossed homomorphism reduces to a compatible system. A continuous F : G → ℤ_p with F (x * y) = χ x * F y + F x reduces modulo the pⁱ to continuous 1-cocycles fᵢ : G → I(χ)/pⁱ, compatible under the reductions, with fᵢ x = F x mod pⁱ.

theorem TauCeti.HasPrescriptionProperty.exists_continuous_forall_mul_eq_and_apply_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {χ : G →ₜ* ℤ_[p]ˣ} [IsTopologicalGroup G] [CompactSpace G] {ι : Type u_1} {g : ι → G} (hχ : HasPrescriptionProperty χ) (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hg : LinearIndependent (ZMod p) fun (k : ι) => Additive.ofMul ((QuotientGroup.mk' (proPFrattini p G)) (g k))) (c : ι → ℤ_[p]) : ∃ (F : G → ℤ_[p]), Continuous F ∧ (∀ (x y : G), F (x * y) = ↑(χ x) * F y + F x) ∧ ∀ (k : ι), F (g k) = c k

The prescription property gives p-adic crossed homomorphisms with prescribed values. Let G be a topologically finitely generated pro-p group, χ a continuous character with the prescription property and g : ι → G a family whose classes in the Frattini quotient are linearly independent over 𝔽_p. Then for every c : ι → ℤ_p there is a continuous F : G → ℤ_p with F (x * y) = χ x * F y + F x and F (g k) = c k.

theorem TauCeti.hasPrescriptionProperty_of_forall_exists_continuous_forall_mul_eq_and_apply_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] {χ : G →ₜ* ℤ_[p]ˣ} [IsTopologicalGroup G] {ι : Type u_1} {g : ι → G} (hg : (Subgroup.closure (Set.range g)).topologicalClosure = ⊤) (h : ∀ (c : ι → ℤ_[p]), ∃ (F : G → ℤ_[p]), Continuous F ∧ (∀ (x y : G), F (x * y) = ↑(χ x) * F y + F x) ∧ ∀ (k : ι), F (g k) = c k) : HasPrescriptionProperty χ

p-adic crossed homomorphisms with prescribed values give the prescription property. If g generates G topologically and every c : ι → ℤ_p is the tuple of values on g of a continuous F : G → ℤ_p with F (x * y) = χ x * F y + F x, then χ has the prescription property. No pro-p or finite-generation hypothesis on G is needed.

theorem TauCeti.IsProP.hasPrescriptionProperty_iff_forall_exists_continuous_forall_mul_eq_and_apply_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {ι : Type u_1} {g : ι → G} [TotallyDisconnectedSpace G] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (b : Module.Basis ι (ZMod p) (Additive (G ⧸ proPFrattini p G))) (hgb : ∀ (k : ι), Additive.ofMul ((QuotientGroup.mk' (proPFrattini p G)) (g k)) = b k) (χ : G →ₜ* ℤ_[p]ˣ) : HasPrescriptionProperty χ ↔ ∀ (c : ι → ℤ_[p]), ∃ (F : G → ℤ_[p]), Continuous F ∧ (∀ (x y : G), F (x * y) = ↑(χ x) * F y + F x) ∧ ∀ (k : ι), F (g k) = c k

Labute's third formulation of the prescription property, p-adic form (Labute, Prop. 6, (i) ⇔ (iii)). Let G be a topologically finitely generated pro-p group and g : ι → G a minimal generating tuple, that is a family of lifts of a basis b of the Frattini quotient over 𝔽_p. A continuous character χ has the prescription property exactly when every c : ι → ℤ_p is the tuple of values on g of a continuous crossed homomorphism F : G → ℤ_p for χ, that is a continuous F with F (x * y) = χ x * F y + F x.