FoxDifferential/Completed/Residue/FreeGroup/Universal.lean
1import FoxDifferential.Completed.Residue.FreeGroup.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Residue/FreeGroup/Universal.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Residue coefficient stages
14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
15-/
16namespace FoxDifferential
18noncomputable section
20open scoped BigOperators
22universe u v
25variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
27/-- Universal representation theorem for residue crossed differentials on a free group. -/
29 (n : ℕ) (ψ : FreeGroup X →* H) :
30 {delta : FreeGroup X → ResidueFreeFoxCoordinates n H X //
31 IsCrossedDifferential (residueGroupRingScalar n ψ) delta} ≃
32 (ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
33 ResidueFreeFoxCoordinates n H X) :=
35 (A := ResidueFreeFoxCoordinates n H X) n ψ
37/-- The linear map from the residue universal module representing the residue derivative
38vector. -/
40 (n : ℕ) (ψ : FreeGroup X →* H) :
41 ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
42 ResidueFreeFoxCoordinates n H X :=
44 (A := ResidueFreeFoxCoordinates n H X) n ψ
48/-- The representing linear map evaluates on the universal differential as the residue
49derivative vector. -/
50@[simp]
52 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
54 (residueUniversalDifferential n ψ w) =
55 residueFreeGroupFoxDerivativeVector n ψ w := by
57 (A := ResidueFreeFoxCoordinates n H X) n ψ
61/-- Existence and uniqueness of the linear map representing the residue derivative vector. -/
63 (n : ℕ) (ψ : FreeGroup X →* H) :
64 ∃! f :
65 ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
66 ResidueFreeFoxCoordinates n H X,
67 ∀ w : FreeGroup X,
68 f (residueUniversalDifferential n ψ w) =
69 residueFreeGroupFoxDerivativeVector n ψ w := by
71 (A := ResidueFreeFoxCoordinates n H X) n ψ
75end
77end FoxDifferential