ProCGroups.FreeProC.Characterization.InverseLimitTowers
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
structure CountableSurjectiveFreeProCSystem
(ProC : ProCGroups.ProC.ProCGroupPredicate) where
stage : ℕ → FreeProCGroupOnConvergingSetData (ProC := ProC)
transition :
∀ {m n : ℕ}, m ≤ n → (stage n).carrier →* (stage m).carrier
continuous_transition :
∀ {m n : ℕ} (hmn : m ≤ n), Continuous (transition hmn)
transition_id :
∀ n : ℕ, transition (le_rfl : n ≤ n) = MonoidHom.id (stage n).carrier
transition_comp :
∀ {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n),
(transition hlm).comp (transition hmn) = transition (hlm.trans hmn)
surjective_transition :
∀ {m n : ℕ} (hmn : m ≤ n), Function.Surjective (transition hmn)A countable surjective inverse system of free pro-\(C\) groups. This record stores the transition maps for all m \(\le\) n, together with the identity and composition laws. Its limit is the canonical subtype inverse limit supplied by InverseSystems.InverseSystem.
def bonding (T : CountableSurjectiveFreeProCSystem ProC) (n : ℕ) :
(T.stage (n + 1)).carrier →* (T.stage n).carrier :=
T.transition (Nat.le_succ n)The adjacent bonding map in the countable system.
theorem continuous_bonding (T : CountableSurjectiveFreeProCSystem ProC) (n : ℕ) :
Continuous (T.bonding n)The bonding map in the countable free pro-\(C\) system is continuous.
Show proof
T.continuous_transition (Nat.le_succ n)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 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 surjective_bonding (T : CountableSurjectiveFreeProCSystem ProC) (n : ℕ) :
Function.Surjective (T.bonding n)The bonding maps in the countable surjective free pro-\(C\) system are surjective.
Show proof
T.surjective_transition (Nat.le_succ n)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 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 inverseSystem (T : CountableSurjectiveFreeProCSystem ProC) :
InverseSystem (I := ℕ) where
X := fun n => (T.stage n).carrier
topologicalSpace := fun n => inferInstance
map := fun {_m _n} hmn => T.transition hmn
continuous_map := fun {_m _n} hmn => T.continuous_transition hmn
map_id := by
intro n
funext x
simpa using congrArg (fun f : (T.stage n).carrier →* (T.stage n).carrier => f x)
(T.transition_id n)
map_comp := by
intro l m n hlm hmn
funext x
simpa [Function.comp, MonoidHom.comp_apply] using
congrArg (fun f : (T.stage n).carrier →* (T.stage l).carrier => f x)
(T.transition_comp hlm hmn)The underlying inverse system associated to the countable tower data.
instance instGroupInverseSystemStage (T : CountableSurjectiveFreeProCSystem ProC)
(n : ℕ) : Group (T.inverseSystem.X n) := by
change Group (T.stage n).carrier
infer_instanceThe constructed carrier inherits its group structure from the coordinatewise group structure of the construction.
instance instIsTopologicalGroupInverseSystemStage (T : CountableSurjectiveFreeProCSystem ProC)
(n : ℕ) : IsTopologicalGroup (T.inverseSystem.X n) := by
change IsTopologicalGroup (T.stage n).carrier
infer_instanceThe object is a topological group with the induced group operations and topology.
def isGroupSystem (T : CountableSurjectiveFreeProCSystem ProC) :
IsGroupSystem T.inverseSystem where
map_one := by
intro m n hmn
exact (T.transition hmn).map_one
map_mul := by
intro m n hmn x y
exact (T.transition hmn).map_mul x y
map_inv := by
intro m n hmn x
exact (T.transition hmn).map_inv xThe free pro-\(C\) construction forms a group system satisfying the corresponding universal or quotient-level property.
abbrev limitCarrier (T : CountableSurjectiveFreeProCSystem ProC) : Type u :=
T.inverseSystem.inverseLimitThe canonical inverse-limit carrier of a countable surjective free pro-\(C\) system.
instance instGroupLimitCarrier (T : CountableSurjectiveFreeProCSystem ProC) :
Group T.limitCarrier := by
letI : IsGroupSystem T.inverseSystem := T.isGroupSystem
infer_instanceThe constructed carrier inherits its group structure from the coordinatewise group structure of the construction.
instance instTopologicalSpaceLimitCarrier (T : CountableSurjectiveFreeProCSystem ProC) :
TopologicalSpace T.limitCarrier := by
infer_instanceThe constructed object carries the topological space structure inherited from its construction.
instance instIsTopologicalGroupLimitCarrier (T : CountableSurjectiveFreeProCSystem ProC) :
IsTopologicalGroup T.limitCarrier := by
letI : IsGroupSystem T.inverseSystem := T.isGroupSystem
infer_instanceThe object is a topological group with the induced group operations and topology.
def projection (T : CountableSurjectiveFreeProCSystem ProC) (n : ℕ) :
T.limitCarrier →* (T.stage n).carrier := by
letI : IsGroupSystem T.inverseSystem := T.isGroupSystem
exact projectionHom (S := T.inverseSystem) nThe canonical projection homomorphism from the inverse limit to a stage.
theorem continuous_projection (T : CountableSurjectiveFreeProCSystem ProC) (n : ℕ) :
Continuous (T.projection n)Each canonical projection from an inverse limit is continuous.
Show proof
by
simpa [projection, projectionHom] using T.inverseSystem.continuous_projection nProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem compatible (T : CountableSurjectiveFreeProCSystem ProC) (n : ℕ)
(x : T.limitCarrier) :
T.bonding n (T.projection (n + 1) x) = T.projection n xShow proof
by
simpa [bonding, projection, inverseSystem] using
T.inverseSystem.projection_compatible x n (n + 1) (Nat.le_succ n)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 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.
□theorem isInverseLimit_projection (T : CountableSurjectiveFreeProCSystem ProC) :
T.inverseSystem.IsInverseLimit (fun n => T.projection n)The canonical projection family satisfies the inverse-limit universal property.
Show proof
by
letI : IsGroupSystem T.inverseSystem := T.isGroupSystem
simpa [projection] using T.inverseSystem.isInverseLimit_projectionProof. 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. 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 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. 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.
□structure CountableSurjectiveSystemFreenessCriterion
{ProC : ProCGroups.ProC.ProCGroupPredicate}
(T : CountableSurjectiveFreeProCSystem ProC) : Prop where
free_limit_of_countable_generating_family :
Nonempty (ConvergingGeneratingMap ℕ T.limitCarrier) →
∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
Nonempty (Fdata.carrier ≃ₜ* T.limitCarrier)External freeness input for countable surjective inverse systems. The inverse-system data now determines the limit object itself; this criterion only records the additional mathematical input needed to identify that canonical limit as a free pro-\(C\) group.
theorem apply
{ProC : ProCGroups.ProC.ProCGroupPredicate}
(T : CountableSurjectiveFreeProCSystem ProC)
(hcrit : CountableSurjectiveSystemFreenessCriterion T)
(hcount : Nonempty (ConvergingGeneratingMap ℕ T.limitCarrier)) :
∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
Nonempty (Fdata.carrier ≃ₜ* T.limitCarrier)Apply the freeness criterion to the canonical inverse limit of a countable system.
Show proof
hcrit.free_limit_of_countable_generating_family hcountProof. 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 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 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.
□