Source: ProCGroups.LocalWeight.SubgroupChains
1import ProCGroups.ProC.OpenNormalSubgroups.CountableChains
3/-!
4# Intersections of subgroup chains
6This file packages linearly ordered families of subgroups, defines their carrier union and
7intersection, and gives membership and trivial-intersection criteria used in transfinite
8closed-normal series arguments.
9-/
11namespace ProCGroups.LocalWeight
13universe u v
16section Chains
18variable {ι : Type v}
19variable {G : Type u} [Group G]
21/-- A family of subgroups forming a chain indexed for transfinite local-weight statements. -/
22abbrev SubgroupChain (ι : Type v) (G : Type u) [Group G] := ι → Subgroup G
24/-- The set-theoretic union of the members of a subgroup chain. -/
25def subgroupChainCarrier (c : SubgroupChain ι G) : Set G :=
26 { g | ∃ i, g ∈ c i }
28/-- The infimum of all members of a subgroup chain. -/
29def subgroupChainInf (c : SubgroupChain ι G) : Subgroup G :=
30 sInf (Set.range c)
32/--
33Membership in the carrier of a subgroup chain is equivalent to the displayed coordinate
34condition.
35-/
36@[simp] theorem mem_subgroupChainCarrier_iff {c : SubgroupChain ι G} {g : G} :
37 g ∈ subgroupChainCarrier c ↔ ∃ i, g ∈ c i :=
38 Iff.rfl
40/-- The infimum of a subgroup chain is contained in each subgroup in the chain. -/
41theorem subgroupChainInf_le (c : SubgroupChain ι G) (i : ι) :
42 subgroupChainInf c ≤ c i := by
43 exact sInf_le (Set.mem_range_self i)
45/--
46Membership in the infimum of a subgroup chain is equivalent to the displayed coordinate
47condition.
48-/
49@[simp] theorem mem_subgroupChainInf_iff {c : SubgroupChain ι G} {g : G} :
50 g ∈ subgroupChainInf c ↔ ∀ i, g ∈ c i := by
51 simp only [subgroupChainInf, Subgroup.mem_sInf, Set.mem_range, forall_exists_index,
52 forall_apply_eq_imp_iff]
54/--
55The subgroup-chain infimum is trivial exactly when every nontrivial element is excluded at some
56stage.
57-/
58theorem subgroupChainInf_eq_bot_iff {c : SubgroupChain ι G} :
59 subgroupChainInf c = ⊥ ↔ ∀ g : G, (∀ i, g ∈ c i) → g = 1 := by
60 constructor
61 · intro h g hg
62 have hmem : g ∈ subgroupChainInf c := by
63 exact (mem_subgroupChainInf_iff.mpr hg)
64 have : g ∈ (⊥ : Subgroup G) := by
65 simpa [h] using hmem
66 simpa using this
67 · intro h
68 ext g
69 constructor
70 · intro hg
71 have hgall : ∀ i, g ∈ c i :=
72 mem_subgroupChainInf_iff.mp hg
73 have : g = 1 := h g hgall
74 simp only [this, one_mem]
75 · intro hg
76 have hg1 : g = 1 := by
77 simpa using hg
78 subst hg1
79 exact (mem_subgroupChainInf_iff).2 (fun i => (c i).one_mem)
81/--
82The infimum of a subgroup chain is bottom exactly when every nontrivial element is excluded at
83some stage.
84-/
85theorem subgroupChainInf_eq_bot_iff_forall_ne_one {c : SubgroupChain ι G} :
86 subgroupChainInf c = ⊥ ↔ ∀ g : G, g ≠ 1 → ∃ i, g ∉ c i := by
87 constructor
88 · intro h g hg
89 by_contra hneg
90 have hgall : ∀ i, g ∈ c i := by
91 intro i
92 by_contra hgi
93 exact hneg ⟨i, hgi⟩
94 have hbot : ∀ x : G, (∀ i, x ∈ c i) → x = 1 :=
95 (subgroupChainInf_eq_bot_iff (c := c)).mp h
96 exact hg (hbot g hgall)
97 · intro h
98 rw [subgroupChainInf_eq_bot_iff (c := c)]
99 intro g hgall
100 by_contra hg1
101 rcases h g hg1 with ⟨i, hgi⟩
102 exact hgi (hgall i)
104end Chains
106end ProCGroups.LocalWeight