FoxDifferential/Discrete/DifferentialModule/Boundary.lean
1import FoxDifferential.Discrete.DifferentialModule.Universal
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/DifferentialModule/Boundary.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Discrete group-ring Fox calculus
14The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
15-/
16namespace FoxDifferential
18noncomputable section
20variable {H G : Type*} [Group H] [Group G]
22/-- The standard map `G → ℤ[H]`, `g ↦ ψ(g) - 1`, viewed as a differential map. -/
23def groupRingBoundary (ψ : G →* H) (g : G) : GroupRing H :=
24 MonoidAlgebra.of ℤ H (ψ g) - 1
26/-- The Fox boundary vanishes at the identity. -/
27@[simp]
28theorem groupRingBoundary_one (ψ : G →* H) :
29 groupRingBoundary ψ (1 : G) = 0 := by
30 simp only [groupRingBoundary, map_one, groupRing_of_one (H := H), sub_self]
32/-- The Fox boundary is zero on elements in the kernel of `ψ`. -/
33@[simp]
34theorem groupRingBoundary_eq_zero_of_mem_ker (ψ : G →* H) {g : G} (hg : ψ g = 1) :
35 groupRingBoundary ψ g = 0 := by
36 rw [groupRingBoundary, hg, groupRing_of_one (H := H)]
37 simp only [sub_self]
39/-- The Fox boundary vanishes on the kernel subgroup of `ψ`. -/
40@[simp]
41theorem groupRingBoundary_subtype_ker (ψ : G →* H) (g : ψ.ker) :
42 groupRingBoundary ψ g = 0 :=
43 groupRingBoundary_eq_zero_of_mem_ker (ψ := ψ) g.2
45/-- The Fox boundary is itself a crossed differential. -/
46theorem groupRingBoundary_isDifferential (ψ : G →* H) :
47 IsDifferentialMap (A := GroupRing H) ψ (groupRingBoundary ψ) := by
48 intro g₁ g₂
49 simp only [groupRingBoundary, map_mul, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one,
50 sub_eq_add_neg, add_comm, groupRingScalar_apply, smul_eq_mul, mul_add, mul_neg, add_assoc,
51 add_neg_cancel_comm_assoc]
53/-- Group-ring functoriality carries Fox boundaries to Fox boundaries. -/
54@[simp]
55theorem groupRingMap_groupRingBoundary {K : Type*} [Group K]
56 (φ : H →* K) (ψ : G →* H) (g : G) :
57 groupRingMap φ (groupRingBoundary ψ g) = groupRingBoundary (φ.comp ψ) g := by
58 simp only [groupRingBoundary, MonoidAlgebra.of_apply, map_sub, groupRingMap_single, map_one,
59 MonoidHom.coe_comp, Function.comp_apply]
61/-- The universal boundary map `A_ψ → ℤ[H]`, `universalDifferential(g) ↦ ψ(g) - 1`. -/
62def toGroupRing (ψ : G →* H) : DifferentialModule ψ →ₗ[GroupRing H] GroupRing H :=
63 lift (A := GroupRing H) ψ (groupRingBoundary ψ) (groupRingBoundary_isDifferential ψ)
65/-- The universal boundary sends `universalDifferential g` to `[ψ g] - 1`. -/
66theorem toGroupRing_d (ψ : G →* H) (g : G) :
67 toGroupRing ψ (universalDifferential ψ g) = groupRingBoundary ψ g := by
68 simpa [toGroupRing] using
69 lift_d (A := GroupRing H) ψ (groupRingBoundary ψ) (groupRingBoundary_isDifferential ψ) g
72/-- The standard group-ring generator `h - 1` appearing in Fox boundary formulas. -/
73def augmentationGenerator (H : Type*) [Group H] (h : H) : GroupRing H :=
74 MonoidAlgebra.of Int H h - 1
76/-- The standard augmentation generator at the identity is zero. -/
77@[simp]
78theorem augmentationGenerator_one (H : Type*) [Group H] :
79 augmentationGenerator H (1 : H) = 0 := by
80 simp only [augmentationGenerator, groupRing_of_one (H := H), sub_self]
82/-- The augmentation generator is the identity-coefficient Fox boundary. -/
83@[simp]
84theorem augmentationGenerator_eq_groupRingBoundary (H : Type*) [Group H] (h : H) :
85 augmentationGenerator H h = groupRingBoundary (MonoidHom.id H) h :=
86 rfl
88/-- Group-ring functoriality carries augmentation generators to augmentation generators. -/
89@[simp]
90theorem groupRingMap_augmentationGenerator {K : Type*} [Group K]
91 (φ : H →* K) (h : H) :
92 groupRingMap φ (augmentationGenerator H h) = augmentationGenerator K (φ h) := by
93 simp only [augmentationGenerator, MonoidAlgebra.of_apply, map_sub, groupRingMap_single, map_one]
96end
98end FoxDifferential