ProCGroups.Generation.QuotientGeneratorConvergingPairs
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
import
structure QuotientGeneratorConvergingPair where
N : Subgroup G
normal_N : N.Normal
closed_N : IsClosed (N : Set G)
Y : Set (G ⧸ N)
subset_compl : Y ⊆ ({1} : Set (G ⧸ N))ᶜ
converges : ConvergesToOne (G := G ⧸ N) Y
generates : TopologicallyGenerates (G := G ⧸ N) YA quotient generator converging pair records compatible source and quotient generator data.
def QuotientGeneratorConvergingPair.sourceSet
(A : QuotientGeneratorConvergingPair (G := G)) :
Set (G ⧸ A.N) :=
({1} : Set (G ⧸ A.N)) ∪ A.YThe source set is the set of generators carried by the quotient generator pair.
abbrev QuotientGeneratorConvergingPair.Source
(A : QuotientGeneratorConvergingPair (G := G)) :=
↥(A.sourceSet)instance instTopologicalSpaceQuotientGeneratorConvergingPairSource
(A : QuotientGeneratorConvergingPair (G := G)) :
TopologicalSpace A.Source :=
inferInstanceAs (TopologicalSpace ↥(A.sourceSet))The constructed object carries the topological space structure inherited from its construction.
def QuotientGeneratorConvergingPair.sourceOne
(A : QuotientGeneratorConvergingPair (G := G)) : A.Source :=
⟨1, Or.inl rfl⟩The identity element belongs to the source data of the quotient generator pair.
def QuotientGeneratorConvergingPair.sourceOfY
(A : QuotientGeneratorConvergingPair (G := G)) (y : A.Y) : A.Source :=
⟨y.1, Or.inr y.2⟩theorem QuotientGeneratorConvergingPair.source_cases
(A : QuotientGeneratorConvergingPair (G := G)) (x : A.Source) :
x = A.sourceOne ∨ ∃ y : A.Y, x = A.sourceOfY yShow proof
by
rcases x with ⟨x, hx⟩
rcases hx with hx1 | hxY
· left
ext
simpa [QuotientGeneratorConvergingPair.sourceOne] using hx1
· right
refine ⟨⟨x, hxY⟩, ?_⟩
ext
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.
□def QuotientGeneratorConvergingPair.yImage
(A B : QuotientGeneratorConvergingPair (G := G))
(σ : A.Source → G ⧸ B.N) : Set (G ⧸ B.N) :=
Set.range fun y : A.Y => σ (A.sourceOfY y)def QuotientGeneratorConvergingPair.Le
(A B : QuotientGeneratorConvergingPair (G := G)) : Prop :=
∃ hBA : B.N ≤ A.N,
∃ σ : A.Source → (G ⧸ B.N),
Continuous σ ∧
(∀ x : A.Source, leftQuotientProjection (B.N) (A.N) hBA (σ x) = x.1) ∧
σ A.sourceOne = 1 ∧
(∀ y : A.Y, σ (A.sourceOfY y) ∈ B.Y) ∧
B.Y \ A.yImage B σ ⊆
{q : G ⧸ B.N | leftQuotientProjection (B.N) (A.N) hBA q = 1}This relation orders quotient generator pairs by refinement of their quotient data.
instance instLEQuotientGeneratorConvergingPair :
LE (QuotientGeneratorConvergingPair (G := G)) where
le := QuotientGeneratorConvergingPair.LeThe order relation is the refinement relation on the corresponding data.
instance instPreorderQuotientGeneratorConvergingPair :
Preorder (QuotientGeneratorConvergingPair (G := G)) where
le_refl A := by
refine ⟨le_rfl, Subtype.val, ?_, ?_, rfl, ?_, ?_⟩
· change Continuous (fun x : A.Source => (x : G ⧸ A.N))
exact continuous_subtype_val
· intro q
simp only [leftQuotientProjection_id, id_eq]
· intro y
simp only [QuotientGeneratorConvergingPair.sourceOfY, Subtype.coe_prop]
· simp only [QuotientGeneratorConvergingPair.yImage, QuotientGeneratorConvergingPair.sourceOfY,
Subtype.range_coe_subtype, setOf_mem_eq, sdiff_self, bot_eq_empty, leftQuotientProjection_id, id_eq,
setOf_eq_eq_singleton, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff, implies_true]
le_trans A B C hAB hBC := by
classical
rcases hAB with ⟨hBA, σAB, hσABcont, hσABright, hσABone, hσABmem, hσABdiff⟩
rcases hBC with ⟨hCB, σBC, hσBCcont, hσBCright, hσBCone, hσBCmem, hσBCdiff⟩
let τ : A.Source → B.Source := fun x =>
⟨σAB x, by
rcases A.source_cases x with h1 | ⟨y, rfl⟩
· rw [h1]
exact Or.inl hσABone
· exact Or.inr (hσABmem y)⟩
have hτcont : Continuous τ := by
exact hσABcont.subtype_mk <| by
intro x
rcases A.source_cases x with h1 | ⟨y, rfl⟩
· rw [h1]
exact Or.inl hσABone
· exact Or.inr (hσABmem y)
have hτone : τ A.sourceOne = B.sourceOne := by
apply Subtype.ext
exact hσABone
have hτofY (y : A.Y) :
τ (A.sourceOfY y) = B.sourceOfY ⟨σAB (A.sourceOfY y), hσABmem y⟩ := by
apply Subtype.ext
rfl
have hEqBC :
∀ (y : B.Y) {q : G ⧸ C.N},
q ∈ C.Y →
leftQuotientProjection (C.N) (B.N) hCB q = y.1 →
q = σBC (B.sourceOfY y) := by
intro y q hqY hqproj
by_cases hqim : q ∈ B.yImage C σBC
· rcases hqim with ⟨y', hy'Eq⟩
have hproj' :
leftQuotientProjection (C.N) (B.N) hCB q = y'.1 := by
simpa [hy'Eq] using hσBCright (B.sourceOfY y')
have hyEq : y' = y := by
apply Subtype.ext
exact hproj'.symm.trans hqproj
simpa [hyEq] using hy'Eq.symm
· have hker :
leftQuotientProjection (C.N) (B.N) hCB q = 1 := hσBCdiff ⟨hqY, hqim⟩
have hyne : y.1 ≠ 1 := by
simpa using B.subset_compl y.2
exact False.elim (hyne (hqproj.symm.trans hker))
refine ⟨hCB.trans hBA, fun x => σBC (τ x), hσBCcont.comp hτcont, ?_, ?_, ?_, ?_⟩
· intro x
calc
leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) (σBC (τ x)) =
leftQuotientProjection (B.N) (A.N) hBA
(leftQuotientProjection (C.N) (B.N) hCB (σBC (τ x))) := by
exact leftQuotientProjection_comp_apply_symm
(K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
(L := (A.N : Subgroup G)) hCB hBA (σBC (τ x))
_ = leftQuotientProjection (B.N) (A.N) hBA ((τ x).1) := by
rw [hσBCright (τ x)]
_ = leftQuotientProjection (B.N) (A.N) hBA (σAB x) := by
rfl
_ = x.1 := hσABright x
· simpa [hτone] using hσBCone
· intro y
let yB : B.Y := ⟨σAB (A.sourceOfY y), hσABmem y⟩
simpa [hτofY, yB] using hσBCmem yB
· intro q hq
rcases hq with ⟨hqY, hqnotAC⟩
by_cases hqimB : q ∈ B.yImage C σBC
· rcases hqimB with ⟨z, hzEq⟩
have hzNotInA : z.1 ∉ A.yImage B σAB := by
intro hzInA
rcases hzInA with ⟨y, hyEq⟩
let yB : B.Y := ⟨σAB (A.sourceOfY y), hσABmem y⟩
have hprojqz :
leftQuotientProjection (C.N) (B.N) hCB q = z.1 := by
simpa [hzEq] using hσBCright (B.sourceOfY z)
have hprojq :
leftQuotientProjection (C.N) (B.N) hCB q = yB.1 := by
calc
leftQuotientProjection (C.N) (B.N) hCB q = z.1 := hprojqz
_ = yB.1 := by
simpa [yB] using hyEq.symm
have hqEq : q = σBC (B.sourceOfY yB) := hEqBC yB hqY hprojq
have hqInAC : q ∈ A.yImage C (fun x => σBC (τ x)) := by
refine ⟨y, ?_⟩
simpa [hτofY] using hqEq.symm
exact hqnotAC hqInAC
have hzProjA :
leftQuotientProjection (B.N) (A.N) hBA z.1 = 1 :=
hσABdiff ⟨z.2, hzNotInA⟩
have hprojqB :
leftQuotientProjection (C.N) (B.N) hCB q = z.1 := by
simpa [hzEq] using hσBCright (B.sourceOfY z)
calc
leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) q =
leftQuotientProjection (B.N) (A.N) hBA
(leftQuotientProjection (C.N) (B.N) hCB q) := by
exact leftQuotientProjection_comp_apply_symm
(K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
(L := (A.N : Subgroup G)) hCB hBA q
_ = leftQuotientProjection (B.N) (A.N) hBA z.1 := by
rw [hprojqB]
_ = 1 := hzProjA
· have hprojqB :
leftQuotientProjection (C.N) (B.N) hCB q = 1 := hσBCdiff ⟨hqY, hqimB⟩
calc
leftQuotientProjection (C.N) (A.N) (hCB.trans hBA) q =
leftQuotientProjection (B.N) (A.N) hBA
(leftQuotientProjection (C.N) (B.N) hCB q) := by
exact leftQuotientProjection_comp_apply_symm
(K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
(L := (A.N : Subgroup G)) hCB hBA q
_ = leftQuotientProjection (B.N) (A.N) hBA 1 := by
rw [hprojqB]
_ = 1 := by
rflThe preorder is induced by refinement of the corresponding data.
noncomputable def QuotientGeneratorConvergingPair.le_hBA
{A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
B.N ≤ A.N :=
Classical.choose hABThe refinement relation includes the required compatibility between the source and target quotient data.
noncomputable def QuotientGeneratorConvergingPair.le_map
{A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
A.Source → G ⧸ B.N :=
Classical.choose (Classical.choose_spec hAB)The refinement relation provides the induced map between quotient generator pairs.
theorem QuotientGeneratorConvergingPair.le_map_continuous
{A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
Continuous (A.le_map hAB)For a refinement of quotient generator pairs, the chosen lift map between source sets is continuous.
Show proof
(Classical.choose_spec (Classical.choose_spec hAB)).1Proof. 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. 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.
□@[simp] theorem QuotientGeneratorConvergingPair.le_map_right
{A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)
(x : A.Source) :
leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) (A.le_map hAB x) = x.1The quotient generator pair is compatible with the specified quotient map.
Show proof
(Classical.choose_spec (Classical.choose_spec hAB)).2.1 xProof. 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.
□@[simp] theorem QuotientGeneratorConvergingPair.le_map_one
{A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
A.le_map hAB A.sourceOne = 1The quotient generator pair is compatible with the specified quotient map.
Show proof
(Classical.choose_spec (Classical.choose_spec hAB)).2.2.1Proof. 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.
□@[simp] theorem QuotientGeneratorConvergingPair.le_map_mem
{A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)
(y : A.Y) :
A.le_map hAB (A.sourceOfY y) ∈ B.YUnder a refinement, the chosen lift map sends every distinguished generator of the smaller pair into the distinguished set of the larger pair.
Show proof
(Classical.choose_spec (Classical.choose_spec hAB)).2.2.2.1 yProof. 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 QuotientGeneratorConvergingPair.le_map_diff
{A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B) :
B.Y \ A.yImage B (A.le_map hAB) ⊆
{q : G ⧸ B.N |
leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = 1}Elements of the larger distinguished set not in the lifted image project to the identity in the smaller quotient.
Show proof
(Classical.choose_spec (Classical.choose_spec hAB)).2.2.2.2Proof. 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 QuotientGeneratorConvergingPair.eq_le_map_of_mem_of_proj_eq
{A B : QuotientGeneratorConvergingPair (G := G)} (hAB : A ≤ B)
(y : A.Y) {q : G ⧸ B.N}
(hqY : q ∈ B.Y)
(hqproj : leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = y.1) :
q = A.le_map hAB (A.sourceOfY y)The quotient generator comparison respects membership and projection equality.
Show proof
by
by_cases hqim : q ∈ A.yImage B (A.le_map hAB)
· rcases hqim with ⟨y', hy'Eq⟩
have hproj' :
leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = y'.1 := by
simpa [hy'Eq] using A.le_map_right hAB (A.sourceOfY y')
have hyEq : y' = y := by
ext
exact hproj'.symm.trans hqproj
simpa [hyEq] using hy'Eq.symm
· have hker :
leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) q = 1 :=
A.le_map_diff hAB ⟨hqY, hqim⟩
have hyne : y.1 ≠ 1 := by
simpa using A.subset_compl y.2
exact False.elim (hyne (hqproj.symm.trans hker))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. 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 QuotientGeneratorConvergingPair.le_map_compat
{A B C : QuotientGeneratorConvergingPair (G := G)}
(hAB : A ≤ B) (hAC : A ≤ C) (hBC : B ≤ C)
(y : A.Y) :
leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
(A.le_map hAC (A.sourceOfY y)) =
A.le_map hAB (A.sourceOfY y)The induced map between quotient generator pairs is compatible with refinement.
Show proof
by
have hCy :
A.le_map hAC (A.sourceOfY y) ∈ C.Y := A.le_map_mem hAC y
have hIn :
A.le_map hAC (A.sourceOfY y) ∈ B.yImage C (B.le_map hBC) := by
by_contra hNot
have hker :
leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
(A.le_map hAC (A.sourceOfY y)) = 1 :=
B.le_map_diff hBC ⟨hCy, hNot⟩
have hy1 : y.1 = 1 := by
calc
y.1 = leftQuotientProjection (C.N) (A.N) (A.le_hBA hAC)
(A.le_map hAC (A.sourceOfY y)) := by
exact (A.le_map_right hAC (A.sourceOfY y)).symm
_ = leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB)
(leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
(A.le_map hAC (A.sourceOfY y))) := by
exact
(leftQuotientProjection_comp_apply_symm
(K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
(L := (A.N : Subgroup G)) (B.le_hBA hBC) (A.le_hBA hAB)
(A.le_map hAC (A.sourceOfY y)))
_ = leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB) 1 := by rw [hker]
_ = 1 := by rfl
have hyne : y.1 ≠ 1 := by
simpa using A.subset_compl y.2
exact hyne hy1
rcases hIn with ⟨z, hzEq⟩
have hqY :
leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
(A.le_map hAC (A.sourceOfY y)) ∈ B.Y := by
have hEq :
leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
(A.le_map hAC (A.sourceOfY y)) = z.1 := by
simpa [hzEq] using B.le_map_right hBC (B.sourceOfY z)
exact hEq ▸ z.2
have hqproj :
leftQuotientProjection (B.N) (A.N) (A.le_hBA hAB)
(leftQuotientProjection (C.N) (B.N) (B.le_hBA hBC)
(A.le_map hAC (A.sourceOfY y))) = y.1 := by
exact (leftQuotientProjection_comp_apply
(K := (C.N : Subgroup G)) (H := (B.N : Subgroup G))
(L := (A.N : Subgroup G)) (B.le_hBA hBC) (A.le_hBA hAB)
(A.le_map hAC (A.sourceOfY y))).trans
(A.le_map_right hAC (A.sourceOfY y))
exact A.eq_le_map_of_mem_of_proj_eq hAB y hqY hqprojProof. 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 ConvergesToOne.range_subtype_pointed
{H : Type v} [Group H] [TopologicalSpace H]
(hG : IsProfiniteGroup G) {X : Set G}
{f : ↥((({1} : Set G) ∪ X)) → H}
(hf : Continuous f)
(hf1 : f ⟨1, Or.inl rfl⟩ = 1)
(hX : ConvergesToOne (G := G) X) :
ConvergesToOne (G := H)
(Set.range fun x : X => f ⟨x.1, Or.inr x.2⟩)The range subtype of a pointed map contains the chosen basepoint.
Show proof
by
letI : T2Space G := IsProfiniteGroup.t2Space hG
let S : Set G := ({1} : Set G) ∪ X
let g : X → H := fun x => f ⟨x.1, Or.inr x.2⟩
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
intro U
have hpre : IsOpen (f ⁻¹' (U : Set H)) :=
(openSubgroup_isOpen (G := H) U).preimage hf
have h1pre : (⟨1, Or.inl rfl⟩ : ↥S) ∈ f ⁻¹' (U : Set H) := by
simp only [singleton_union, mem_preimage, hf1, SetLike.mem_coe, one_mem, S]
rcases isOpen_induced_iff.mp hpre with ⟨W, hWopen, hWeq⟩
have h1W : (1 : G) ∈ W := by
have : (⟨1, Or.inl rfl⟩ : ↥S) ∈ Subtype.val ⁻¹' W := by
exact hWeq.symm ▸ h1pre
simpa using this
rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hWopen h1W with ⟨V, hVW⟩
have hsubset :
Set.range g \ (U : Set H) ⊆ g '' {x : X | (x : G) ∉ (V : Set G)} := by
intro y hy
rcases hy with ⟨hyY, hyU⟩
rcases hyY with ⟨x, rfl⟩
refine ⟨x, ?_, rfl⟩
intro hxV
have hxW : (x : G) ∈ W := hVW hxV
have hxpre : (⟨x.1, Or.inr x.2⟩ : ↥S) ∈ Subtype.val ⁻¹' W := by
simpa [S] using hxW
have hxpreU : (⟨x.1, Or.inr x.2⟩ : ↥S) ∈ f ⁻¹' (U : Set H) := by
exact hWeq ▸ hxpre
have : g x ∈ (U : Set H) := by
simpa [g] using hxpreU
exact hyU this
have hfinite_pre : {x : X | (x : G) ∉ (V : Set G)}.Finite := by
let e : X ↪ G := ⟨Subtype.val, Subtype.val_injective⟩
have hfinite : (X \ (V : Set G)).Finite := hX V.toOpenSubgroup
have hfinite' : {x : X | e x ∈ X ∧ e x ∉ (V : Set G)}.Finite := by
simpa [Set.preimage] using hfinite.preimage_embedding e
have hEq : {x : X | e x ∈ X ∧ e x ∉ (V : Set G)} = {x : X | (x : G) ∉ (V : Set G)} := by
ext x
simp only [Function.Embedding.coeFn_mk, Subtype.coe_prop, SetLike.mem_coe, true_and, mem_setOf_eq, e]
exact hEq ▸ hfinite'
exact hfinite_pre.image g |>.subset hsubsetProof. 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 exists_quotientPair_le_openSubgroup_of_chain_iInf_le [CompactSpace G]
{c : Set (QuotientGeneratorConvergingPair (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)The quotient generator-converging-pair construction is compatible with open-normal finite quotients and refinement maps.
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 : QuotientGeneratorConvergingPair (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 (QuotientGeneratorConvergingPair.le_hBA (hmax p hp)) 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\). 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 quotientGeneratorPair_exists_liftToInf
(hG : IsProfiniteGroup G)
{c : Set (QuotientGeneratorConvergingPair (G := G))}
(hc : IsChain (· ≤ ·) c) (a : c) :
let K : Subgroup GA chain of quotient generator pairs has a refinement lifting to the intersection of its kernels.
Show proof
iInf fun p : c => p.1.N
letI : K.Normal := Subgroup.normal_iInf_normal fun p : c => p.1.normal_N
∃ σ : a.1.Source → G ⧸ K,
Continuous σ ∧
(∀ b : c, ∀ hab : a.1 ≤ b.1,
leftQuotientProjection K b.1.N
(iInf_le (fun p : c => p.1.N) b) ∘ σ =
a.1.le_map hab) ∧
σ a.1.sourceOne = 1 := by
classical
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
let Tail := {b : c // a.1 ≤ b.1}
letI : Nonempty Tail := ⟨⟨a, le_rfl⟩⟩
let L : Tail → ClosedSubgroup G := fun b =>
⟨b.1.1.N, b.1.1.closed_N⟩
have hL : ∀ {i j : Tail}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G) := by
intro i j hij
exact QuotientGeneratorConvergingPair.le_hBA hij
have hdir : Directed (· ≤ ·) (id : Tail → Tail) := by
intro i j
by_cases hij : i ≤ j
· exact ⟨j, hij, le_rfl⟩
· have hji : j ≤ i := by
by_cases hEq : i = j
· exact hEq ▸ le_rfl
· rcases hc i.1.2 j.1.2 (by
intro h
exact hEq (Subtype.ext (Subtype.ext h))) with hij' | hji'
· exact False.elim (hij hij')
· exact hji'
exact ⟨i, le_rfl, hji⟩
let η : ∀ b : Tail, a.1.Source → G ⧸ (L b : Subgroup G) := fun b =>
a.1.le_map b.2
have hηcont : ∀ b : Tail, Continuous (η b) := by
intro b
exact a.1.le_map_continuous b.2
have hηcompat : ∀ {i j : Tail} (hij : i ≤ j),
leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j = η i := by
intro i j hij
funext x
rcases a.1.source_cases x with rfl | ⟨y, rfl⟩
· have h1j : η j a.1.sourceOne = 1 := by
change a.1.le_map j.2 a.1.sourceOne = 1
exact a.1.le_map_one j.2
have h1i : η i a.1.sourceOne = 1 := by
change a.1.le_map i.2 a.1.sourceOne = 1
exact a.1.le_map_one i.2
calc
(leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j)
a.1.sourceOne
= leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij)
(η j a.1.sourceOne) := by
simp only [Function.comp]
_ = leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) 1 := by
rw [h1j]
_ = 1 := by rfl
_ = η i a.1.sourceOne := by rw [h1i]
· simpa [η] using a.1.le_map_compat i.2 j.2 hij y
have hηone : ∀ b : Tail, η b a.1.sourceOne = 1 := by
intro b
change a.1.le_map b.2 a.1.sourceOne = 1
exact a.1.le_map_one b.2
obtain ⟨ηinf, hηinf_continuous, hηinf_fac, hηinf_one⟩ :=
exists_continuous_leftQuotient_lift_of_directed
(G := G) hG L hL hdir η hηcont hηcompat a.1.sourceOne hηone
let H : Subgroup G := ((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)
have hKeq : H = K := by
apply le_antisymm
· refine le_iInf ?_
intro p
by_cases hap : a.1 ≤ p.1
· exact iInf_le (fun b : Tail => (L b : Subgroup G)) ⟨p, hap⟩
· have hKa :
H ≤ a.1.N :=
iInf_le (fun b : Tail => (L b : Subgroup G)) ⟨a, le_rfl⟩
by_cases hEq : p = a
· simpa [K, hEq] using hKa
· rcases hc p.2 a.2 (by
intro h
exact hEq (Subtype.ext h)) with hpa | hap'
· exact hKa.trans (QuotientGeneratorConvergingPair.le_hBA hpa)
· exact False.elim (hap hap')
· refine le_iInf ?_
intro b
exact iInf_le (fun p : c => p.1.N) b.1
letI : H.Normal := by
exact Subgroup.normal_iInf_normal fun b : Tail => b.1.1.normal_N
have hGoal :
∃ σ : a.1.Source → G ⧸ H,
Continuous σ ∧
(∀ b : c, ∀ hab : a.1 ≤ b.1,
leftQuotientProjection H b.1.N
(closedSubgroup_sInf_le (L := L) ⟨b, hab⟩) ∘ σ =
a.1.le_map hab) ∧
σ a.1.sourceOne = 1 := by
refine ⟨ηinf, hηinf_continuous, ?_, hηinf_one⟩
intro b hab
simpa [Tail, L, η] using hηinf_fac ⟨b, hab⟩
have hGoal' :
∃ σ : a.1.Source → G ⧸ H,
Continuous σ ∧
(∀ b : c, ∀ hab : a.1 ≤ b.1,
leftQuotientProjection H b.1.N
(hKeq.trans_le (iInf_le (fun p : c => p.1.N) b)) ∘ σ =
a.1.le_map hab) ∧
σ a.1.sourceOne = 1 := by
rcases hGoal with ⟨σ, hσcont, hσfac, hσone⟩
refine ⟨σ, hσcont, ?_, hσone⟩
intro b hab
simpa using hσfac b hab
change
∃ σ : a.1.Source → G ⧸ K,
Continuous σ ∧
(∀ b : c, ∀ hab : a.1 ≤ b.1,
leftQuotientProjection K b.1.N
(iInf_le (fun p : c => p.1.N) b) ∘ σ =
a.1.le_map hab) ∧
σ a.1.sourceOne = 1
let Data : Type _ := { J : Subgroup G // J.Normal ∧ ∀ b : c, J ≤ b.1.N }
let P : Data → Prop := fun d =>
letI : d.1.Normal := d.2.1
∃ σ : a.1.Source → G ⧸ d.1,
Continuous σ ∧
(∀ b : c, ∀ hab : a.1 ≤ b.1,
leftQuotientProjection d.1 b.1.N (d.2.2 b) ∘ σ =
a.1.le_map hab) ∧
σ a.1.sourceOne = 1
let dH : Data :=
⟨H, ⟨inferInstance, fun b => hKeq.trans_le (iInf_le (fun p : c => p.1.N) b)⟩⟩
let dK : Data :=
⟨K, ⟨inferInstance, fun b => iInf_le (fun p : c => p.1.N) b⟩⟩
have hd : dH = dK := by
apply Subtype.ext
exact hKeq
have hPdH : P dH := by
simpa [P, dH] using hGoal'
have hPdK : P dK := by
exact Eq.mp (congrArg P hd) hPdH
simpa [P, dK] using hPdKProof. 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.
□noncomputable def quotientGeneratorPairTop :
QuotientGeneratorConvergingPair (G := G) where
N := ⊤
normal_N := by infer_instance
closed_N := isClosed_univ
Y := ∅
subset_compl := by intro q hq; simp only [mem_empty_iff_false] at hq
converges := by intro U; simp only [empty_diff, finite_empty]
generates := by
classical
rw [TopologicallyGenerates]
apply top_unique
intro q hq
rcases Quotient.exists_rep q with ⟨g, rfl⟩
have hg1 : QuotientGroup.mk' (⊤ : Subgroup G) g = (1 : G ⧸ (⊤ : Subgroup G)) := by
exact (QuotientGroup.eq_one_iff (N := (⊤ : Subgroup G)) g).2 (by simp only [Subgroup.mem_top])
have hbot :
QuotientGroup.mk' (⊤ : Subgroup G) g ∈ (⊥ : Subgroup (G ⧸ (⊤ : Subgroup G))) := by
change QuotientGroup.mk' (⊤ : Subgroup G) g = (1 : G ⧸ (⊤ : Subgroup G))
exact hg1
simpa [Subgroup.closure_eq] using
(Subgroup.le_topologicalClosure (⊥ : Subgroup (G ⧸ (⊤ : Subgroup G))) hbot)theorem quotientGeneratorPair_exists_strictExtension
(hG : IsProfiniteGroup G)
(p : QuotientGeneratorConvergingPair (G := G))
(hne : p.N ≠ ⊥) :
∃ p' : QuotientGeneratorConvergingPair (G := G), p ≤ p' ∧ ¬ p' ≤ pShow proof
by
classical
rcases (Subgroup.ne_bot_iff_exists_ne_one).1 hne with ⟨m, hmne⟩
have hmne' : (m : G) ≠ 1 := by
intro hm1
apply hmne
ext
simpa using hm1
rcases exists_openNormalSubgroup_not_mem (G := G) hG hmne' with ⟨U, hmU⟩
let N' : Subgroup G := (U : Subgroup G) ⊓ p.N
have hN'closed : IsClosed (N' : Set G) := by
exact (openNormalSubgroup_isClosed (G := G) U).inter p.closed_N
have hN'proper : ¬ p.N ≤ N' := by
intro hp
exact hmU (hp m.2).1
obtain ⟨σ, hσcont, hσright, hσone⟩ :=
leftQuotientProjection_hasContinuousSection
(G := G) hG
⟨N', hN'closed⟩
⟨p.N, p.closed_N⟩
inf_le_right
rcases exists_finite_subset_generating_subgroup_mod_openNormal (G := G) hG
(M := p.N) (hMclosed := p.closed_N) U with ⟨T, hTfin, hTsub, hTgen⟩
let Tbar : Set (G ⧸ N') := (QuotientGroup.mk' N') '' T
let Y' : Set (G ⧸ N') := σ '' p.Y ∪ Tbar
have hY'compl : Y' ⊆ ({1} : Set (G ⧸ N'))ᶜ := by
intro q hq
rcases hq with hq | hq
· rcases hq with ⟨y, hy, rfl⟩
intro hq1
have hσy1 : σ y = 1 := by
simpa using hq1
have : y = 1 := by
calc
y = leftQuotientProjection (N') (p.N) inf_le_right (σ y) := (hσright y).symm
_ = leftQuotientProjection (N') (p.N) inf_le_right 1 := by rw [hσy1]
_ = 1 := rfl
exact p.subset_compl hy this
· rcases hq with ⟨t, ht, rfl⟩
intro hq1
have htN' : t ∈ N' := (QuotientGroup.eq_one_iff (N := N') t).1 hq1
exact (hTsub ht).2 htN'
have hY'conv : ConvergesToOne (G := G ⧸ N') Y' := by
let hGquot : IsProfiniteGroup (G ⧸ p.N) :=
isProfinite_quotient_closedNormal (G := G) hG p.closed_N
letI : T2Space (G ⧸ p.N) := IsProfiniteGroup.t2Space hGquot
intro V
have hσconv :
((σ '' p.Y) \ (V : Set (G ⧸ N'))).Finite := by
exact
(ConvergesToOne.image_of_continuous_pointed
(G := G ⧸ p.N) (H := G ⧸ N')
hGquot
hσcont hσone p.converges) V
have hTconv : (Tbar \ (V : Set (G ⧸ N'))).Finite :=
(hTfin.image (QuotientGroup.mk' N')).subset (by
intro q hq
exact hq.1)
exact (hσconv.union hTconv).subset (by
intro q hq
rcases hq with ⟨hqY, hqV⟩
rcases hqY with hqσ | hqT
· exact Or.inl ⟨hqσ, hqV⟩
· exact Or.inr ⟨hqT, hqV⟩)
have hY'gen :
TopologicallyGenerates (G := G ⧸ N') Y' := by
exact topologicallyGenerates_of_quotient_section_union_kernel
(G := G) hG p.closed_N hN'closed inf_le_right
p.generates hσright hTgen
refine ⟨{ N := N'
normal_N := by infer_instance
closed_N := hN'closed
Y := Y'
subset_compl := hY'compl
converges := hY'conv
generates := hY'gen }, ?_, ?_⟩
· let σ' : p.Source → G ⧸ N' := fun x => σ x.1
refine ⟨inf_le_right, σ', ?_, ?_, ?_, ?_, ?_⟩
· change Continuous (fun x : p.Source => σ x.1)
exact hσcont.comp continuous_subtype_val
· intro x
exact hσright x.1
· exact hσone
· intro q
exact Or.inl ⟨q.1, q.2, rfl⟩
· intro q hq
rcases hq with ⟨hqY', hqnotσ⟩
rcases hqY' with hqσ | hqT
· rcases hqσ with ⟨y, hy, rfl⟩
exact False.elim (hqnotσ ⟨⟨y, hy⟩, rfl⟩)
· rcases hqT with ⟨t, ht, rfl⟩
have htN : t ∈ p.N := (hTsub ht).1
simpa [leftQuotientProjection_mk] using
(QuotientGroup.eq_one_iff (N := p.N) t).2 htN
· intro hp'
exact hN'proper hp'.1Proof. 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 isClosed_bot_subgroup (hG : IsProfiniteGroup G) :
IsClosed (((⊥ : Subgroup G) : Set G))The trivial subgroup of a profinite group is closed.
Show proof
by
letI : T2Space G := IsProfiniteGroup.t2Space hG
exact (isClosed_singleton : IsClosed ({(1 : G)} : Set G))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. 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 closedNormalQuotientSection_bot_eq (hG : IsProfiniteGroup G) :
closedNormalQuotientSection (G := G) hG
(N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG) =
(quotientBotContinuousMulEquiv (G := G) hG).symmThe closed-normal quotient section at the bottom subgroup is the identity section.
Show proof
by
funext q
apply (quotientBotContinuousMulEquiv (G := G) hG).injective
have h1 :
quotientBotContinuousMulEquiv (G := G) hG
(closedNormalQuotientSection (G := G) hG
(N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG) q) = q := by
simpa [quotientBotContinuousMulEquiv] using
(closedNormalQuotientSection_rightInverse (G := G) hG
(N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG) q)
have h2 :
quotientBotContinuousMulEquiv (G := G) hG
((quotientBotContinuousMulEquiv (G := G) hG).symm q) = q := by
simp only [ContinuousMulEquiv.apply_symm_apply]
exact h1.trans h2.symmProof. 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.
□noncomputable def QuotientGeneratorConvergingPair.toAmbientSet
(p : QuotientGeneratorConvergingPair (G := G))
(hG : IsProfiniteGroup G) : Set G :=
closedNormalQuotientSection (G := G) hG (N := p.N) p.closed_N '' p.YThe quotient generator pair maps its source set into the ambient generating set.
theorem QuotientGeneratorConvergingPair.toAmbientSet_generatesAndConvergesToOne
(p : QuotientGeneratorConvergingPair (G := G))
(hG : IsProfiniteGroup G) (hbot : p.N = ⊥) :
GeneratesAndConvergesToOne (G := G) (p.toAmbientSet hG)The ambient representatives attached to a quotient generator pair topologically generate and converge to one.
Show proof
by
rcases p with ⟨N, hNnormal, hNclosed, Y, hYcompl, hYconv, hYgen⟩
cases hbot
constructor
· let e : (G ⧸ (⊥ : Subgroup G)) ≃ₜ* G := (quotientBotContinuousMulEquiv (G := G) hG).symm
have hgen :
TopologicallyGenerates (G := G)
(e '' Y) := topologicallyGenerates_continuousMulEquiv_image
(G := G ⧸ (⊥ : Subgroup G)) e hYgen
rw [QuotientGeneratorConvergingPair.toAmbientSet, closedNormalQuotientSection_bot_eq]
simpa using hgen
· let hqbot : IsProfiniteGroup (G ⧸ (⊥ : Subgroup G)) :=
IsProfiniteGroup.ofContinuousMulEquiv
(G := G) hG (quotientBotContinuousMulEquiv (G := G) hG)
have hconv :
ConvergesToOne (G := G)
((closedNormalQuotientSection (G := G) hG
(N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG)) '' Y) := by
exact ConvergesToOne.image_of_continuous_pointed
(G := G ⧸ (⊥ : Subgroup G)) (H := G)
hqbot
(closedNormalQuotientSection_continuous (G := G) hG
(N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG))
(closedNormalQuotientSection_one (G := G) hG
(N := (⊥ : Subgroup G)) (isClosed_bot_subgroup (G := G) hG))
hYconv
rw [QuotientGeneratorConvergingPair.toAmbientSet]
simpa [closedNormalQuotientSection_bot_eq] using hconvProof. 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 quotientGeneratorPair_exists_upperBound_of_chain
(hG : IsProfiniteGroup G)
(c : Set (QuotientGeneratorConvergingPair (G := G)))
(hc : IsChain (· ≤ ·) c) (hcn : c.Nonempty) :
∃ ub : QuotientGeneratorConvergingPair (G := G), ∀ a ∈ c, a ≤ ubEvery nonempty chain of quotient generator pairs has an upper bound.
Show proof
by
classical
letI : CompactSpace G := IsProfiniteGroup.compactSpace 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)
let hGquotK : IsProfiniteGroup (G ⧸ K) :=
isProfinite_quotient_closedNormal (G := G) hG hKclosed
letI : T2Space (G ⧸ K) := IsProfiniteGroup.t2Space hGquotK
letI : TotallyDisconnectedSpace (G ⧸ K) :=
IsProfiniteGroup.totallyDisconnectedSpace hGquotK
let lift : (a : c) → a.1.Source → G ⧸ K := fun a =>
Classical.choose (quotientGeneratorPair_exists_liftToInf (G := G) hG hc a)
have hlift_continuous : ∀ a : c, Continuous (lift a) := by
intro a
exact (Classical.choose_spec
(quotientGeneratorPair_exists_liftToInf (G := G) hG hc a)).1
have hlift_fac :
∀ (a b : c) (hab : a.1 ≤ b.1),
leftQuotientProjection K b.1.N
(iInf_le (fun p : c => p.1.N) b) ∘ lift a =
a.1.le_map hab := by
intro a b hab
exact (Classical.choose_spec
(quotientGeneratorPair_exists_liftToInf (G := G) hG hc a)).2.1 b hab
have hlift_one : ∀ a : c, lift a a.1.sourceOne = 1 := by
intro a
exact (Classical.choose_spec
(quotientGeneratorPair_exists_liftToInf (G := G) hG hc a)).2.2
have exists_stage_above_le_open :
∀ (a : c) {U : OpenSubgroup G}, K ≤ (U : Subgroup G) →
∃ b : c, a.1 ≤ b.1 ∧ b.1.N ≤ (U : Subgroup G) := by
intro a U hKU
let d : Set (QuotientGeneratorConvergingPair (G := G)) :=
{p | p ∈ c ∧ a.1 ≤ p}
have hdchain : IsChain (· ≤ ·) d := by
intro x hx y hy hxy
exact hc hx.1 hy.1 hxy
have hdne : d.Nonempty := ⟨a.1, a.2, le_rfl⟩
have hdEq : iInf (fun p : d => p.1.N) = K := by
apply le_antisymm
· refine le_iInf ?_
intro p
by_cases hap : a.1 ≤ p.1
· exact iInf_le (fun q : d => q.1.N) ⟨p.1, p.2, hap⟩
· have hda :
iInf (fun q : d => q.1.N) ≤ a.1.N :=
iInf_le (fun q : d => q.1.N) ⟨a.1, a.2, le_rfl⟩
by_cases hEq : p.1 = a.1
· simpa [hEq] using hda
· rcases hc p.2 a.2 hEq with hpa | hap'
· exact hda.trans (QuotientGeneratorConvergingPair.le_hBA hpa)
· exact False.elim (hap hap')
· refine le_iInf ?_
intro p
exact iInf_le (fun q : c => q.1.N) ⟨p.1, p.2.1⟩
have hdKU : iInf (fun p : d => p.1.N) ≤ (U : Subgroup G) := by
simpa [hdEq] using hKU
rcases exists_quotientPair_le_openSubgroup_of_chain_iInf_le
(G := G) hdchain hdne U hdKU with ⟨b, hbU⟩
exact ⟨⟨b.1, b.2.1⟩, b.2.2, hbU⟩
let stageImage : c → Set (G ⧸ K) := fun a =>
Set.range fun y : a.1.Y => lift a (a.1.sourceOfY y)
have hlift_eq_of_le :
∀ {a b : c} (hAB : a.1 ≤ b.1) (y : a.1.Y),
lift a (a.1.sourceOfY y) =
lift b (b.1.sourceOfY
⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩) := by
intro a b hAB y
let yb : b.1.Y :=
⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩
let q1 := lift a (a.1.sourceOfY y)
let q2 := lift b (b.1.sourceOfY yb)
have hmem :
∀ W : OpenNormalSubgroup (G ⧸ K), q1⁻¹ * q2 ∈ (W : Set (G ⧸ K)) := by
intro W
let V : OpenNormalSubgroup G :=
OpenNormalSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W
have hKV : K ≤ (V : Subgroup G) := by
intro g hg
change QuotientGroup.mk' K g ∈ W
have hg1 : QuotientGroup.mk' K g = (1 : G ⧸ K) :=
(QuotientGroup.eq_one_iff (N := K) g).2 hg
rw [hg1]
exact W.one_mem'
obtain ⟨p, hbp, hpV⟩ := exists_stage_above_le_open b hKV
have hcompat :
a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y) =
b.1.le_map hbp (b.1.sourceOfY yb) := by
have hqY :
a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y) ∈ p.1.Y :=
a.1.le_map_mem (hAB.trans hbp) y
have hqproj :
leftQuotientProjection (p.1.N) (b.1.N) (b.1.le_hBA hbp)
(a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y)) = yb.1 := by
simpa [yb] using a.1.le_map_compat hAB (hAB.trans hbp) hbp y
exact b.1.eq_le_map_of_mem_of_proj_eq hbp yb hqY hqproj
have hEqp :
leftQuotientProjection K p.1.N
(iInf_le (fun r : c => r.1.N) p) q1 =
leftQuotientProjection K p.1.N
(iInf_le (fun r : c => r.1.N) p) q2 := by
have hq1 :=
congrFun (hlift_fac a p (hAB.trans hbp)) (a.1.sourceOfY y)
have hq2 :=
congrFun (hlift_fac b p hbp) (b.1.sourceOfY yb)
calc
leftQuotientProjection K p.1.N
(iInf_le (fun r : c => r.1.N) p) q1
= a.1.le_map (hAB.trans hbp) (a.1.sourceOfY y) := by
simpa [q1] using hq1
_ = b.1.le_map hbp (b.1.sourceOfY yb) := hcompat
_ = leftQuotientProjection K p.1.N
(iInf_le (fun r : c => r.1.N) p) q2 := by
simpa [q2] using hq2.symm
have hEqV :
leftQuotientProjection K (V : Subgroup G) hKV q1 =
leftQuotientProjection K (V : Subgroup G) hKV q2 := by
calc
leftQuotientProjection K (V : Subgroup G) hKV q1
= leftQuotientProjection (p.1.N) (V : Subgroup G) hpV
(leftQuotientProjection K p.1.N
(iInf_le (fun r : c => r.1.N) p) q1) := by
exact
leftQuotientProjection_comp_apply_symm
(K := (K : Subgroup G)) (H := (p.1.N : Subgroup G))
(L := (V : Subgroup G)) (iInf_le (fun r : c => r.1.N) p)
hpV q1
_ = leftQuotientProjection (p.1.N) (V : Subgroup G) hpV
(leftQuotientProjection K p.1.N
(iInf_le (fun r : c => r.1.N) p) q2) := by
rw [hEqp]
_ = leftQuotientProjection K (V : Subgroup G) hKV q2 := by
exact (leftQuotientProjection_comp_apply_symm
(K := (K : Subgroup G)) (H := (p.1.N : Subgroup G))
(L := (V : Subgroup G)) (iInf_le (fun r : c => r.1.N) p) hpV q2).symm
revert hEqV
refine Quotient.inductionOn₂' q1 q2 ?_
intro g1 g2 hEqV
change QuotientGroup.mk' K (g1⁻¹ * g2) ∈ W
have hEqV' :
QuotientGroup.mk' (V : Subgroup G) g1 =
QuotientGroup.mk' (V : Subgroup G) g2 := by
simpa [leftQuotientProjection_mk] using hEqV
have hgV : g1⁻¹ * g2 ∈ (V : Subgroup G) := (QuotientGroup.eq).1 hEqV'
simpa [V, OpenNormalSubgroup.mem_comap] using hgV
have hq1 :
q1⁻¹ * q2 = 1 := by
exact IsProfiniteGroup.eq_one_of_mem_all_openNormalSubgroups
(G := G ⧸ K) hmem
calc
q1 = q1 * 1 := by simp only [mul_one]
_ = q1 * (q1⁻¹ * q2) := by rw [hq1]
_ = q2 := by simp only [mul_inv_cancel_left]
have hstage_mono :
∀ {a b : c} (hAB : a.1 ≤ b.1), stageImage a ⊆ stageImage b := by
intro a b hAB q hq
rcases hq with ⟨y, rfl⟩
refine ⟨⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩, ?_⟩
exact (hlift_eq_of_le hAB y).symm
have hstage_diff :
∀ {a b : c} (hAB : a.1 ≤ b.1),
stageImage b \ stageImage a ⊆
{q : G ⧸ K |
leftQuotientProjection K a.1.N
(iInf_le (fun p : c => p.1.N) a) q = 1} := by
intro a b hAB q hq
rcases hq.1 with ⟨yb, rfl⟩
by_cases hybim : yb.1 ∈ a.1.yImage b.1 (a.1.le_map hAB)
· rcases hybim with ⟨y, hyEq⟩
have hEq :
lift b (b.1.sourceOfY yb) = lift a (a.1.sourceOfY y) := by
calc
lift b (b.1.sourceOfY yb)
= lift b (b.1.sourceOfY
⟨a.1.le_map hAB (a.1.sourceOfY y), a.1.le_map_mem hAB y⟩) := by
simp only [hyEq, Subtype.coe_eta]
_ = lift a (a.1.sourceOfY y) := (hlift_eq_of_le hAB y).symm
exact False.elim (hq.2 ⟨y, hEq.symm⟩)
· have hybker :
leftQuotientProjection (b.1.N) (a.1.N) (a.1.le_hBA hAB) yb.1 = 1 :=
a.1.le_map_diff hAB ⟨yb.2, hybim⟩
have hqb :
leftQuotientProjection K b.1.N
(iInf_le (fun p : c => p.1.N) b)
(lift b (b.1.sourceOfY yb)) = yb.1 := by
calc
leftQuotientProjection K b.1.N
(iInf_le (fun p : c => p.1.N) b)
(lift b (b.1.sourceOfY yb)) = b.1.le_map le_rfl (b.1.sourceOfY yb) := by
exact congrFun (hlift_fac b b le_rfl) (b.1.sourceOfY yb)
_ = yb.1 := by
simpa [QuotientGeneratorConvergingPair.le_map,
QuotientGeneratorConvergingPair.le_hBA] using
b.1.le_map_right le_rfl (b.1.sourceOfY yb)
calc
leftQuotientProjection K a.1.N
(iInf_le (fun p : c => p.1.N) a)
(lift b (b.1.sourceOfY yb))
= leftQuotientProjection (b.1.N) (a.1.N) (a.1.le_hBA hAB)
(leftQuotientProjection K b.1.N
(iInf_le (fun p : c => p.1.N) b)
(lift b (b.1.sourceOfY yb))) := by
exact
(leftQuotientProjection_comp_apply
(K := (K : Subgroup G)) (H := (b.1.N : Subgroup G))
(L := (a.1.N : Subgroup G)) (iInf_le (fun p : c => p.1.N) b)
(a.1.le_hBA hAB) (lift b (b.1.sourceOfY yb))).symm
_ = leftQuotientProjection (b.1.N) (a.1.N) (a.1.le_hBA hAB) yb.1 := by
rw [hqb]
_ = 1 := hybker
let Y : Set (G ⧸ K) := ⋃ a : c, stageImage a
have hYcompl : Y ⊆ ({1} : Set (G ⧸ K))ᶜ := by
intro q hq
rcases mem_iUnion.mp hq with ⟨a, hqa⟩
rcases hqa with ⟨y, rfl⟩
have hqy :
leftQuotientProjection K a.1.N
(iInf_le (fun p : c => p.1.N) a)
(lift a (a.1.sourceOfY y)) = y.1 := by
have hliftProjection := congrFun (hlift_fac a a le_rfl) (a.1.sourceOfY y)
calc
leftQuotientProjection K a.1.N
(iInf_le (fun p : c => p.1.N) a)
(lift a (a.1.sourceOfY y))
= a.1.le_map le_rfl (a.1.sourceOfY y) := by
simpa using hliftProjection
_ = y.1 := by
simpa [QuotientGeneratorConvergingPair.le_map,
QuotientGeneratorConvergingPair.le_hBA] using
a.1.le_map_right le_rfl (a.1.sourceOfY y)
intro hq1
have hq1' : lift a (a.1.sourceOfY y) = 1 := by simpa using hq1
have hy1 : y.1 = 1 := by
calc
y.1 = leftQuotientProjection K a.1.N
(iInf_le (fun p : c => p.1.N) a)
(lift a (a.1.sourceOfY y)) := hqy.symm
_ = leftQuotientProjection K a.1.N
(iInf_le (fun p : c => p.1.N) a) 1 := by rw [hq1']
_ = 1 := by rfl
exact a.1.subset_compl y.2 hy1
have hYconv : ConvergesToOne (G := G ⧸ K) Y := by
intro W
let V : OpenSubgroup G :=
OpenSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W
have hKV : K ≤ (V : Subgroup G) := by
intro g hg
change QuotientGroup.mk' K g ∈ W
have hg1 : QuotientGroup.mk' K g = (1 : G ⧸ K) :=
(QuotientGroup.eq_one_iff (N := K) g).2 hg
rw [hg1]
exact W.one_mem'
rcases exists_quotientPair_le_openSubgroup_of_chain_iInf_le
(G := G) hc hcn V (by simpa [K] using hKV) with ⟨a, haV⟩
have hstageconv : ConvergesToOne (G := G ⧸ K) (stageImage a) := by
let hGquotA : IsProfiniteGroup (G ⧸ a.1.N) :=
isProfinite_quotient_closedNormal (G := G) hG a.1.closed_N
letI : T2Space (G ⧸ a.1.N) := IsProfiniteGroup.t2Space hGquotA
letI : TotallyDisconnectedSpace (G ⧸ a.1.N) :=
IsProfiniteGroup.totallyDisconnectedSpace hGquotA
simpa [stageImage] using
(ConvergesToOne.range_subtype_pointed
(G := G ⧸ a.1.N) (H := G ⧸ K)
hGquotA (hf := hlift_continuous a) (hf1 := hlift_one a) (hX := a.1.converges))
have hsubset : Y \ (W : Set (G ⧸ K)) ⊆ stageImage a \ (W : Set (G ⧸ K)) := by
intro q hq
rcases hq with ⟨hqY, hqW⟩
rcases mem_iUnion.mp hqY with ⟨b, hbq⟩
by_cases hba : b.1 ≤ a.1
· exact ⟨hstage_mono hba hbq, hqW⟩
· have hcmp : a.1 ≤ b.1 := by
by_cases hEq : a = b
· exact hEq ▸ le_rfl
· rcases hc a.2 b.2 (by
intro h
exact hEq (Subtype.ext h)) with hab | hba'
· exact hab
· exact False.elim (hba hba')
by_cases hqa : q ∈ stageImage a
· exact ⟨hqa, hqW⟩
· have hq1 :
leftQuotientProjection K a.1.N
(iInf_le (fun p : c => p.1.N) a) q = 1 :=
hstage_diff hcmp ⟨hbq, hqa⟩
have hqWin : q ∈ W := by
rcases Quotient.exists_rep q with ⟨g, rfl⟩
change QuotientGroup.mk' K g ∈ W
have hgA : g ∈ a.1.N := by
simpa [leftQuotientProjection_mk] using
(QuotientGroup.eq_one_iff (N := a.1.N) g).1 hq1
have hgV : g ∈ (V : Subgroup G) := haV hgA
simpa [V, OpenSubgroup.mem_comap] using hgV
exact False.elim (hqW hqWin)
exact (hstageconv W).subset hsubset
have hYgen : TopologicallyGenerates (G := G ⧸ K) Y := by
have hbotclosed : IsClosed ((⊥ : Subgroup (G ⧸ K)) : Set (G ⧸ K)) := by
change IsClosed ({(1 : G ⧸ K)} : Set (G ⧸ K))
simp only [finite_singleton, Finite.isClosed]
have hgen1 :
TopologicallyGenerates (G := G ⧸ K) (Y ∪ ({1} : Set (G ⧸ K))) := by
apply (topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient
(G := G ⧸ K) hGquotK
(N := (⊥ : Subgroup (G ⧸ K))) (X := Y)).2
intro W hbotW
let V : OpenNormalSubgroup G :=
OpenNormalSubgroup.comap (QuotientGroup.mk' K) QuotientGroup.continuous_mk W
have hKV : K ≤ (V : Subgroup G) := by
intro g hg
change QuotientGroup.mk' K g ∈ W
have hg1 : QuotientGroup.mk' K g = (1 : G ⧸ K) :=
(QuotientGroup.eq_one_iff (N := K) g).2 hg
rw [hg1]
exact W.one_mem'
rcases exists_quotientPair_le_openSubgroup_of_chain_iInf_le
(G := G) hc hcn V.toOpenSubgroup (by simpa [K] using hKV) with ⟨a, haV⟩
have hVaClosed : IsClosed ((V : Subgroup G) : Set G) :=
openNormalSubgroup_isClosed (G := G) V
have hmapW :
((V : Subgroup G).map (QuotientGroup.mk' K)) = (W : Subgroup (G ⧸ K)) := by
ext q
rcases Quotient.exists_rep q with ⟨g, rfl⟩
constructor
· rintro ⟨g', hg'V, hg'q⟩
have : QuotientGroup.mk' K g' ∈ W := by
simpa [V, OpenNormalSubgroup.mem_comap] using hg'V
simpa [hg'q] using this
· intro hgW
refine ⟨g, ?_, rfl⟩
simpa [V, OpenNormalSubgroup.mem_comap] using hgW
let QV : Subgroup (G ⧸ K) := (V : Subgroup G).map (QuotientGroup.mk' K)
let Wmap : OpenNormalSubgroup (G ⧸ K) :=
{ toOpenSubgroup :=
{ toSubgroup := QV
isOpen' := by
simpa [QV, hmapW] using W.isOpen' }
isNormal' := by
simpa [QV, hmapW] using (show (W : Subgroup (G ⧸ K)).Normal from inferInstance) }
have hWmap : Wmap = W := by
ext q
change q ∈ QV ↔ q ∈ (W : Subgroup (G ⧸ K))
simp only [hmapW, OpenSubgroup.mem_toSubgroup, QV]
let e0 :
((G ⧸ K) ⧸ QV) ≃ₜ* G ⧸ (V : Subgroup G) :=
quotientQuotientContinuousMulEquiv
(G := G) hG hVaClosed hKclosed hKV
have hstageProj :
∀ y : a.1.Y,
leftQuotientProjection K (V : Subgroup G) hKV
(lift a (a.1.sourceOfY y)) =
leftQuotientProjection a.1.N (V : Subgroup G) haV y.1 := by
intro y
have hqy0 :=
congrFun (hlift_fac a a le_rfl) (a.1.sourceOfY y)
have hqy :
leftQuotientProjection K a.1.N
(iInf_le (fun p : c => p.1.N) a)
(lift a (a.1.sourceOfY y)) = y.1 := by
calc
leftQuotientProjection K a.1.N
(iInf_le (fun p : c => p.1.N) a)
(lift a (a.1.sourceOfY y)) = a.1.le_map le_rfl (a.1.sourceOfY y) := by
exact hqy0
_ = y.1 := by
simpa [QuotientGeneratorConvergingPair.le_map,
QuotientGeneratorConvergingPair.le_hBA] using
a.1.le_map_right le_rfl (a.1.sourceOfY y)
calc
leftQuotientProjection K (V : Subgroup G) hKV
(lift a (a.1.sourceOfY y))
= leftQuotientProjection (a.1.N) (V : Subgroup G) haV
(leftQuotientProjection K a.1.N
(iInf_le (fun p : c => p.1.N) a)
(lift a (a.1.sourceOfY y))) := by
exact
leftQuotientProjection_comp_apply_symm
(K := (K : Subgroup G)) (H := (a.1.N : Subgroup G))
(L := (V : Subgroup G)) (iInf_le (fun p : c => p.1.N) a) haV
(lift a (a.1.sourceOfY y))
_ = leftQuotientProjection (a.1.N) (V : Subgroup G) haV y.1 := by
rw [hqy]
have hstageImgEq :
(leftQuotientProjection K (V : Subgroup G) hKV) '' stageImage a =
(leftQuotientProjection a.1.N (V : Subgroup G) haV) '' a.1.Y := by
ext q
constructor
· rintro ⟨x, ⟨y, rfl⟩, rfl⟩
exact ⟨y.1, y.2, (hstageProj y).symm⟩
· rintro ⟨y, hyY, hyq⟩
let y' : a.1.Y := ⟨y, hyY⟩
refine ⟨lift a (a.1.sourceOfY y'), ⟨y', rfl⟩, ?_⟩
calc
leftQuotientProjection K (V : Subgroup G) hKV
(lift a (a.1.sourceOfY y'))
= leftQuotientProjection a.1.N (V : Subgroup G) haV y := by
simpa [y'] using hstageProj y'
_ = q := hyq
have hstageGenV :
TopologicallyGenerates (G := G ⧸ (V : Subgroup G))
((leftQuotientProjection K (V : Subgroup G) hKV) '' stageImage a) := by
let fV : (G ⧸ a.1.N) →* G ⧸ (V : Subgroup G) :=
{ toFun := leftQuotientProjection a.1.N (V : Subgroup G) haV
map_one' := rfl
map_mul' := by
intro x y
refine Quotient.inductionOn₂' x y ?_
intro g h
rfl }
have hgenV :
TopologicallyGenerates (G := G ⧸ (V : Subgroup G))
(fV '' a.1.Y) := by
exact topologicallyGenerates_image_of_continuousSurjective
(G := G ⧸ a.1.N) (H := G ⧸ (V : Subgroup G)) fV
(by
simpa [fV] using
(continuous_leftQuotientProjection
(G := G) (K := a.1.N) (H := (V : Subgroup G)) haV))
(by
simpa [fV] using
(surjective_leftQuotientProjection
(G := G) (K := a.1.N) (H := (V : Subgroup G)) haV))
a.1.generates
rw [hstageImgEq]
simpa [fV] using hgenV
have hquotProj0 :
∀ y : G ⧸ K,
e0 ((QuotientGroup.mk' QV) y) =
leftQuotientProjection K (V : Subgroup G) hKV y := by
intro y
refine Quotient.inductionOn y ?_
intro g
rfl
have hquotPreimgEq0 :
e0.symm '' ((leftQuotientProjection K (V : Subgroup G) hKV) '' Y) =
(QuotientGroup.mk' QV '' Y) := by
ext q
constructor
· rintro ⟨z, ⟨y, hy, hzy⟩, hqz⟩
refine ⟨y, hy, ?_⟩
have hzq : z = e0 q := by
calc
z = e0 (e0.symm z) := by symm; exact e0.right_inv z
_ = e0 q := by rw [hqz]
have heqy : e0 ((QuotientGroup.mk' QV) y) = z := by
exact (hquotProj0 y).trans hzy
exact e0.injective (heqy.trans hzq)
· rintro ⟨y, hy, rfl⟩
refine ⟨leftQuotientProjection K (V : Subgroup G) hKV y, ⟨y, hy, rfl⟩, ?_⟩
calc
e0.symm (leftQuotientProjection K (V : Subgroup G) hKV y)
= e0.symm (e0 ((QuotientGroup.mk' QV) y)) := by
rw [hquotProj0 y]
_ = QuotientGroup.mk' QV y := e0.left_inv _
have hgenYV :
TopologicallyGenerates (G := G ⧸ (V : Subgroup G))
((leftQuotientProjection K (V : Subgroup G) hKV) '' Y) := by
exact topologicallyGenerates_mono hstageGenV (by
intro q hq
rcases hq with ⟨x, hx, rfl⟩
exact ⟨x, mem_iUnion.mpr ⟨a, hx⟩, rfl⟩)
have hgenQuot0 :
TopologicallyGenerates (G := ((G ⧸ K) ⧸ QV))
((QuotientGroup.mk' QV) '' Y) := by
rw [← hquotPreimgEq0]
exact topologicallyGenerates_continuousMulEquiv_image
(G := G ⧸ (V : Subgroup G)) e0.symm hgenYV
have hgenQuotMap :
TopologicallyGenerates
(G := ((G ⧸ K) ⧸ (Wmap : Subgroup (G ⧸ K))))
((QuotientGroup.mk' (Wmap : Subgroup (G ⧸ K))) '' Y) := by
simpa [QV, Wmap] using hgenQuot0
have hgenQuot :
TopologicallyGenerates (G := ((G ⧸ K) ⧸ (W : Subgroup (G ⧸ K))))
((QuotientGroup.mk' (W : Subgroup (G ⧸ K))) '' Y) := by
simpa using (hWmap ▸ hgenQuotMap)
exact hgenQuot
exact (topologicallyGenerates_union_one_iff (G := G ⧸ K) (X := Y)).1 hgen1
refine ⟨{ N := K
normal_N := inferInstance
closed_N := hKclosed
Y := Y
subset_compl := hYcompl
converges := hYconv
generates := hYgen }, ?_⟩
intro a ha
let a' : c := ⟨a, ha⟩
refine ⟨iInf_le (fun p : c => p.1.N) a', lift a', ?_, ?_, ?_, ?_, ?_⟩
· exact hlift_continuous a'
· intro x
have hliftProjection := congrFun (hlift_fac a' a' le_rfl) x
calc
leftQuotientProjection K a.N (iInf_le (fun p : c => p.1.N) a')
(lift a' x) = a.le_map le_rfl x := by
simpa using hliftProjection
_ = x.1 := by
simpa [QuotientGeneratorConvergingPair.le_map,
QuotientGeneratorConvergingPair.le_hBA] using
a.le_map_right le_rfl x
· exact hlift_one a'
· intro y
exact mem_iUnion.mpr ⟨a', ⟨y, rfl⟩⟩
· intro q hq
rcases mem_iUnion.mp hq.1 with ⟨b, hbq⟩
by_cases hba : b.1 ≤ a
· exact False.elim (hq.2 (hstage_mono (a := b) (b := a') hba hbq))
· have hab : a ≤ b.1 := by
by_cases hEq : a = b.1
· exact hEq ▸ le_rfl
· rcases hc ha b.2 (by
intro h
exact hEq h) with hab | hba'
· exact hab
· exact False.elim (hba hba')
exact hstage_diff (a := a') (b := b) hab ⟨hbq, hq.2⟩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 exists_generatorsConvergingToOne (hG : IsProfiniteGroup G) :
∃ X : Set G, GeneratesAndConvergesToOne (G := G) X4.4. Existence theorem used by the public theorem.
Show proof
by
classical
let Pair := QuotientGeneratorConvergingPair (G := G)
letI : Nonempty Pair := ⟨quotientGeneratorPairTop (G := G)⟩
obtain ⟨m, hmmax⟩ := zorn_le_nonempty (α := Pair) <| by
intro c hc hcn
rcases quotientGeneratorPair_exists_upperBound_of_chain (G := G) hG c hc hcn with
⟨ub, hub⟩
exact ⟨ub, hub⟩
have hmbot : m.N = ⊥ := by
by_contra hne
rcases quotientGeneratorPair_exists_strictExtension (G := G) hG m hne with
⟨m', hmm', hm'm⟩
exact hm'm (hmmax hmm')
exact ⟨m.toAmbientSet hG, m.toAmbientSet_generatesAndConvergesToOne hG hmbot⟩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. 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.
□theorem GeneratesAndConvergesToOne.image_of_continuousSurjective
(hG : IsProfiniteGroup G)
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(f : G →* H) (hf : Continuous f) (hfsurj : Function.Surjective f)
{X : Set G} (hX : GeneratesAndConvergesToOne (G := G) X) :
GeneratesAndConvergesToOne (G := H) (f '' X)A surjective continuous homomorphism preserves generating sets converging to \(1\).
Show proof
by
refine ⟨?_, ?_⟩
· exact topologicallyGenerates_image_of_continuousSurjective
(G := G) (H := H) f hf hfsurj hX.1
· exact ConvergesToOne.image_of_continuous_pointed
(G := G) (H := H) hG hf (by simp only [map_one]) hX.2Proof. 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. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage. 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 GeneratesAndConvergesToOne.image_of_continuousMulEquiv
(hG : IsProfiniteGroup G)
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(e : G ≃ₜ* H) {X : Set G}
(hX : GeneratesAndConvergesToOne (G := G) X) :
GeneratesAndConvergesToOne (G := H) (e '' X)A continuous multiplicative equivalence preserves generating sets converging to \(1\).
Show proof
by
refine ⟨?_, ?_⟩
· exact topologicallyGenerates_continuousMulEquiv_image
(G := G) e hX.1
· exact ConvergesToOne.image_of_continuous_pointed
(G := G) (H := H) hG e.continuous (by simp only [Homeomorph.homeomorph_mk_coe, ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toEquiv_eq_coe,
EquivLike.coe_coe, map_one]) hX.2Proof. 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. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. 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. 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 ConvergesToOne.image_of_continuousMulEquiv_iff
(hG : IsProfiniteGroup G)
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(hH : IsProfiniteGroup H)
(e : G ≃ₜ* H) {X : Set G} :
ConvergesToOne (G := H) (e '' X) ↔ ConvergesToOne (G := G) XConvergence to \(1\) is preserved and reflected by the indicated finite union, insertion, or continuous equivalence operation.
Show proof
by
constructor
· intro h
have hback : ConvergesToOne (G := G) (e.symm '' (e '' X)) :=
ConvergesToOne.image_of_continuous_pointed
(G := H) (H := G) hH e.symm.continuous (by simp only [Homeomorph.homeomorph_mk_coe, ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toEquiv_eq_coe,
EquivLike.coe_coe, map_one]) (X := e '' X) h
have himage : e.symm '' (e '' X) = X := by
ext x
constructor
· rintro ⟨y, ⟨z, hz, rfl⟩, rfl⟩
simpa using hz
· intro hx
exact ⟨e x, ⟨x, hx, rfl⟩, by simp only [ContinuousMulEquiv.symm_apply_apply]⟩
simpa [himage] using hback
· intro h
exact ConvergesToOne.image_of_continuous_pointed
(G := G) (H := H) hG e.continuous (by simp only [Homeomorph.homeomorph_mk_coe, ContinuousMulEquiv.toMulEquiv_eq_coe, MulEquiv.toEquiv_eq_coe,
EquivLike.coe_coe, map_one]) hProof. 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. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. 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. 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 GeneratesAndConvergesToOne.image_of_continuousMulEquiv_iff
(hG : IsProfiniteGroup G)
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(hH : IsProfiniteGroup H)
(e : G ≃ₜ* H) {X : Set G} :
GeneratesAndConvergesToOne (G := H) (e '' X) ↔ GeneratesAndConvergesToOne (G := G) XConvergence to \(1\) is preserved and reflected by the indicated finite union, insertion, or continuous equivalence operation.
Show proof
by
constructor
· intro h
exact ⟨
(topologicallyGenerates_continuousMulEquiv_image_iff (G := G) (H := H) e (X := X)).1 h.1,
(ConvergesToOne.image_of_continuousMulEquiv_iff
(G := G) (H := H) hG hH e (X := X)).1 h.2⟩
· intro h
exact ⟨
(topologicallyGenerates_continuousMulEquiv_image_iff (G := G) (H := H) e (X := X)).2 h.1,
(ConvergesToOne.image_of_continuousMulEquiv_iff
(G := G) (H := H) hG hH e (X := X)).2 h.2⟩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. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. 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. 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 topologicalRank_eq_of_continuousMulEquiv
(hG : IsProfiniteGroup G)
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(hH : IsProfiniteGroup H) (e : G ≃ₜ* H) :
topologicalRank G = topologicalRank HThe topological rank equality of continuous multiplicative equivalence is compatible with the profinite topology and gives the continuous map or equivalence determined by the finite-quotient data.
Show proof
by
apply le_antisymm
· rcases exists_generatorsConvergingToOne (G := H) hH with ⟨Y, hY⟩
rcases exists_generatesAndConvergesToOne_card_eq_topologicalRank
(G := H) ⟨Y, hY⟩ with
⟨Ymin, hYmin, hYcard⟩
calc
topologicalRank G ≤ Cardinal.mk (e.symm '' Ymin) := by
exact topologicalRank_le_mk_of_generatesAndConvergesToOne
(G := G)
(GeneratesAndConvergesToOne.image_of_continuousMulEquiv
(G := H) hH e.symm hYmin)
_ ≤ Cardinal.mk Ymin := Cardinal.mk_image_le
_ = topologicalRank H := hYcard
· rcases exists_generatorsConvergingToOne (G := G) hG with ⟨X, hX⟩
rcases exists_generatesAndConvergesToOne_card_eq_topologicalRank
(G := G) ⟨X, hX⟩ with
⟨Xmin, hXmin, hXcard⟩
calc
topologicalRank H ≤ Cardinal.mk (e '' Xmin) := by
exact topologicalRank_le_mk_of_generatesAndConvergesToOne
(G := H)
(GeneratesAndConvergesToOne.image_of_continuousMulEquiv
(G := G) hG e hXmin)
_ ≤ Cardinal.mk Xmin := Cardinal.mk_image_le
_ = topologicalRank G := hXcardProof. 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. 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.
□