ProCGroups.FreeProC.CanonicalData
This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.
import
- Mathlib.FieldTheory.IsAlgClosed.Basic
- ProCGroups.Completion.ProCIntegerPrimePower
- ProCGroups.FreeProC.Basic
- ProCGroups.ProC.GroupPredicates.Standard
Imported by
noncomputable def deltaBasisMap
{X : Type u} {A : Type v} [One A] (a : A) : X → (X → A) := by
classical
exact fun x y => if y = x then a else 1
@[simp]The usual \(\delta\)-basis map into a direct product.
theorem deltaBasisMap_apply_self
{X : Type u} {A : Type v} [One A] (a : A) (x : X) :
deltaBasisMap (X := X) (A := A) a x x = aThe \(\delta\)-basis map is one on the coordinate of the chosen generator.
Show proof
by
classical
simp only [deltaBasisMap, ↓reduceIte]
@[simp]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. 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps. 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 deltaBasisMap_apply_ne
{X : Type u} {A : Type v} [One A] (a : A) {x y : X} (h : y ≠ x) :
deltaBasisMap (X := X) (A := A) a x y = 1The \(\delta\)-basis map is zero on a basis coordinate different from the chosen generator.
Show proof
by
classical
simp only [deltaBasisMap, h, ↓reduceIte]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. 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps. 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 familyConvergesToOne_rankOneBasisMap
{G : Type u} [Group G] [TopologicalSpace G] (g : G) :
FamilyConvergesToOne (G := G) (Function.const PUnit g)Show proof
by
exact FamilyConvergesToOne.of_finite_domain (G := G) (Function.const PUnit 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. 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 topologicallyGenerates_rankOneBasisMap
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {g : G}
(hg : Generation.TopologicallyGenerates (G := G) ({g} : Set G)) :
Generation.TopologicallyGenerates (G := G) (Set.range (Function.const PUnit g))Show proof
by
have hrange : Set.range (Function.const PUnit g) = ({g} : Set G) := by
ext y
simp only [mem_range, Function.const, exists_const, mem_singleton_iff, eq_comm]
rw [hrange]
exact hgProof. 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 profiniteInteger_rankOneGeneratingData :
∃ ι : PUnit →
Multiplicative
(Completion.ProCIntegerLimitCarrier
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0})),
ProCGroups.ProC.allFiniteProC (G :=
Multiplicative
(Completion.ProCIntegerLimitCarrier
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))) ∧
FamilyConvergesToOne (G :=
Multiplicative
(Completion.ProCIntegerLimitCarrier
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))) ι ∧
Generation.TopologicallyGenerates (G :=
Multiplicative
(Completion.ProCIntegerLimitCarrier
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0})))
(Set.range ι)Show proof
by
let G : Type := Multiplicative
(Completion.ProCIntegerLimitCarrier
(ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))
let g : G := Completion.proCIntegerOne
(C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))
refine ⟨Function.const PUnit g, ?_, ?_, ?_⟩
· exact Completion.isProCGroup_multiplicative_proCInteger_allFinite.1
· exact familyConvergesToOne_rankOneBasisMap (G := G) g
· exact topologicallyGenerates_rankOneBasisMap
(G := G) (g := g)
Completion.topologicallyGenerates_singleton_proCIntegerOne_allFiniteProof. 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 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 proPInteger_rankOneGeneratingData (p : ℕ) [Fact (Nat.Prime p)] :
∃ ι : PUnit →
Multiplicative
(Completion.ProCIntegerLimitCarrier
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0})),
ProCGroups.ProC.proPProC p (G :=
Multiplicative
(Completion.ProCIntegerLimitCarrier
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))) ∧
FamilyConvergesToOne (G :=
Multiplicative
(Completion.ProCIntegerLimitCarrier
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))) ι ∧
Generation.TopologicallyGenerates (G :=
Multiplicative
(Completion.ProCIntegerLimitCarrier
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0})))
(Set.range ι)Show proof
by
let G : Type := Multiplicative
(Completion.ProCIntegerLimitCarrier
(ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))
let g : G := Completion.proCIntegerOne
(C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))
refine ⟨Function.const PUnit g, ?_, ?_, ?_⟩
· exact Completion.isProPGroup_multiplicative_proCInteger_pGroup (p := p)
· exact familyConvergesToOne_rankOneBasisMap (G := G) g
· exact topologicallyGenerates_rankOneBasisMap
(G := G) (g := g)
(Completion.topologicallyGenerates_singleton_proCIntegerOne_pGroup (p := p))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 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. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□structure ModelData
(K : Type u) [Field K] [IsAlgClosed K] where
carrier : Type u
instGroup : Group carrier
instTopologicalSpace : TopologicalSpace carrier
instIsTopologicalGroup : IsTopologicalGroup carrier
isGaloisModel : Prop
basis : Type u
basisCard : Cardinal.mk basis = Cardinal.mk K
basisMap : basis → carrier
freeProfiniteBasis :
IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.allFiniteProC) basis carrier basisMapApplication-specific bundled data for a profinite group modeled on \(\operatorname{Gal}(K(t)^{\mathrm{alg}}/K(t))\). This lives outside the reusable FreeProC formulation because the Galois interpretation is extra mathematical input, not part of the abstract free pro-\(C\) interface.