Relations from cocycles on a free pro-p group

We construct a locally constant cocycle on a free pro-p group with standard basis values on the free generators. A locally constant cocycle sends the kernel of a presentation to the span of its values on normal generators. When it takes standard basis values on free generators, the relation module is contained in the span of those values. Its values on Frattini elements have zero augmentation in every coordinate. These results supply the relation and augmentation hypotheses of the algebraic Golod–Shafarevich inequality for A = 𝔽_p[G], as used in TauCeti.Topology.Algebra.Group.Profinite.ProP.GolodShafarevich.

Main results

• TauCeti.freeProP.exists_locallyConstant_cocycle_forall_apply_of_eq: construction with standard basis values on the free generators.
• TauCeti.freeProP.mem_span_range_cocycle_of_map_eq_one: the kernel maps into the span of the cocycle values on normal generators.
• TauCeti.freeProP.relationModule_le_span: containment of the relation module in that span.
• TauCeti.freeProP.augmentation_cocycle_eq_zero_of_mem_proPFrattini: vanishing of every coordinate's augmentation on Frattini elements.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.9.7).
• L. Ribes and P. Zalesskii, Profinite Groups, Theorem 7.8.5.

theorem TauCeti.freeProP.exists_locallyConstant_cocycle_forall_apply_of_eq {p : ℕ} [Fact (Nat.Prime p)] {X G : Type u} [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [Finite X] [DecidableEq X] (π : freeProP p X →ₜ* G) : ∃ (D : freeProP p X → X → MonoidAlgebra (ZMod p) G), IsLocallyConstant D ∧ (∀ (g h : freeProP p X), D (g * h) = MonoidAlgebra.single (π g) 1 • D h + D g) ∧ ∀ (i : X), D (of i) = Pi.single i 1

The cocycle D : F → 𝔽_p[G]^X of a continuous homomorphism π : F → G from a free pro-p group to a finite discrete group, for the action of F on 𝔽_p[G]^X by left multiplication through π: it is locally constant and sends the generators to the standard basis vectors.

theorem TauCeti.freeProP.mem_span_range_cocycle_of_map_eq_one {p : ℕ} [Fact (Nat.Prime p)] {X G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G] {π : freeProP p X →ₜ* G} {D : freeProP p X → X → MonoidAlgebra (ZMod p) G} (hcoc : ∀ (g h : freeProP p X), D (g * h) = MonoidAlgebra.single (π g) 1 • D h + D g) {s : Finset (freeProP p X)} (hs : ∀ (w : freeProP p X), π w = 1 ↔ w ∈ (Subgroup.normalClosure ↑s).topologicalClosure) (hD : IsLocallyConstant D) {w : freeProP p X} (hw : π w = 1) : D w ∈ Submodule.span (MonoidAlgebra (ZMod p) G) (Set.range fun (ρ : ↥s) => D ↑ρ)

The cocycle maps the kernel of π into the span of the images of its normal generators. If the kernel of π is the closed normal closure of a finite set s, then D w is an 𝔽_p[G]-combination of the D ρ, ρ ∈ s, for every w with π w = 1: the set of such w is closed and contains the normal closure of s, since D is additive and conjugation-equivariant on the kernel.

theorem TauCeti.freeProP.relationModule_le_span {p : ℕ} [Fact (Nat.Prime p)] {X : Type u} [Fintype X] {G : Type u} [Group G] [TopologicalSpace G] [DiscreteTopology G] {π : freeProP p X →ₜ* G} {D : freeProP p X → X → MonoidAlgebra (ZMod p) G} (hcoc : ∀ (g h : freeProP p X), D (g * h) = MonoidAlgebra.single (π g) 1 • D h + D g) [DecidableEq X] (hπ : Function.Surjective ⇑π) {s : Finset (freeProP p X)} (hs : ∀ (w : freeProP p X), π w = 1 ↔ w ∈ (Subgroup.normalClosure ↑s).topologicalClosure) (hD : IsLocallyConstant D) (hDof : ∀ (i : X), D (of i) = Pi.single i 1) : (MonoidAlgebra.relationModule (ZMod p) G fun (i : X) => π (of i)) ≤ Submodule.span (MonoidAlgebra (ZMod p) G) (Set.range fun (ρ : ↥s) => D ↑ρ)

The relations among the π xᵢ - 1 lie in the span of the relator images. Let π : F ↠ G be a continuous surjection from a free pro-p group onto a discrete group, whose kernel is the closed normal closure of a finite set s, and let D : F → 𝔽_p[G]^X be a locally constant cocycle with D xᵢ = eᵢ. Then the relation module of the family π xᵢ is contained in the 𝔽_p[G]-span of the D ρ, ρ ∈ s.

theorem TauCeti.freeProP.augmentation_cocycle_eq_zero_of_mem_proPFrattini {p : ℕ} [Fact (Nat.Prime p)] {X G : Type u} [Group G] [TopologicalSpace G] {π : freeProP p X →ₜ* G} {D : freeProP p X → X → MonoidAlgebra (ZMod p) G} (hcoc : ∀ (g h : freeProP p X), D (g * h) = MonoidAlgebra.single (π g) 1 • D h + D g) (hD : IsLocallyConstant D) {ρ : freeProP p X} (hρ : ρ ∈ proPFrattini p (freeProP p X)) (i : X) : (MonoidAlgebra.augmentation (ZMod p) G) (D ρ i) = 0

The cocycle image of a Frattini element has every coordinate in the augmentation ideal. The cocycle, composed with the augmentation 𝔽_p[G] → 𝔽_p, is a continuous homomorphism to an elementary abelian p-group, so it vanishes on the Frattini subgroup.