FoxDifferential/Completed/Residue/FreeGroup/Boundary.lean
1import FoxDifferential.Common.FoxBoundary
2import FoxDifferential.Completed.Residue.FreeGroup.Basic
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Residue/FreeGroup/Boundary.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]
28section FiniteBasis
30variable [Fintype X]
32/-- The residue Fox boundary/Euler map
33`v ↦ ∑ i, v_i * ([ψ x_i] - 1)`. -/
34def residueFreeGroupFoxBoundary (n : ℕ) (ψ : FreeGroup X →* H) :
35 ResidueFreeFoxCoordinates n H X →ₗ[ResidueGroupRing n H] ResidueGroupRing n H where
36 toFun v :=
37 ∑ i : X,
38 v i *
39 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)
40 map_add' := by
41 intro v w
42 simp only [Pi.add_apply, MonoidAlgebra.of_apply, add_mul, Finset.sum_add_distrib]
43 map_smul' := by
44 intro r v
45 simp only [Pi.smul_apply, smul_eq_mul, MonoidAlgebra.of_apply, mul_assoc, RingHom.id_apply, Finset.mul_sum]
47omit [DecidableEq X] in
48/-- Evaluation formula for the residue Fox boundary/Euler map. -/
50 (n : ℕ) (ψ : FreeGroup X →* H) (v : ResidueFreeFoxCoordinates n H X) :
51 residueFreeGroupFoxBoundary n ψ v =
52 ∑ i : X,
53 v i *
54 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1) :=
55 rfl
57/-- The residue Fox boundary sends a coordinate basis vector to the corresponding augmentation
58generator. -/
59@[simp]
60theorem residueFreeGroupFoxBoundary_single (n : ℕ) (ψ : FreeGroup X →* H) (i : X) :
62 (Pi.single i (1 : ResidueGroupRing n H)) =
63 residueGroupRingBoundary n ψ (FreeGroup.of i) := by
65 rw [Finset.sum_eq_single i]
66 · simp only [Pi.single_eq_same, MonoidAlgebra.of_apply, one_mul, residueGroupRingBoundary]
67 · intro j _ hji
68 simp only [Pi.single_eq_of_ne hji, MonoidAlgebra.of_apply, zero_mul]
69 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, MonoidAlgebra.of_apply, one_mul,
70 IsEmpty.forall_iff]
72end FiniteBasis
75end
77end FoxDifferential