CrowellExactSequence.Profinite.FiniteRank
This module develops the Crowell--Blanchfield--Lyndon exact sequence and its completed coordinate forms.
import
noncomputable def finiteRank_freeProCSourceData
{sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
(hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate
(ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
(Fin r) F X) :
FreeProCSourceData (ProCGroups.ProC.proSigmaProC.{u} sigma) where
basis := ULift.{u} (Fin r)
carrier := F
instGroup := inferInstance
instTopologicalSpace := inferInstance
instIsTopologicalGroup := inferInstance
inclusion := fun i => X i.down
isFree := by
simpa [ProCGroups.ProC.proSigmaProC] using
hFree.precompEquiv (Equiv.ulift : ULift.{u} (Fin r) ≃ Fin r)
proCGroup := by
refine
{ isProC := by
simpa [ProCGroups.ProC.proSigmaProC] using hFree.isProC
isProCGroup := ?_ }
exact hFree.isProC.mono (D :=
(ProCGroups.ProC.proSigmaProC.{u} sigma).finiteQuotientClass) (by
intro Q _ hQ
letI : Finite Q := ProCGroups.FiniteGroupClass.finite hQ
exact (ProCGroups.ProC.proSigmaProC_finiteQuotientClass_iff
(sigma := sigma) (Q := Q)).2 hQ)Package a finite-rank free pro-\(\Sigma\) group as CES free-source data.
theorem finiteRank_freeProCSourceData_basis_card
{sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
(hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate
(ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
(Fin r) F X) :
Cardinal.mk (finiteRank_freeProCSourceData (F := F) X hFree).basis = rThe finite-rank CES source data has the expected basis cardinality.
Show proof
by
simp only [finiteRank_freeProCSourceData, Cardinal.mk_fintype, Fintype.card_ulift,
Fintype.card_fin]Proof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. The augmentation module terms are generated by the chosen basis elements, so equality on those generators determines each coordinate map. The finite-stage exactness assertions are stable under the comparison isomorphisms used to move between separated and unseparated coordinates. Consequently the completed sequence inherits the same exactness calculation. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. 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.
□noncomputable def finiteRank_topologicalAbelianization_sepCoordinateMap
{sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
(hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate
(ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
(Fin r) F X) :=
freeProCChosenULift_sepCoordinateMap
(H := TopologicalAbelianization F)
(ProC := ProCGroups.ProC.proSigmaProC.{u} sigma)
(finiteRank_freeProCSourceData (F := F) X hFree)
(finiteRank_freeProCSourceData_basis_card (F := F) X hFree)
(TopologicalAbelianization.mkₜ F)
(by
change Function.Surjective (TopologicalAbelianization.mk F)
exact TopologicalAbelianization.surjective_mk F)The separated coordinate map for the topological abelianization of a finite-rank free pro-\(\Sigma\) group.
theorem mem_topDerivedTop_two_of_finiteRank_topologicalAbelianization_sepCoordinateMap_eq_zero
{sigma : Set ℕ} {r : ℕ} (X : Fin r → F)
(hFree : ProCGroups.FreeProC.IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate
(ProCGroups.FiniteGroupClass.sigmaGroup.{u} sigma))
(Fin r) F X)
{a : F}
(haψ : TopologicalAbelianization.mkₜ F a = 1)
(hzero :
finiteRank_topologicalAbelianization_sepCoordinateMap (F := F) X hFree
(FoxDifferential.zcSeparatedUniversalDifferential
(ProCGroups.ProC.proSigmaProC.{u} sigma).finiteQuotientClass
(TopologicalAbelianization.mkₜ F).toMonoidHom a) = 0) :
a ∈ topDerivedTop F 2If the separated abelianized CES coordinate vector of a kernel element vanishes, the element lies in the second closed derived subgroup.
Show proof
by
let sourceData := finiteRank_freeProCSourceData (F := F) (sigma := sigma) X hFree
let hbasis := finiteRank_freeProCSourceData_basis_card (F := F) X hFree
let ProC := ProCGroups.ProC.proSigmaProC.{u} sigma
let ψ : F →ₜ* TopologicalAbelianization F := TopologicalAbelianization.mkₜ F
have hψsurj : Function.Surjective ψ := by
change Function.Surjective (TopologicalAbelianization.mk F)
exact TopologicalAbelianization.surjective_mk F
let htarget :=
freeProCClosedGeneratedTarget_proC_of_surjective
(H := TopologicalAbelianization F) (ProC := ProC) sourceData hbasis ψ hψsurj
have hDzero :
freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger
(H := TopologicalAbelianization F) (ProC := ProC) sourceData hbasis ψ htarget a = 0 := by
have happly := hzero
dsimp [finiteRank_topologicalAbelianization_sepCoordinateMap, sourceData, hbasis, ProC, ψ] at happly
change
freeProCChosenULift_sepCoordinateMap
(H := TopologicalAbelianization F) (ProC := ProC) sourceData hbasis ψ hψsurj
(FoxDifferential.zcSeparatedUniversalDifferential ProC.finiteQuotientClass
ψ.toMonoidHom a) = 0 at happly
rw [freeProCChosenULift_sepCoordinateMap_universal] at happly
simpa [finiteRank_topologicalAbelianization_sepCoordinateMap, sourceData, hbasis, ProC, ψ,
freeProCCompletedFoxDerivativeVectorViaClosedGeneratedProCInteger, htarget] using happly
have ha_closed :
(⟨a, haψ⟩ : ProCGroups.ProC.ProfiniteKernelSubgroup ψ) ∈
Subgroup.closedCommutator (ProCGroups.ProC.ProfiniteKernelSubgroup ψ) :=
freeProC_closedGeneratedFoxVector_kernel_le_closedCommutator
(H := TopologicalAbelianization F) (ProC := ProC) sourceData hbasis ψ hψsurj htarget
⟨a, haψ⟩ hDzero
exact
(mem_topDerivedTop_two_iff_mem_closedCommutator_topologicalAbelianizationKernel
(G := F) haψ).2 ha_closedProof. Use the Crowell--Blanchfield--Lyndon complex with its augmentation module, Fox differential, and boundary maps. The proof evaluates the relevant boundary, coordinate, or comparison map on the canonical generators and extends the calculation by linearity. The finite-stage Fox fundamental formula identifies the boundary terms with the corresponding augmentation-kernel terms, so the kernel of one map is the image of the preceding map. For separated or completed versions, each map is compared after all finite-stage projections; those projections separate points and commute with the sequence maps. The passage from finite stages to the profinite object uses the inverse-limit topology, so compatibility of all coordinates gives a continuous completed map. Thus the coordinate calculation supplies the displayed injectivity, kernel--image, or surjectivity assertion for the completed Crowell sequence. The comparison maps in the sequence are determined by their values on the free generators and by the module structure. After applying a finite-stage projection, the completed boundary map becomes the ordinary Fox boundary map in a finite group algebra. Since these finite calculations are compatible with all transition maps, the same kernel, image, and coordinate identities hold in the completed sequence. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation. 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.
□