ProCGroups.ProC.Quotients.DescendingClosedSubgroupQuotients
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.
def closedSubgroup_sInf (L : I → ClosedSubgroup G) : ClosedSubgroup G where
toSubgroup := iInf fun i => (L i : Subgroup G)
isClosed' := by
convert isClosed_iInter fun i => (L i).isClosed' using 1
ext x
simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid,
Subgroup.mem_iInf, mem_iInter]The infimum of a family of closed subgroups, repackaged as a closed subgroup.
theorem closedSubgroup_sInf_le {I : Type v} {G : Type u} [Group G] [TopologicalSpace G]
(L : I → ClosedSubgroup G) (i : I) :
(closedSubgroup_sInf L : Subgroup G) ≤ (L i : Subgroup G)The infimum subgroup is contained in each term of the family.
Show proof
by
exact iInf_le _ iProof. 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. 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 descendingClosedSubgroupSystem (L : I → ClosedSubgroup G)
(hL : ∀ {i j}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G)) :
InverseSystems.InverseSystem (I := I) where
X i := G ⧸ (L i : Subgroup G)
topologicalSpace i := inferInstance
map := fun {i j} hij =>
leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij)
continuous_map := by
intro i j hij
exact continuous_leftQuotientProjection
(K := (L j : Subgroup G)) (H := (L i : Subgroup G)) (hL hij)
map_id := by
intro i
exact leftQuotientProjection_id (K := (L i : Subgroup G))
map_comp := by
intro i j k hij hjk
exact
leftQuotientProjection_comp
(K := (L k : Subgroup G)) (H := (L j : Subgroup G)) (L := (L i : Subgroup G))
(hL hjk) (hL hij)The inverse system of left quotient spaces attached to a decreasing family of closed subgroups.
theorem exists_continuous_leftQuotient_lift_of_directed
(hG : IsProfiniteGroup G) (L : I → ClosedSubgroup G)
(hL : ∀ {i j}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G))
(hdir : Directed (· ≤ ·) (id : I → I))
{Y : Type v} [TopologicalSpace Y]
(η : ∀ i, Y → G ⧸ (L i : Subgroup G))
(hηcont : ∀ i, Continuous (η i))
(hηcompat : ∀ {i j} (hij : i ≤ j),
leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j = η i)
(y0 : Y)
(hηone : ∀ i, η i y0 = QuotientGroup.mk (s := (L i : Subgroup G)) (1 : G)) :
∃ ηinf : Y → G ⧸ ((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G),
Continuous ηinf ∧
(∀ i,
leftQuotientProjection
(((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))
(L i : Subgroup G)
(closedSubgroup_sInf_le (L := L) i) ∘ ηinf = η i) ∧
ηinf y0 =
QuotientGroup.mk (s := (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)))
(1 : G)A compatible family of maps into a decreasing family of left quotient spaces lifts uniquely to the quotient by the infimum subgroup.
Show proof
by
classical
let Linf : ClosedSubgroup G := closedSubgroup_sInf L
let S : InverseSystems.InverseSystem (I := I) := descendingClosedSubgroupSystem L hL
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : IsClosed (((Linf : ClosedSubgroup G) : Subgroup G) : Set G) := Linf.isClosed'
letI : ∀ i, IsClosed (((L i : ClosedSubgroup G) : Subgroup G) : Set G) := fun i => (L i).isClosed'
letI : ∀ i, T2Space (S.X i) := fun i => by
change T2Space (G ⧸ (L i : Subgroup G))
infer_instance
let ψ : ∀ i, G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) → S.X i := fun i =>
leftQuotientProjection
(((Linf : ClosedSubgroup G) : Subgroup G))
(L i : Subgroup G)
(closedSubgroup_sInf_le (L := L) i)
have hψcont : ∀ i, Continuous (ψ i) := by
intro i
exact continuous_leftQuotientProjection
(K := (((Linf : ClosedSubgroup G) : Subgroup G)))
(H := (L i : Subgroup G))
(closedSubgroup_sInf_le (L := L) i)
have hψcompat : S.CompatibleMaps ψ := by
intro i j hij
convert
(leftQuotientProjection_comp
(K := (((Linf : ClosedSubgroup G) : Subgroup G)))
(H := (L j : Subgroup G))
(L := (L i : Subgroup G))
(closedSubgroup_sInf_le (L := L) j) (hL hij)) using 1
let φ : G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) → S.inverseLimit :=
S.inverseLimitLift ψ hψcompat
have hφcont : Continuous φ := S.continuous_inverseLimitLift ψ hψcont hψcompat
have hψsurj : ∀ i, Function.Surjective (ψ i) := by
intro i
exact surjective_leftQuotientProjection
(K := (((Linf : ClosedSubgroup G) : Subgroup G)))
(H := (L i : Subgroup G))
(closedSubgroup_sInf_le (L := L) i)
have hφsurj : Function.Surjective φ :=
S.surjective_inverseLimitLift ψ hψcont hψcompat hψsurj hdir
have hφinj : Function.Injective φ := by
intro x y hxy
rcases Quotient.exists_rep x with ⟨gx, rfl⟩
rcases Quotient.exists_rep y with ⟨gy, rfl⟩
apply QuotientGroup.eq.2
have hcoord :
∀ i, gx⁻¹ * gy ∈ (L i : Subgroup G) := by
intro i
have hi : ψ i (QuotientGroup.mk (s := (((Linf : ClosedSubgroup G) : Subgroup G))) gx) =
ψ i (QuotientGroup.mk (s := (((Linf : ClosedSubgroup G) : Subgroup G))) gy) := by
exact congrArg (fun z : S.inverseLimit => S.projection i z) hxy
exact QuotientGroup.eq.1 hi
change gx⁻¹ * gy ∈ iInf fun i => (L i : Subgroup G)
rw [Subgroup.mem_iInf]
exact hcoord
let eTop : G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) ≃ₜ S.inverseLimit :=
hφcont.homeoOfBijectiveCompactToT2 ⟨hφinj, hφsurj⟩
let ηinf : Y → G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) :=
eTop.symm ∘ S.inverseLimitLift η (by
intro i j hij
simpa only [S, descendingClosedSubgroupSystem, Function.comp] using hηcompat hij)
have hηinf_continuous : Continuous ηinf := by
exact eTop.continuous_invFun.comp <| S.continuous_inverseLimitLift η hηcont <| by
intro i j hij
simpa only [S, descendingClosedSubgroupSystem, Function.comp] using hηcompat hij
have hηinf_fac :
∀ i,
leftQuotientProjection
(((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))
(L i : Subgroup G)
(closedSubgroup_sInf_le (L := L) i) ∘ ηinf = η i := by
intro i
funext y
have hfac :=
congrFun (S.projection_comp_inverseLimitLift η
(by
intro i j hij
simpa only [S, descendingClosedSubgroupSystem, Function.comp] using hηcompat hij) i) y
have hcoord :
S.projection i (eTop (ηinf y)) = η i y := by
simpa [ηinf, Function.comp] using hfac
exact hcoord
have hηinf_one :
ηinf y0 =
QuotientGroup.mk (s := (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)))
(1 : G) := by
apply eTop.injective
apply S.ext
intro i
have hy0 := congrFun (hηinf_fac i) y0
change leftQuotientProjection
(((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))
(L i : Subgroup G)
(closedSubgroup_sInf_le (L := L) i) (ηinf y0) =
leftQuotientProjection
(((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))
(L i : Subgroup G)
(closedSubgroup_sInf_le (L := L) i)
(QuotientGroup.mk
(s := (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))) (1 : G))
simpa [hηone i]
using hy0
exact ⟨ηinf, hηinf_continuous, hηinf_fac, hηinf_one⟩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. 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.
□