FoxDifferential.Completed.Continuous.Free.Continuity
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
import
theorem continuous_freeProCZCCompletedFoxSemidirectGenerator
[TopologicalSpace X]
(φ : X → H)
(hleft : Continuous (fun x : X =>
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)))
(hφ : Continuous φ) :
Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)The completed Fox semidirect generator map is continuous when both component maps are continuous.
Show proof
by
rw [continuous_induced_rng]
exact hleft.prodMk hφ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\). 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. 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 continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
[TopologicalSpace X] [DiscreteTopology X] (φ : X → H) :
Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)The completed Fox semidirect generator map is continuous for a discrete generating space.
Show proof
continuous_of_discreteTopologyProof. 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. 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. 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 continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(ψ : F →* H)
(delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(hdelta : IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ) :
Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(ProC := ProC) (X := X) (F := F) (H := H) ψ delta hdelta)A crossed-differential graph into the completed Fox semidirect target is continuous when both its component maps are continuous.
Show proof
by
rw [continuous_induced_rng]
exact hdelta_continuous.prodMk hψ_continuousProof. 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. 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 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 continuous_freeProCZCCompletedFoxRightHom
{ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
Continuous (freeProCZCCompletedFoxRightHom
(ProC := ProC) hι htarget φ hφ)The target-group component of the free pro-\(C\) completed Fox semidirect lift is continuous.
Show proof
by
change Continuous (fun g : F =>
(freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ g).right)
exact (continuous_zcCompletedFoxSemidirect_right ProC.finiteQuotientClass X H).comp
(continuous_freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ)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\). 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. 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. 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 continuous_freeProCZCCompletedFoxRightHomOfConvergingSet
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
Continuous (freeProCZCCompletedFoxRightHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen)The right component of the converging-set completed Fox semidirect lift is continuous.
Show proof
by
change Continuous (fun g : F =>
(freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen g).right)
exact (continuous_zcCompletedFoxSemidirect_right ProC.finiteQuotientClass X H).comp
(continuous_freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen)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\). 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. 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. 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 freeProCZCCompletedFoxRightHomOfConvergingSet_eq_lift
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X F ι)
(hH : ProC (G := H))
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)))
(hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ)
(hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
freeProCZCCompletedFoxRightHomOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen =
hι.lift hH φ hφHconv hφHgenThe right component of the converging-set semidirect Fox lift is exactly the universal free-pro-\(C\) lift of its generator values.
Show proof
by
apply hι.lift_unique hH φ hφHconv hφHgen
· exact continuous_freeProCZCCompletedFoxRightHomOfConvergingSet
(ProC := ProC) X H hι htarget φ hφconv hφgen
· intro x
simp only [freeProCZCCompletedFoxRightHomOfConvergingSet_generator]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\). Exactness is proved by identifying the image of the previous boundary map with the elements whose Fox coordinates vanish under the next boundary map, giving both inclusions at the finite stages. 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem continuous_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
Continuous (freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv)The closed-generated completed Fox semidirect lift is continuous as a map to the full semidirect target.
Show proof
by
change Continuous (fun g : F =>
(freeProCZCCompletedFoxSemidirectLiftToClosedGenerated
(ProC := ProC) hι φ htarget hφconv g :
ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
exact continuous_subtype_val.comp
(freeProCZCCompletedFoxSemidirectLiftHomToClosedGenerated
(ProC := ProC) hι φ htarget hφconv).continuous_toFunProof. 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. 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. 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 continuous_freeProCZCCompletedFoxRightHomViaClosedGenerated
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
Continuous (freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv)The right component of the closed-generated completed Fox semidirect lift is continuous.
Show proof
by
change Continuous (fun g : F =>
(freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv g).right)
exact (continuous_zcCompletedFoxSemidirect_right ProC.finiteQuotientClass X H).comp
(continuous_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) X H hι φ htarget hφconv)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\). 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. 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. 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 freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_lift
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X F ι)
(hH : ProC (G := H))
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
(hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ)
(hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ)) :
freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv =
hι.lift hH φ hφHconv hφHgenThe right component of the closed-generated semidirect Fox lift is the universal free-pro-\(C\) lift of its generator values.
Show proof
by
apply hι.lift_unique hH φ hφHconv hφHgen
· exact continuous_freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) X H hι φ htarget hφconv
· intro x
simp only [freeProCZCCompletedFoxRightHomViaClosedGenerated_generator]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\). 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. 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. 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 freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_continuousHom
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X F ι)
(hH : ProC (G := H))
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ))
(hφHconv : ProCGroups.FreeProC.FamilyConvergesToOne (G := H) φ)
(hφHgen : ProCGroups.Generation.TopologicallyGenerates (G := H) (Set.range φ))
(ψ : F →ₜ* H)
(hψ_gen : ∀ x : X, ψ (ι x) = φ x) :
freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv =
ψ.toMonoidHomThe right component of the closed-generated semidirect Fox lift is the intended continuous homomorphism with the same generator values.
Show proof
by
have hright_lift :
freeProCZCCompletedFoxRightHomViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv =
hι.lift hH φ hφHconv hφHgen :=
freeProCZCCompletedFoxRightHomViaClosedGenerated_eq_lift
(ProC := ProC) X H hι hH φ htarget hφconv hφHconv hφHgen
have hψ_lift :
ψ.toMonoidHom = hι.lift hH φ hφHconv hφHgen := by
apply hι.lift_unique hH φ hφHconv hφHgen
· exact ψ.continuous_toFun
· exact hψ_gen
exact hright_lift.trans hψ_lift.symmtheorem continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X F ι)
(φ : X → H)
(htarget :
ProC (G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))))
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G :=
(freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
(ProC := ProC) φ : Subgroup
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)))
(freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator (ProC := ProC) φ)) :
Continuous (freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv)The derivative-vector component of the closed-generated semidirect lift is continuous.
Show proof
by
change Continuous (fun g : F =>
(freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) hι φ htarget hφconv g).left)
exact (continuous_zcCompletedFoxSemidirect_left ProC.finiteQuotientClass X H).comp
(continuous_freeProCZCCompletedFoxSemidirectLiftViaClosedGenerated
(ProC := ProC) X H hι φ htarget hφconv)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\). 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. 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. 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 continuous_freeProCZCCompletedFoxDerivativeVector
{ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
Continuous (freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ hφ)The completed Fox derivative-vector component of the free pro-\(C\) semidirect lift is continuous.
Show proof
by
change Continuous (fun g : F =>
(freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ g).left)
exact (continuous_zcCompletedFoxSemidirect_left ProC.finiteQuotientClass X H).comp
(continuous_freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ)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\). 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. 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. 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 continuous_freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProC) X F ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφconv :
ProCGroups.FreeProC.FamilyConvergesToOne
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(hφgen :
ProCGroups.Generation.TopologicallyGenerates
(G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(Set.range (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))) :
Continuous (freeProCZCCompletedFoxDerivativeVectorOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen)The derivative-vector component of the converging-set completed Fox semidirect lift is continuous.
Show proof
by
change Continuous (fun g : F =>
(freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen g).left)
exact (continuous_zcCompletedFoxSemidirect_left ProC.finiteQuotientClass X H).comp
(continuous_freeProCZCCompletedFoxSemidirectLiftOfConvergingSet
(ProC := ProC) hι htarget φ hφconv hφgen)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\). 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. 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. 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 continuous_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff
{ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(ψ : F →* H)
(delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(hdelta : IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
(hbasis :
∀ x : X, delta (ι x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) :
Continuous (freeProCZCCompletedFoxSemidirectGenerator
(ProC := ProC) (fun x : X => ψ (ι x)))The semidirect generator map attached to a continuous crossed differential is continuous once the component maps are continuous.
Show proof
continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
(ProC := ProC) hι ψ delta hdelta
(continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(ProC := ProC) (X := X) (F := F) (H := H)
ψ delta hdelta hdelta_continuous hψ_continuous)
hbasisProof. 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. 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. 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 freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDiff_components
{ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(ψ : F →* H)
(delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(hdelta : IsCrossedDifferential
(zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
(hdelta_continuous : Continuous delta) (hψ_continuous : Continuous ψ)
(hbasis :
∀ x : X, delta (ι x) =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) :
delta =
freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget (fun x : X => ψ (ι x))
(continuous_freeProCZCFoxSemiGenerator_of_continuousCrossedDiff
(ProC := ProC) X H hι ψ delta hdelta hdelta_continuous hψ_continuous hbasis)Continuous completed crossed differentials with continuous coefficient homomorphism are uniquely identified with the canonical free pro-\(C\) completed Fox derivative vector.
Show proof
freeProCZCCompletedFoxDerivativeVector_unique_of_continuousCrossedDifferential
(ProC := ProC) hι htarget ψ delta hdelta
(continuous_freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(ProC := ProC) (X := X) (F := F) (H := H)
ψ delta hdelta hdelta_continuous hψ_continuous)
hbasisProof. 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. 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. 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. 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.
□