ProCGroups.LocalWeight.SubgroupChains
This module studies subgroup chains for pro cgroups. A family of subgroups intended to model a chain appearing in the transfinite local-weight arguments. The set-theoretic union of the members of a subgroup chain.
abbrev SubgroupChain (ι : Type v) (G : Type u) [Group G] := ι → Subgroup GA family of subgroups intended to model a chain appearing in the transfinite local-weight arguments.
def subgroupChainCarrier (c : SubgroupChain ι G) : Set G :=
{ g | ∃ i, g ∈ c i }The set-theoretic union of the members of a subgroup chain.
def subgroupChainInf (c : SubgroupChain ι G) : Subgroup G :=
sInf (Set.range c)The infimum of all members of a subgroup chain.
@[simp] theorem mem_subgroupChainCarrier_iff {c : SubgroupChain ι G} {g : G} :
g ∈ subgroupChainCarrier c ↔ ∃ i, g ∈ c iMembership in the carrier of a subgroup chain is equivalent to the displayed coordinate condition.
Show proof
Iff.rflProof. Use the clopen-neighborhood basis of a profinite space. Left translations and continuous maps preserve clopen sets by continuity, and local-weight or cardinal estimates are obtained by counting the relevant clopen neighborhoods, finite discrete quotients, and maps determined on a topological generating set. The inequalities then follow from the standard basis and cardinal-arithmetic comparisons.
□theorem subgroupChainInf_le (c : SubgroupChain ι G) (i : ι) :
subgroupChainInf c ≤ c iThe infimum of a subgroup chain is contained in each subgroup in the chain.
Show proof
by
exact sInf_le (Set.mem_range_self i)Proof. Use the clopen-neighborhood basis of a profinite space. Left translations and continuous maps preserve clopen sets by continuity, and local-weight or cardinal estimates are obtained by counting the relevant clopen neighborhoods, finite discrete quotients, and maps determined on a topological generating set. The inequalities then follow from the standard basis and cardinal-arithmetic comparisons.
□@[simp] theorem mem_subgroupChainInf_iff {c : SubgroupChain ι G} {g : G} :
g ∈ subgroupChainInf c ↔ ∀ i, g ∈ c iMembership in the infimum of a subgroup chain is equivalent to the displayed coordinate condition.
Show proof
by
simp only [subgroupChainInf, Subgroup.mem_sInf, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]Proof. Use the clopen-neighborhood basis of a profinite space. Left translations and continuous maps preserve clopen sets by continuity, and local-weight or cardinal estimates are obtained by counting the relevant clopen neighborhoods, finite discrete quotients, and maps determined on a topological generating set. The inequalities then follow from the standard basis and cardinal-arithmetic comparisons.
□theorem subgroupChainInf_eq_bot_iff {c : SubgroupChain ι G} :
subgroupChainInf c = ⊥ ↔ ∀ g : G, (∀ i, g ∈ c i) → g = 1The subgroup-chain infimum is trivial exactly when every nontrivial element is excluded at some stage.
Show proof
by
constructor
· intro h g hg
have hmem : g ∈ subgroupChainInf c := by
exact (mem_subgroupChainInf_iff.mpr hg)
have : g ∈ (⊥ : Subgroup G) := by
simpa [h] using hmem
simpa using this
· intro h
ext g
constructor
· intro hg
have hgall : ∀ i, g ∈ c i :=
mem_subgroupChainInf_iff.mp hg
have : g = 1 := h g hgall
simp only [this, one_mem]
· intro hg
have hg1 : g = 1 := by
simpa using hg
subst hg1
exact (mem_subgroupChainInf_iff).2 (fun i => (c i).one_mem)Proof. Use the clopen-neighborhood basis of a profinite space. Left translations and continuous maps preserve clopen sets by continuity, and local-weight or cardinal estimates are obtained by counting the relevant clopen neighborhoods, finite discrete quotients, and maps determined on a topological generating set. The inequalities then follow from the standard basis and cardinal-arithmetic comparisons.
□theorem subgroupChainInf_eq_bot_iff_forall_ne_one {c : SubgroupChain ι G} :
subgroupChainInf c = ⊥ ↔ ∀ g : G, g ≠ 1 → ∃ i, g ∉ c iThe infimum of a subgroup chain is bottom exactly when every nontrivial element is excluded at some stage.
Show proof
by
constructor
· intro h g hg
by_contra hneg
have hgall : ∀ i, g ∈ c i := by
intro i
by_contra hgi
exact hneg ⟨i, hgi⟩
have hbot : ∀ x : G, (∀ i, x ∈ c i) → x = 1 :=
(subgroupChainInf_eq_bot_iff (c := c)).mp h
exact hg (hbot g hgall)
· intro h
rw [subgroupChainInf_eq_bot_iff (c := c)]
intro g hgall
by_contra hg1
rcases h g hg1 with ⟨i, hgi⟩
exact hgi (hgall i)Proof. Unfold the corresponding finite-stage, relator-set, or comparison construction. The claim follows by reading off the defining projection, relator family, deletion/replacement data, or inclusion map and checking the stated compatibility field.
□