Levelwise comparison along the lower p-series

A PLowerCentralSeriesComparison p G H S assigns to each datum in S k a continuous surjection G ⧸ λ_k → H ⧸ λ_k. Its bonding maps commute with the quotient projections; when the data are themselves continuous homomorphisms of the finite levels, the descent ContinuousMonoidHom.pLowerCentralSeriesDesc of TauCeti.Topology.Algebra.Group.Profinite.ProP.LowerCentralSeries supplies them. When every S k is finite and nonempty, there is a compatible sequence of data. If G is compact and H is a pro-p group, the corresponding quotient maps come from a continuous surjection G → H.

Surjectivity of the bonding maps is unnecessary: a tower of nonempty finite sets already has a compatible sequence. Surjectivity of the realization maps is essential.

Main results

• PLowerCentralSeriesComparison.exists_continuous_surjective: a compatible sequence of finite comparison data is realized at every level by a continuous surjection.
• PLowerCentralSeriesComparison.exists_continuousMulEquiv: comparison data in both directions give a topological isomorphism realizing the forward data.
• PLowerCentralSeriesComparison.exists_continuousMulEquiv_preserving: self-comparison data preserving marked elements and all finite character quotients give an automorphism preserving the marked elements and the character.
• TauCeti.IsProP.exists_continuousMulEquiv_apply_eq_of_forall_exists_surjective: in a topologically finitely generated pro-p group, if for every k a continuous surjective endomorphism carries r to w modulo λ_k and moves each marked element a i by an element of a closed subgroup C i, then a continuous automorphism carries r to w and moves each a i by an element of C i. The comparison data are the surjective endomorphisms of the finite quotients carrying the class of r to the class of w and moving the class of each a i inside the image of C i.

The last two results apply to basis changes of a finite-rank free pro-p group with a marked relator. Constructing the finite nonempty sets of admissible basis changes, or the finite approximations, is a separate hypothesis; the theorems do not construct the corrections used in a normal-form argument.

structure TauCeti.PLowerCentralSeriesComparison (p : ℕ) (G : Type u_1) (H : Type u_2) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (S : ℕ → Type u_3) : Type (max (max u_1 u_2) u_3)

Surjective maps between lower p-series quotients, indexed by a tower of comparison data. Applications put their finite-level constraints in S; finiteness and nonemptiness are required only by the realization theorems.

• map (k : ℕ) : S k → G ⧸ pLowerCentralSeries p G k →ₜ* H ⧸ pLowerCentralSeries p H k

  The map realized by one comparison datum.

• map_surjective (k : ℕ) (s : S k) : Function.Surjective ⇑(self.map k s)

  Every realization covers the target quotient.

• bond (k : ℕ) : S (k + 1) → S k

  Forgetting the last level of comparison data.

• commutes (k : ℕ) (s : S (k + 1)) (x : G ⧸ pLowerCentralSeries p G (k + 1)) : (QuotientGroup.mapOfLE ⋯) ((self.map (k + 1) s) x) = (self.map k (self.bond k s)) ((QuotientGroup.mapOfLE ⋯) x)

  Realization commutes with forgetting a level.

theorem TauCeti.PLowerCentralSeriesComparison.exists_continuous_surjective {p : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {S : ℕ → Type u_3} [CompactSpace G] [CompactSpace H] [TotallyDisconnectedSpace H] [∀ (k : ℕ), Finite (S k)] [∀ (k : ℕ), Nonempty (S k)] (C : PLowerCentralSeriesComparison p G H S) (hH : IsProP p H) (hp : Nat.Prime p) : ∃ (s : (k : ℕ) → S k) (φ : G →ₜ* H), (∀ (k : ℕ), C.bond k (s (k + 1)) = s k) ∧ Function.Surjective ⇑φ ∧ ∀ (k : ℕ) (g : G), ↑(φ g) = (C.map k (s k)) ↑g

Levelwise comparison. Finite nonempty comparison data give a compatible sequence and a continuous surjection inducing its realization on every quotient. The source need only be compact and the target any pro-p group; neither is assumed finitely generated.

theorem TauCeti.PLowerCentralSeriesComparison.exists_continuousMulEquiv {p : ℕ} {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {S : ℕ → Type u_3} [CompactSpace G] [CompactSpace H] [TotallyDisconnectedSpace H] [∀ (k : ℕ), Finite (S k)] [∀ (k : ℕ), Nonempty (S k)] [TotallyDisconnectedSpace G] {T : ℕ → Type u_4} [∀ (k : ℕ), Finite (T k)] [∀ (k : ℕ), Nonempty (T k)] (C : PLowerCentralSeriesComparison p G H S) (D : PLowerCentralSeriesComparison p H G T) (hG : IsProP p G) (hGfg : IsTopologicallyFinitelyGenerated G) (hH : IsProP p H) (hp : Nat.Prime p) : ∃ (s : (k : ℕ) → S k) (e : G ≃ₜ* H), (∀ (k : ℕ), C.bond k (s (k + 1)) = s k) ∧ ∀ (k : ℕ) (g : G), ↑(e g) = (C.map k (s k)) ↑g

Two-sided comparison. For a topologically finitely generated pro-p source and a pro-p target, comparison data in both directions give an isomorphism realizing a compatible sequence of the forward data.

theorem TauCeti.PLowerCentralSeriesComparison.exists_continuousMulEquiv_preserving {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {S : ℕ → Type u_3} [CompactSpace G] [∀ (k : ℕ), Finite (S k)] [∀ (k : ℕ), Nonempty (S k)] [TotallyDisconnectedSpace G] {ι : Type u_4} {K : Type u_5} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [TotallyDisconnectedSpace K] (C : PLowerCentralSeriesComparison p G G S) (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) (a b : ι → G) (χ ψ : G →ₜ* K) (hmark : ∀ (k : ℕ) (s : S k) (i : ι), (C.map k s) ↑(a i) = ↑(b i)) (hchar : ∀ (U : OpenNormalSubgroup K), ∃ (k : ℕ), ∀ (s : S k) (x y : G), (C.map k s) ↑x = ↑y → ↑(ψ y) = ↑(χ x)) : ∃ (s : (k : ℕ) → S k) (e : G ≃ₜ* G), (∀ (k : ℕ), C.bond k (s (k + 1)) = s k) ∧ (∀ (k : ℕ) (g : G), ↑(e g) = (C.map k (s k)) ↑g) ∧ (∀ (i : ι), e (a i) = b i) ∧ ψ.comp ↑e = χ

Comparison preserving relators and characters. Suppose every level map takes the marked elements a to b, and each finite quotient of the character is respected at some level. Then a self-comparison is realized by an automorphism taking a to b and intertwining the characters. The character target may be any profinite group.

The character condition is entirely finite-level: equality of the level-k image of x with the class of y must imply equality of the prescribed character values modulo U. The level k may depend on U.

theorem TauCeti.IsProP.exists_continuousMulEquiv_apply_eq_of_forall_exists_surjective {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {ι : Type u_4} (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) (hp : Nat.Prime p) (r w : G) (a : ι → G) (C : ι → Subgroup G) (hC : ∀ (i : ι), IsClosed ↑(C i)) (h : ∀ (k : ℕ), ∃ (φ : G →ₜ* G), Function.Surjective ⇑φ ∧ (∀ (i : ι), (a i)⁻¹ * φ (a i) ∈ C i) ∧ (φ r)⁻¹ * w ∈ pLowerCentralSeries p G k) : ∃ (e : G ≃ₜ* G), (∀ (i : ι), (a i)⁻¹ * e (a i) ∈ C i) ∧ e r = w

From finite approximations to an automorphism. Let G be a topologically finitely generated pro-p group, let a : ι → G be marked elements and let C : ι → Subgroup G be closed subgroups. If for every k some continuous surjective endomorphism φ_k of G moves each a i inside C i, that is (a i)⁻¹ * φ_k (a i) ∈ C i, and has φ_k r ≡ w mod λ_k(G), then a continuous automorphism e of G carries r to w and moves each a i inside C i.

The constraints pass to the limit because membership in a closed subgroup is detected on the quotients G ⧸ λ_k (TauCeti.IsProP.mem_of_forall_mk_mem_map_pLowerCentralSeries).