FoxDifferential.Completed.FreeProC.Uniqueness.Derivative
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.
theorem freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)
(hf : Continuous f)
(hleft :
∀ x : X, (f (ι x)).left =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))
(hright : ∀ x : X, (f (ι x)).right = φ x) :
(fun g : F => (f g).left) =
freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ hφAny continuous semidirect lift with the prescribed generator components has the canonical free pro-\(C\) completed Fox derivative vector as its left component.
Show proof
by
have hgenerator :
∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x := by
intro x
apply ZCCompletedFoxSemidirect.ext
· exact hleft x
· exact hright x
have hf_eq := hι.lift_unique htarget
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ hf hgenerator
funext g
rw [hf_eq]
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\). 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_continuousCrossedDifferential
{ι : X → F} (hι : 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)
(hcontinuous :
Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ delta hdelta))
(hbasis :
∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) :
delta =
freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget (fun x : X => ψ (ι x))
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
(ProC := ProC) hι ψ delta hdelta hcontinuous hbasis)Continuous completed crossed differentials on a free pro-\(C\) source are uniquely determined by their standard generator values, provided their semidirect graph is continuous.
Show proof
by
have hleft :
∀ x : X,
(freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ delta hdelta (ι x)).left =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) := by
intro x
exact hbasis x
have hright :
∀ x : X,
(freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ delta hdelta (ι x)).right = ψ (ι x) := by
intro x
rfl
have hunique := freeProCZCCompletedFoxDerivativeVector_unique_of_semidirect
(ProC := ProC) hι htarget (fun x : X => ψ (ι x))
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
(ProC := ProC) hι ψ delta hdelta hcontinuous hbasis)
(freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ delta hdelta)
hcontinuous hleft hright
simpa using huniqueProof. 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 freeProCZCCompletedCrossedDifferential_ext
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(ψ : F →* H)
(delta epsilon :
F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H))
(hdelta :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) delta)
(hepsilon :
IsCrossedDifferential (zcCompletedGroupAlgebraScalar ProC.finiteQuotientClass ψ) epsilon)
(hdelta_continuous :
Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ delta hdelta))
(hepsilon_continuous :
Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ epsilon hepsilon))
(hbasis : ∀ x : X, delta (ι x) = epsilon (ι x)) :
delta = epsilonExtensionality for continuous completed crossed differentials on a free pro-\(C\) source. The continuity hypotheses are put on the associated semidirect homomorphisms, which is the form used by the completed Fox construction before the target topology is fully structural.
Show proof
by
let f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ delta hdelta
let g : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H :=
freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ epsilon hepsilon
have hfg : ∀ x : X, f (ι x) = g (ι x) := by
intro x
apply ZCCompletedFoxSemidirect.ext
· exact hbasis x
· rfl
have hsemidirect : f = g := hι.hom_ext htarget hdelta_continuous hepsilon_continuous hfg
funext a
exact congrArg
(fun q : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => (q a).left)
hsemidirectProof. 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 freeProCZCCompletedFoxRightHom_eq_of_continuousCrossedDifferential
{ι : X → F} (hι : 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)
(hcontinuous :
Continuous (freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ delta hdelta))
(hbasis :
∀ x : X, delta (ι x) = Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) :
ψ =
freeProCZCCompletedFoxRightHom
(ProC := ProC) hι htarget (fun x : X => ψ (ι x))
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
(ProC := ProC) hι ψ delta hdelta hcontinuous hbasis)The coefficient homomorphism of a continuous completed crossed differential agrees with the right component of the canonical free pro-\(C\) semidirect lift.
Show proof
by
apply MonoidHom.ext
intro g
have hgenerator :
∀ x : X,
freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ delta hdelta (ι x) =
freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) (fun x : X => ψ (ι x)) x := by
intro x
apply ZCCompletedFoxSemidirect.ext
· exact hbasis x
· rfl
have hsemidirect := hι.lift_unique htarget
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) (fun x : X => ψ (ι x)))
(continuous_freeProCZCCompletedFoxSemidirectGenerator_of_crossedDifferential
(ProC := ProC) hι ψ delta hdelta hcontinuous hbasis)
(f := freeProCZCCompletedFoxSemidirectHomOfCrossedDifferential
(X := X) ψ delta hdelta)
hcontinuous hgenerator
simpa [freeProCZCCompletedFoxRightHom] using
congrArg (fun f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H => (f g).right) hsemidirectProof. 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.
□theorem existsUnique_freeProCZCCompletedFoxDerivativeVector_of_semidirect
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
∃! delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
∃ f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
Continuous f ∧
(∀ g : F, delta g = (f g).left) ∧
(∀ x : X, (f (ι x)).left =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) ∧
∀ x : X, (f (ι x)).right = φ xExistence and uniqueness of the free pro-\(C\) completed Fox derivative vector, formulated as the left component of a continuous semidirect lift with prescribed generator data.
Show proof
by
refine ⟨freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ hφ, ?_, ?_⟩
· refine ⟨freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ, ?_, ?_, ?_, ?_⟩
· exact continuous_freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ
· intro g
rfl
· exact freeProCZCCompletedFoxSemidirectLift_left_generator
(ProC := ProC) hι htarget φ hφ
· exact freeProCZCCompletedFoxSemidirectLift_right_generator
(ProC := ProC) hι htarget φ hφ
· intro delta hdelta
rcases hdelta with ⟨f, hf, hdelta_left, hleft, hright⟩
have hgenerator :
∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x := by
intro x
apply ZCCompletedFoxSemidirect.ext
· exact hleft x
· exact hright x
have hf_eq := hι.lift_unique htarget
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ hf hgenerator
funext g
calc
delta g = (f g).left := hdelta_left g
_ = (freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφ g).left := by
rw [hf_eq]
rfl
_ = freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι htarget φ hφ g := 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\). 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.
□