CrowellExactSequence/Profinite/ContinuousMagnus/Injectivity.lean
1import CrowellExactSequence.Profinite.ContinuousMagnus.KernelClosedCommutator
2import CrowellExactSequence.Profinite.KernelInjectivity
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/CrowellExactSequence/Profinite/ContinuousMagnus/Injectivity.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Profinite Crowell exact sequence
15Crowell-specific material is kept separate from general Fox calculus: relation modules, kernel boundaries, Blanchfield-Lyndon maps, and discrete/profinite exactness statements are assembled here.
16-/
17namespace CrowellExactSequence
19noncomputable section
21open ProCGroups.ProC
23universe u
25variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
26variable {ProC : ProCGroupPredicate.{u}}
28variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass]
30omit [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass] in
31/-- Continuous Magnus injectivity for the displayed boundary
32`d_N : N^ab(C) -> A_psi(C)`.
34This is the paper step obtained by combining the completed Fox-vector kernel theorem with the
35general kernel criterion for the genuine topological kernel abelianization. -/
37 [T2Space H]
38 [ProC.HasFiniteQuotientFormation] [ProC.HasFiniteQuotientFinite]
39 [ProC.HasFiniteQuotientHereditary] [ProC.HasFiniteQuotientMelnikovFormation]
40 [ProC.DeterminedByFiniteQuotients]
41 (sourceData : FreeProCSourceData ProC)
42 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
43 (psi : ContinuousMonoidHom sourceData.carrier H) (hpsi : Function.Surjective psi)
44 (htarget :
45 ProC
46 (G :=
48 (ProC := ProC)
49 (fun i : ULift.{u} (Fin r) =>
51 (ProC := ProC) sourceData hbasis i)) : Subgroup
53 ProC.finiteQuotientClass (ULift.{u} (Fin r)) H))))
54 (hwell_dN :
56 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi) :
57 Function.Injective
59 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi hwell_dN) :=
61 (G := sourceData.carrier) (H := H) ProC.finiteQuotientClass psi hwell_dN
63 (H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget
65 (H := H) (ProC := ProC) sourceData hbasis psi hpsi htarget))
68end
70end CrowellExactSequence