Free class-module extensions over their presented quotient

Let g : ι → G generate a profinite group topologically, F be the free profinite group on ι, and R = ker(lift g). The first isomorphism theorem identifies F/R with G. Transporting the quotient action on Rᵃᵇ(p) and the class-module extension along this identification gives an extension over G, with projection induced by lift g.

Choosing lifts of the g i to any profinite extension of G whose kernel is an abelian pro-p group gives a continuous comparison with it over the identity of G, since the relation group lands in the kernel and so kills the kernel of R → Rᵃᵇ(p). Thus the free extension can be used in the extension-lifting criterion against such an extension.

If moreover the class of the target extension generates its second cohomology group, of p-power order, then a continuous equivariant surjection Rᵃᵇ(p) → N that is bijective on H² lifts, after a prime-to-p power correction, to a surjection of extensions. The total group of the target is then topologically generated by lifts of the g i, by freeProfiniteGroup.exists_topologicalClosure_closure_range_eq_top_of_bijective_explicitCoeff2. For a finite quotient G = G_K/V of an absolute Galois group, with target the class-module extension G_K / ker(V → Vᵃᵇ(p)), this is the finite-level generation step of the proof of NSW (7.4.1).

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.4.1).

@[reducible, inline]

noncomputable abbrev TauCeti.freeProfiniteGroup.presentationClassModuleAction (p : ℕ) {ι G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {g : ι → G} (hg : Dense ↑(Subgroup.closure (Set.range g))) : MulDistribMulAction G (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker)

The action of the presented group on its pro-p relation group, transported from the conjugation action of F/ker(lift g) along the first isomorphism theorem.

theorem TauCeti.freeProfiniteGroup.presentationClassModuleAction_smul (p : ℕ) {ι G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {g : ι → G} (hg : Dense ↑(Subgroup.closure (Set.range g))) (h : G) (x : abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker) : h • x = ((lift g).quotientKerEquivOfSurjective ⋯).symm h • x

The transported action is conjugation by the corresponding class in F/ker(lift g).

@[simp]

theorem TauCeti.freeProfiniteGroup.presentationClassModuleAction_lift_smul (p : ℕ) {ι G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {g : ι → G} (hg : Dense ↑(Subgroup.closure (Set.range g))) (f : ↑(freeProfiniteGroup ι).toProfinite.toTop) (x : abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker) : (lift g) f • x = ↑f • x

The image of a free-group element acts by its class in F/ker(lift g).

theorem TauCeti.freeProfiniteGroup.continuousSMul_presentationClassModuleAction (p : ℕ) {ι G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {g : ι → G} (hg : Dense ↑(Subgroup.closure (Set.range g))) : ContinuousSMul G (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker)

The transported conjugation action on the pro-p relation group is jointly continuous.

@[reducible, inline]

noncomputable abbrev TauCeti.freeProfiniteGroup.presentationProfiniteExtension (p : ℕ) {ι G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {g : ι → G} (hg : Dense ↑(Subgroup.closure (Set.range g))) : ProfiniteGroupExtension G (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker)

The class-module extension of a free presentation, with quotient the presented group. Its total group remains the canonical quotient F/ker(R → Rᵃᵇ(p)).

theorem TauCeti.freeProfiniteGroup.presentationProfiniteExtension_rightHom_mk (p : ℕ) {ι G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {g : ι → G} (hg : Dense ↑(Subgroup.closure (Set.range g))) (f : ↑(freeProfiniteGroup ι).toProfinite.toTop) : (presentationProfiniteExtension p hg).toGroupExtension.rightHom ↑f = (lift g) f

The projection of the free presentation extension sends the class of f to lift g f.

theorem TauCeti.freeProfiniteGroup.exists_presentationProfiniteExtension_comparison (p : ℕ) {ι G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {g : ι → G} (hg : Dense ↑(Subgroup.closure (Set.range g))) {N : Type u} [CommGroup N] [TopologicalSpace N] [MulDistribMulAction G N] (Y : ProfiniteGroupExtension G N) (hN : IsProP p N) : ∃ (ψ : (presentationProfiniteExtension p hg).E →ₜ* Y.E), Y.toGroupExtension.rightHom.comp ψ.toMonoidHom = (presentationProfiniteExtension p hg).toGroupExtension.rightHom

The free class-module extension admits a continuous comparison, over the identity of G, with every profinite extension of G whose kernel is an abelian pro-p group. No surjectivity of the comparison is asserted.

theorem TauCeti.freeProfiniteGroup.exists_topologicalClosure_closure_range_eq_top_of_bijective_explicitCoeff2 (p : ℕ) {ι G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {g : ι → G} (hg : Dense ↑(Subgroup.closure (Set.range g))) {N : Type u} [CommGroup N] [TopologicalSpace N] [MulDistribMulAction G N] [Fact (Nat.Prime p)] [IsTopologicalGroup N] [ContinuousSMul G N] [CompactSpace N] [TotallyDisconnectedSpace N] (Y : ProfiniteGroupExtension G N) (hN : IsProP p N) (hy : AddSubgroup.zmultiples Y.contCohomologyClass = ⊤) (hcard : ∃ (r : ℕ), Nat.card (ContCohomology.H2 G (Additive N)) = p ^ r) (f : abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker →*[G] N) (hf : Continuous ⇑f) : Function.Surjective ⇑f → Function.Bijective ⇑(ContCohomology.explicitCoeff2 G (Additive (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker)) f.toAdditive ⋯) → ∃ (y : ι → Y.E), (∀ (i : ι), Y.toGroupExtension.rightHom (y i) = g i) ∧ (Subgroup.closure (Set.range y)).topologicalClosure = ⊤

Generation of an extension by lifts of a presentation (NSW, proof of (7.4.1)). Let Y be a profinite extension of G by an abelian pro-p group N whose class generates H²(G, N), a group of p-power order. If a continuous equivariant surjection f : Rᵃᵇ(p) → N is bijective on H², then lifts of the g i to Y topologically generate its total group.

@[simp]

theorem TauCeti.freeProfiniteGroup.abelianizationProPEquivRelationModule_presentation_smul (p : ℕ) [Fact (Nat.Prime p)] {G ι : Type} [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [Fintype ι] [DecidableEq ι] {g : ι → G} (hgen : Subgroup.closure (Set.range g) = ⊤) (t : G) (x : Additive (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker)) : (abelianizationProPEquivRelationModule p hgen) (t • x) = MonoidAlgebra.single t 1 • (abelianizationProPEquivRelationModule p hgen) x

Lyndon's coordinates intertwine the presented group's conjugation action with its left group-algebra action on the relation module.