FoxDifferential/Completed/Residue/FreeGroup/Basic.lean
1import FoxDifferential.Common.FreeCrossedDifferential
2import FoxDifferential.Completed.Residue.Core
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Residue/FreeGroup/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Residue coefficient stages
15Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
16-/
17namespace FoxDifferential
19noncomputable section
21open scoped BigOperators
23universe u v
26variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
28/-- Residue Fox-coordinate vectors with coefficients in `(Z/nZ)[H]`. -/
29abbrev ResidueFreeFoxCoordinates (n : ℕ) (H : Type v) (X : Type u) : Type (max u v) :=
30 X → ResidueGroupRing n H
32/-- Residue free-group Fox derivative vector, with coefficients pushed forward along
33`ψ : FreeGroup X ->* H`. -/
34def residueFreeGroupFoxDerivativeVector (n : ℕ) (ψ : FreeGroup X →* H)
35 (w : FreeGroup X) :
36 ResidueFreeFoxCoordinates n H X :=
38 (A := ResidueFreeFoxCoordinates n H X)
39 (residueGroupRingScalar n ψ)
40 (fun x => Pi.single x (1 : ResidueGroupRing n H))
41 w
43/-- A coordinate of the residue free-group Fox derivative. -/
44def residueFreeGroupFoxDerivative (n : ℕ) (ψ : FreeGroup X →* H) (i : X)
45 (w : FreeGroup X) : ResidueGroupRing n H :=
48/-- The residue free-group derivative vector sends the identity word to zero. -/
49@[simp]
50theorem residueFreeGroupFoxDerivativeVector_one (n : ℕ) (ψ : FreeGroup X →* H) :
51 residueFreeGroupFoxDerivativeVector n ψ (1 : FreeGroup X) = 0 := by
54/-- Component form of the identity rule for the residue free-group derivative. -/
55@[simp]
56theorem residueFreeGroupFoxDerivative_one (n : ℕ) (ψ : FreeGroup X →* H) (i : X) :
57 residueFreeGroupFoxDerivative n ψ i (1 : FreeGroup X) = 0 := by
58 simp only [residueFreeGroupFoxDerivative, residueFreeGroupFoxDerivativeVector_one, Pi.zero_apply]
60/-- The residue free-group derivative vector sends a free generator to the corresponding
61coordinate basis vector. -/
62@[simp]
63theorem residueFreeGroupFoxDerivativeVector_of (n : ℕ) (ψ : FreeGroup X →* H) (x : X) :
64 residueFreeGroupFoxDerivativeVector n ψ (FreeGroup.of x) =
65 Pi.single x (1 : ResidueGroupRing n H) := by
68/-- Component form of the residue generator value. -/
69@[simp]
70theorem residueFreeGroupFoxDerivative_of (n : ℕ) (ψ : FreeGroup X →* H) (i x : X) :
71 residueFreeGroupFoxDerivative n ψ i (FreeGroup.of x) =
72 (Pi.single x (1 : ResidueGroupRing n H) :
73 ResidueFreeFoxCoordinates n H X) i := by
76/-- The residue free-group derivative vector is a crossed differential. -/
78 (n : ℕ) (ψ : FreeGroup X →* H) :
80 (residueGroupRingScalar n ψ) (residueFreeGroupFoxDerivativeVector n ψ) := by
82 (A := ResidueFreeFoxCoordinates n H X)
83 (residueGroupRingScalar n ψ)
84 (fun x => Pi.single x (1 : ResidueGroupRing n H))
86/-- Uniqueness of the residue free-group derivative vector among crossed differentials with
87standard coordinate values on free generators. -/
89 (n : ℕ) (ψ : FreeGroup X →* H)
90 (delta : FreeGroup X → ResidueFreeFoxCoordinates n H X)
91 (hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta)
92 (hbasis :
93 ∀ x : X, delta (FreeGroup.of x) =
94 Pi.single x (1 : ResidueGroupRing n H)) :
95 delta = residueFreeGroupFoxDerivativeVector n ψ := by
97 (A := ResidueFreeFoxCoordinates n H X)
98 (residueGroupRingScalar n ψ)
99 (fun x => Pi.single x (1 : ResidueGroupRing n H))
100 delta hdelta hbasis
102/-- Existence and uniqueness theorem for the residue free-group derivative vector. -/
104 (n : ℕ) (ψ : FreeGroup X →* H) :
105 ∃! delta : FreeGroup X → ResidueFreeFoxCoordinates n H X,
106 IsCrossedDifferential (residueGroupRingScalar n ψ) delta ∧
107 ∀ x : X, delta (FreeGroup.of x) =
108 Pi.single x (1 : ResidueGroupRing n H) := by
110 (A := ResidueFreeFoxCoordinates n H X)
111 (residueGroupRingScalar n ψ)
112 (fun x => Pi.single x (1 : ResidueGroupRing n H))
115end
117end FoxDifferential