FoxDifferential.Completed.Continuous.Automorphism
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
def allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (φ : X → H) :
ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) →ₗ[ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H]
ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) :=
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := X) (F := F) (F' := F) hι e.symm.toMonoidHom
(allFiniteProC_freeProCZCCompletedFoxPullbackGenerator
(X := X) (F := F) hι e.toMonoidHom φ ι)
ιThe named inverse linear map for the completed Fox-Jacobian of a continuous automorphism.
def allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (φ : X → H) :
Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) :=
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := X) (Y := X) (F := F) (F' := F) hι e.symm.toMonoidHom
(allFiniteProC_freeProCZCCompletedFoxPullbackGenerator
(X := X) (F := F) hι e.toMonoidHom φ ι)
ιThe named inverse matrix for the completed Fox-Jacobian of a continuous automorphism.
def allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (φ : X → H)
(j : ZCCompletedGroupAlgebraIndex ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) :
Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j) :=
fun x y =>
zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j
(allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
(X := X) (F := F) (H := H) hι e φ x y)A finite-stage projection of the named inverse matrix for a completed Fox-Jacobian of a continuous automorphism.
theorem allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage_apply
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (φ : X → H)
(j : ZCCompletedGroupAlgebraIndex ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) (x y : X) :
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
(X := X) (F := F) (H := H) hι e φ j x y =
zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j
(allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
(X := X) (F := F) (H := H) hι e φ x y)Evaluation of the finite-stage inverse matrix for a completed Fox-Jacobian of a continuous automorphism.
Show proof
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\). 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 allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (φ : X → H)
(v : ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H)) :
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
(X := X) (F := F) (H := H) hι e φ v =
Matrix.vecMul v
(allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
(X := X) (F := F) (H := H) hι e φ)The named inverse linear map is row-vector multiplication by the named inverse matrix.
Show proof
by
exact allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul
(X := X) (F := F) hι e.symm.toMonoidHom
(allFiniteProC_freeProCZCCompletedFoxPullbackGenerator
(X := X) (F := F) hι e.toMonoidHom φ ι)
ι vProof. 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_freeProCZCCompletedFoxAutomorphism_pullback_symm
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
allFiniteProC_freeProCZCCompletedFoxPullbackGenerator
(X := X) (F := F) hι e.symm.toMonoidHom
(allFiniteProC_freeProCZCCompletedFoxPullbackGenerator
(X := X) (F := F) hι e.toMonoidHom φ ι)
ι =
φShow proof
by
let htarget : ProCGroups.ProC.allFiniteProC
(G := ZCCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H) :=
allFiniteProC_zcCompletedFoxSemidirect ProCGroups.ProC.allFiniteProC.finiteQuotientClass X H
let hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProCGroups.ProC.allFiniteProC) φ) :=
continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H φ
let φe : X → H :=
allFiniteProC_freeProCZCCompletedFoxPullbackGenerator
(X := X) (F := F) hι e.toMonoidHom φ ι
let hφe : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProCGroups.ProC.allFiniteProC) φe) :=
continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProCGroups.ProC.allFiniteProC) X H φe
have hρ := allFiniteProC_freeProCZCCompletedFoxRightHom_comp
(X := X) (Y := X) (F := F) (F' := F) (H := H)
hι hι e.toMonoidHom he_continuous φ
funext x
change freeProCZCCompletedFoxRightHom
(ProC := ProCGroups.ProC.allFiniteProC) hι htarget φe hφe
(e.symm (ι x)) = φ x
have happ := congrFun (congrArg DFunLike.coe hρ) (e.symm (ι x))
calc
freeProCZCCompletedFoxRightHom
(ProC := ProCGroups.ProC.allFiniteProC) hι htarget φe hφe
(e.symm (ι x)) =
((freeProCZCCompletedFoxRightHom
(ProC := ProCGroups.ProC.allFiniteProC) hι htarget φ hφ).comp
e.toMonoidHom) (e.symm (ι x)) := by
simpa [φe, htarget, hφ, hφe] using happ
_ = freeProCZCCompletedFoxRightHom
(ProC := ProCGroups.ProC.allFiniteProC) hι htarget φ hφ (ι x) := by
simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
MulEquiv.apply_symm_apply, freeProCZCCompletedFoxRightHom_apply, freeProCZCCompletedFoxSemidirectLift_generator,
freeProCZCCompletedFoxSemidirectGenerator_right]
_ = φ x := by
simp only [freeProCZCCompletedFoxRightHom_apply, freeProCZCCompletedFoxSemidirectLift_generator,
freeProCZCCompletedFoxSemidirectGenerator_right]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_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι).comp
(allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
(X := X) (F := F) (H := H) hι e φ) =
LinearMap.idComposing the completed Fox-Jacobian linear map of a continuous automorphism with its named inverse gives the identity.
Show proof
by
apply linearMap_ext_pi_single
intro x
have hchain := allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp
(X := X) (Y := X) (F := F) (F' := F) (H := H)
hι hι e.toMonoidHom he_continuous φ (e.symm (ι x))
simpa [LinearMap.comp_apply,
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse,
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap,
allFiniteProC_freeProCZCCompletedFoxJacobian] using hchain.symmProof. 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_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
(φ : X → H) :
(allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
(X := X) (F := F) (H := H) hι e φ).comp
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι) =
LinearMap.idComposing the named inverse for the completed Fox-Jacobian linear map of a continuous automorphism with the Jacobian gives the identity.
Show proof
by
apply linearMap_ext_pi_single
intro x
let φe : X → H :=
allFiniteProC_freeProCZCCompletedFoxPullbackGenerator
(X := X) (F := F) hι e.toMonoidHom φ ι
have hpull :
allFiniteProC_freeProCZCCompletedFoxPullbackGenerator
(X := X) (F := F) hι e.symm.toMonoidHom φe ι =
φ := by
simpa [φe] using
allFiniteProC_freeProCZCCompletedFoxAutomorphism_pullback_symm
(X := X) (F := F) (H := H) hι e he_continuous φ
have hchain := allFiniteProC_freeProCZCCompletedFoxDerivativeVector_comp
(X := X) (Y := X) (F := F) (F' := F) (H := H)
hι hι e.symm.toMonoidHom he_symm_continuous φe (e (ι x))
rw [hpull] at hchain
simpa [LinearMap.comp_apply,
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse,
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap,
allFiniteProC_freeProCZCCompletedFoxJacobian, φe] using hchain.symmProof. 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_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse_mul
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (he_continuous : Continuous e) (φ : X → H) :
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
(X := X) (F := F) (H := H) hι e φ *
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι =
(1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H))The named inverse matrix is a left inverse for the completed Fox-Jacobian matrix of a continuous automorphism.
Show proof
by
rw [Matrix.ext_iff_vecMul]
intro v
have hlin :=
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse
(X := X) (F := F) (H := H) hι e he_continuous φ
have happ := congrFun (congrArg DFunLike.coe hlin) v
simpa [LinearMap.comp_apply,
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul,
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul,
Matrix.vecMul_vecMul, Matrix.vecMul_one] using happProof. 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_freeProCZCCompletedFoxAutomorphismJacobianMatrix_mul_inverse
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
(φ : X → H) :
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix
(X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι *
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse
(X := X) (F := F) (H := H) hι e φ =
(1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H))The named inverse matrix is a right inverse for the completed Fox-Jacobian matrix of a continuous automorphism.
Show proof
by
rw [Matrix.ext_iff_vecMul]
intro v
have hlin :=
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp
(X := X) (F := F) (H := H) hι e he_continuous he_symm_continuous φ
have happ := congrFun (congrArg DFunLike.coe hlin) v
simpa [LinearMap.comp_apply,
allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap_eq_vecMul,
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse_eq_vecMul,
Matrix.vecMul_vecMul, Matrix.vecMul_one] using happProof. 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_freeProCZCCompletedFoxAutomorphismJacobianMatrixStageInverse_mul
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (he_continuous : Continuous e) (φ : X → H)
(j : ZCCompletedGroupAlgebraIndex ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) :
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
(X := X) (F := F) (H := H) hι e φ j *
allFiniteProC_freeProCZCCompletedFoxJacobianMatrixStage
(X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι j =
(1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j))Show proof
by
apply Matrix.ext
intro x y
have h := congrArg
(fun M : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) =>
zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j (M x y))
(allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverse_mul
(X := X) (F := F) (H := H) hι e he_continuous φ)
have hone :
zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j
((1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H)) x y) =
(1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j)) x y := by
by_cases hxy : x = y
· subst y
simp only [zcCompletedGroupAlgebraProjection, Matrix.one_apply_eq, zcCompletedGroupAlgebraProjection_one]
· simp only [zcCompletedGroupAlgebraProjection, ne_eq, hxy, not_false_eq_true, Matrix.one_apply_ne,
zcCompletedGroupAlgebraProjection_zero]
simp only [Matrix.mul_apply] at h
rw [zcCompletedGroupAlgebraProjection_sum] at h
rw [hone] at h
simp only [zcCompletedGroupAlgebraProjection, MulEquiv.toMonoidHom_eq_coe,
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix_apply, zcCompletedGroupAlgebraProjection_mul] at h
simpa [Matrix.mul_apply,
allFiniteProC_freeProCZCCompletedFoxJacobianMatrixStage,
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage] 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_freeProCZCCompletedFoxAutomorphismJacobianMatrixStage_mul_inverse
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
(φ : X → H) (j : ZCCompletedGroupAlgebraIndex ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) :
allFiniteProC_freeProCZCCompletedFoxJacobianMatrixStage
(X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι j *
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage
(X := X) (F := F) (H := H) hι e φ j =
(1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j))Show proof
by
apply Matrix.ext
intro x y
have h := congrArg
(fun M : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H) =>
zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j (M x y))
(allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrix_mul_inverse
(X := X) (F := F) (H := H) hι e he_continuous he_symm_continuous φ)
have hone :
zcCompletedGroupAlgebraProjection ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j
((1 : Matrix X X (ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H)) x y) =
(1 : Matrix X X (ZCCompletedGroupAlgebraStage ProCGroups.ProC.allFiniteProC.finiteQuotientClass H j)) x y := by
by_cases hxy : x = y
· subst y
simp only [zcCompletedGroupAlgebraProjection, Matrix.one_apply_eq, zcCompletedGroupAlgebraProjection_one]
· simp only [zcCompletedGroupAlgebraProjection, ne_eq, hxy, not_false_eq_true, Matrix.one_apply_ne,
zcCompletedGroupAlgebraProjection_zero]
simp only [Matrix.mul_apply] at h
rw [zcCompletedGroupAlgebraProjection_sum] at h
rw [hone] at h
simp only [zcCompletedGroupAlgebraProjection, MulEquiv.toMonoidHom_eq_coe,
allFiniteProC_freeProCZCCompletedFoxJacobianMatrix_apply, zcCompletedGroupAlgebraProjection_mul] at h
simpa [Matrix.mul_apply,
allFiniteProC_freeProCZCCompletedFoxJacobianMatrixStage,
allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianMatrixInverseStage] 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.
□def allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearEquiv
{ι : X → F}
(hι : ProCGroups.FreeProC.IsFreeProCGroup
(ProC := ProCGroups.ProC.allFiniteProC) ι)
(e : F ≃* F) (he_continuous : Continuous e) (he_symm_continuous : Continuous e.symm)
(φ : X → H) :
ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) ≃ₗ[ZCCompletedGroupAlgebra ProCGroups.ProC.allFiniteProC.finiteQuotientClass H]
ZCFreeFoxCoordinates ProCGroups.ProC.allFiniteProC.finiteQuotientClass (X := X) (H := H) := by
refine LinearEquiv.ofLinear
(allFiniteProC_freeProCZCCompletedFoxJacobianLinearMap
(X := X) (Y := X) (F := F) (F' := F) hι e.toMonoidHom φ ι)
(allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMapInverse
(X := X) (F := F) (H := H) hι e φ)
?_ ?_
· exact allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_comp_inverse
(X := X) (F := F) (H := H) hι e he_continuous φ
· exact allFiniteProC_freeProCZCCompletedFoxAutomorphismJacobianLinearMap_inverse_comp
(X := X) (F := F) (H := H) hι e he_continuous he_symm_continuous φThe completed Fox-Jacobian of a continuous automorphism is bundled into a linear equivalence.