Source: ProCGroups.CrowellExactSequence.Profinite.ContinuousMagnus.Injectivity
1import ProCGroups.FoxDifferential.Completed.Continuous.Magnus.KernelClosedCommutator
2import ProCGroups.CrowellExactSequence.Profinite.KernelInjectivity
4/-!
5# Crowell Exact Sequence / Profinite / Continuous Magnus / Injectivity
7This module proves injectivity of the completed Magnus map on the
8abelianized presentation kernel, using the closed-commutator kernel
9calculation and the general kernel-injectivity criterion.
10-/
12namespace CrowellExactSequence
14noncomputable section
16open ProCGroups.ProC
18universe u
20variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
21variable {C : ProCGroups.FiniteGroupClass.{u}}
26/--
27Continuous Magnus injectivity for the displayed boundary \(d_N\): \(N^{\mathrm{ab}}(C)\)
28\(\to\) \(A_{\psi}(C)\). This step is obtained by combining the completed Fox-vector kernel
29theorem with the general kernel criterion for the topological kernel abelianization.
30-/
31theorem freeProC_profKerAbBoundaryAddZC_inj_of_continuousMagnus
32 [CompactSpace H]
33 [T2Space H]
34 [TotallyDisconnectedSpace H]
36 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
37 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
38 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
39 (htarget :
40 HasOpenNormalBasisInClass C
42 (C := C)
43 (fun i : ULift.{u} (Fin r) =>
44 psi (freeProCChosenULiftFamilyOfBasisCard
45 (C := C) sourceData hbasis i)) : Subgroup
47 C (ULift.{u} (Fin r)) H)))
48 (hwell_dN :
49 CompletedBoundaryKillsTopologicalCommutatorProCInteger
50 (G := sourceData.carrier) (H := H) C psi) :
51 Function.Injective
52 (profiniteKernelAbelianizationBoundaryAddProCInteger
53 (G := sourceData.carrier) (H := H) C psi hwell_dN) :=
54 profKerAbBoundaryAddZC_inj_of_kernel_le_closedCommutator
55 (G := sourceData.carrier) (H := H) C psi hwell_dN
56 (freeProC_zcUnivDiff_kernel_le_closedCommutator_of_closedGenFoxVector
57 (H := H) (C := C) hC.melnikovFormation.formation
58 sourceData hbasis psi hpsi htarget
59 (freeProC_closedGeneratedFoxVector_kernel_le_closedCommutator
60 (H := H) (C := C) hC sourceData hbasis psi hpsi htarget))
63end
65end CrowellExactSequence