ProCGroups.Generation.WordProductsAndClosure
This module studies word products and closure for pro cgroups. The identity element belongs to the word-product set. Multiplying elements from two word-product sets lands in the word-product set with summed length.
import
@[simp] theorem wordProducts_one (X : Set G) :
wordProducts X 1 = XThe identity element belongs to the word-product set.
Show proof
by
simp only [wordProducts, singleton_mul, one_mul, image_id']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 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem wordProducts_mul_wordProducts (X : Set G) :
∀ m n, wordProducts X m * wordProducts X n = wordProducts X (m + n)
| m, 0 => by
simp only [wordProducts, mul_singleton, mul_one, image_id', add_zero]
| m, n + 1 => by
calc
wordProducts X m * wordProducts X (n + 1)
= wordProducts X m * (wordProducts X n * X)Multiplying elements from two word-product sets lands in the word-product set with summed length.
Show proof
by
rfl
_ = (wordProducts X m * wordProducts X n) * X := by
rw [mul_assoc]
_ = wordProducts X (m + n) * X := by
rw [wordProducts_mul_wordProducts X m n]
_ = wordProducts X (m + n + 1) := by
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 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem one_mem_wordProducts {X : Set G} (h1 : (1 : G) ∈ X) :
∀ n, (1 : G) ∈ wordProducts X n
| 0 => by
simp only [wordProducts, mem_singleton_iff]
| n + 1 => by
exact ⟨1, one_mem_wordProducts h1 n, 1, h1, by simp only [mul_one]⟩The identity element belongs to the corresponding word-product set.
Show proof
No Lean proof was detected.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. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. 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.
□theorem wordProducts_subset_closure (X : Set G) :
∀ n, wordProducts X n ⊆ ((Subgroup.closure X : Subgroup G) : Set G)
| 0 => by
intro x hx
simp only [wordProducts, mem_singleton_iff] at hx
simp only [hx, SetLike.mem_coe, one_mem]
| n + 1 => by
intro x hx
rcases hx with ⟨a, ha, b, hb, rfl⟩
exact (Subgroup.closure X).mul_mem
(wordProducts_subset_closure X n ha)
(Subgroup.subset_closure hb)Every word product of elements of \(X\) lies in the subgroup generated by \(X\).
Show proof
No Lean proof was detected.Proof. Induct on the word length. The length-zero product is the identity, which lies in the subgroup closure. In the successor step, multiply an element already in the subgroup closure by an element of \(X\), using closure under multiplication and the inclusion \(X\subseteq\langle X\rangle\).
□theorem wordProducts_inv_mem {X : Set G} (hXinv : X = Inv.inv '' X) :
∀ {n : ℕ} {x : G}, x ∈ wordProducts X n → x⁻¹ ∈ wordProducts X n
| 0, x, hx => by
simpa [wordProducts] using hx
| n + 1, x, hx => by
rcases hx with ⟨a, ha, b, hb, rfl⟩
have hb' : b⁻¹ ∈ XThe word-product set is closed under taking inverses.
Show proof
by
rw [hXinv]
exact ⟨b, hb, by simp only⟩
have ha' : a⁻¹ ∈ wordProducts X n := wordProducts_inv_mem hXinv ha
have hmem : b⁻¹ * a⁻¹ ∈ wordProducts X 1 * wordProducts X n := by
exact ⟨b⁻¹, by
show b⁻¹ ∈ wordProducts X 1
simpa [wordProducts_one] using hb', a⁻¹, ha', rfl⟩
have hEq : wordProducts X 1 * wordProducts X n = wordProducts X (1 + n) := by
simpa using (wordProducts_mul_wordProducts X 1 n)
have hmem' : b⁻¹ * a⁻¹ ∈ wordProducts X (1 + n) := by
exact hEq ▸ hmem
simpa [Nat.succ_eq_add_one, Nat.add_comm] using hmem'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 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem wordProducts_mono_len {X : Set G} (h1 : (1 : G) ∈ X) {m n : ℕ} (hmn : m ≤ n) :
wordProducts X m ⊆ wordProducts X nWord-product sets are monotone in the allowed word length.
Show proof
by
rcases Nat.exists_eq_add_of_le hmn with ⟨k, rfl⟩
intro x hx
have hk : (1 : G) ∈ wordProducts X k := one_mem_wordProducts h1 k
have hmem : x * 1 ∈ wordProducts X m * wordProducts X k := by
exact ⟨x, hx, 1, hk, by simp only [mul_one]⟩
simpa [wordProducts_mul_wordProducts, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm] using hmemProof. 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 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem subgroupClosure_eq_iUnion_wordProducts {X : Set G}
(hXinv : X = Inv.inv '' X) :
(((Subgroup.closure X : Subgroup G) : Set G)) = ⋃ n, wordProducts X nThe subgroup generated by word products has the stated closure property.
Show proof
by
let S : Subgroup G := {
carrier := {g : G | ∃ n : ℕ, g ∈ wordProducts X n}
one_mem' := ⟨0, by simp only [wordProducts, mem_singleton_iff]⟩
mul_mem' := by
intro a b ha hb
rcases ha with ⟨m, hm⟩
rcases hb with ⟨n, hn⟩
refine ⟨m + n, ?_⟩
have hmem : a * b ∈ wordProducts X m * wordProducts X n := by
exact ⟨a, hm, b, hn, rfl⟩
simpa [wordProducts_mul_wordProducts] using hmem
inv_mem' := by
intro a ha
rcases ha with ⟨n, hn⟩
exact ⟨n, wordProducts_inv_mem hXinv hn⟩
}
have hXsubset : X ⊆ (S : Set G) := by
intro x hx
exact ⟨1, by simpa using hx⟩
have hle : Subgroup.closure X ≤ S := (Subgroup.closure_le (K := S)).mpr hXsubset
ext g
constructor
· intro hg
rcases hle hg with ⟨n, hn⟩
exact mem_iUnion.mpr ⟨n, hn⟩
· intro hg
rcases mem_iUnion.mp hg with ⟨n, hn⟩
exact wordProducts_subset_closure X n hnProof. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem wordProducts_isCompact [CompactSpace G] {X : Set G}
(hXclosed : IsClosed X) :
∀ n, IsCompact (wordProducts X n)
| 0 => by
simp only [wordProducts, finite_singleton, Finite.isCompact]
| n + 1 => by
have hprev : IsCompact (wordProducts X n)The subgroup generated by word products has the stated closure property.
Show proof
wordProducts_isCompact hXclosed n
have hEq :
wordProducts X (n + 1) =
(fun p : G × G => p.1 * p.2) '' ((wordProducts X n) ×ˢ X) := by
ext x
constructor
· intro hx
rcases hx with ⟨a, ha, b, hb, rfl⟩
exact ⟨(a, b), ⟨ha, hb⟩, rfl⟩
· intro hx
rcases hx with ⟨⟨a, b⟩, hab, rfl⟩
exact ⟨a, hab.1, b, hab.2, rfl⟩
rw [hEq]
exact (hprev.prod hXclosed.isCompact).image (continuous_fst.mul continuous_snd)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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem wordProducts_isClosed [CompactSpace G] [T2Space G] {X : Set G}
(hXclosed : IsClosed X) (n : ℕ) :
IsClosed (wordProducts X n)The word-product set is closed in the profinite topology.
Show proof
(wordProducts_isCompact (G := G) hXclosed n).isClosedProof. 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.
□theorem exists_openNormalSubgroup_inf_eq_bot_of_finite
(hG : IsProfiniteGroup G) (K : Subgroup G) [Finite K] :
∃ U : OpenNormalSubgroup G, ((U : Subgroup G) ⊓ K) = ⊥A finite subgroup of a profinite group can be separated from 1 by an open normal subgroup.
Show proof
by
classical
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
letI : Fintype K := Fintype.ofFinite K
let topU : OpenNormalSubgroup G :=
{ toSubgroup := ⊤
isOpen' := isOpen_univ
isNormal' := inferInstance }
have hsep :
∀ k : K, k ≠ 1 → ∃ U : OpenNormalSubgroup G, (k : G) ∉ (U : Subgroup G) := by
intro k hk
have hnotall : ¬ ∀ U : OpenNormalSubgroup G, (k : G) ∈ (U : Subgroup G) := by
intro hkall
have hkone : (k : G) = 1 :=
IsProfiniteGroup.eq_one_of_mem_all_openNormalSubgroups (G := G) hkall
apply hk
apply Subtype.ext
simpa using hkone
rcases not_forall.mp hnotall with ⟨U, hkU⟩
exact ⟨U, hkU⟩
choose U hU using hsep
let s : Finset K := Finset.univ.filter fun k : K => k ≠ 1
by_cases hs : s.Nonempty
· let t : Finset s := s.attach
have ht : t.Nonempty := by simpa [t] using hs
let V : OpenNormalSubgroup G := t.inf' ht fun k => U k.1 ((Finset.mem_filter.mp k.2).2)
refine ⟨V, ?_⟩
rw [Subgroup.eq_bot_iff_forall]
intro x hx
let k : K := ⟨x, hx.2⟩
by_cases hk : k = 1
· exact congrArg Subtype.val hk
· have hk_mem : k ∈ s := by
simp only [ne_eq, Finset.mem_filter, Finset.mem_univ, hk, not_false_eq_true, and_self, s]
have hxV :
x ∈ ((U k hk : OpenNormalSubgroup G) : Subgroup G) := by
exact (show (V : OpenNormalSubgroup G) ≤ U k hk from by
dsimp [V]
exact Finset.inf'_le (s := t)
(f := fun k => U k.1 ((Finset.mem_filter.mp k.2).2))
(h := by
change ⟨k, hk_mem⟩ ∈ s.attach
simp only [Finset.mem_attach])) hx.1
have hkV : (k : G) ∈ ((U k hk : OpenNormalSubgroup G) : Subgroup G) := by
simpa [k] using hxV
exact False.elim (hU k hk hkV)
· refine ⟨topU, ?_⟩
rw [Subgroup.eq_bot_iff_forall]
intro x hx
let k : K := ⟨x, hx.2⟩
have hk_eq : k = 1 := by
by_contra hk
exact hs ⟨k, by simp only [ne_eq, Finset.mem_filter, Finset.mem_univ, hk, not_false_eq_true, and_self, s]⟩
exact congrArg Subtype.val hk_eqProof. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□