FoxDifferential.Completed.DifferentialModule.TargetQuotient.StageMap
import
theorem primePowerCompletedGroupAlgebraMapStage_targetQuotient_transition_source
[TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
[DiscreteTopology (FreeGroup X)]
(N : Subgroup (FreeGroup X)) [N.Normal]
[TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
[IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
(hfinite : ∀ a : ℕ,
Finite (FreeGroup X ⧸
finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
(j : PrimePowerCompletedGroupAlgebraIndex
(finiteFoxStageTargetQuotient (X := X) N))
(x : PrimePowerCompletedGroupAlgebraStage ℓ (FreeGroup X)
(j.1, finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1)) :
primePowerCompletedGroupAlgebraMapStage
(ℓ := ℓ) (G := FreeGroup X)
(H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j
(primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := FreeGroup X)
(show
(j.1, completedGroupAlgebraComapIndex
(G := FreeGroup X) (H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j.2) ≤
(j.1, finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1) from
⟨le_rfl,
finiteFoxStagePrimePowerSourceCompletedIndex_le_targetQuotientComap
(ℓ := ℓ) (X := X) N hfinite j⟩) x) =
modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
(finiteFoxStageTargetQuotient (X := X) N) j.2
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N (ℓ ^ j.1) x)Show proof
by
let hidx :
(j.1, completedGroupAlgebraComapIndex
(G := FreeGroup X) (H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j.2) ≤
(j.1, finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1) :=
⟨le_rfl,
finiteFoxStagePrimePowerSourceCompletedIndex_le_targetQuotientComap
(ℓ := ℓ) (X := X) N hfinite j⟩
let leftMap :
PrimePowerCompletedGroupAlgebraStage ℓ (FreeGroup X)
(j.1, finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1) →+*
PrimePowerCompletedGroupAlgebraStage ℓ
(finiteFoxStageTargetQuotient (X := X) N) j :=
(primePowerCompletedGroupAlgebraMapStage
(ℓ := ℓ) (G := FreeGroup X)
(H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j).comp
(primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := FreeGroup X) hidx)
let rightMap :
PrimePowerCompletedGroupAlgebraStage ℓ (FreeGroup X)
(j.1, finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1) →+*
PrimePowerCompletedGroupAlgebraStage ℓ
(finiteFoxStageTargetQuotient (X := X) N) j :=
(modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
(finiteFoxStageTargetQuotient (X := X) N) j.2).comp
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N (ℓ ^ j.1))
change leftMap x = rightMap x
have hmaps : leftMap = rightMap := by
apply MonoidAlgebra.ringHom_ext
· intro r
rcases ZMod.intCast_surjective r with ⟨t, rfl⟩
simp only [primePowerCompletedGroupAlgebraMapStage, MonoidAlgebra.mapDomainRingHom,
primePowerCompletedGroupAlgebraTransition, modNCompletedGroupAlgebraStageCoeffMapInClass_rfl,
modNCompletedGroupAlgebraTransition, RingHomCompTriple.comp_eq, RingHom.coe_comp, RingHom.coe_mk, MonoidHom.coe_mk,
OneHom.coe_mk, Function.comp_apply, Finsupp.mapDomain_single, map_one, modNCompletedGroupAlgebraStageMap,
finiteFoxCommutatorPowerGroupAlgebraMap, leftMap, rightMap]
· intro q
rcases QuotientGroup.mk'_surjective
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1)) q with
⟨w, rfl⟩
change
leftMap
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1))
(FreeGroup X ⧸
finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1))
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1)) w)) =
rightMap
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1))
(FreeGroup X ⧸
finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1))
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1)) w))
dsimp [leftMap, rightMap]
change
primePowerCompletedGroupAlgebraMapStage
(ℓ := ℓ) (G := FreeGroup X)
(H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j
(primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := FreeGroup X)
hidx
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient (FreeGroup X)
(finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1))
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1)) w))) =
modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
(finiteFoxStageTargetQuotient (X := X) N) j.2
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N (ℓ ^ j.1)
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient (FreeGroup X)
(finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1))
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1)) w)))
rw [primePowerCompletedGroupAlgebraTransition_of]
change
primePowerCompletedGroupAlgebraMapStage
(ℓ := ℓ) (G := FreeGroup X)
(H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1))
(_root_.CompletedGroupAlgebra.CompletedGroupAlgebraQuotient (FreeGroup X)
(completedGroupAlgebraComapIndex
(G := FreeGroup X) (H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j.2))
((OpenNormalSubgroupInClass.map
(C := ProCGroups.FiniteGroupClass.allFinite) (G := FreeGroup X)
(U := OrderDual.ofDual
(completedGroupAlgebraComapIndex
(G := FreeGroup X) (H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j.2))
(V := OrderDual.ofDual
(finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1))
(finiteFoxStagePrimePowerSourceCompletedIndex_le_targetQuotientComap
(ℓ := ℓ) (X := X) N hfinite j))
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1)) w))) =
modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
(finiteFoxStageTargetQuotient (X := X) N) j.2
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N (ℓ ^ j.1)
(MonoidAlgebra.of (ModNCompletedCoeff (ℓ ^ j.1))
(FreeGroup X ⧸
finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1))
(QuotientGroup.mk'
(finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ j.1)) w)))
rw [primePowerCompletedGroupAlgebraMapStage_of,
finiteFoxCommutatorPowerGroupAlgebraMap_of,
modNCompletedGroupAlgebraStageMap_of]
rfl
rw [hmaps]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. 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. 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 primePowerCompletedGAProj_map_targetQuotient_eq_freeDerivativeSource
[TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
[DiscreteTopology (FreeGroup X)]
(N : Subgroup (FreeGroup X)) [N.Normal]
[TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
[IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
(hfinite : ∀ a : ℕ,
Finite (FreeGroup X ⧸
finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
(z : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X))
(j : PrimePowerCompletedGroupAlgebraIndex
(finiteFoxStageTargetQuotient (X := X) N)) :
primePowerCompletedGroupAlgebraProjection
(ℓ := ℓ) (G := finiteFoxStageTargetQuotient (X := X) N) j
(primePowerCompletedGroupAlgebraMap
(ℓ := ℓ) (G := FreeGroup X)
(H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) z) =
modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
(finiteFoxStageTargetQuotient (X := X) N) j.2
(finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N (ℓ ^ j.1)
(primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
(j.1, finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1) z))The target finite-stage projection of the completed quotient map can be computed using the completed free derivative source projection at the same prime-power exponent.
Show proof
by
let hidx :
(j.1, completedGroupAlgebraComapIndex
(G := FreeGroup X) (H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j.2) ≤
(j.1, finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1) :=
⟨le_rfl,
finiteFoxStagePrimePowerSourceCompletedIndex_le_targetQuotientComap
(ℓ := ℓ) (X := X) N hfinite j⟩
rw [primePowerCompletedGroupAlgebraProjection_map]
have hz := z.2
(j.1, completedGroupAlgebraComapIndex
(G := FreeGroup X) (H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j.2)
(j.1, finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1) hidx
change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := FreeGroup X) hidx
(primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
(j.1, finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1) z) =
primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
(j.1, completedGroupAlgebraComapIndex
(G := FreeGroup X) (H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) j.2) z at hz
rw [← hz]
exact
primePowerCompletedGroupAlgebraMapStage_targetQuotient_transition_source
(ℓ := ℓ) (X := X) N hfinite j
(primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
(j.1, finiteFoxStagePrimePowerSourceCompletedIndex
(ℓ := ℓ) (X := X) N hfinite j.1) z)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. 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. 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 primePowerCompletedGroupAlgebraMap_targetQuotient_of
[TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
[DiscreteTopology (FreeGroup X)]
(N : Subgroup (FreeGroup X)) [N.Normal]
[TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
[IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
(w : FreeGroup X) :
primePowerCompletedGroupAlgebraMap
(ℓ := ℓ) (G := FreeGroup X)
(H := finiteFoxStageTargetQuotient (X := X) N)
(finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N)
(primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) =
primePowerCompletedGroupAlgebraOf (ell := ℓ)
(H := finiteFoxStageTargetQuotient (X := X) N) (QuotientGroup.mk' N w)Coefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
Show proof
by
rw [primePowerCompletedGroupAlgebraMap_of]
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. 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.
□