FoxDifferential/Completed/FiniteStage/RelationAction.lean
1import FoxDifferential.Completed.FiniteStage.RelationModule
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FiniteStage/RelationAction.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
15This file records the Fox-calculus calculation that the relation boundary is equivariant with
16respect to conjugation and the `Z/nZ[F/N]` basis action. This is the algebraic input needed to
17upgrade relation-word derivatives from an additive subgroup to the module image used in the
19-/
21namespace FoxDifferential
23noncomputable section
25open ProCGroups.InverseSystems
26open ProCGroups.ProC
28universe u
30variable {X : Type u} [DecidableEq X]
31variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
33/-- Conjugating a finite-stage relation by an arbitrary source-quotient element gives another
36 (s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
37 (q : finiteFoxStageRelationGroup (X := X) N n) :
38 finiteFoxStageRelationGroup (X := X) N n :=
39 ⟨s * q.1 * s⁻¹, by
41 (F := FreeGroup X) N n (s * q.1 * s⁻¹) = 1
43 simp only [mul_one, mul_inv_cancel]⟩
45omit [DecidableEq X] in
46@[simp]
48 (s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
49 (q : finiteFoxStageRelationGroup (X := X) N n) :
50 (finiteFoxStageRelationConjBySource (X := X) N n s q).1 = s * q.1 * s⁻¹ :=
51 rfl
53/-- Relation-boundary equivariance for conjugation by a source-quotient element. -/
55 (s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)
56 (q : finiteFoxStageRelationGroup (X := X) N n) :
57 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n
58 (Additive.ofMul (finiteFoxStageRelationConjBySource (X := X) N n s q)) =
59 finiteFoxStageQuotientCoefficient (X := X) N n s •
60 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q) := by
64 have hconj :=
65 IsCrossedDifferential.conj
66 (finiteFoxStageQuotientDerivativeVector_isCrossedDifferential (X := X) N n)
67 s q.1
68 have hcoeff :
69 finiteFoxStageQuotientCoefficient (X := X) N n (s * q.1 * s⁻¹) = 1 := by
70 have htarget :
72 (F := FreeGroup X) N n (s * q.1 * s⁻¹) = 1 := by
74 simp only [mul_one, mul_inv_cancel]
75 rw [finiteFoxStageQuotientCoefficient_apply, htarget]
76 rfl
77 calc
78 finiteFoxStageQuotientDerivativeVector (X := X) N n (s * q.1 * s⁻¹) =
79 finiteFoxStageQuotientDerivativeVector (X := X) N n s +
80 finiteFoxStageQuotientCoefficient (X := X) N n s •
81 finiteFoxStageQuotientDerivativeVector (X := X) N n q.1 -
82 finiteFoxStageQuotientCoefficient (X := X) N n (s * q.1 * s⁻¹) •
83 finiteFoxStageQuotientDerivativeVector (X := X) N n s := hconj
84 _ = finiteFoxStageQuotientCoefficient (X := X) N n s •
85 finiteFoxStageQuotientDerivativeVector (X := X) N n q.1 := by
86 rw [hcoeff, one_smul]
87 abel
89/-- A chosen source-quotient lift of an element of `F/N`. -/
91 (h : finiteFoxStageTargetQuotient (X := X) N) :
92 FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n :=
93 Classical.choose
95 (F := FreeGroup X) N n h)
97omit [DecidableEq X] in
98@[simp]
100 (h : finiteFoxStageTargetQuotient (X := X) N) :
101 finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n
102 (finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) = h :=
103 Classical.choose_spec
105 (F := FreeGroup X) N n h)
107omit [DecidableEq X] in
108/-- The coefficient of a chosen source lift is the corresponding group-ring basis element. -/
109@[simp]
111 (h : finiteFoxStageTargetQuotient (X := X) N) :
112 finiteFoxStageQuotientCoefficient (X := X) N n
113 (finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) =
114 MonoidAlgebra.of (ModNCompletedCoeff n)
115 (finiteFoxStageTargetQuotient (X := X) N) h := by
119/-- Basis-element equivariance of the relation boundary over `Z/nZ[F/N]`. -/
121 (h : finiteFoxStageTargetQuotient (X := X) N)
122 (q : finiteFoxStageRelationGroup (X := X) N n) :
123 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n
124 (Additive.ofMul
125 (finiteFoxStageRelationConjBySource (X := X) N n
126 (finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) q)) =
127 (MonoidAlgebra.of (ModNCompletedCoeff n)
128 (finiteFoxStageTargetQuotient (X := X) N) h) •
129 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q) := by
133/-- The relation-boundary image is stable under multiplication by target group basis elements. -/
135 (h : finiteFoxStageTargetQuotient (X := X) N)
136 {v : finiteFoxStageCoordinateVector (X := X) N n}
137 (hv : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n) :
138 (MonoidAlgebra.of (ModNCompletedCoeff n)
139 (finiteFoxStageTargetQuotient (X := X) N) h) • v ∈
140 finiteFoxStageRelationBoundaryRange (X := X) N n := by
141 rw [mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n] at hv
142 rcases hv with ⟨q, hq⟩
143 let qmul : finiteFoxStageRelationGroup (X := X) N n := Additive.toMul q
144 rw [mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n]
145 refine ⟨Additive.ofMul
146 (finiteFoxStageRelationConjBySource (X := X) N n
147 (finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) qmul), ?_⟩
148 calc
149 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n
150 (Additive.ofMul
151 (finiteFoxStageRelationConjBySource (X := X) N n
152 (finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) qmul)) =
153 (MonoidAlgebra.of (ModNCompletedCoeff n)
154 (finiteFoxStageTargetQuotient (X := X) N) h) •
155 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n
156 (Additive.ofMul qmul) := by
157 exact finiteFoxStageRelationBoundary_of_basis_smul (X := X) N n h qmul
158 _ = (MonoidAlgebra.of (ModNCompletedCoeff n)
159 (finiteFoxStageTargetQuotient (X := X) N) h) • v := by
160 have hqmul :
161 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n
162 (Additive.ofMul qmul) = v := by
163 simpa [qmul] using hq
164 rw [hqmul]
166end
168end FoxDifferential