ProCGroups.ProC.OpenNormalSubgroups.LimitPresentation
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
import
noncomputable def openNormalSubgroupInClassMulEquivInverseLimit
(hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
G ≃ₜ* (openNormalSubgroupInClassSystem C G).inverseLimit := by
let S := openNormalSubgroupInClassSystem C G
letI : Nonempty (OpenNormalSubgroupInClass C G) := openNormalSubgroupInClass_nonempty hG
letI : Nonempty (OrderDual (OpenNormalSubgroupInClass C G)) := inferInstance
letI : CompactSpace G := IsProCGroup.compactSpace hG
letI : T2Space G := IsProCGroup.t2Space hG
letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), Group (S.X U) := fun U => by
dsimp [S, openNormalSubgroupInClassSystem]
infer_instance
letI : InverseSystems.IsGroupSystem S := by
dsimp [S]
infer_instance
letI : ∀ U : OrderDual (OpenNormalSubgroupInClass C G), T2Space (S.X U) := fun U => by
letI : DiscreteTopology (S.X U) := by
dsimp [S, openNormalSubgroupInClassSystem]
exact QuotientGroup.discreteTopology
(openNormalSubgroup_isOpen (G := G) ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))
infer_instance
letI : Group S.inverseLimit := by infer_instance
letI : T2Space S.inverseLimit := S.t2Space_inverseLimit
let φ : G →* S.inverseLimit :=
{ toFun := S.inverseLimitLift
(fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
openNormalSubgroupInClassProj (C := C) (G := G) U)
(openNormalSubgroupInClassProj_compatible (C := C) (G := G))
map_one' := by
apply S.ext
intro i
rfl
map_mul' := by
intro x y
apply S.ext
intro i
rfl }
have hφcont : Continuous φ :=
S.continuous_inverseLimitLift
(fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
openNormalSubgroupInClassProj (C := C) (G := G) U)
(fun _ => continuous_quotient_mk')
(openNormalSubgroupInClassProj_compatible (C := C) (G := G))
have hφinj : Function.Injective φ := by
intro x y hxy
have hmem :
x⁻¹ * y ∈ iInf (fun U : OpenNormalSubgroupInClass C G => (U.1 : Subgroup G)) := by
rw [Subgroup.mem_iInf]
intro U
let i : OrderDual (OpenNormalSubgroupInClass C G) := OrderDual.toDual U
have hi :
openNormalSubgroupInClassProj (C := C) (G := G) i x =
openNormalSubgroupInClassProj (C := C) (G := G) i y := by
simpa [φ] using congrArg (fun z : S.inverseLimit => S.projection i z) hxy
exact QuotientGroup.eq.1 (by
simpa [openNormalSubgroupInClassProj] using hi)
have hone : x⁻¹ * y = 1 := by
have : x⁻¹ * y ∈ (⊥ : Subgroup G) := by
simpa [hG.iInf_openNormalSubgroupInClass_eq_bot] using hmem
simpa using this
calc
x = x * 1 := by simp only [mul_one]
_ = x * (x⁻¹ * y) := by rw [hone]
_ = y := by simp only [mul_inv_cancel_left]
have hφsurj : Function.Surjective φ :=
InverseSystems.InverseSystem.surjective_inverseLimitLift (S := S)
(fun U : OrderDual (OpenNormalSubgroupInClass C G) =>
openNormalSubgroupInClassProj (C := C) (G := G) U)
(fun _ => continuous_quotient_mk')
(openNormalSubgroupInClassProj_compatible (C := C) (G := G))
(fun U => openNormalSubgroupInClassProj_surjective (C := C) (G := G) U)
(directed_openNormalSubgroupInClass (C := C) (G := G) hForm)
exact ContinuousMulEquiv.ofBijectiveCompactToT2 φ hφcont ⟨hφinj, hφsurj⟩A pro-\(C\) group is canonically the inverse limit of its quotients by open normal subgroups whose quotients lie in \(C\).
@[simp] theorem openNormalSubgroupInClassMulEquivInverseLimit_projection
(hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G)
(U : OrderDual (OpenNormalSubgroupInClass C G)) (g : G) :
(openNormalSubgroupInClassSystem C G).projection U
(openNormalSubgroupInClassMulEquivInverseLimit
(C := C) (G := G) hForm hG g) =
openNormalSubgroupInClassProj (C := C) (G := G) U gUnder the canonical equivalence from a pro-\(C\) group to the inverse limit of its open-normal \(C\)-quotients, the \(U\)-coordinate of an element is its quotient class modulo \(U\).
Show proof
by
simp only [openNormalSubgroupInClassMulEquivInverseLimit, ContinuousMulEquiv.ofBijectiveCompactToT2, id_eq,
MonoidHom.coe_mk, OneHom.coe_mk, ContinuousMulEquiv.coe_mk', Equiv.toHomeomorphOfContinuousClosed_apply,
Equiv.ofBijective_apply, InverseSystems.InverseSystem.inverseLimitLift,
InverseSystems.InverseSystem.projection_apply]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 isomorphic_to_inverseLimit_finiteGroupsInClass
(hForm : FiniteGroupClass.Formation C) (hG : IsProCGroup C G) :
let SA pro-\(C\) group is topologically isomorphic to an inverse limit of finite groups in \(C\), realized using the quotient system indexed by the open normal subgroups whose quotients lie in \(C\).
Show proof
openNormalSubgroupInClassSystem C G
(∀ U : OrderDual (OpenNormalSubgroupInClass C G), C (S.X U) ∧ Finite (S.X U)) ∧
Nonempty (G ≃ₜ* S.inverseLimit) := by
let S := openNormalSubgroupInClassSystem C G
refine ⟨?_, ⟨openNormalSubgroupInClassMulEquivInverseLimit (C := C) (G := G) hForm hG⟩⟩
intro U
dsimp [S, openNormalSubgroupInClassSystem]
refine ⟨(OrderDual.ofDual U).2, ?_⟩
exact hForm.finiteOnly (OrderDual.ofDual 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. 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.
□def HasExactOpenNormalQuotientBasisInClass (C : FiniteGroupClass.{u})
(G : Type u) [Group G] [TopologicalSpace G] : Prop :=
CompactSpace 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)Existence of an open-normal subgroup basis whose quotients lie in \(C\) and whose quotient presentations are exact.
theorem t2Space_of_exactOpenNormalQuotientBasisInClass
(hC : HasExactOpenNormalQuotientBasisInClass C G) : T2Space GAn open-normal family with trivial intersection makes the group Hausdorff.
Show proof
by
rcases hC with ⟨_, ι, U, _, _, hInf⟩
refine ⟨?_⟩
intro x y hxy
have hxy' : x⁻¹ * y ≠ 1 := by
intro h1
apply hxy
simpa using inv_mul_eq_one.mp h1
have hsep : ∃ i : ι, x⁻¹ * y ∉ (U i : Subgroup G) := by
by_contra hsep
have hxall : ∀ i : ι, x⁻¹ * y ∈ (U i : Subgroup G) := by
intro i
by_contra hxyi
exact hsep ⟨i, hxyi⟩
have hxinf : x⁻¹ * y ∈ iInf (fun i => (U i : Subgroup G)) := by
simpa [Subgroup.mem_iInf] using hxall
have hxbot : x⁻¹ * y ∈ (⊥ : Subgroup G) := by
simpa [hInf] using hxinf
exact hxy' (by simpa using hxbot)
rcases hsep with ⟨i, hxyi⟩
have hclopenCoset :
∀ z : G, IsClopen {g : G | z⁻¹ * g ∈ (U i : Subgroup G)} := by
intro z
let f : G → G := fun g => z⁻¹ * g
have hf : Continuous f := continuous_const.mul continuous_id
refine ⟨?_, ?_⟩
· simpa [f] using (openSubgroup_isClosed (G := G) (U i).toOpenSubgroup).preimage hf
· simpa [f] using (openSubgroup_isOpen (G := G) (U i).toOpenSubgroup).preimage hf
refine ⟨{g : G | x⁻¹ * g ∈ (U i : Subgroup G)},
{g : G | y⁻¹ * g ∈ (U i : Subgroup G)}, ?_, ?_, ?_, ?_, ?_⟩
· exact (hclopenCoset x).2
· exact (hclopenCoset y).2
· simp only [OpenSubgroup.mem_toSubgroup, Set.mem_setOf_eq, inv_mul_cancel, one_mem]
· simp only [OpenSubgroup.mem_toSubgroup, Set.mem_setOf_eq, inv_mul_cancel, one_mem]
· refine Set.disjoint_left.2 ?_
intro g hx hg
apply hxyi
have hmul :
(x⁻¹ * g) * (y⁻¹ * g)⁻¹ ∈ (U i : Subgroup G) :=
(U i).mul_mem hx ((U i).inv_mem hg)
simpa [mul_assoc] using hmulProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem totallyDisconnectedSpace_of_exactOpenNormalQuotientBasisInClass
(hC : HasExactOpenNormalQuotientBasisInClass C G) : TotallyDisconnectedSpace GAn open-normal family yields a clopen basis and hence total disconnectedness.
Show proof
by
have hC' := hC
rcases hC' with ⟨_, ι, U, _, hbasis, _⟩
letI : T2Space G := t2Space_of_exactOpenNormalQuotientBasisInClass (C := C) hC
have hclopenBasis : TopologicalSpace.IsTopologicalBasis {s : Set G | IsClopen s} := by
refine TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
· intro s hs
exact hs.2
· intro x W hxW hW
let W₁ : Set G := (fun g : G => x * g) ⁻¹' W
have hW₁ : IsOpen W₁ := hW.preimage (continuous_const.mul continuous_id)
have h1W₁ : (1 : G) ∈ W₁ := by
simpa [W₁] using hxW
rcases hbasis W₁ hW₁ h1W₁ with ⟨i, hi⟩
have hclopenCoset : IsClopen {g : G | x⁻¹ * g ∈ (U i : Subgroup G)} := by
let f : G → G := fun g => x⁻¹ * g
have hf : Continuous f := continuous_const.mul continuous_id
refine ⟨?_, ?_⟩
· simpa [f] using (openSubgroup_isClosed (G := G) (U i).toOpenSubgroup).preimage hf
· simpa [f] using (openSubgroup_isOpen (G := G) (U i).toOpenSubgroup).preimage hf
refine ⟨{g : G | x⁻¹ * g ∈ (U i : Subgroup G)}, ?_, by simp only [OpenSubgroup.mem_toSubgroup, Set.mem_setOf_eq, inv_mul_cancel, one_mem], ?_⟩
· exact hclopenCoset
· intro g hg
have hxgW₁ : x⁻¹ * g ∈ W₁ := hi hg
simpa [W₁, mul_assoc] using hxgW₁
exact InverseSystems.totallyDisconnectedSpace_of_t2_basis_clopen G hclopenBasisProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem isProCGroup_of_hasExactOpenNormalQuotientBasisInClass
(hC : HasExactOpenNormalQuotientBasisInClass C G) : IsProCGroup C GAn open-normal family with quotients in \(C\) implies the working notion of a pro-\(C\) group. This direction needs no formation closure because the chosen basis already supplies the required open-normal quotients in \(C\).
Show proof
by
have hC' := hC
rcases hC' with ⟨hcompact, ι, U, hCU, hbasis, hInf⟩
letI : CompactSpace G := hcompact
letI : T2Space G := t2Space_of_exactOpenNormalQuotientBasisInClass (C := C) hC
letI : TotallyDisconnectedSpace G :=
totallyDisconnectedSpace_of_exactOpenNormalQuotientBasisInClass (C := C) hC
refine ⟨⟨inferInstance, hcompact, inferInstance, inferInstance⟩, ?_⟩
intro W hW h1W
rcases hbasis W hW h1W with ⟨i, hiW⟩
exact ⟨U i, hiW, hCU i⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□