ProCGroups.Generation.GeneratorConvergingPairs
This module studies generator converging pairs for pro cgroups. A partial generating set together with a closed normal subgroup modulo which it converges. The order relation is the refinement relation on the corresponding data.
import
structure GeneratorConvergingPair where
N : Subgroup G
normal_N : N.Normal
closed_N : IsClosed (N : Set G)
X : Set G
subset_compl : X ⊆ (N : Set G)ᶜ
convergesToOne_mod :
∀ U : OpenSubgroup G, N ≤ (U : Subgroup G) → (X \ (U : Set G)).Finite
generates : TopologicallyGenerates (G := G) (X ∪ (N : Set G))A partial generating set together with a closed normal subgroup modulo which it converges.
instance instLEGeneratorConvergingPair : LE (GeneratorConvergingPair (G := G)) where
le A B := B.N ≤ A.N ∧ A.X ⊆ B.X ∧ B.X \ A.X ⊆ (A.N : Set G)The order relation is the refinement relation on the corresponding data.
instance instPreorderGeneratorConvergingPair : Preorder (GeneratorConvergingPair (G := G)) where
le_refl A := ⟨le_rfl, subset_rfl, by simp only [sdiff_self, bot_eq_empty, empty_subset]⟩
le_trans A B C hAB hBC := by
rcases hAB with ⟨hABN, hABX, hABdiff⟩
rcases hBC with ⟨hBCN, hBCX, hBCdiff⟩
refine ⟨hBCN.trans hABN, hABX.trans hBCX, ?_⟩
intro x hx
rcases hx with ⟨hxC, hxA⟩
by_cases hxB : x ∈ B.X
· exact hABdiff ⟨hxB, hxA⟩
· exact hABN (hBCdiff ⟨hxC, hxB⟩)The preorder is induced by refinement of the corresponding data.
noncomputable def initialGeneratorConvergingPair : GeneratorConvergingPair (G := G) where
N := ⊤
normal_N := by infer_instance
closed_N := isClosed_univ
X := ∅
subset_compl := by intro x hx; simp only [mem_empty_iff_false] at hx
convergesToOne_mod := by
intro U hU
simp only [empty_diff, finite_empty]
generates := by
simpa [TopologicallyGenerates, Set.empty_union, Subgroup.closure_eq] using
(top_unique (Subgroup.le_topologicalClosure (⊤ : Subgroup G)) :
(⊤ : Subgroup G).topologicalClosure = ⊤)The initial generator-converging pair.
theorem finite_subset_chain_has_upper {α : Type*} [Preorder α] {c : Set α}
(hc : IsChain (· ≤ ·) c) :
∀ s : Finset α, ↑s ⊆ c → s.Nonempty → ∃ m ∈ s, ∀ z ∈ s, z ≤ mA finite subset of a chain has an upper element from that subset.
Show proof
by
classical
intro s
refine Finset.induction_on s ?_ ?_
· intro hs hne
exact False.elim (hne.ne_empty rfl)
· intro a s ha ih hs hne
by_cases hsne : s.Nonempty
· rcases ih
(by
intro z hz
exact hs (by simp only [Finset.coe_insert, mem_insert_iff, hz, or_true]))
hsne with ⟨m, hm, hmax⟩
have ha' : a ∈ c := hs (by simp only [Finset.coe_insert, mem_insert_iff, SetLike.mem_coe, true_or])
have hm' : m ∈ c := hs (by simp only [Finset.coe_insert, mem_insert_iff, SetLike.mem_coe, hm, or_true])
have hcmp : a ≤ m ∨ m ≤ a := by
by_cases hEq : a = m
· exact Or.inl (hEq ▸ le_rfl)
· exact hc ha' hm' hEq
cases hcmp with
| inl ham =>
refine ⟨m, by simp only [Finset.mem_insert, hm, or_true], ?_⟩
intro z hz
rcases Finset.mem_insert.mp hz with rfl | hz'
· exact ham
· exact hmax z hz'
| inr hma =>
refine ⟨a, by simp only [Finset.mem_insert, true_or], ?_⟩
intro z hz
rcases Finset.mem_insert.mp hz with rfl | hz'
· exact le_rfl
· exact (hmax z hz').trans hma
· have hs0 : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hsne
refine ⟨a, by simp only [hs0, insert_empty_eq, Finset.mem_singleton], ?_⟩
intro z hz
have hz' : z = a := by simpa [hs0] using hz
subst z
exact le_rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem exists_pair_le_openSubgroup_of_chain_iInf_le [CompactSpace G]
{c : Set (GeneratorConvergingPair (G := G))}
(hc : IsChain (· ≤ ·) c) (hcne : c.Nonempty)
(U : OpenSubgroup G)
(hInf : iInf (fun p : c => p.1.N) ≤ (U : Subgroup G)) :
∃ p : c, p.1.N ≤ (U : Subgroup G)If the infimum of the closed normal subgroups in a chain lies in an open subgroup, then one stage already lies in that open subgroup.
Show proof
by
classical
have hInter :
(⋂ p : c, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := by
intro x hx
exact hInf (by simpa [Subgroup.mem_iInf] using hx)
rcases finite_iInter_subgroup_subset_openSubgroup (G := G)
(H := fun p : c => p.1.N)
(hclosed := fun p => p.1.closed_N)
U hInter with ⟨s, hs⟩
by_cases hsne : s.Nonempty
· have hc' : IsChain (· ≤ ·) (Set.univ : Set c) := by
intro a ha b hb hne
have hne' : (a : GeneratorConvergingPair (G := G)) ≠ b := by
intro h
exact hne (Subtype.ext h)
simpa using hc a.2 b.2 hne'
rcases finite_subset_chain_has_upper hc' s (by intro z hz; simp only [mem_univ]) hsne with ⟨m, hm, hmax⟩
refine ⟨m, ?_⟩
intro x hx
have hx' :
x ∈ ⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G)) := by
refine mem_iInter₂.2 ?_
intro p hp
exact (hmax p hp).1 hx
exact hs hx'
· rcases hcne with ⟨p, hp⟩
refine ⟨⟨p, hp⟩, ?_⟩
have htop : ((⊤ : Subgroup G) : Set G) ⊆ ((U : Subgroup G) : Set G) := by
have : (⋂ p ∈ s, (((p.1.N : Subgroup G) : Set G))) ⊆ ((U : Subgroup G) : Set G) := hs
simpa [Finset.not_nonempty_iff_eq_empty.mp hsne] using this
intro x hx
exact htop (by simp only [Subgroup.coe_top, mem_univ])Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□noncomputable def chainUpperBoundOfNonempty
(hG : IsProfiniteGroup G)
{c : Set (GeneratorConvergingPair (G := G))}
(hc : IsChain (· ≤ ·) c) (hcne : c.Nonempty) :
GeneratorConvergingPair (G := G) where
N := iInf fun p : c => p.1.N
normal_N := by
classical
exact Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
closed_N := by
classical
simpa using isClosed_iInter (fun p : c => p.1.closed_N)
X := ⋃ p : c, p.1.X
subset_compl := by
intro x hx
rcases mem_iUnion.mp hx with ⟨p, hpx⟩
refine by
intro hxK
exact p.1.subset_compl hpx ((iInf_le (fun q : c => q.1.N) p) hxK)
convergesToOne_mod := by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
intro U hKU
rcases exists_pair_le_openSubgroup_of_chain_iInf_le (G := G) hc hcne U
hKU with ⟨p, hpU⟩
have hEq : ((⋃ q : c, q.1.X) \ (U : Set G)) = (p.1.X \ (U : Set G)) := by
ext x
constructor
· intro hx
rcases hx with ⟨hxX, hxU⟩
rcases mem_iUnion.mp hxX with ⟨q, hqx⟩
have hcmp :
(q.1 ≤ p.1) ∨ (p.1 ≤ q.1) := by
by_cases hqp : q = p
· exact Or.inl (hqp ▸ le_rfl)
· have hqp' : (q : GeneratorConvergingPair (G := G)) ≠ p := by
intro h
exact hqp (Subtype.ext h)
exact hc q.2 p.2 hqp'
cases hcmp with
| inl hqp =>
exact ⟨hqp.2.1 hqx, hxU⟩
| inr hpq =>
by_cases hxp : x ∈ p.1.X
· exact ⟨hxp, hxU⟩
· have hxN : x ∈ (p.1.N : Set G) := hpq.2.2 ⟨hqx, hxp⟩
exact False.elim (hxU (hpU hxN))
· intro hx
exact ⟨mem_iUnion.mpr ⟨p, hx.1⟩, hx.2⟩
rw [hEq]
exact p.1.convergesToOne_mod U hpU
generates := by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
let K : Subgroup G := iInf fun p : c => p.1.N
letI : K.Normal := Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
have hKclosed : IsClosed (K : Set G) := by
simpa [K] using isClosed_iInter (fun p : c => p.1.closed_N)
apply (topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient
(G := G) hG
(N := K) (X := ⋃ p : c, p.1.X)).2
intro U hKU
rcases exists_pair_le_openSubgroup_of_chain_iInf_le (G := G) hc hcne U.toOpenSubgroup
(by simpa [K] using hKU) with ⟨p, hpU⟩
have hpgen :
TopologicallyGenerates (G := G ⧸ (U : Subgroup G))
((QuotientGroup.mk' (U : Subgroup G)) '' p.1.X) := by
letI : p.1.N.Normal := p.1.normal_N
exact
(topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient
(G := G) hG
(N := p.1.N) (X := p.1.X)).1
p.1.generates U hpU
exact topologicallyGenerates_mono hpgen (by
intro y hy
rcases hy with ⟨x, hx, rfl⟩
exact ⟨x, mem_iUnion.mpr ⟨p, hx⟩, rfl⟩)Upper bound of a nonempty chain of generator-converging pairs.
theorem chain_bounded_generatorConvergingPair (hG : IsProfiniteGroup G)
(c : Set (GeneratorConvergingPair (G := G)))
(hc : IsChain (· ≤ ·) c) :
BddAbove cThe generator-converging-pair order is inductive over chains.
Show proof
by
classical
rcases c.eq_empty_or_nonempty with rfl | hcne
· exact ⟨initialGeneratorConvergingPair (G := G), by intro a ha; cases ha⟩
· refine ⟨chainUpperBoundOfNonempty (G := G) hG hc hcne, ?_⟩
intro p hp
refine ⟨?_, ?_, ?_⟩
· exact iInf_le (fun q : {q // q ∈ c} => q.1.N) ⟨p, hp⟩
· intro x hx
exact mem_iUnion.mpr ⟨⟨p, hp⟩, hx⟩
· intro x hx
rcases hx with ⟨hxX, hxpX⟩
rcases mem_iUnion.mp hxX with ⟨q, hqx⟩
by_cases hqp : q = ⟨p, hp⟩
· exact False.elim (hxpX (by simpa [hqp] using hqx))
· have hqp' : (q : GeneratorConvergingPair (G := G)) ≠ p := by
intro h
exact hqp (Subtype.ext h)
rcases hc q.2 hp hqp' with hqle | hple
· exact False.elim (hxpX (hqle.2.1 hqx))
· exact hple.2.2 ⟨hqx, hxpX⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem exists_finite_subset_generating_subgroup_mod_openNormal
(hG : IsProfiniteGroup G) {M : Subgroup G}
(hMclosed : IsClosed (M : Set G)) (U : OpenNormalSubgroup G) :
∃ T : Set G,
T.Finite ∧
T ⊆ (M : Set G) \ (((U : Subgroup G) ⊓ M : Subgroup G) : Set G) ∧
M ≤ Subgroup.closure (T ∪ ((((U : Subgroup G) ⊓ M : Subgroup G) : Subgroup G) : Set G))An open-normal quotient of a closed normal subgroup has a finite generating set modulo the intersection with the open normal subgroup.
Show proof
by
classical
have hMprof : IsProfiniteGroup M := IsProfiniteGroup.of_isClosed_subgroup (G := G) hG M hMclosed
letI : CompactSpace M := IsProfiniteGroup.compactSpace hMprof
let UM : OpenNormalSubgroup M :=
OpenNormalSubgroup.comap (M.subtype) continuous_subtype_val U
obtain ⟨σ, -, hσright, -⟩ :=
quotient_openNormalSubgroup_hasContinuousSection (G := M) UM
let q1 : M ⧸ (UM : Subgroup M) := ((1 : M) : M ⧸ (UM : Subgroup M))
let Tsub : Set M := σ '' ({q1} : Set (M ⧸ (UM : Subgroup M)))ᶜ
let T : Set G := Subtype.val '' Tsub
refine ⟨T, ?_, ?_, ?_⟩
· letI : Finite (M ⧸ (UM : Subgroup M)) := openNormalSubgroup_finiteQuotient (G := M) UM
have hfin : ({q1} : Set (M ⧸ (UM : Subgroup M)))ᶜ.Finite := Set.toFinite _
exact hfin.image σ |>.image Subtype.val
· intro x hx
rcases hx with ⟨y, hy, rfl⟩
rcases hy with ⟨q, hq, rfl⟩
refine ⟨(σ q).2, ?_⟩
intro hxUM
have hσUM : σ q ∈ (UM : Subgroup M) := by
change (((σ q : M) : G) ∈ (U : Subgroup G))
exact hxUM.1
have : q = q1 := by
calc
q = QuotientGroup.mk' (UM : Subgroup M) (σ q) := (hσright q).symm
_ = q1 := by
have hq1 :
QuotientGroup.mk' (UM : Subgroup M) (σ q) = (1 : M ⧸ (UM : Subgroup M)) :=
(QuotientGroup.eq_one_iff (N := (UM : Subgroup M)) (σ q)).2 hσUM
simpa [q1] using hq1
exact hq this
· intro m hmM
let mM : M := ⟨m, hmM⟩
let q : M ⧸ (UM : Subgroup M) := QuotientGroup.mk' (UM : Subgroup M) mM
by_cases hq : q = q1
· have hmUM : (⟨m, hmM⟩ : M) ∈ (UM : Subgroup M) := by
have hq1 : QuotientGroup.mk' (UM : Subgroup M) mM = (1 : M ⧸ (UM : Subgroup M)) := by
simpa [q, q1, mM] using hq
exact (QuotientGroup.eq_one_iff (N := (UM : Subgroup M)) mM).1 hq1
have hmN' : m ∈ ((U : Subgroup G) ⊓ M : Subgroup G) := by
refine ⟨?_, hmM⟩
change (((⟨m, hmM⟩ : M) : G) ∈ (U : Subgroup G))
simpa using hmUM
exact Subgroup.subset_closure (Or.inr hmN')
· have hT : ((σ q : M) : G) ∈ T := by
exact ⟨σ q, ⟨q, hq, rfl⟩, rfl⟩
have hEq :
QuotientGroup.mk' (UM : Subgroup M) (σ q) =
QuotientGroup.mk' (UM : Subgroup M) mM := by
simpa [q, mM] using hσright q
have hdiv : (σ q)⁻¹ * mM ∈ (UM : Subgroup M) := by
exact (QuotientGroup.eq).1 hEq
have hdivU : (((σ q : M) : G)⁻¹ * m) ∈ (U : Subgroup G) := by
change ((((σ q)⁻¹ * mM : M) : G) ∈ (U : Subgroup G))
simpa [mM] using hdiv
have hdivM : (((σ q : M) : G)⁻¹ * m) ∈ M := by
change ((((σ q)⁻¹ * mM : M) : G) ∈ M)
exact (((σ q)⁻¹ * mM : M)).2
have hN' : (((σ q : M) : G)⁻¹ * m) ∈ ((U : Subgroup G) ⊓ M : Subgroup G) := by
exact ⟨hdivU, hdivM⟩
have hσ' :
((σ q : M) : G) ∈
Subgroup.closure (T ∪ ((((U : Subgroup G) ⊓ M : Subgroup G) : Subgroup G) : Set G)) :=
Subgroup.subset_closure (Or.inl hT)
have hdiv' :
((σ q : M) : G)⁻¹ * m ∈
Subgroup.closure (T ∪ ((((U : Subgroup G) ⊓ M : Subgroup G) : Subgroup G) : Set G)) :=
Subgroup.subset_closure (Or.inr hN')
have hmEq : m = ((σ q : M) : G) * (((σ q : M) : G)⁻¹ * m) := by
simp only [mul_inv_cancel_left]
rw [hmEq]
exact (Subgroup.closure _).mul_mem hσ' hdiv'Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□