FoxDifferential.Completed.FreeProC.Uniqueness.Lift
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 freeProCZCCompletedFoxSemidirectLift_unique
{ι : 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)
(hgenerator :
∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x) :
f = freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφContinuous completed Fox semidirect lifts from a free pro-\(C\) source are unique once their generator values are prescribed.
Show proof
hι.lift_unique htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
hφ hf hgeneratorProof. 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 freeProCZCCompletedFoxSemidirectLift_unique_of_components
{ι : 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) :
f = freeProCZCCompletedFoxSemidirectLift
(ProC := ProC) hι htarget φ hφComponentwise uniqueness for continuous completed Fox semidirect lifts from a free pro-\(C\) source.
Show proof
by
apply freeProCZCCompletedFoxSemidirectLift_unique
(ProC := ProC) hι htarget φ hφ f hf
intro x
apply ZCCompletedFoxSemidirect.ext
· exact hleft x
· exact hright xProof. 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 freeProCZCCompletedFoxSemidirectLiftHom_unique
{ι : 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)
(hgenerator :
∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x) :
f = freeProCZCCompletedFoxSemidirectLiftHom
(ProC := ProC) hι htarget φ hφContinuous completed Fox semidirect homomorphisms from a free pro-\(C\) source are unique once their generator values are prescribed.
Show proof
hι.liftHom_unique htarget (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)
hφ hgeneratorProof. 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 freeProCZCCompletedFoxSemidirectLiftHom_unique_of_components
{ι : 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)
(hleft :
∀ x : X, (f (ι x)).left =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H))
(hright : ∀ x : X, (f (ι x)).right = φ x) :
f = freeProCZCCompletedFoxSemidirectLiftHom
(ProC := ProC) hι htarget φ hφComponentwise uniqueness for continuous completed Fox semidirect homomorphisms from a free pro-\(C\) source.
Show proof
by
apply freeProCZCCompletedFoxSemidirectLiftHom_unique
(ProC := ProC) hι htarget φ hφ f
intro x
apply ZCCompletedFoxSemidirect.ext
· exact hleft x
· exact hright xProof. 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 existsUnique_freeProCZCCompletedFoxSemidirectLiftHom
{ι : 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,
∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ xExistence and uniqueness of the continuous completed Fox semidirect homomorphism from a free pro-\(C\) source.
Show proof
by
refine ⟨freeProCZCCompletedFoxSemidirectLiftHom
(ProC := ProC) hι htarget φ hφ, ?_, ?_⟩
· exact freeProCZCCompletedFoxSemidirectLiftHom_generator
(ProC := ProC) hι htarget φ hφ
· intro f hf
exact freeProCZCCompletedFoxSemidirectLiftHom_unique
(ProC := ProC) hι htarget φ hφ f hfProof. 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 existsUnique_freeProCZCCompletedFoxSemidirectLiftHom_components
{ι : 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,
(∀ x : X, (f (ι x)).left =
Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) ∧
∀ x : X, (f (ι x)).right = φ xComponentwise existence and uniqueness of the continuous completed Fox semidirect homomorphism from a free pro-\(C\) source.
Show proof
by
refine ⟨freeProCZCCompletedFoxSemidirectLiftHom
(ProC := ProC) hι htarget φ hφ, ?_, ?_⟩
· exact ⟨
freeProCZCCompletedFoxSemidirectLiftHom_left_generator
(ProC := ProC) hι htarget φ hφ,
freeProCZCCompletedFoxSemidirectLiftHom_right_generator
(ProC := ProC) hι htarget φ hφ⟩
· intro f hf
exact freeProCZCCompletedFoxSemidirectLiftHom_unique_of_components
(ProC := ProC) hι htarget φ hφ f hf.1 hf.2Proof. Work from the defining Fox differential and its crossed-derivation rule. The values on generators determine the map; the product rule gives \(d(xy)=d(x)+x d(y)\), and the inverse rule follows by applying the product rule to \(x x^{-1}=1\). 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.
□