FoxDifferential/Completed/FiniteStage/BoundaryCycleHom.lean
1import FoxDifferential.Completed.FiniteStage.BoundaryCycles
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FiniteStage/BoundaryCycleHom.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite-stage boundary-cycle homomorphism
15kernel of
16`F / ([N,N] N^n) -> F/N`, the descended crossed Fox differential is additive because the
19inclusion.
20-/
22namespace FoxDifferential
24noncomputable section
26open ProCGroups.InverseSystems
27open ProCGroups.ProC
29universe u
31variable {X : Type u} [DecidableEq X]
32variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
34/-- The kernel of the finite source-to-target quotient `F/[N,N]N^n -> F/N`. -/
35abbrev finiteFoxStageSourceKernel : Type u :=
39/-- The descended finite-stage Fox derivative, restricted to the source quotient kernel, is an
40additive homomorphism. -/
42 Additive (finiteFoxStageSourceKernel (X := X) N n) →+
43 finiteFoxStageCoordinateVector (X := X) N n where
44 toFun q :=
45 finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1
46 map_zero' := by
47 change finiteFoxStageQuotientDerivativeVector (X := X) N n
48 (1 : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) = 0
49 simp only [finiteFoxStageQuotientDerivativeVector_one]
50 map_add' := by
51 intro q r
52 change finiteFoxStageQuotientDerivativeVector (X := X) N n
53 ((Additive.toMul q).1 * (Additive.toMul r).1) =
54 finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1 +
55 finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul r).1
57 have hqcoeff :
58 finiteFoxStageQuotientCoefficient (X := X) N n (Additive.toMul q).1 = 1 :=
59 finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n
60 (Additive.toMul q).2
61 rw [hqcoeff]
62 simp only [one_smul]
64@[simp]
66 (q : finiteFoxStageSourceKernel (X := X) N n) :
67 finiteFoxStageSourceKernelDerivativeAddHom (X := X) N n (Additive.ofMul q) =
68 finiteFoxStageQuotientDerivativeVector (X := X) N n q.1 :=
69 rfl
71/-- The range of the additive source-kernel derivative map is exactly the source-kernel derivative
74 AddMonoidHom.range (finiteFoxStageSourceKernelDerivativeAddHom (X := X) N n) =
75 finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n := by
76 ext v
77 constructor
78 · intro hv
79 rcases hv with ⟨q, rfl⟩
80 refine ⟨(Additive.toMul q).1, (Additive.toMul q).2, rfl⟩
81 · intro hv
82 rcases hv with ⟨q, hq, rfl⟩
83 exact ⟨Additive.ofMul
84 (⟨q, hq⟩ : finiteFoxStageSourceKernel (X := X) N n), rfl⟩
86/-- The source-kernel derivative map, with codomain restricted to finite Fox boundary cycles. -/
87def finiteFoxStageSourceKernelDerivativeToBoundaryCycles [Fintype X] :
88 Additive (finiteFoxStageSourceKernel (X := X) N n) →+
89 finiteFoxStageBoundaryCycleSubmodule (X := X) N n where
90 toFun q :=
91 ⟨finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1,
93 ⟨(Additive.toMul q).1, (Additive.toMul q).2, rfl⟩⟩
94 map_zero' := by
95 apply Subtype.ext
96 change finiteFoxStageQuotientDerivativeVector (X := X) N n
97 (1 : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) = 0
98 simp only [finiteFoxStageQuotientDerivativeVector_one]
99 map_add' := by
100 intro q r
101 apply Subtype.ext
102 change finiteFoxStageQuotientDerivativeVector (X := X) N n
103 ((Additive.toMul q).1 * (Additive.toMul r).1) =
104 finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1 +
105 finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul r).1
107 have hqcoeff :
108 finiteFoxStageQuotientCoefficient (X := X) N n (Additive.toMul q).1 = 1 :=
109 finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n
110 (Additive.toMul q).2
111 rw [hqcoeff]
112 simp only [one_smul]
114@[simp]
116 [Fintype X] (q : finiteFoxStageSourceKernel (X := X) N n) :
117 (finiteFoxStageSourceKernelDerivativeToBoundaryCycles (X := X) N n
118 (Additive.ofMul q) : finiteFoxStageCoordinateVector (X := X) N n) =
119 finiteFoxStageQuotientDerivativeVector (X := X) N n q.1 :=
120 rfl
122/-- The finite-stage coverage statement is precisely surjectivity of the source-kernel derivative
123map onto the boundary-cycle subgroup. -/
125 [Fintype X] :
126 finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n ↔
127 Function.Surjective
128 (finiteFoxStageSourceKernelDerivativeToBoundaryCycles (X := X) N n) := by
129 constructor
130 · intro hcover y
131 rcases hcover y.2 with ⟨q, hq, hqy⟩
132 refine ⟨Additive.ofMul
133 (⟨q, hq⟩ : finiteFoxStageSourceKernel (X := X) N n), ?_⟩
134 apply Subtype.ext
135 simpa using hqy
136 · intro hsurj v hv
137 rcases hsurj ⟨v, hv⟩ with ⟨q, hq⟩
138 refine ⟨(Additive.toMul q).1, (Additive.toMul q).2, ?_⟩
139 exact congrArg Subtype.val hq
141/-- If the restricted source-kernel derivative map is surjective, then the source-kernel image is
144 [Fintype X]
145 (hsurj : Function.Surjective
146 (finiteFoxStageSourceKernelDerivativeToBoundaryCycles (X := X) N n)) :
147 finiteFoxStageSourceKernelDerivativeSet (X := X) N n =
148 (finiteFoxStageBoundaryCycleSubmodule (X := X) N n :
149 Set (finiteFoxStageCoordinateVector (X := X) N n)) := by
150 exact
152 (X := X) N n).2
154 (X := X) N n).2 hsurj)
156end
158end FoxDifferential