FoxDifferential.Completed.Continuous.ChainRule.Iterated
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.
abbrev allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
{mu : Z → F''}
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(θ : F' →* F'') (φ : Z → H) (κ : Y → F') : Y → H :=
allFiniteProC_freeProCZCCompletedFoxPullbackGenerator
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κThe pulled-back target generator on the middle free source in a two-step source chain.
abbrev allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
{κ : Y → F'} {mu : Z → F''}
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →* F') (θ : F' →* F'') (φ : Z → H) (ι : X → F) : X → H :=
allFiniteProC_freeProCZCCompletedFoxPullbackGenerator
(X := X) (Y := Y) (F := F) (F' := F') hκ η
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
ιThe pulled-back target generator on the first free source in a two-step source chain.
theorem allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap_comp_comp
{ι : X → F} {κ : Y → F'} {mu : Z → F''}
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →* F') (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) :
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := Z) (F := F) (F' := F'') hmu (θ.comp η) φ ι =
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ).comp
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := Y) (F := F) (F' := F') hκ η
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
ι)Completed Fox-Jacobian functoriality for two composable continuous free pro-\(C\) source maps, as a composition of finite linear maps.
Show proof
by
classical
apply linearMap_ext_pi_single
intro x
have hchain := allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp
(X := Y) (Y := Z) (F := F') (F' := F'') (H := H)
hκ hmu θ hθ_continuous φ (η (ι x))
simpa [LinearMap.comp_apply,
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap,
allFiniteProC_freeProCZCCompletedFoxJacobian,
allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator] using hchainProof. 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 allFiniteProC_freeProCZCCompletedFoxJacobianMatrix_comp_comp
{ι : X → F} {κ : Y → F'} {mu : Z → F''}
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →* F') (θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) :
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := X) (Y := Z) (F := F) (F' := F'') hmu (θ.comp η) φ ι =
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := X) (Y := Y) (F := F) (F' := F') hκ η
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
ι *
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κCompleted Fox-Jacobian functoriality for two composable continuous free pro-\(C\) source maps, as a matrix product.
Show proof
by
apply Matrix.ext
intro x z
have h := congrFun
(allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp
(X := Y) (Y := Z) (F := F') (F' := F'') (H := H)
hκ hmu θ hθ_continuous φ (η (ι x))) z
simpa [Matrix.mul_apply,
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix,
allFiniteProC_freeProCZCCompletedFoxJacobian,
allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator] using hProof. 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 allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp
{ι : X → F} {κ : Y → F'} {mu : Z → F''}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →* F') (hη_continuous : Continuous η)
(θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) (g : F) :
freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hmu
(allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) =
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := Y) (F := F) (F' := F') hκ η
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
ι
(freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hι
(allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η θ φ ι)
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η θ φ ι)) g))Three-term completed pro-\(C\) Fox chain rule in vector form.
Show proof
by
calc
freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hmu
(allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) =
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
(freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hκ
(allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Y H)
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) Y H
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)) (η g)) := by
exact allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp
(X := Y) (Y := Z) (F := F') (F' := F'') (H := H)
hκ hmu θ hθ_continuous φ (η g)
_ =
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := Y) (F := F) (F' := F') hκ η
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
ι
(freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hι
(allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η θ φ ι)
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η θ φ ι)) g)) := by
exact congrArg
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ)
(allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp
(X := X) (Y := Y) (F := F) (F' := F') (H := H)
hι hκ η hη_continuous
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ) g)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. 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 allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix
{ι : X → F} {κ : Y → F'} {mu : Z → F''}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →* F') (hη_continuous : Continuous η)
(θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) (g : F) :
freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hmu
(allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) =
Matrix.vecMul
(Matrix.vecMul
(freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hι
(allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η θ φ ι)
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η θ φ ι)) g)
(allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := X) (Y := Y) (F := F) (F' := F') hκ η
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
ι))
(allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ)The three-term completed pro-\(C\) Fox chain rule in matrix form.
Show proof
by
rw [allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp
(X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
hι hκ hmu η hη_continuous θ hθ_continuous φ g]
rw [allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul]
rw [allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul]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. 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 allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply
{ι : X → F} {κ : Y → F'} {mu : Z → F''}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →* F') (hη_continuous : Continuous η)
(θ : F' →* F'') (hθ_continuous : Continuous θ) (φ : Z → H) (g : F) (z : Z) :
freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hmu
(allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) z =
∑ y : Y,
(∑ x : X,
freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hι
(allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η θ φ ι)
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η θ φ ι)) g x *
allFiniteProC_freeProCZCCompletedFoxJacobian
(X := X) (Y := Y) (F := F) (F' := F') hκ η
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ φ κ)
ι x y) *
allFiniteProC_freeProCZCCompletedFoxJacobian
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ φ κ y zThree-term completed pro-\(C\) Fox chain rule in component form.
Show proof
by
have h := congrFun
(allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix
(X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
hι hκ hmu η hη_continuous θ hθ_continuous φ g) z
simpa [Matrix.vecMul, dotProduct,
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix] using hProof. 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. 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 allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap_comp_comp_continuousMonoidHom
{ι : X → F} {κ : Y → F'} {mu : Z → F''}
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) :
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := Z) (F := F) (F' := F'') hmu
(θ.toMonoidHom.comp η.toMonoidHom) φ ι =
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ).comp
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
ι)Continuous-homomorphism form of completed Fox-Jacobian functoriality, as a composition of finite linear maps.
Show proof
by
exact allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap_comp_comp
(X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
hκ hmu η.toMonoidHom θ.toMonoidHom θ.continuous_toFun φ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 allFiniteProC_freeProCZCCompletedFoxJacobianMatrix_comp_comp_continuousMonoidHom
{ι : X → F} {κ : Y → F'} {mu : Z → F''}
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) :
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := X) (Y := Z) (F := F) (F' := F'') hmu
(θ.toMonoidHom.comp η.toMonoidHom) φ ι =
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
ι *
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κContinuous-homomorphism form of completed Fox-Jacobian functoriality, as a matrix product.
Show proof
by
exact allFiniteProC_freeProCZCCompletedFoxJacobianMatrix_comp_comp
(X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
hκ hmu η.toMonoidHom θ.toMonoidHom θ.continuous_toFun φ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 allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp_continuousMonoidHom
{ι : X → F} {κ : Y → F'} {mu : Z → F''}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) (g : F) :
freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hmu
(allFiniteProC_zcCompletedFoxSemidirect
ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) =
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
ι
(freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hι
(allFiniteProC_zcCompletedFoxSemidirect
ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProCGroups.ProC.allFiniteProC) X H
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)) g))Continuous-homomorphism form of the three-term completed pro-\(C\) Fox chain rule.
Show proof
by
exact allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp
(X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
hι hκ hmu η.toMonoidHom η.continuous_toFun θ.toMonoidHom θ.continuous_toFun φ gProof. 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 allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix_continuousMonoidHom
{ι : X → F} {κ : Y → F'} {mu : Z → F''}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) (g : F) :
freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hmu
(allFiniteProC_zcCompletedFoxSemidirect
ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) =
Matrix.vecMul
(Matrix.vecMul
(freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hι
(allFiniteProC_zcCompletedFoxSemidirect
ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProCGroups.ProC.allFiniteProC) X H
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)) g)
(allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
ι))
(allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ)The continuous-homomorphism form of the three-term completed pro-\(C\) Fox chain rule in matrix form.
Show proof
by
exact allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp_matrix
(X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
hι hκ hmu η.toMonoidHom η.continuous_toFun θ.toMonoidHom θ.continuous_toFun φ gProof. 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 allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply_continuousMonoidHom
{ι : X → F} {κ : Y → F'} {mu : Z → F''}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(hκ : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) κ)
(hmu : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) mu)
(η : F →ₜ* F') (θ : F' →ₜ* F'') (φ : Z → H) (g : F) (z : Z) :
freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hmu
(allFiniteProC_zcCompletedFoxSemidirect
ProCGroups.ProC.allFiniteProC.finiteQuotientClass Z H) φ
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProCGroups.ProC.allFiniteProC) Z H φ) (θ (η g)) z =
∑ y : Y,
(∑ x : X,
freeProCZCCompletedFoxDerivativeVector
(ProC := ProCGroups.ProC.allFiniteProC) hι
(allFiniteProC_zcCompletedFoxSemidirect
ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H)
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete
(ProC := ProCGroups.ProC.allFiniteProC) X H
(allFiniteProC_freeProCZCCompletedFoxFirstPullbackGenerator
(X := X) (F := F) (Y := Y) (F' := F') (Z := Z) (F'' := F'')
hκ hmu η.toMonoidHom θ.toMonoidHom φ ι)) g x *
allFiniteProC_freeProCZCCompletedFoxJacobian
(X := X) (Y := Y) (F := F) (F' := F') hκ η.toMonoidHom
(allFiniteProC_freeProCZCCompletedFoxMiddlePullbackGenerator
(Y := Y) (F' := F') (Z := Z) (F'' := F'') hmu θ.toMonoidHom φ κ)
ι x y) *
allFiniteProC_freeProCZCCompletedFoxJacobian
(X := Y) (Y := Z) (F := F') (F' := F'') hmu θ.toMonoidHom φ κ y zContinuous-homomorphism form of the three-term completed pro-\(C\) Fox chain rule in component form.
Show proof
by
exact allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp_comp_apply
(X := X) (Y := Y) (Z := Z) (F := F) (F' := F') (F'' := F'') (H := H)
hι hκ hmu η.toMonoidHom η.continuous_toFun θ.toMonoidHom θ.continuous_toFun φ g zProof. 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.
□