FoxDifferential.Completed.FreeProC.FiniteQuotientStages
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
import
def freeProCFiniteQuotientStageHom
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
FreeGroup X →* CompletedGroupAlgebraQuotientInClass H C U :=
FreeGroup.lift fun x : X =>
openNormalSubgroupInClassProj (C := C) (G := H) U (φ x)
@[simp]The free-group map to a finite quotient of H induced by a family X \(\to\) H.
theorem freeProCFiniteQuotientStageHom_of
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) (x : X) :
freeProCFiniteQuotientStageHom (C := C) φ U (FreeGroup.of x) =
(QuotientGroup.mk (φ x) :
CompletedGroupAlgebraQuotientInClass H C U)The finite-quotient stage homomorphism for a free pro-\(C\) group has the stated value on representatives.
Show proof
by
simp only [freeProCFiniteQuotientStageHom, openNormalSubgroupInClassProj, QuotientGroup.mk'_apply,
FreeGroup.lift_apply_of]Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem freeProCFiniteQuotientStageHom_eq_comp
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
freeProCFiniteQuotientStageHom (C := C) φ U =
(openNormalSubgroupInClassProj (C := C) (G := H) U).comp (FreeGroup.lift φ)The free quotient-stage map is the quotient projection after the original free-group map.
Show proof
by
ext x
unfold freeProCFiniteQuotientStageHom
rw [FreeGroup.lift_apply_of]
change
openNormalSubgroupInClassProj (C := C) (G := H) U (φ x) =
openNormalSubgroupInClassProj (C := C) (G := H) U
(FreeGroup.lift φ (FreeGroup.of x))
rw [FreeGroup.lift_apply_of]Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 freeProCFiniteQuotientStageHom_transition
(φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V)
(w : FreeGroup X) :
(OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
(freeProCFiniteQuotientStageHom (C := C) φ V w) =
freeProCFiniteQuotientStageHom (C := C) φ U wCompatibility of finite quotient-stage maps under quotient refinement.
Show proof
by
rw [freeProCFiniteQuotientStageHom_eq_comp,
freeProCFiniteQuotientStageHom_eq_comp]
exact congrFun
(openNormalSubgroupInClassProj_compatible (C := C) (G := H) U V hUV)
(FreeGroup.lift φ w)Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 freeProCFiniteQuotientStageKernel
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
Subgroup (FreeGroup X) :=
(freeProCFiniteQuotientStageHom (C := C) φ U).kerinstance freeProCFiniteQuotientStageKernel_normal
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C) :
(freeProCFiniteQuotientStageKernel (C := C) φ U).Normal := by
dsimp [freeProCFiniteQuotientStageKernel]
infer_instanceThe finite-stage relation kernel is a normal subgroup.
theorem freeProCFiniteQuotientStageKernel_antitone
(φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V) :
freeProCFiniteQuotientStageKernel (C := C) φ V ≤
freeProCFiniteQuotientStageKernel (C := C) φ UThe finite-stage relation kernels are antitone with respect to quotient refinement.
Show proof
by
intro w hw
change freeProCFiniteQuotientStageHom (C := C) φ U w = 1
calc
freeProCFiniteQuotientStageHom (C := C) φ U w
=
(OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
(freeProCFiniteQuotientStageHom (C := C) φ V w) :=
(freeProCFiniteQuotientStageHom_transition (C := C) φ hUV w).symm
_ = 1 := by
rw [show freeProCFiniteQuotientStageHom (C := C) φ V w = 1 from hw]
exact map_one _Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
[DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C U)]
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)If the original family topologically generates \(H\), then its image generates every discrete finite quotient \(H/U\), so the corresponding free-group map is surjective.
Show proof
by
let π : H →ₜ* CompletedGroupAlgebraQuotientInClass H C U :=
{ toMonoidHom := openNormalSubgroupInClassProj (C := C) (G := H) U
continuous_toFun := by
change Continuous
(QuotientGroup.mk'
(((OrderDual.ofDual U).1 : OpenNormalSubgroup H) : Subgroup H))
exact continuous_quotient_mk' }
have hπsurj : Function.Surjective π :=
openNormalSubgroupInClassProj_surjective (C := C) (G := H) U
have hgen :
ProCGroups.Generation.TopologicallyGenerates
(G := CompletedGroupAlgebraQuotientInClass H C U)
(Set.range (π ∘ φ)) :=
ProCGroups.FiniteGeneration.topologicallyGenerates_range_comp_of_surjective
(G := H) (H := CompletedGroupAlgebraQuotientInClass H C U)
π hπsurj φ hφgen
simpa [π, freeProCFiniteQuotientStageHom, Function.comp] using
ProCGroups.FiniteGeneration.freeGroup_lift_surjective_of_topologicallyGenerates_discrete
(G := CompletedGroupAlgebraQuotientInClass H C U)
(g := fun x : X => π (φ x)) hgenProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. 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.
□def freeProCFiniteQuotientStageTargetEquiv
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
(hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)) :
finiteFoxStageTargetQuotient
(X := X) (freeProCFiniteQuotientStageKernel (C := C) φ U) ≃*
CompletedGroupAlgebraQuotientInClass H C U :=
QuotientGroup.quotientKerEquivOfSurjective
(freeProCFiniteQuotientStageHom (C := C) φ U) hsurj
@[simp]The canonical identification \(F_X / \ker(F_X \to H/U) \simeq H/U\).
theorem freeProCFiniteQuotientStageTargetEquiv_mk
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
(hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))
(w : FreeGroup X) :
freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurj
(QuotientGroup.mk'
(freeProCFiniteQuotientStageKernel (C := C) φ U) w) =
freeProCFiniteQuotientStageHom (C := C) φ U wShow proof
by
rflProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 freeProCFiniteQuotientStageQMap
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
(hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)) :
CompletedGroupAlgebraQuotientInClass H C U →*
finiteFoxStageTargetQuotient
(X := X) (freeProCFiniteQuotientStageKernel (C := C) φ U) :=
(freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurj).symm.toMonoidHomThe finite quotient stage map sends a target quotient class into the corresponding free-group quotient stage through the inverse of the target equivalence.
theorem freeProCFiniteQuotientStageQMap_injective
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
(hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U)) :
Function.Injective (freeProCFiniteQuotientStageQMap (C := C) φ U hsurj)The finite-quotient stage quotient map is injective.
Show proof
(freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurj).symm.injective
@[simp]Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem freeProCFiniteQuotientStageQMap_generator
(φ : X → H) (U : CompletedGroupAlgebraIndexInClass H C)
(hsurj : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))
(x : X) :
freeProCFiniteQuotientStageQMap (C := C) φ U hsurj
(QuotientGroup.mk (φ x)) =
QuotientGroup.mk'
(freeProCFiniteQuotientStageKernel (C := C) φ U) (FreeGroup.of x)Show proof
by
apply (freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurj).injective
rw [freeProCFiniteQuotientStageTargetEquiv_mk]
simp only [freeProCFiniteQuotientStageQMap, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe,
MulEquiv.apply_symm_apply, freeProCFiniteQuotientStageHom_of]Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem freeProCFiniteQuotientStageTargetEquiv_transition
(φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V)
(hsurjU : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))
(hsurjV : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ V))
(y : finiteFoxStageTargetQuotient
(X := X) (freeProCFiniteQuotientStageKernel (C := C) φ V)) :
freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurjU
(finiteFoxStageTargetQuotientMap
(X := X) (freeProCFiniteQuotientStageKernel_antitone (C := C) φ hUV) y) =
(OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)
(freeProCFiniteQuotientStageTargetEquiv (C := C) φ V hsurjV y)The compatibility between the canonical \(F_X/kernel \to H/U\) equivalences and quotient refinement.
Show proof
by
rcases QuotientGroup.mk'_surjective
(freeProCFiniteQuotientStageKernel (C := C) φ V) y with ⟨w, rfl⟩
rw [finiteFoxStageTargetQuotientMap_mk,
freeProCFiniteQuotientStageTargetEquiv_mk,
freeProCFiniteQuotientStageTargetEquiv_mk,
freeProCFiniteQuotientStageHom_transition]Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. 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. 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.
□theorem freeProCFiniteQuotientStageQMap_transition
(φ : X → H) {U V : CompletedGroupAlgebraIndexInClass H C} (hUV : U ≤ V)
(hsurjU : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ U))
(hsurjV : Function.Surjective (freeProCFiniteQuotientStageHom (C := C) φ V))
(q : CompletedGroupAlgebraQuotientInClass H C V) :
freeProCFiniteQuotientStageQMap (C := C) φ U hsurjU
((OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) =
finiteFoxStageTargetQuotientMap
(X := X) (freeProCFiniteQuotientStageKernel_antitone (C := C) φ hUV)
(freeProCFiniteQuotientStageQMap (C := C) φ V hsurjV q)The canonical quotient maps commute with quotient refinement.
Show proof
by
apply (freeProCFiniteQuotientStageTargetEquiv (C := C) φ U hsurjU).injective
rw [freeProCFiniteQuotientStageTargetEquiv_transition
(C := C) φ hUV hsurjU hsurjV]
simp only [freeProCFiniteQuotientStageQMap, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe,
MulEquiv.apply_symm_apply]Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Surjectivity is obtained by choosing finite-stage lifts of the target coefficients and supports, verifying the derivative formula there, and assembling the compatible lifts. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 freeProCFiniteQuotientStageKernelFamily
(φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H) :
J → Subgroup (FreeGroup X) :=
fun j => freeProCFiniteQuotientStageKernel (C := C) φ (zcIndex j).2The finite relation subgroup family attached to a family of \(\mathbb{Z}_C\llbracket H\rrbracket\) stage indices.
instance freeProCFiniteQuotientStageKernelFamily_normal
(φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H) (j : J) :
(freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j).Normal := by
dsimp [freeProCFiniteQuotientStageKernelFamily]
infer_instanceThe finite-stage relation kernel is a normal subgroup.
theorem freeProCFiniteQuotientStageKernelFamily_antitone
(φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
[Preorder J]
(hzcIndex : ∀ {i j : J}, i ≤ j → zcIndex i ≤ zcIndex j) :
∀ {i j : J}, i ≤ j →
freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j ≤
freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex iThe finite relation subgroup family is antitone under refinement of the \(\mathbb{Z}_C\llbracket H\rrbracket\) stages.
Show proof
by
intro i j hij
exact freeProCFiniteQuotientStageKernel_antitone (C := C) φ (hzcIndex hij).2Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 freeProCFiniteQuotientStageQMapFamily
(φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
[∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
∀ j : J,
CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2 →*
finiteFoxStageTargetQuotient
(X := X) (freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j) :=
fun j =>
freeProCFiniteQuotientStageQMap (C := C) φ (zcIndex j).2
(freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
(C := C) φ (zcIndex j).2 hφgen)The canonical \(H/U_j \to F/N_j\) comparison maps for a finite quotient stage family.
theorem freeProCFiniteQuotientStageQMapFamily_injective
(φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
[∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
∀ j : J,
Function.Injective
(freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen j)The finite-quotient stage family map is injective.
Show proof
by
intro j
exact freeProCFiniteQuotientStageQMap_injective (C := C) φ (zcIndex j).2
(freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
(C := C) φ (zcIndex j).2 hφgen)
@[simp]Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem freeProCFiniteQuotientStageQMapFamily_generator
(φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
[∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
(j : J) (x : X) :
freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen j
(QuotientGroup.mk (φ x)) =
QuotientGroup.mk'
(freeProCFiniteQuotientStageKernelFamily (C := C) φ zcIndex j)
(FreeGroup.of x)Show proof
by
exact freeProCFiniteQuotientStageQMap_generator (C := C) φ (zcIndex j).2
(freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
(C := C) φ (zcIndex j).2 hφgen) xProof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem freeProCFiniteQuotientStageQMapFamily_transition
(φ : X → H) (zcIndex : J → ZCCompletedGroupAlgebraIndex C H)
[Preorder J]
(hzcIndex : ∀ {i j : J}, i ≤ j → zcIndex i ≤ zcIndex j)
[∀ j, DiscreteTopology (CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2)]
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
∀ {i j : J} (hij : i ≤ j),
∀ q : CompletedGroupAlgebraQuotientInClass H C (zcIndex j).2,
freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen i
((OpenNormalSubgroupInClass.map
(C := C) (G := H)
(U := OrderDual.ofDual (zcIndex i).2)
(V := OrderDual.ofDual (zcIndex j).2)
(hzcIndex hij).2) q) =
finiteFoxStageTargetQuotientMap
(X := X)
(freeProCFiniteQuotientStageKernelFamily_antitone
(C := C) φ zcIndex hzcIndex hij)
(freeProCFiniteQuotientStageQMapFamily (C := C) φ zcIndex hφgen j q)The canonical comparison maps commute with refinement of the \(\mathbb{Z}_C\llbracket H\rrbracket\) stage family.
Show proof
by
intro i j hij q
exact freeProCFiniteQuotientStageQMap_transition (C := C) φ (hzcIndex hij).2
(freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
(C := C) φ (zcIndex i).2 hφgen)
(freeProCFiniteQuotientStageHom_surjective_of_topologicallyGenerates
(C := C) φ (zcIndex j).2 hφgen)
qProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). Completed assertions are checked after projection to every finite stage; continuity and closure follow from the inverse-limit topology and the closedness of the coordinate conditions. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. The finite-stage quotient maps preserve the chosen generators, so the crossed-derivation calculation does not depend on the representative of a coset. Linearity over the completed coefficient ring is checked after projection to each coefficient stage. The completed identity is therefore the unique compatible family whose coordinates are the verified finite Fox identities. 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 freeProCZCBifilteredFiniteQuotientStageCoeffMap
(φ : X → H) (nstage : J → ℕ) [∀ j, Fact (0 < nstage j)]
(zcIndex : J → ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H)
(hmod : ∀ j : J, nstage j ∣ (zcIndex j).1.modulus)
[∀ j, DiscreteTopology
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass (zcIndex j).2)]
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
(j : J) :
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+*
finiteFoxStageTargetGroupAlgebra
(X := X)
(freeProCFiniteQuotientStageKernelFamily
(C := ProC.finiteQuotientClass) φ zcIndex j)
(nstage j) :=
zcCompletedGroupAlgebraBifilteredStageCoeffMap
(ProC := ProC) (X := X) (H := H)
(freeProCFiniteQuotientStageKernelFamily
(C := ProC.finiteQuotientClass) φ zcIndex)
nstage zcIndex hmod
(freeProCFiniteQuotientStageQMapFamily
(C := ProC.finiteQuotientClass) φ zcIndex hφgen) jdef freeProCZCBifilteredAllFiniteQuotientStageCoeffMap
(φ : X → H)
(hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
(j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) :
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+*
finiteFoxStageTargetGroupAlgebra
(X := X)
(freeProCFiniteQuotientStageKernelFamily
(C := ProC.finiteQuotientClass) φ
(id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H) j)
j.1.modulus := by
letI :
∀ j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H,
Fact (0 < j.1.modulus) :=
fun j => ProCIntegerIndex.positiveFact j.1
letI :
∀ j : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H,
DiscreteTopology
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2) :=
fun j =>
QuotientGroup.discreteTopology
(ProCGroups.openNormalSubgroup_isOpen (G := H)
((OrderDual.ofDual j.2).1 : OpenNormalSubgroup H))
exact
freeProCZCBifilteredFiniteQuotientStageCoeffMap
(ProC := ProC) (X := X) (H := H) φ (fun j => j.1.modulus)
(id : ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H →
ZCCompletedGroupAlgebraIndex ProC.finiteQuotientClass H)
(fun _ => dvd_rfl) hφgen jtheorem zcCompletedGroupAlgebraAllStageQuotientMap_identity_basis_of_isProCGroup
[ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
(hH : IsProCGroup C H) :
HasIdentityQuotientKernelNeighbourhoodBasis
(Y := H)
(fun j : ZCCompletedGroupAlgebraIndex C H =>
openNormalSubgroupInClassProj (C := C) (G := H) j.2)The full family of quotient maps \(H \to H/U\), indexed by the \(\mathbb{Z}_C\)-completed group-algebra indices for \(C\) and \(H\), has identity-neighborhood kernels for any pro-\(C\) group \(H\). The coefficient coordinate of the index is unspecified here; it is filled with the terminal coefficient quotient.
Show proof
by
intro U hU hUone
rcases hH.hasOpenNormalBasisInClass U hU hUone with ⟨V, hVU, hCV⟩
let Vc : OpenNormalSubgroupInClass C H := ⟨V, hCV⟩
refine ⟨(ProCIntegerIndex.terminal (C := C) inferInstance, OrderDual.toDual Vc), ?_⟩
intro z hz
apply hVU
exact
(QuotientGroup.eq_one_iff
(N := ((V : OpenNormalSubgroup H) : Subgroup H)) z).1 hzProof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). At finite coefficient or quotient stages, the source and target coordinates are obtained by applying the same quotient map to supports and the given coefficient map to coefficients. Kernel and augmentation-ideal statements use the Fox fundamental identity, which expresses an element minus its augmentation in terms of the Fox derivatives of the chosen generators. Finiteness at a stage follows because the quotient group and coefficient ring at that stage are finite, so the group-algebra support space is finite. Since the generator formulas determine the differential or homomorphism uniquely, equality of all finite-stage Fox coordinates proves the asserted completed identity. The finite-stage verification is made before passing to completion, so no topological density argument changes the algebraic calculation. Each completed coefficient system is obtained as a compatible family, and the quotient maps commute with the Fox differential by the generator formula. Thus the identity proved on generators persists under products, inverses, finite linear combinations, and finally under the inverse-limit passage. 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.
□