import
def HasOpenNormalBasisInClass (C : FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] : Prop :=
∀ W : Set G, IsOpen W → (1 : G) ∈ W →
∃ U : OpenNormalSubgroup G,
((U : Subgroup G) : Set G) ⊆ W ∧ C (G ⧸ (U : Subgroup G))A neighborhood-basis formulation using open normal subgroups whose quotients lie in \(C\). We isolate it as a separate predicate because it is the main usable local output for later mathematicalization steps.
theorem mono {C D : FiniteGroupClass.{u}} {G : Type u} [Group G] [TopologicalSpace G]
(hbasis : HasOpenNormalBasisInClass C G)
(hmono : ∀ {Q : Type u} [Group Q], C Q → D Q) :
HasOpenNormalBasisInClass D GThe existence of an open-normal basis in a class is monotone under enlarging the finite-group class.
Show proof
by
intro W hW h1W
rcases hbasis W hW h1W with ⟨U, hUW, hCU⟩
exact ⟨U, hUW, hmono hCU⟩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.
□abbrev OpenNormalSubgroupInClass (C : FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] :=
{U : OpenNormalSubgroup G // C (G ⧸ (U : Subgroup G))}Open normal subgroups whose quotient lies in the chosen class \(C\). This packages the specified family as an actual type so later inverse-limit and basis constructions can quantify over it directly.
def ofOpenNormal (U : OpenNormalSubgroup G) (hU : C (G ⧸ (U : Subgroup G))) :
OpenNormalSubgroupInClass C G :=
⟨U, hU⟩Repackage an open normal subgroup together with a proof that its quotient lies in \(C\).
theorem quotient_mem (U : OpenNormalSubgroupInClass C G) :
C (G ⧸ (U.1 : Subgroup G))The quotient attached to a normal subgroup in the finite-quotient index family lies in \(C\).
Show proof
U.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. 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.
□def of_mono {D : FiniteGroupClass.{u}}
(hmono : ∀ {Q : Type u} [Group Q], C Q → D Q)
(U : OpenNormalSubgroupInClass C G) :
OpenNormalSubgroupInClass D G :=
⟨U.1, hmono U.2⟩Move an open-normal-in-class subgroup along an inclusion of finite-group classes.
def top [FiniteGroupClass.ContainsTrivialQuotients C] :
OpenNormalSubgroupInClass C G :=
⟨⊤, by
have hsub : Subsingleton (G ⧸ (⊤ : Subgroup G)) := by
constructor
intro x y
rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) x with ⟨a, rfl⟩
rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) y with ⟨b, rfl⟩
exact QuotientGroup.eq.2 (by simp only [Subgroup.mem_top])
exact FiniteGroupClass.ContainsTrivialQuotients.of_subsingleton hsub⟩The top subgroup belongs to any finite-group class containing trivial quotients.
theorem nonempty_of_containsTrivialQuotients [FiniteGroupClass.ContainsTrivialQuotients C] :
Nonempty (OpenNormalSubgroupInClass C G)There is an open-normal-in-class subgroup whenever the class contains trivial quotients.
Show proof
⟨top (C := C) (G := 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. 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.
□def of_allFinite [ContinuousMul G] [CompactSpace G] (U : OpenNormalSubgroup G) :
OpenNormalSubgroupInClass FiniteGroupClass.allFinite G :=
⟨U, openNormalSubgroup_finiteQuotient (G := G) U⟩Every open normal quotient of a compact group lies in the all-finite class.
noncomputable def comap {H : Type u} [Group H] [TopologicalSpace H]
(hHer : FiniteGroupClass.Hereditary C) (f : G →ₜ* H)
(U : OpenNormalSubgroupInClass C H) : OpenNormalSubgroupInClass C G :=
let N : OpenNormalSubgroup G :=
OpenNormalSubgroup.comap f.toMonoidHom f.continuous_toFun U.1
⟨N, by
let qmap : G ⧸ (N : Subgroup G) →* H ⧸ (U.1 : Subgroup H) :=
QuotientGroup.map (N := (N : Subgroup G)) (M := (U.1 : Subgroup H))
f.toMonoidHom (by
intro x hx
exact hx)
have hqmap_inj : Function.Injective qmap := by
rw [← MonoidHom.ker_eq_bot_iff qmap]
ext z
constructor
· intro hz
rcases QuotientGroup.mk'_surjective (N : Subgroup G) z with ⟨x, rfl⟩
have hxU : f x ∈ (U.1 : Subgroup H) := by
apply (QuotientGroup.eq_one_iff (N := (U.1 : Subgroup H)) (f x)).1
simpa [qmap, MonoidHom.mem_ker] using hz
exact (QuotientGroup.eq_one_iff (N := (N : Subgroup G)) x).2 hxU
· intro hz
subst z
simp only [one_mem]
exact hHer.of_injective U.2 qmap hqmap_inj⟩Pull back an open-normal-in-class subgroup along a continuous homomorphism, when the class is hereditary.
def mapOpenNormal {H : Type u} [Group H] [TopologicalSpace H]
(f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
(U : OpenNormalSubgroupInClass C G)
(hC : C (H ⧸ ((OpenNormalSubgroup.map f hfopen hfsurj U.1 : OpenNormalSubgroup H) :
Subgroup H))) :
OpenNormalSubgroupInClass C H :=
⟨OpenNormalSubgroup.map f hfopen hfsurj U.1, hC⟩An open surjective continuous homomorphism sends an open-normal-in-class subgroup to an open normal subgroup when target quotient membership is supplied explicitly. This is the lightweight bridge; stronger automatic versions can be derived from class closure hypotheses as needed.
def mapOpenNormal_of_formation {H : Type u} [Group H] [TopologicalSpace H]
(hForm : FiniteGroupClass.Formation C)
(f : G →ₜ* H) (hfopen : IsOpenMap f) (hfsurj : Function.Surjective f)
(U : OpenNormalSubgroupInClass C G) :
OpenNormalSubgroupInClass C H :=
mapOpenNormal (C := C) (G := G) f hfopen hfsurj U (by
let M : OpenNormalSubgroup H := OpenNormalSubgroup.map f hfopen hfsurj U.1
let qmap : G ⧸ (U.1 : Subgroup G) →* H ⧸ (M : Subgroup H) :=
QuotientGroup.map (N := (U.1 : Subgroup G)) (M := (M : Subgroup H))
f.toMonoidHom (by
intro x hx
exact ⟨x, hx, rfl⟩)
have hqmap_surj : Function.Surjective qmap :=
QuotientGroup.map_surjective_of_surjective
(N := (U.1 : Subgroup G)) (M : Subgroup H) f.toMonoidHom (by
intro y
rcases QuotientGroup.mk'_surjective (M : Subgroup H) y with ⟨h, rfl⟩
rcases hfsurj h with ⟨g, rfl⟩
exact ⟨g, rfl⟩) (by
intro x hx
exact ⟨x, hx, rfl⟩)
have hquot :
C ((G ⧸ (U.1 : Subgroup G)) ⧸ qmap.ker) :=
hForm.quotientClosed qmap.ker U.2
let e :
(G ⧸ (U.1 : Subgroup G)) ⧸ qmap.ker ≃*
H ⧸ (M : Subgroup H) :=
QuotientGroup.quotientKerEquivOfSurjective qmap hqmap_surj
exact hForm.isomClosed ⟨e⟩ hquot)An open surjective continuous homomorphism sends an in-class open normal subgroup to an in-class open normal subgroup. Formation closure supplies the target quotient membership.
def inf (hForm : FiniteGroupClass.Formation C)
(U V : OpenNormalSubgroupInClass C G) : OpenNormalSubgroupInClass C G :=
⟨U.1 ⊓ V.1,
FiniteGroupClass.Formation.quotient_inf_mem
(C := C) (G := G) hForm U.1 V.1 U.2 V.2⟩Finite intersections stay in class for a formation.
def quotientProj (U : OpenNormalSubgroupInClass C G) :
G →ₜ* G ⧸ (U.1 : Subgroup G) :=
OpenNormalSubgroup.quotientProj U.1The quotient projection attached to an open-normal-in-class subgroup.
theorem quotientProj_apply (U : OpenNormalSubgroupInClass C G) (x : G) :
quotientProj (C := C) U x = QuotientGroup.mk' (U.1 : Subgroup G) xThe quotient projection evaluates to the quotient class of the element.
Show proof
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. 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 quotientProj_surjective (U : OpenNormalSubgroupInClass C G) :
Function.Surjective (quotientProj (C := C) U)The quotient projection attached to an open-normal-in-class subgroup is surjective.
Show proof
OpenNormalSubgroup.quotientProj_surjective U.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. 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 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.
□theorem quotientProj_eq_one_iff {U : OpenNormalSubgroupInClass C G} {x : G} :
quotientProj (C := C) U x = 1 ↔ x ∈ (U.1 : Subgroup G)The kernel predicate of the quotient projection is membership in the subgroup.
Show proof
OpenNormalSubgroup.quotientProj_eq_one_iff (U := U.1)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. 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 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem quotientProj_eq_quotientProj_iff {U : OpenNormalSubgroupInClass C G} {x y : G} :
quotientProj (C := C) U x = quotientProj (C := C) U y ↔
x / y ∈ (U.1 : Subgroup G)Equality in the quotient attached to an open-normal-in-class subgroup.
Show proof
OpenNormalSubgroup.quotientProj_eq_quotientProj_iff (U := U.1)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 mem_ker_quotientProj [ContinuousMul G] {U : OpenNormalSubgroupInClass C G} {x : G} :
x ∈ OpenNormalSubgroup.ker (quotientProj (C := C) U) ↔
x ∈ (U.1 : Subgroup G)Kernel membership for the quotient projection attached to an open-normal-in-class subgroup.
Show proof
OpenNormalSubgroup.mem_ker_quotientProj (U := U.1)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. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For 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 ker_quotientProj [ContinuousMul G] (U : OpenNormalSubgroupInClass C G) :
((OpenNormalSubgroup.ker (quotientProj (C := C) U) : OpenNormalSubgroup G) :
Subgroup G) = (U.1 : Subgroup G)The open-normal kernel of the quotient projection is the original subgroup.
Show proof
OpenNormalSubgroup.ker_quotientProj U.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. 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. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For 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.
□def map {U V : OpenNormalSubgroupInClass C G}
(hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G)) :
G ⧸ (V.1 : Subgroup G) →* G ⧸ (U.1 : Subgroup G) :=
QuotientGroup.map _ _ (MonoidHom.id G) hUVThe canonical transition map between quotients attached to nested open normal subgroups in the class-indexing family.
theorem map_surjective {U V : OpenNormalSubgroupInClass C G}
(hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G)) :
Function.Surjective (map (C := C) (G := G) hUV)These transition maps are the natural quotient epimorphisms.
Show proof
by
intro x
rcases QuotientGroup.mk'_surjective (U.1 : Subgroup G) x with ⟨g, rfl⟩
exact ⟨QuotientGroup.mk' (V.1 : Subgroup G) g, rfl⟩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 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.
□theorem map_id (U : OpenNormalSubgroupInClass C G) :
map (C := C) (G := G) (le_rfl : (U.1 : Subgroup G) ≤ (U.1 : Subgroup G)) = MonoidHom.id _The identity transition map is the identity monoid homomorphism.
Show proof
by
simp only [map, QuotientGroup.map_id]Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. 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\). 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem map_comp {U V W : OpenNormalSubgroupInClass C G}
(hUV : (V.1 : Subgroup G) ≤ (U.1 : Subgroup G))
(hVW : (W.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
(map (C := C) (G := G) hUV).comp (map (C := C) (G := G) hVW) =
map (C := C) (G := G) (hVW.trans hUV)Maps induced on topological abelianizations compose as expected.
Show proof
by
simpa [map] using QuotientGroup.map_comp_map
(N := (W.1 : Subgroup G)) (M := (V.1 : Subgroup G)) (O := (U.1 : Subgroup G))
(f := MonoidHom.id G) (g := MonoidHom.id G) hVW hUVProof. 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\). 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.
□def transition [ContinuousMul G] {U V : OpenNormalSubgroupInClass C G}
(hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
G ⧸ (U.1 : Subgroup G) →ₜ* G ⧸ (V.1 : Subgroup G) :=
OpenNormalSubgroup.transition (G := G) (U := U.1) (V := V.1) hUVThe continuous transition map between quotients attached to nested open-normal-in-class subgroups.
theorem transition_mk [ContinuousMul G] {U V : OpenNormalSubgroupInClass C G}
(hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) (x : G) :
transition (C := C) (G := G) hUV (QuotientGroup.mk' (U.1 : Subgroup G) x) =
QuotientGroup.mk' (V.1 : Subgroup G) xTransition maps send quotient classes to the corresponding quotient classes.
Show proof
OpenNormalSubgroup.transition_mk (G := G) (U := U.1) (V := V.1) hUV 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. 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. 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 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem transition_comp_quotientProj [ContinuousMul G] {U V : OpenNormalSubgroupInClass C G}
(hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
(transition (C := C) (G := G) hUV).comp (quotientProj (C := C) U) =
quotientProj (C := C) VComposing the transition map with the smaller quotient projection gives the larger quotient projection.
Show proof
OpenNormalSubgroup.transition_comp_quotientProj (G := G) (U := U.1) (V := V.1) hUVProof. 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. 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 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem transition_surjective [ContinuousMul G] {U V : OpenNormalSubgroupInClass C G}
(hUV : (U.1 : Subgroup G) ≤ (V.1 : Subgroup G)) :
Function.Surjective (transition (C := C) (G := G) hUV)Transition maps between quotients by nested open-normal-in-class subgroups are surjective.
Show proof
OpenNormalSubgroup.transition_surjective (G := G) (U := U.1) (V := V.1) hUVProof. 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. 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 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. 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.
□def openNormalSubgroupInClassSystem (C : FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
InverseSystems.InverseSystem (I := OrderDual (OpenNormalSubgroupInClass C G)) where
X := fun U => G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
topologicalSpace := fun _ => inferInstance
map := fun {U V} hUV =>
OpenNormalSubgroupInClass.map (C := C) (G := G)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV
continuous_map := by
intro U V hUV
letI : DiscreteTopology
(G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)) :=
QuotientGroup.discreteTopology
(openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
exact continuous_of_discreteTopology
map_id := by
intro U
funext x
exact congrFun
(congrArg DFunLike.coe
(OpenNormalSubgroupInClass.map_id
(C := C) (G := G) (U := OrderDual.ofDual U))) x
map_comp := by
intro U V W hUV hVW
funext x
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual W).1 : OpenNormalSubgroup G) : Subgroup G)) x with ⟨g, rfl⟩
rflThe inverse system of quotient groups indexed by open normal subgroups whose quotients lie in \(C\), ordered by reverse inclusion.
instance instGroupOpenNormalSubgroupInClassSystemX
(U : OrderDual (OpenNormalSubgroupInClass C G)) :
Group ((openNormalSubgroupInClassSystem C G).X U) := by
dsimp [openNormalSubgroupInClassSystem]
infer_instanceEvery coordinate of the open-normal-in-class inverse system is a quotient group.
def openNormalSubgroupInClassProj
(U : OrderDual (OpenNormalSubgroupInClass C G)) :
G →* G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G) :=
QuotientGroup.mk' (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)The canonical quotient homomorphisms from \(G\) into the open-normal-subgroup inverse system whose quotients lie in \(C\).
theorem openNormalSubgroupInClassProj_compatible :
(openNormalSubgroupInClassSystem C G).CompatibleMaps
(fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
openNormalSubgroupInClassProj (C := C) (G := G) U)The canonical quotient homomorphisms are compatible with the transition maps.
Show proof
by
intro U V hUV
funext g
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. 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.
□instance instIsGroupSystemOpenNormalSubgroupInClassSystem :
InverseSystems.IsGroupSystem (openNormalSubgroupInClassSystem C G) where
map_one := by
intro i j hij
change
OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij 1 = 1
exact
(OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_one
map_mul := by
intro i j hij x y
change
OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij (x * y) =
OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x *
OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij y
exact
(OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_mul x y
map_inv := by
intro i j hij x
change
OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x⁻¹ =
(OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij x)⁻¹
exact
(OpenNormalSubgroupInClass.map
(C := C) (G := G)
(U := OrderDual.ofDual i) (V := OrderDual.ofDual j) hij).map_inv xThe quotient system attached to open normal subgroups in \(C\) is group-valued.
theorem openNormalSubgroupInClassProj_surjective
(U : OrderDual (OpenNormalSubgroupInClass C G)) :
Function.Surjective (openNormalSubgroupInClassProj (C := C) (G := G) U)Each projection from \(G\) to an open-normal-in-class quotient is surjective.
Show proof
QuotientGroup.mk'_surjective _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 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.
□theorem directed_openNormalSubgroupInClass
(hForm : FiniteGroupClass.Formation C) :
Directed (α := OrderDual (OpenNormalSubgroupInClass C G)) (· ≤ ·) fun U => UThe open-normal-in-class index family is directed under reverse inclusion.
Show proof
by
intro U V
let W : OpenNormalSubgroupInClass C G :=
⟨U.1 ⊓ V.1,
FiniteGroupClass.Formation.quotient_inf_mem
(C := C) (G := G) hForm U.1 V.1 U.2 V.2⟩
refine ⟨OrderDual.toDual W, ?_, ?_⟩
· change ((W.1 : Subgroup G) ≤ (U.1 : Subgroup G))
exact inf_le_left
· change ((W.1 : Subgroup G) ≤ (V.1 : Subgroup G))
exact inf_le_rightProof. 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.
□def HasAllOpenNormalQuotientsInClass (C : FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] : Prop :=
∀ U : OpenNormalSubgroup G, C (G ⧸ (U : Subgroup G))Every quotient by an open normal subgroup belongs to the class \(C\). This is stronger than the standard basis formulation unless \(C\) is quotient-closed.
structure IsProCGroup (C : FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] : Prop where
isProfinite : IsProfiniteGroup G
basis : HasOpenNormalBasisInClass C GA standard pro-\(C\) group is profinite and has a neighborhood basis of open normal subgroups whose quotients lie in \(C\).
structure IsStrictProCGroup (C : FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] : Prop where
isProfinite : IsProfiniteGroup G
all_open_normal_quotients : HasAllOpenNormalQuotientsInClass C GA strict pro-\(C\) group is a profinite group for which every open-normal quotient lies in \(C\).
theorem to_isProCGroup (hG : IsStrictProCGroup C G) : IsProCGroup C GA strict pro-\(C\) group is pro-\(C\) in the standard basis sense.
Show proof
by
refine ⟨hG.isProfinite, ?_⟩
intro W hW h1W
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG.isProfinite
letI : T2Space G := IsProfiniteGroup.t2Space hG.isProfinite
letI : TotallyDisconnectedSpace G :=
IsProfiniteGroup.totallyDisconnectedSpace hG.isProfinite
rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W with ⟨U, hUW⟩
exact ⟨U, hUW, hG.all_open_normal_quotients U⟩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 isProfiniteGroup (hG : IsProCGroup C G) : IsProfiniteGroup GThe underlying topological group of a pro-\(C\) group is profinite.
Show proof
hG.isProfiniteProof. 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.
□theorem isTopologicalGroup (hG : IsProCGroup C G) : IsTopologicalGroup GThe topological group component of a pro-\(C\) group.
Show proof
hG.isProfiniteGroup.isTopologicalGroupProof. 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 compactSpace (hG : IsProCGroup C G) : CompactSpace GThe compact-space instance on a profinite space.
Show proof
IsProfiniteGroup.compactSpace hG.isProfiniteProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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 t2Space (hG : IsProCGroup C G) : T2Space GA pro-\(C\) group is Hausdorff.
Show proof
IsProfiniteGroup.t2Space hG.isProfiniteProof. 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.
□theorem t1Space (hG : IsProCGroup C G) : T1Space GThe \(T_1\) property of a pro-\(C\) group.
Show proof
hG.isProfiniteGroup.t1SpaceProof. 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 totallyDisconnectedSpace (hG : IsProCGroup C G) : TotallyDisconnectedSpace GA pro-\(C\) group is totally disconnected.
Show proof
IsProfiniteGroup.totallyDisconnectedSpace hG.isProfiniteProof. 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.
□theorem mono {D : FiniteGroupClass.{u}}
(hG : IsProCGroup C G)
(hmono : ∀ {Q : Type u} [Group Q], C Q → D Q) :
IsProCGroup D GPro-\(C\) membership is monotone under enlarging the finite-group class.
Show proof
⟨hG.isProfiniteGroup, hG.basis.mono hmono⟩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 hasOpenNormalBasisInClass (hG : IsProCGroup C G) :
HasOpenNormalBasisInClass C GIn a pro-\(C\) group, every open neighborhood of \(1\) contains an open normal subgroup whose quotient still belongs to \(C\).
Show proof
hG.basisProof. 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 hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
(hIso : FiniteGroupClass.IsomClosed C)
(hQuot : FiniteGroupClass.QuotientClosed C)
(hG : IsProCGroup C G) :
HasAllOpenNormalQuotientsInClass C GWith isomorphism and quotient closure, the basis definition implies the older all-open normal quotient condition.
Show proof
by
intro U
rcases hG.basis (((U : Subgroup G) : Set G))
(openNormalSubgroup_isOpen (G := G) U) U.one_mem' with
⟨V, hVU, hCV⟩
let q : G ⧸ (V : Subgroup G) →ₜ* G ⧸ (U : Subgroup G) :=
OpenNormalSubgroup.transition (G := G) hVU
have hqsurj : Function.Surjective q := OpenNormalSubgroup.transition_surjective (G := G) hVU
have hQuot :
C ((G ⧸ (V : Subgroup G)) ⧸ q.toMonoidHom.ker) :=
hQuot (N := q.toMonoidHom.ker) hCV
exact hIso ⟨QuotientGroup.quotientKerEquivOfSurjective q.toMonoidHom hqsurj⟩ hQuotProof. 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 quotient_mem (hForm : FiniteGroupClass.Formation C)
(hG : IsProCGroup C G) (U : OpenNormalSubgroup G) :
C (G ⧸ (U : Subgroup G))The quotient attached to a normal subgroup in the finite-quotient index family lies in \(C\).
Show proof
hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
hForm.isomClosed hForm.quotientClosed hG UProof. 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 isStrictProCGroup_iff_isProCGroup_of_formation
(hForm : FiniteGroupClass.Formation C) :
IsStrictProCGroup C G ↔ IsProCGroup C GFor formations, the strict and basis definitions agree.
Show proof
by
constructor
· exact IsStrictProCGroup.to_isProCGroup
· intro hG
exact
{ isProfinite := hG.isProfinite
all_open_normal_quotients :=
hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
hForm.isomClosed hForm.quotientClosed hG }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 finite_quotient (hG : IsProCGroup C G) (U : OpenNormalSubgroup G) :
Finite (G ⧸ (U : Subgroup G))Any quotient by an open normal subgroup of a pro-\(C\) group is finite.
Show proof
by
letI : CompactSpace G := IsProCGroup.compactSpace hG
letI : T2Space G := IsProCGroup.t2Space hG
exact openNormalSubgroup_finiteQuotient (G := G) UProof. 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 exists_openNormalSubgroupInClass_sub_open_nhds_of_one (hG : IsProCGroup C G)
{W : Set G} (hW : IsOpen W) (h1W : (1 : G) ∈ W) :
∃ U : OpenNormalSubgroupInClass C G, (((U.1 : Subgroup G) : Set G)) ⊆ WIn a pro-\(C\) group, every open neighborhood of \(1\) contains an indexed open normal subgroup whose quotient lies in \(C\).
Show proof
by
rcases hG.hasOpenNormalBasisInClass W hW h1W with ⟨U, hUW, hCU⟩
exact ⟨⟨U, hCU⟩, hUW⟩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 exists_openNormalSubgroupInClass_eq_on_right_coset_of_continuous_discrete
(hG : IsProCGroup C G)
{A : Type v} [TopologicalSpace A] [DiscreteTopology A]
(f : G → A) (hf : Continuous f) (g₀ : G) :
∃ U : OpenNormalSubgroupInClass C G,
∀ g : G, g * g₀⁻¹ ∈ (U.1 : Subgroup G) → f g = f g₀A continuous map to a discrete target is locally fixed on a sufficiently small right coset, with the small subgroup chosen among the open normal pro-\(C\) quotients.
Show proof
by
letI : IsTopologicalGroup G := hG.isTopologicalGroup
let W : Set G := {x | f (x * g₀) = f g₀}
have hW : IsOpen W := by
change IsOpen ((fun x : G => f (x * g₀)) ⁻¹' ({f g₀} : Set A))
exact isOpen_discrete _ |>.preimage (hf.comp (continuous_id.mul continuous_const))
have h1W : (1 : G) ∈ W := by
simp only [Set.mem_setOf_eq, one_mul, W]
rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
refine ⟨U, ?_⟩
intro g hg
have hmem : g * g₀⁻¹ ∈ W := hUW hg
have hrewrite : (g * g₀⁻¹) * g₀ = g := by
simp only [mul_assoc, inv_mul_cancel, mul_one]
simpa [W, hrewrite] using hmemProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. 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. 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. 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 iInf_openNormalSubgroupInClass_eq_bot (hG : IsProCGroup C G) :
iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) = (⊥ : Subgroup G)In a pro-\(C\) group, the open normal subgroups whose quotients lie in \(C\) have trivial total intersection.
Show proof
by
letI : T2Space G := IsProCGroup.t2Space hG
apply le_antisymm
· intro x hx
change x = 1
by_contra hxne
let W : Set G := ({x} : Set G)ᶜ
have hW : IsOpen W := by
simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
have h1W : (1 : G) ∈ W := by
have hx1 : (1 : G) ≠ x := by
intro h1x
exact hxne h1x.symm
simpa [W] using hx1
rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
have hxall : ∀ U : OpenNormalSubgroupInClass C G, x ∈ (U.1 : Subgroup G) := by
simpa [Subgroup.mem_iInf] using hx
have hxU : x ∈ (U.1 : Subgroup G) := hxall U
have hxW : x ∈ W := hUW hxU
exact hxW (by simp only [Set.mem_singleton_iff])
· exact bot_leProof. 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 iInter_openNormalSubgroupInClass_eq_singleton (hG : IsProCGroup C G) :
(⋂ U : OpenNormalSubgroupInClass C G, (((U.1 : Subgroup G) : Set G))) = ({1} : Set G)The open-normal-in-class subgroups of a pro-\(C\) group intersect in the singleton \(\{1\}\).
Show proof
by
ext x
constructor
· intro hx
have hx' : x ∈ iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) := by
simpa [Subgroup.mem_iInf, Set.mem_iInter] using hx
have hxbot : x ∈ (⊥ : Subgroup G) := by
simpa [hG.iInf_openNormalSubgroupInClass_eq_bot] using hx'
simpa using hxbot
· rintro rfl
simp only [OpenSubgroup.coe_toSubgroup, Set.mem_iInter, SetLike.mem_coe, one_mem, implies_true]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\). 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 exists_openNormalBasisInClassFamily (hG : IsProCGroup C G) :
∃ ι : Type u, ∃ U : ι → OpenNormalSubgroup G,
(∀ i, C (G ⧸ (U i : Subgroup G))) ∧
(∀ W : Set G, IsOpen W → (1 : G) ∈ W →
∃ i, (((U i : Subgroup G) : Set G)) ⊆ W) ∧
iInf (fun i => (U i : Subgroup G)) = (⊥ : Subgroup G)Explicit family form of the open-normal basis and trivial-intersection package.
Show proof
by
refine ⟨OpenNormalSubgroupInClass C G, fun i => i.1, ?_, ?_, ?_⟩
· intro i
exact i.2
· intro W hW h1W
rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1W with ⟨U, hUW⟩
exact ⟨U, hUW⟩
· simpa using hG.iInf_openNormalSubgroupInClass_eq_botProof. 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. 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 eq_one_of_mem_all_openNormalSubgroupInClass (hG : IsProCGroup C G) {x : G}
(hx : ∀ U : OpenNormalSubgroupInClass C G, x ∈ (U.1 : Subgroup G)) :
x = 1Membership in every open-normal-in-class subgroup forces an element to be trivial.
Show proof
by
have hx' : x ∈ iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) := by
simpa [Subgroup.mem_iInf] using hx
have hxbot : x ∈ (⊥ : Subgroup G) := by
simpa [hG.iInf_openNormalSubgroupInClass_eq_bot] using hx'
simpa using hxbotProof. 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\). 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 exists_openNormalSubgroupInClass_not_mem (hG : IsProCGroup C G) {x : G} (hx : x ≠ 1) :
∃ U : OpenNormalSubgroupInClass C G, x ∉ (U.1 : Subgroup G)If x \(\neq\) 1, then some open normal subgroup in the class-family omits x.
Show proof
by
by_contra h
apply hx
apply hG.eq_one_of_mem_all_openNormalSubgroupInClass
intro U
by_contra hxU
exact h ⟨U, hxU⟩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\). 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 eq_of_forall_openNormalSubgroupInClass_quotient_eq (hG : IsProCGroup C G) {x y : G}
(hxy : ∀ U : OpenNormalSubgroupInClass C G,
QuotientGroup.mk' (U.1 : Subgroup G) x = QuotientGroup.mk' (U.1 : Subgroup G) y) :
x = yTwo elements of a pro-\(C\) group are equal once they agree in every quotient by an open normal subgroup whose quotient lies in \(C\).
Show proof
by
have hxy' : x⁻¹ * y = 1 := by
apply hG.eq_one_of_mem_all_openNormalSubgroupInClass
intro U
exact QuotientGroup.eq.1 (hxy U)
calc
x = x * 1 := by simp only [mul_one]
_ = x * (x⁻¹ * y) := by rw [hxy']
_ = y := by simp only [mul_inv_cancel_left]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 eq_of_forall_openNormalSubgroupInClassProj_eq (hG : IsProCGroup C G) {x y : G}
(hxy : ∀ U : OrderDual (OpenNormalSubgroupInClass C G),
openNormalSubgroupInClassProj (C := C) (G := G) U x =
openNormalSubgroupInClassProj (C := C) (G := G) U y) :
x = yCoordinatewise equality in the canonical inverse-system projections already forces equality in the ambient pro-\(C\) group.
Show proof
by
apply hG.eq_of_forall_openNormalSubgroupInClass_quotient_eq
intro U
simpa [openNormalSubgroupInClassProj] using hxy (OrderDual.toDual U)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\). 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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem of_allOpenNormalQuotients (hprof : IsProfiniteGroup G)
(hquot : HasAllOpenNormalQuotientsInClass C G) :
IsProCGroup C GA direct constructor for IsProCGroup from the stronger open-normal quotient criterion.
Show proof
(IsStrictProCGroup.mk hprof hquot).to_isProCGroupProof. 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 openNormalSubgroupInClass_nonempty (hG : IsProCGroup C G) :
Nonempty (OpenNormalSubgroupInClass C G)In a pro-\(C\) group there is at least one open normal subgroup with quotient in \(C\).
Show proof
by
rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one
(W := Set.univ) isOpen_univ (by simp only [Set.mem_univ]) with ⟨U, _⟩
exact ⟨U⟩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 isProCGroup_iff {C : FiniteGroupClass.{u}}
{G : Type u} [Group G] [TopologicalSpace G] :
IsProCGroup C G ↔
IsProfiniteGroup G ∧ HasOpenNormalBasisInClass C GThe chosen Lean definition of a pro-\(C\) group matches the open-normal basis condition.
Show proof
by
constructor
· intro hG
exact ⟨hG.isProfinite, hG.basis⟩
· rintro ⟨hprof, hbasis⟩
exact ⟨hprof, hbasis⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. 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 isStrictProCGroup_iff {C : FiniteGroupClass.{u}}
{G : Type u} [Group G] [TopologicalSpace G] :
IsStrictProCGroup C G ↔
IsProfiniteGroup G ∧ HasAllOpenNormalQuotientsInClass C GThe strict pro-\(C\) definition matches the all-open-normal-quotient condition.
Show proof
by
constructor
· intro hG
exact ⟨hG.isProfinite, hG.all_open_normal_quotients⟩
· rintro ⟨hprof, hall⟩
exact ⟨hprof, hall⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. 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.
□