FoxDifferential.Completed.FreeProC.ProCIntegerStageCoeffProjection
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
import
def zcCompletedGroupAlgebraStageToFiniteFoxStage
(hmod : n ∣ i.1.modulus)
(qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
finiteFoxStageTargetQuotient (X := X) N) :
ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H i →+*
finiteFoxStageTargetGroupAlgebra (X := X) N n := by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Algebra (ModNCompletedCoeff i.1.modulus) (ModNCompletedCoeff n) :=
ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := i.1.modulus) hmod
letI : Algebra (ModNCompletedCoeff i.1.modulus)
(finiteFoxStageTargetGroupAlgebra (X := X) N n) := inferInstance
exact
(MonoidAlgebra.lift (ModNCompletedCoeff i.1.modulus)
(finiteFoxStageTargetGroupAlgebra (X := X) N n)
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2)
((MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N)).comp qmap)).toRingHomtheorem zcCompletedGroupAlgebraStageToFiniteFoxStage_of
(hmod : n ∣ i.1.modulus)
(qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
finiteFoxStageTargetQuotient (X := X) N)
(q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2) :
zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N n i hmod qmap
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2) q) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) (qmap q)Evaluation on a completed group-algebra stage basis element.
Show proof
by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
simp only [zcCompletedGroupAlgebraStageToFiniteFoxStage, AlgHom.toRingHom_eq_coe, MonoidAlgebra.of_apply,
RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.coe_comp, Function.comp_apply, MonoidAlgebra.smul_single,
one_smul]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. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem zcCompletedGroupAlgebraStageToFiniteFoxStage_single
(hmod : n ∣ i.1.modulus)
(qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
finiteFoxStageTargetQuotient (X := X) N)
(q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2)
(a : ModNCompletedCoeff i.1.modulus) :
zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N n i hmod qmap
(MonoidAlgebra.single q a) =
MonoidAlgebra.single (qmap q)
(modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod a)Evaluation on a single coefficient at a stage quotient element.
Show proof
by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Algebra (ModNCompletedCoeff i.1.modulus) (ModNCompletedCoeff n) :=
ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := i.1.modulus) hmod
have hcoeff :
algebraMap (ModNCompletedCoeff i.1.modulus) (ModNCompletedCoeff n) a =
modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod a := by
rfl
rw [zcCompletedGroupAlgebraStageToFiniteFoxStage]
ext q'
simp only [AlgHom.toRingHom_eq_coe, MonoidAlgebra.single, RingHom.coe_coe, MonoidAlgebra.lift_single,
MonoidHom.coe_comp, Function.comp_apply, MonoidAlgebra.of_apply, Algebra.smul_def, MonoidAlgebra.coe_algebraMap,
hcoeff, MonoidAlgebra.single_mul_single, one_mul, mul_one]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\). 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem zcCompletedGroupAlgebraStageToFiniteFoxStage_self_injective
(qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
finiteFoxStageTargetQuotient (X := X) N)
(hqmap : Function.Injective qmap) :
Function.Injective
(zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N i.1.modulus i dvd_rfl qmap)If no coefficient reduction is taken and the target quotient comparison is injective, then the finite-stage map from the completed group-algebra stage to the finite Fox target group algebra is injective.
Show proof
by
classical
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
have hstage :
zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N i.1.modulus i dvd_rfl qmap =
MonoidAlgebra.mapDomainRingHom (ModNCompletedCoeff i.1.modulus) qmap := by
apply MonoidAlgebra.ringHom_ext
· intro r
rw [zcCompletedGroupAlgebraStageToFiniteFoxStage_single]
simp only [map_one, modNCompletedCoeffMap_rfl, RingHom.id_apply, MonoidAlgebra.mapDomainRingHom_apply,
Finsupp.mapDomain_single]
· intro q
rw [← MonoidAlgebra.of_apply,
zcCompletedGroupAlgebraStageToFiniteFoxStage_of]
simp only [MonoidAlgebra.of_apply, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
rw [hstage]
intro x y hxy
exact (MonoidAlgebra.mapDomain_injective
(R := ModNCompletedCoeff i.1.modulus) hqmap) (by
simpa [MonoidAlgebra.mapDomainRingHom_apply] using hxy)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\). 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. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements.
□def zcCompletedGroupAlgebraFiniteFoxStageCoeffMap
(hmod : n ∣ i.1.modulus)
(qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
finiteFoxStageTargetQuotient (X := X) N) :
ZCCompletedGroupAlgebra ProC.finiteQuotientClass H →+*
finiteFoxStageTargetGroupAlgebra (X := X) N n :=
(zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N n i hmod qmap).comp
(zcCompletedGroupAlgebraProjectionRingHom ProC.finiteQuotientClass H i)The resulting completed-to-finite coefficient map.
theorem zcCompletedGroupAlgebraFiniteFoxStageCoeffMap_apply
(hmod : n ∣ i.1.modulus)
(qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
finiteFoxStageTargetQuotient (X := X) N)
(a : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) :
zcCompletedGroupAlgebraFiniteFoxStageCoeffMap
(ProC := ProC) (X := X) (H := H) N n i hmod qmap a =
zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N n i hmod qmap
(zcCompletedGroupAlgebraProjection ProC.finiteQuotientClass H i a)The coefficient-change map is evaluated coordinatewise: the support in the finite quotient is unchanged and every coefficient is carried through the given ring homomorphism.
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. 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem zcCompletedGroupAlgebraFiniteFoxStageCoeffMap_groupLike
(hmod : n ∣ i.1.modulus)
(qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
finiteFoxStageTargetQuotient (X := X) N)
(h : H) :
zcCompletedGroupAlgebraFiniteFoxStageCoeffMap
(ProC := ProC) (X := X) (H := H) N n i hmod qmap
(zcGroupLike ProC.finiteQuotientClass H h) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N)
(qmap (QuotientGroup.mk h))Group-like formula for the completed-to-finite coefficient map.
Show proof
by
rw [zcCompletedGroupAlgebraFiniteFoxStageCoeffMap_apply,
zcCompletedGroupAlgebraProjection_groupLike,
zcCompletedGroupAlgebraStageToFiniteFoxStage_of]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\). 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. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□theorem zcCompletedGroupAlgebraFiniteFoxStageCoeffMap_groupLike_eq_stageRight
(hmod : n ∣ i.1.modulus)
(qmap : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
finiteFoxStageTargetQuotient (X := X) N)
(stageRight : H →* finiteFoxStageTargetQuotient (X := X) N)
(hqmap : ∀ h : H, qmap (QuotientGroup.mk h) = stageRight h)
(h : H) :
zcCompletedGroupAlgebraFiniteFoxStageCoeffMap
(ProC := ProC) (X := X) (H := H) N n i hmod qmap
(zcGroupLike ProC.finiteQuotientClass H h) =
MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) N) (stageRight h)Group-like formula rewritten through a named finite right quotient map.
Show proof
by
rw [zcCompletedGroupAlgebraFiniteFoxStageCoeffMap_groupLike]
rw [hqmap h]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\). 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem finiteFoxStageTargetGroupAlgebraMap_single_apply
(q : finiteFoxStageTargetQuotient (X := X) N)
(a : ModNCompletedCoeff n) :
finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n
(MonoidAlgebra.single q a) =
MonoidAlgebra.single (finiteFoxStageTargetQuotientMap (X := X) hNM q) aTarget quotient maps send a single group-algebra coefficient to the mapped basis element.
Show proof
by
rw [finiteFoxStageTargetGroupAlgebraMap]
rw [MonoidAlgebra.mapDomainRingHom_apply, MonoidAlgebra.mapDomain_single]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\). 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem finiteFoxStageBifilteredTargetGroupAlgebraMap_single_apply
(q : finiteFoxStageTargetQuotient (X := X) N)
(a : ModNCompletedCoeff m) :
finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
(MonoidAlgebra.single q a) =
MonoidAlgebra.single (finiteFoxStageTargetQuotientMap (X := X) hNM q)
(modNCompletedCoeffMap (n := n) (m := m) hnm a)The bifiltered target transition on a single group-algebra coefficient.
Show proof
by
rw [finiteFoxStageBifilteredTargetGroupAlgebraMap_apply,
finiteFoxStageTargetGroupAlgebraCoeffMap_single_apply,
finiteFoxStageTargetGroupAlgebraMap_single_apply]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\). 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. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□theorem zcCompletedGroupAlgebraStageToFiniteFoxStage_transition
(hmod_i : n ∣ i.1.modulus)
(hmod_j : m ∣ j.1.modulus)
(hcoeff : ∀ a : ModNCompletedCoeff j.1.modulus,
modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod_i
(modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a) =
modNCompletedCoeffMap (n := n) (m := m) hnm
(modNCompletedCoeffMap (n := m) (m := j.1.modulus) hmod_j a))
(qmap_i : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
finiteFoxStageTargetQuotient (X := X) M)
(qmap_j : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2 →*
finiteFoxStageTargetQuotient (X := X) N)
(hqmap : ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2,
qmap_i
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) =
finiteFoxStageTargetQuotientMap (X := X) hNM (qmap_j q))
(x : ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j) :
finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
(zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j x) =
zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
(zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij x)Stage-to-finite maps commute with completed-group-algebra transitions when the coefficient reductions and quotient maps commute.
Show proof
by
letI : Fact (0 < i.1.modulus) := ⟨i.1.positive⟩
letI : Fact (0 < j.1.modulus) := ⟨j.1.positive⟩
refine MonoidAlgebra.induction_on
(p := fun x : ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j =>
finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
(zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j x) =
zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
(zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij x))
x ?_ ?_ ?_
· intro q
calc
finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
(zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j
(MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2) q)) =
finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
(MonoidAlgebra.of (ModNCompletedCoeff m)
(finiteFoxStageTargetQuotient (X := X) N) (qmap_j q)) := by
rw [zcCompletedGroupAlgebraStageToFiniteFoxStage_of]
_ = MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) M)
(finiteFoxStageTargetQuotientMap (X := X) hNM (qmap_j q)) := by
rw [finiteFoxStageBifilteredTargetGroupAlgebraMap_apply,
finiteFoxStageTargetGroupAlgebraCoeffMap_of_quotient,
finiteFoxStageTargetGroupAlgebraMap_of_quotient]
_ = MonoidAlgebra.of (ModNCompletedCoeff n)
(finiteFoxStageTargetQuotient (X := X) M)
(qmap_i
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)) := by
rw [← hqmap q]
_ = zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
(MonoidAlgebra.of (ModNCompletedCoeff i.1.modulus)
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2)
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q)) := by
rw [zcCompletedGroupAlgebraStageToFiniteFoxStage_of]
_ = zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
(zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij
(MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
(CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2) q)) := by
rw [zcCompletedGroupAlgebraTransition_of]
rfl
· intro x y hx hy
rw [map_add, map_add, map_add, hx, hy]
exact (map_add
(zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i)
((zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij) x)
((zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij) y)).symm
· intro a x hx
have hscalar :
finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
(zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j
(algebraMap (ModNCompletedCoeff j.1.modulus)
(ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j) a)) =
zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
(zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij
(algebraMap (ModNCompletedCoeff j.1.modulus)
(ZCCompletedGroupAlgebraStage ProC.finiteQuotientClass H j) a)) := by
change
finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
(zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j
(MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2)
a)) =
zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i
(zcCompletedGroupAlgebraTransition ProC.finiteQuotientClass H hij
(MonoidAlgebra.single
(1 : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2)
a))
rw [zcCompletedGroupAlgebraStageToFiniteFoxStage_single,
finiteFoxStageBifilteredTargetGroupAlgebraMap_single_apply,
zcCompletedGroupAlgebraTransition_single,
zcCompletedGroupAlgebraStageToFiniteFoxStage_single]
rw [← hqmap 1]
rw [hcoeff a]
rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul,
RingHom.map_mul, RingHom.map_mul, hx]
rw [hscalar]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\). 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. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem zcCompletedGroupAlgebraFiniteFoxStageCoeffMap_transition
(hmod_i : n ∣ i.1.modulus)
(hmod_j : m ∣ j.1.modulus)
(hcoeff : ∀ a : ModNCompletedCoeff j.1.modulus,
modNCompletedCoeffMap (n := n) (m := i.1.modulus) hmod_i
(modNCompletedCoeffMap (n := i.1.modulus) (m := j.1.modulus) hij.1 a) =
modNCompletedCoeffMap (n := n) (m := m) hnm
(modNCompletedCoeffMap (n := m) (m := j.1.modulus) hmod_j a))
(qmap_i : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass i.2 →*
finiteFoxStageTargetQuotient (X := X) M)
(qmap_j : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2 →*
finiteFoxStageTargetQuotient (X := X) N)
(hqmap : ∀ q : CompletedGroupAlgebraQuotientInClass H ProC.finiteQuotientClass j.2,
qmap_i
((OpenNormalSubgroupInClass.map
(C := ProC.finiteQuotientClass) (G := H)
(U := OrderDual.ofDual i.2) (V := OrderDual.ofDual j.2) hij.2) q) =
finiteFoxStageTargetQuotientMap (X := X) hNM (qmap_j q))
(a : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H) :
finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
(zcCompletedGroupAlgebraFiniteFoxStageCoeffMap
(ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j a) =
zcCompletedGroupAlgebraFiniteFoxStageCoeffMap
(ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i aThe completed coefficient maps built from stage projections are compatible on completed points once the underlying finite-stage maps commute with transitions.
Show proof
by
rw [zcCompletedGroupAlgebraFiniteFoxStageCoeffMap_apply,
zcCompletedGroupAlgebraFiniteFoxStageCoeffMap_apply]
change finiteFoxStageBifilteredTargetGroupAlgebraMap (X := X) hNM hnm
(zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) N m j hmod_j qmap_j (a.1 j)) =
zcCompletedGroupAlgebraStageToFiniteFoxStage
(ProC := ProC) (X := X) (H := H) M n i hmod_i qmap_i (a.1 i)
rw [← a.2 i j hij]
exact zcCompletedGroupAlgebraStageToFiniteFoxStage_transition
(ProC := ProC) (X := X) (H := H) hNM hnm hij hmod_i hmod_j hcoeff
qmap_i qmap_j hqmap
(a.1 j)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\). 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. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□