ProCGroups.ProC.InverseLimits.Limits
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
instance instTopologicalSpaceX (i : I) : TopologicalSpace (S.X i) := S.topologicalSpace iThe constructed object carries the topological space structure inherited from its construction.
theorem inverseLimit
(hIso : FiniteGroupClass.IsomClosed C)
(hQuot : FiniteGroupClass.QuotientClosed C)
(hdir : Directed (· ≤ ·) (id : I → I))
(hX : ∀ i, IsProCGroup C (S.X i)) :
IsProCGroup C S.inverseLimitA directed inverse limit of pro-\(C\) groups is pro-\(C\).
Show proof
by
letI : ∀ i, CompactSpace (S.X i) := fun i => IsProCGroup.compactSpace (hX i)
letI : ∀ i, T2Space (S.X i) := fun i => IsProCGroup.t2Space (hX i)
letI : ∀ i, TotallyDisconnectedSpace (S.X i) := fun i =>
IsProCGroup.totallyDisconnectedSpace (hX i)
refine IsProCGroup.of_allOpenNormalQuotients (C := C)
⟨inferInstance,
inferInstance,
InverseSystems.InverseSystem.t2Space_inverseLimit (S := S),
InverseSystems.InverseSystem.totallyDisconnectedSpace_inverseLimit (S := S)⟩ ?_
intro U
letI : CompactSpace S.inverseLimit := inferInstance
letI : T2Space S.inverseLimit := InverseSystems.InverseSystem.t2Space_inverseLimit (S := S)
letI : Finite (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
openNormalSubgroup_finiteQuotient (G := S.inverseLimit) U
letI : DiscreteTopology (S.inverseLimit ⧸ (U : Subgroup S.inverseLimit)) :=
QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := S.inverseLimit) U)
let β : S.inverseLimit →* S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) :=
QuotientGroup.mk' (U : Subgroup S.inverseLimit)
rcases InverseSystems.InverseSystem.factors_through_projection_finite_group_hom
(S := S) hdir β continuous_quotient_mk' with ⟨k, βk, hβk_continuous, hβfac⟩
have hβk_surj : Function.Surjective βk := by
intro q
rcases QuotientGroup.mk'_surjective (U : Subgroup S.inverseLimit) q with ⟨x, rfl⟩
exact ⟨S.projection k x, by
simpa [Function.comp] using
(congrArg (fun f : S.inverseLimit → S.inverseLimit ⧸ (U : Subgroup S.inverseLimit) =>
f x) hβfac).symm⟩
have hker_closed : IsClosed ((βk.ker : Subgroup (S.X k)) : Set (S.X k)) := by
simpa [MonoidHom.mem_ker] using
isClosed_eq hβk_continuous continuous_const
have hker_finite : Finite (S.X k ⧸ βk.ker) := by
exact Finite.of_injective (QuotientGroup.quotientKerEquivOfSurjective βk hβk_surj)
(QuotientGroup.quotientKerEquivOfSurjective βk hβk_surj).injective
have hker_open : IsOpen ((βk.ker : Subgroup (S.X k)) : Set (S.X k)) :=
(subgroup_isOpen_iff_isClosed_finite_quotient (G := S.X k) (U := βk.ker)).2
⟨hker_closed, hker_finite⟩
let V : OpenNormalSubgroup (S.X k) :=
{ toOpenSubgroup := ⟨βk.ker, hker_open⟩
isNormal' := inferInstance }
have hQV : C (S.X k ⧸ (V : Subgroup (S.X k))) :=
IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
hIso hQuot (hX k) V
exact hIso ⟨QuotientGroup.quotientKerEquivOfSurjective βk hβk_surj⟩ hQVProof. 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 equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously. 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 quotient_closedNormalSubgroup
(hIso : FiniteGroupClass.IsomClosed C)
(hQuot : FiniteGroupClass.QuotientClosed C)
(hG : IsProCGroup C G)
(K : Subgroup G) [K.Normal] (hK : IsClosed (K : Set G)) :
IsProCGroup C (G ⧸ K)If \(G\) is pro-\(C\) and \(C\) is closed under quotients, then every quotient of \(G\) by a closed normal subgroup is again pro-\(C\). The proof reconstructs \(G/K\) as the inverse limit of the finite quotients \(G/U\) over the open normal subgroups \(U\) containing \(K\), and then applies the inverse-limit permanence theorem.
Show proof
by
classical
let topU : OpenNormalSubgroup G :=
{ toOpenSubgroup := ⟨⊤, isOpen_univ⟩
isNormal' := inferInstance }
letI : Nonempty (OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}) :=
⟨OrderDual.toDual ⟨topU, le_top⟩⟩
let S : InverseSystems.InverseSystem
(I := OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}) := {
X := fun U => G ⧸ (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
topologicalSpace := fun _ => inferInstance
map := fun {U V} hUV =>
QuotientGroup.map
(((OrderDual.ofDual V).1 : OpenNormalSubgroup G) : Subgroup G)
(((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G)
(MonoidHom.id G)
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
simp only [QuotientGroup.map_id, MonoidHom.coe_id]
map_comp := by
intro U V W hUV hVW
funext x
simpa [Function.comp] using congrArg (fun f => f x)
(QuotientGroup.map_comp_map
(N := (((OrderDual.ofDual W).1 : OpenNormalSubgroup G) : Subgroup G))
(M := (((OrderDual.ofDual V).1 : OpenNormalSubgroup G) : Subgroup G))
(O := (((OrderDual.ofDual U).1 : OpenNormalSubgroup G) : Subgroup G))
(f := MonoidHom.id G) (g := MonoidHom.id G) hVW hUV) }
letI : InverseSystems.IsGroupSystem S := {
map_one := by
intro i j hij
rfl
map_mul := by
intro i j hij x y
change
QuotientGroup.map
((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
(MonoidHom.id G) hij (x * y) =
QuotientGroup.map
((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
(MonoidHom.id G) hij x *
QuotientGroup.map
((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
(MonoidHom.id G) hij y
exact
(QuotientGroup.map
((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
(MonoidHom.id G) hij).map_mul x y
map_inv := by
intro i j hij x
change
QuotientGroup.map
((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
(MonoidHom.id G) hij x⁻¹ =
(QuotientGroup.map
((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
(MonoidHom.id G) hij x)⁻¹
exact
(QuotientGroup.map
((((OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G))
((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G))
(MonoidHom.id G) hij).map_inv x }
have hdir :
Directed (· ≤ ·) (id : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)} →
OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}) := by
intro i j
refine ⟨OrderDual.toDual ⟨(OrderDual.ofDual i).1 ⊓ (OrderDual.ofDual j).1, ?_⟩, ?_, ?_⟩
· intro x hx
exact ⟨(OrderDual.ofDual i).2 hx, (OrderDual.ofDual j).2 hx⟩
· exact show
(((OrderDual.ofDual i).1 ⊓ (OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G) ≤
((OrderDual.ofDual i).1 : Subgroup G) from inf_le_left
· exact show
(((OrderDual.ofDual i).1 ⊓ (OrderDual.ofDual j).1 : OpenNormalSubgroup G) : Subgroup G) ≤
((OrderDual.ofDual j).1 : Subgroup G) from inf_le_right
have hX :
∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}, IsProCGroup C (S.X i) :=
by
intro i
let U : OpenNormalSubgroup G := (OrderDual.ofDual i).1
letI : Finite (G ⧸ (U : Subgroup G)) := hG.finite_quotient U
letI : DiscreteTopology (G ⧸ (U : Subgroup G)) :=
QuotientGroup.discreteTopology (openNormalSubgroup_isOpen (G := G) U)
exact IsProCGroup.of_finite_discrete (C := C) (G := G ⧸ (U : Subgroup G))
hQuot
(IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
hIso hQuot hG U)
letI : ∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}, T2Space (S.X i) :=
fun i => IsProCGroup.t2Space (hX i)
have hSinv : IsProCGroup C S.inverseLimit :=
inverseLimit (C := C) (S := S) hIso hQuot hdir hX
let ψ :
∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)},
G ⧸ K → S.X i := fun i =>
QuotientGroup.map
K
(((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G)
(MonoidHom.id G)
(OrderDual.ofDual i).2
have hψcont :
∀ i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)}, Continuous (ψ i) := by
intro i
let U : Subgroup G := (((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G)
have hmk : Continuous (QuotientGroup.mk' U : G → G ⧸ U) := continuous_quotient_mk'
have hconst :
∀ a b : G, QuotientGroup.leftRel K a b →
(QuotientGroup.mk' U) a = (QuotientGroup.mk' U) b := by
intro a b hab
apply QuotientGroup.eq.2
exact (OrderDual.ofDual i).2 (by simpa using (QuotientGroup.leftRel_apply.mp hab))
simpa [ψ, U, QuotientGroup.map, MonoidHom.comp_apply] using hmk.quotient_lift hconst
have hψcompat : S.CompatibleMaps ψ := by
intro i j hij
funext x
rcases QuotientGroup.mk'_surjective K x with ⟨g, rfl⟩
rfl
let φ : G ⧸ K →* S.inverseLimit := {
toFun := S.inverseLimitLift ψ hψcompat
map_one' := by
apply S.ext
intro i
rfl
map_mul' := by
intro x y
apply S.ext
intro i
rcases QuotientGroup.mk'_surjective K x with ⟨gx, rfl⟩
rcases QuotientGroup.mk'_surjective K y with ⟨gy, rfl⟩
rfl }
have hφcont : Continuous φ := S.continuous_inverseLimitLift ψ hψcont hψcompat
have hφsurj : Function.Surjective φ := by
letI : CompactSpace (G ⧸ K) := by
letI : CompactSpace G := IsProCGroup.compactSpace hG
infer_instance
letI : T2Space (G ⧸ K) := by
letI : T2Space G := IsProCGroup.t2Space hG
letI : IsClosed (K : Set G) := hK
infer_instance
exact InverseSystems.InverseSystem.surjective_inverseLimitLift
(S := S) ψ hψcont hψcompat
(fun i => by
intro x
rcases QuotientGroup.mk'_surjective
((((OrderDual.ofDual i).1 : OpenNormalSubgroup G) : Subgroup G)) x with ⟨g, rfl⟩
exact ⟨QuotientGroup.mk' K g, rfl⟩)
hdir
have hφinj : Function.Injective φ := by
intro x y hxy
rcases QuotientGroup.mk'_surjective K x with ⟨gx, rfl⟩
rcases QuotientGroup.mk'_surjective K y with ⟨gy, rfl⟩
apply QuotientGroup.eq.2
have hmem :
∀ U : OpenNormalSubgroup G, K ≤ (U : Subgroup G) → gx⁻¹ * gy ∈ (U : Subgroup G) := by
intro U hKU
let i : OrderDual {U : OpenNormalSubgroup G // K ≤ (U : Subgroup G)} :=
OrderDual.toDual ⟨U, hKU⟩
have hi : ψ i (QuotientGroup.mk' K gx) = ψ i (QuotientGroup.mk' K gy) := by
simpa [φ] using congrArg (fun z : S.inverseLimit => S.projection i z) hxy
exact QuotientGroup.eq.mp hi
let HC : ClosedSubgroup G := { toSubgroup := K, isClosed' := hK }
letI : CompactSpace G := IsProCGroup.compactSpace hG
letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
have hx :
gx⁻¹ * gy ∈
sInf {N : Subgroup G | IsOpen (N : Set G) ∧ K ≤ N ∧ N.Normal} := by
simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
intro N hN
let U : OpenNormalSubgroup G :=
{ toOpenSubgroup := ⟨N, hN.1⟩
isNormal' := hN.2.2 }
exact hmem U hN.2.1
have hxK : gx⁻¹ * gy ∈ K := by
have hEq :
(K : Subgroup G) =
sInf {N : Subgroup G | IsOpen (N : Set G) ∧ K ≤ N ∧ N.Normal} :=
closedSubgroup_eq_sInf_openNormal (G := G) HC
exact hEq.symm ▸ hx
exact hxK
letI : CompactSpace (G ⧸ K) := by
letI : CompactSpace G := IsProCGroup.compactSpace hG
infer_instance
letI : T2Space S.inverseLimit := IsProCGroup.t2Space hSinv
let e : G ⧸ K ≃ₜ* S.inverseLimit :=
ContinuousMulEquiv.ofBijectiveCompactToT2 φ hφcont ⟨hφinj, hφsurj⟩
simpa using IsProCGroup.ofContinuousMulEquiv (C := C) hIso hQuot hSinv e.symmProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□