theorem freeProCZCCompletedFoxSemidirectLiftMorphism_unique
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(f :
ProCGrp.of ProC F ⟶
ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(hgenerator :
∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x) :
f = freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφCategorical completed Fox semidirect morphisms from a free pro-\(C\) source are unique once their generator values are prescribed.
Show proof
hι.liftMorphism_unique
(ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
(freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ) hφ
(f := f) 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\). 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ))
(f :
ProCGrp.of ProC F ⟶
ProCGrp.of ProC (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 = freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφComponentwise uniqueness for categorical completed Fox semidirect morphisms from a free pro-\(C\) source.
Show proof
by
apply freeProCZCCompletedFoxSemidirectLiftMorphism_unique
(ProC := ProC) hι φ 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\). 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
∃! f :
ProCGrp.of ProC F ⟶
ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ xExistence and uniqueness of the categorical completed Fox semidirect morphism from a free pro-\(C\) source.
Show proof
by
refine ⟨freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφ, ?_, ?_⟩
· exact freeProCZCCompletedFoxSemidirectLiftMorphism_generator
(ProC := ProC) hι φ hφ
· intro f hf
exact freeProCZCCompletedFoxSemidirectLiftMorphism_unique
(ProC := ProC) hι φ 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\). 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem existsUnique_freeProCZCCompletedFoxSemidirectLiftMorphism_components
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
∃! f :
ProCGrp.of ProC F ⟶
ProCGrp.of ProC (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 categorical completed Fox semidirect morphism from a free pro-\(C\) source.
Show proof
by
refine ⟨freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφ, ?_, ?_⟩
· exact ⟨
freeProCZCCompletedFoxSemidirectLiftMorphism_left_generator
(ProC := ProC) hι φ hφ,
freeProCZCCompletedFoxSemidirectLiftMorphism_right_generator
(ProC := ProC) hι φ hφ⟩
· intro f hf
exact freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components
(ProC := ProC) hι φ 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\). 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem existsUnique_freeProCZCCompletedFoxDerivativeVector_of_semidirectMorphism
[ProCGroups.ProC.ProCGroup ProC F]
[ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H)]
{ι : X → F} (hι : IsFreeProCGroup (ProC := ProC) ι)
(φ : X → H)
(hφ : Continuous (freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ)) :
∃! delta : F → ZCFreeFoxCoordinates ProC.finiteQuotientClass (X := X) (H := H),
∃ f :
ProCGrp.of ProC F ⟶
ProCGrp.of ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H),
(∀ 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 categorical completed Fox semidirect morphism with prescribed generator data.
Show proof
by
refine ⟨freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι
(inferInstanceAs
(ProCGroups.ProC.ProCGroup ProC (ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))).isProC
φ hφ, ?_, ?_⟩
· refine ⟨freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφ, ?_, ?_, ?_⟩
· intro g
rfl
· exact freeProCZCCompletedFoxSemidirectLiftMorphism_left_generator
(ProC := ProC) hι φ hφ
· exact freeProCZCCompletedFoxSemidirectLiftMorphism_right_generator
(ProC := ProC) hι φ hφ
· intro delta hdelta
rcases hdelta with ⟨f, hdelta_left, hleft, hright⟩
have hf_eq := freeProCZCCompletedFoxSemidirectLiftMorphism_unique_of_components
(ProC := ProC) hι φ hφ f hleft hright
funext g
calc
delta g = (f g).left := hdelta_left g
_ = (freeProCZCCompletedFoxSemidirectLiftMorphism
(ProC := ProC) hι φ hφ g).left := by
rw [hf_eq]
_ = freeProCZCCompletedFoxDerivativeVector
(ProC := ProC) hι
(inferInstanceAs
(ProCGroups.ProC.ProCGroup ProC
(ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))).isProC
φ 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\). 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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□