FoxDifferential/Completed/Residue/Core.lean
1import FoxDifferential.Common.CrossedDifferentialModule
2import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Residue/Core.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
25/-- The residue group ring `(Z/nZ)[H]`. -/
26abbrev ResidueGroupRing (n : ℕ) (H : Type*) : Type _ :=
29section Basic
31variable {G : Type u} {H : Type v} [Group G] [Group H]
33/-- The coefficient homomorphism `G -> (Z/nZ)[H]` induced by a group homomorphism
34`ψ : G ->* H`. -/
35def residueGroupRingScalar (n : ℕ) (ψ : G →* H) : G →* ResidueGroupRing n H :=
36 (MonoidAlgebra.of (ModNCompletedCoeff n) H).comp ψ
38/-- The residue coefficient homomorphism is `g ↦ [ψ g]`. -/
39@[simp]
40theorem residueGroupRingScalar_apply (n : ℕ) (ψ : G →* H) (g : G) :
41 residueGroupRingScalar n ψ g =
42 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ g) : ResidueGroupRing n H) :=
43 rfl
45/-- The residue universal differential module attached to `ψ : G ->* H`. -/
46abbrev ResidueDifferentialModule (n : ℕ) (ψ : G →* H) : Type _ :=
49/-- The universal residue crossed differential. -/
50def residueUniversalDifferential (n : ℕ) (ψ : G →* H) (g : G) :
51 ResidueDifferentialModule n ψ :=
54/-- The universal residue differential is a crossed differential. -/
55theorem residueUniversalDifferential_isCrossedDifferential (n : ℕ) (ψ : G →* H) :
57 (residueGroupRingScalar n ψ) (residueUniversalDifferential n ψ) := by
60/-- The residue Fox boundary `g ↦ [ψ g] - 1`. -/
61def residueGroupRingBoundary (n : ℕ) (ψ : G →* H) (g : G) : ResidueGroupRing n H :=
62 MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ g) - 1
64/-- The residue Fox boundary vanishes at the identity. -/
65@[simp]
66theorem residueGroupRingBoundary_one (n : ℕ) (ψ : G →* H) :
67 residueGroupRingBoundary n ψ (1 : G) = 0 := by
68 simp only [residueGroupRingBoundary, map_one, MonoidAlgebra.one_def, sub_self]
70/-- The residue Fox boundary is a crossed differential. -/
71theorem residueGroupRingBoundary_isCrossedDifferential (n : ℕ) (ψ : G →* H) :
73 (residueGroupRingScalar n ψ) (residueGroupRingBoundary n ψ) := by
74 intro g h
75 simp only [residueGroupRingBoundary, map_mul, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single,
76 mul_one, sub_eq_add_neg, add_comm, residueGroupRingScalar_apply, smul_eq_mul, mul_add, mul_neg, add_assoc,
77 add_neg_cancel_comm_assoc]
79section UniversalProperty
81variable (n : ℕ)
82variable {A : Type*} [AddCommGroup A] [Module (ResidueGroupRing n H) A]
84/-- The universal linear map induced by a residue crossed differential. -/
86 (ψ : G →* H) (delta : G → A)
87 (hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta) :
88 ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A :=
89 crossedDifferentialModuleLift (A := A) (residueGroupRingScalar n ψ) delta hdelta
91/-- The residue universal lift evaluates on the universal differential as the original crossed
92differential. -/
93@[simp]
95 (ψ : G →* H) (delta : G → A)
96 (hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta) (g : G) :
97 residueDifferentialModuleLift (A := A) n ψ delta hdelta
98 (residueUniversalDifferential n ψ g) =
99 delta g := by
101 (A := A) (residueGroupRingScalar n ψ) delta hdelta g
103/-- Linear maps out of the residue universal module are equal when they agree on universal
104residue differentials. -/
105@[ext]
107 (ψ : G →* H)
108 {f h : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A}
109 (hfh : ∀ g, f (residueUniversalDifferential n ψ g) =
110 h (residueUniversalDifferential n ψ g)) :
111 f = h := by
112 exact crossedDifferentialModuleHom_ext (A := A) (residueGroupRingScalar n ψ) hfh
114/-- Existence and uniqueness of the linear map representing a residue crossed differential. -/
116 (ψ : G →* H) (delta : G → A)
117 (hdelta : IsCrossedDifferential (residueGroupRingScalar n ψ) delta) :
118 ∃! f : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A,
119 ∀ g, f (residueUniversalDifferential n ψ g) = delta g := by
121 (A := A) (residueGroupRingScalar n ψ) delta hdelta
123/-- Universal representation theorem for residue crossed differentials. -/
124def residueCrossedDifferentialEquivLinearMap (ψ : G →* H) :
125 {delta : G → A // IsCrossedDifferential (residueGroupRingScalar n ψ) delta} ≃
126 (ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A) :=
127 crossedDifferentialModuleEquivLinearMap (A := A) (residueGroupRingScalar n ψ)
129/-- The universal residue Fox boundary map from the residue differential module to the residue
130group ring. -/
131def residueToGroupRing (ψ : G →* H) :
132 ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] ResidueGroupRing n H :=
133 residueDifferentialModuleLift (A := ResidueGroupRing n H) n ψ
134 (residueGroupRingBoundary n ψ)
137/-- The universal residue Fox boundary sends `d g` to `[ψ g] - 1`. -/
138@[simp]
139theorem residueToGroupRing_universal (ψ : G →* H) (g : G) :
140 residueToGroupRing n ψ (residueUniversalDifferential n ψ g) =
141 residueGroupRingBoundary n ψ g := by
143 (A := ResidueGroupRing n H) n ψ
144 (residueGroupRingBoundary n ψ)
147/-- Existence and uniqueness of the universal residue Fox boundary map. -/
148theorem existsUnique_residueToGroupRing (ψ : G →* H) :
149 ∃! f : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] ResidueGroupRing n H,
150 ∀ g, f (residueUniversalDifferential n ψ g) =
151 residueGroupRingBoundary n ψ g := by
153 (A := ResidueGroupRing n H) n ψ
154 (residueGroupRingBoundary n ψ)
157end UniversalProperty
159end Basic
161end
163end FoxDifferential