ProCGroups/LocalWeight/SubgroupChains.lean
1import ProCGroups.ProC.OpenNormalSubgroups.CountableChains
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/LocalWeight/SubgroupChains.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14Studies local weight, metrizability, quotient size bounds, and cardinal invariants of profinite groups.
15-/
17namespace ProCGroups.LocalWeight
19universe u v
22section Chains
24variable {ι : Type v}
25variable {G : Type u} [Group G]
27/-- A family of subgroups intended to model a chain appearing in the transfinite local-weight
28arguments. -/
29abbrev SubgroupChain (ι : Type v) (G : Type u) [Group G] := ι → Subgroup G
31/-- The set-theoretic union of the members of a subgroup chain. -/
32def subgroupChainCarrier (c : SubgroupChain ι G) : Set G :=
33 { g | ∃ i, g ∈ c i }
35/-- The infimum of all members of a subgroup chain. -/
36def subgroupChainInf (c : SubgroupChain ι G) : Subgroup G :=
37 sInf (Set.range c)
39@[simp] theorem mem_subgroupChainCarrier_iff {c : SubgroupChain ι G} {g : G} :
40 g ∈ subgroupChainCarrier c ↔ ∃ i, g ∈ c i :=
41 Iff.rfl
43theorem subgroupChainInf_le (c : SubgroupChain ι G) (i : ι) :
44 subgroupChainInf c ≤ c i := by
45 exact sInf_le (Set.mem_range_self i)
47@[simp] theorem mem_subgroupChainInf_iff {c : SubgroupChain ι G} {g : G} :
48 g ∈ subgroupChainInf c ↔ ∀ i, g ∈ c i := by
49 simp only [subgroupChainInf, Subgroup.mem_sInf, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
51theorem subgroupChainInf_eq_bot_iff {c : SubgroupChain ι G} :
52 subgroupChainInf c = ⊥ ↔ ∀ g : G, (∀ i, g ∈ c i) → g = 1 := by
53 constructor
54 · intro h g hg
55 have hmem : g ∈ subgroupChainInf c := by
56 exact (mem_subgroupChainInf_iff.mpr hg)
57 have : g ∈ (⊥ : Subgroup G) := by
58 simpa [h] using hmem
59 simpa using this
60 · intro h
61 ext g
62 constructor
63 · intro hg
64 have hgall : ∀ i, g ∈ c i :=
65 mem_subgroupChainInf_iff.mp hg
66 have : g = 1 := h g hgall
67 simp only [this, one_mem]
68 · intro hg
69 have hg1 : g = 1 := by
70 simpa using hg
71 subst hg1
72 exact (mem_subgroupChainInf_iff).2 (fun i => (c i).one_mem)
74theorem subgroupChainInf_eq_bot_iff_forall_ne_one {c : SubgroupChain ι G} :
75 subgroupChainInf c = ⊥ ↔ ∀ g : G, g ≠ 1 → ∃ i, g ∉ c i := by
76 constructor
77 · intro h g hg
78 by_contra hneg
79 have hgall : ∀ i, g ∈ c i := by
80 intro i
81 by_contra hgi
82 exact hneg ⟨i, hgi⟩
83 have hbot : ∀ x : G, (∀ i, x ∈ c i) → x = 1 :=
84 (subgroupChainInf_eq_bot_iff (c := c)).mp h
85 exact hg (hbot g hgall)
86 · intro h
87 rw [subgroupChainInf_eq_bot_iff (c := c)]
88 intro g hgall
89 by_contra hg1
90 rcases h g hg1 with ⟨i, hgi⟩
91 exact hgi (hgall i)
93end Chains
95end ProCGroups.LocalWeight