Projectivity from finite embedding problems

Closed subgroups of A × G that project onto G form lift relations. Compactness of their fibers preserves surjectivity along decreasing chains. Finite p-kernel embedding problems refine a relation at any open-normal quotient of A.

A minimal relation (Subgroup.exists_minimal_isClosed_le) therefore supplies compatible finite-level solutions. The existing inverse-limit assembly gives isProjective_of_hasPGroupSolutions, without finite generation of G. Compactness is applied to fibers in A; the sets of level solutions need not be finite.

Conversely, a projective pro-p group solves every finite embedding problem with p-group kernel (hasPGroupSolutions_of_isProjective): its finite quotients are p-groups, so such a problem is a lifting problem against a surjection of finite p-groups. For a pro-p group the two conditions are therefore equivalent (isProjective_iff_hasPGroupSolutions), and projectivity does not depend on the universes of the groups it quantifies over.

Main definitions

• TauCeti.IsProjective: every continuous homomorphism into a quotient of a profinite pro-p group lifts continuously.

Main results

• TauCeti.isProjective_of_hasPGroupSolutions: solving the finite embedding problems with p-group kernel gives projectivity.
• TauCeti.hasPGroupSolutions_of_isProjective: a projective pro-p group solves the finite embedding problems with p-group kernel.
• TauCeti.isProjective_iff_hasPGroupSolutions: for a pro-p group, projectivity is equivalent to solving the finite embedding problems with p-group kernel.

References

• J.-P. Serre, Galois Cohomology, Chapter I, §3.4 and §5.9.
• L. Ribes and P. Zalesskii, Profinite Groups, Section 7.6.

def TauCeti.IsProjective (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] : Prop

Every continuous map to a quotient of a profinite pro-p group lifts continuously. The source, the covering group and the quotient may lie in independent universes.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.HasPGroupSolutions.exists_compatible_levelSolutions {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] {p : ℕ} (hG : HasPGroupSolutions p G) (hA : IsProP p A) (α : A →ₜ* B) (hα : Function.Surjective ⇑α) (f : G →ₜ* B) : ∃ (β : (U : OpenNormalSubgroup A) → LevelSolution α hα f U), ∀ ⦃V U : OpenNormalSubgroup A⦄ (hVU : V ≤ U), levelSolutionMap α hα f hVU (β V) = β U

Finite p-kernel solvability supplies compatible level solutions without finite generation.

theorem TauCeti.IsProjective.exists_continuous_lift {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [Group A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] {B : Type w} [Group B] [TopologicalSpace B] [IsTopologicalGroup B] [T2Space B] [TotallyDisconnectedSpace A] {p : ℕ} (hG : IsProjective p G) (hA : IsProP p A) (α : A →ₜ* B) (hα : Function.Surjective ⇑α) (f : G →ₜ* B) : ∃ (φ : G →ₜ* A), α.comp φ = f

Apply projectivity to a continuous map and a surjection from a profinite pro-p group.

theorem TauCeti.isProjective_of_hasPGroupSolutions {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {p : ℕ} (hG : HasPGroupSolutions p G) : IsProjective p G

Solving all finite embedding problems with p-group kernel implies projectivity, with no rank or finite-generation restriction on the source.

theorem TauCeti.IsProjective.of_equiv {G : Type u} [Group G] [TopologicalSpace G] {p : ℕ} (hG : IsProjective p G) {H : Type u'} [Group H] [TopologicalSpace H] (e : G ≃ₜ* H) : IsProjective p H

Projectivity is invariant under topological group isomorphism.

The converse for pro-p groups

theorem TauCeti.hasPGroupSolutions_of_isProjective {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {p : ℕ} (hGp : IsProP p G) (hG : IsProjective p G) : HasPGroupSolutions p G

A projective pro-p group solves every finite embedding problem with p-group kernel. The universes v and w in which G is assumed projective are arbitrary.

The pro-p hypothesis cannot be dropped. G = PSL₂(𝔽₅) is perfect, so every continuous homomorphism from it to a pro-2 group is trivial and G is projective at p = 2; but the problem given by SL₂(𝔽₅) ↠ G, with kernel of order 2 and π = id, has no solution, since -1 is the only involution of SL₂(𝔽₅) while G has involutions.

theorem TauCeti.isProjective_iff_hasPGroupSolutions {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {p : ℕ} (hGp : IsProP p G) : IsProjective p G ↔ HasPGroupSolutions p G

Projectivity of a pro-p group is solvability of its finite p-embedding problems. A pro-p group is projective exactly when it solves every finite embedding problem with p-group kernel. Since the right-hand side does not mention the universes v and w, neither does projectivity of a pro-p group.