FoxDifferential/Completed/FiniteStage/TargetMap.lean
1import FoxDifferential.Completed.FiniteStage.CoeffMap.BoundaryCycles
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FiniteStage/TargetMap.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
18-/
20namespace FoxDifferential
22noncomputable section
24open scoped BigOperators
25open ProCGroups.InverseSystems
26open ProCGroups.ProC
28universe u
30variable {X : Type u} [DecidableEq X]
31variable {N M : Subgroup (FreeGroup X)} [N.Normal] [M.Normal]
32variable (hNM : N ≤ M) (n : ℕ)
34omit [DecidableEq X] in
35@[simp]
37 (y : FiniteFoxStageSemidirect (X := X) N n) :
38 (finiteFoxStageSemidirectMap (X := X) hNM n y).left =
39 fun i : X => finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n (y.left i) :=
40 rfl
42omit [DecidableEq X] in
43@[simp]
45 (y : FiniteFoxStageSemidirect (X := X) N n) :
46 (finiteFoxStageSemidirectMap (X := X) hNM n y).right =
47 finiteFoxStageTargetQuotientMap (X := X) hNM y.right :=
48 rfl
50 omit [DecidableEq X] in
51/-- Target-quotient refinement commutes with the finite-stage Fox boundary. -/
53 [Fintype X]
54 (v : finiteFoxStageCoordinateVector (X := X) N n) :
55 finiteFoxStageFoxBoundary (X := X) M n
56 (fun i : X => finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n (v i)) =
57 finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n
58 (finiteFoxStageFoxBoundary (X := X) N n v) := by
59 rw [finiteFoxStageFoxBoundary_apply, finiteFoxStageFoxBoundary_apply, map_sum]
60 apply Finset.sum_congr rfl
61 intro i _
62 rw [map_mul, map_sub, finiteFoxStageTargetGroupAlgebraMap_of, map_one]
64omit [DecidableEq X] in
65/-- Target-quotient refinement sends finite boundary cycles to finite boundary cycles. -/
67 [Fintype X]
68 {v : finiteFoxStageCoordinateVector (X := X) N n}
69 (hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n) :
70 (fun i : X => finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n (v i)) ∈
71 finiteFoxStageBoundaryCycleSubmodule (X := X) M n := by
73 rw [finiteFoxStageFoxBoundary_targetMap (X := X) hNM n v]
74 rw [mem_finiteFoxStageBoundaryCycleSubmodule] at hv
75 rw [hv]
78omit [DecidableEq X] in
79/-- Target-quotient refinement sends semidirect boundary-cycle points to boundary-cycle points. -/
81 [Fintype X]
82 {y : FiniteFoxStageSemidirect (X := X) N n}
83 (hy : y ∈ finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n) :
84 finiteFoxStageSemidirectMap (X := X) hNM n y ∈
85 finiteFoxStageSemidirectBoundaryCycleSet (X := X) M n := by
86 rcases hy with ⟨hyright, hyboundary⟩
87 constructor
89 rw [hyright]
90 exact map_one (finiteFoxStageTargetQuotientMap (X := X) hNM)
92 exact finiteFoxStageBoundaryCycleSubmodule_targetMap_mem (X := X) hNM n hyboundary
94/-- Target-quotient refinement sends finite kernel-word points to finite kernel-word points. -/
96 (w : FreeGroup X) :
97 finiteFoxStageSemidirectMap (X := X) hNM n
98 (finiteFoxStageSemidirectKernelWordPoint (X := X) N n w) =
99 finiteFoxStageSemidirectKernelWordPoint (X := X) M n w := by
100 apply FiniteFoxStageSemidirect.ext
101 · funext i
102 change finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n
103 (finiteFoxStageDerivative (X := X) N n i w) =
104 finiteFoxStageDerivative (X := X) M n i w
105 exact finiteFoxStageDerivative_natural (X := X) hNM n i w
107 simp only [finiteFoxStageSemidirectKernelWordPoint, map_one]
109/-- Target-quotient refinement sends finite source-kernel semidirect points to source-kernel
110semidirect points. -/
112 (q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
113 finiteFoxStageSemidirectMap (X := X) hNM n
114 (finiteFoxStageSemidirectSourceKernelPoint (X := X) N n q) =
115 finiteFoxStageSemidirectSourceKernelPoint (X := X) M n
116 (finiteFoxStageSourceQuotientMap (X := X) hNM n q) := by
117 rcases QuotientGroup.mk'_surjective
118 (finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q with ⟨w, rfl⟩
119 apply FiniteFoxStageSemidirect.ext
120 · funext i
121 change finiteFoxStageTargetGroupAlgebraMap (X := X) hNM n
122 (finiteFoxStageQuotientDerivativeVector (X := X) N n
123 (QuotientGroup.mk'
124 (finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) w) i) =
125 finiteFoxStageQuotientDerivativeVector (X := X) M n
126 (QuotientGroup.mk'
127 (finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) M n) w) i
129 exact finiteFoxStageDerivative_natural (X := X) hNM n i w
130 · simp only [finiteFoxStageSemidirectSourceKernelPoint, QuotientGroup.mk'_apply,
133/-- Target refinement sends the finite semidirect kernel-word derivative set into the refined one. -/
135 (fun y : FiniteFoxStageSemidirect (X := X) N n =>
136 finiteFoxStageSemidirectMap (X := X) hNM n y) ''
137 finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) N n ⊆
138 finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) M n := by
139 intro y hy
140 rcases hy with ⟨z, hz, rfl⟩
141 rcases hz with ⟨w, hwN, hzw⟩
142 refine ⟨w, hNM hwN, ?_⟩
143 rw [← hzw]
144 exact (finiteFoxStageSemidirectMap_kernelWordPoint (X := X) hNM n w).symm
146/-- Target refinement sends source-kernel derivative points into source-kernel derivative points. -/
148 (fun y : FiniteFoxStageSemidirect (X := X) N n =>
149 finiteFoxStageSemidirectMap (X := X) hNM n y) ''
150 finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n ⊆
151 finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) M n := by
154 exact finiteFoxStageSemidirectMap_kernelWordDerivativeSet_subset (X := X) hNM n
156end
158end FoxDifferential