Source: ProCGroups.FoxDifferential.Discrete.DifferentialModule.Boundary
1import ProCGroups.FoxDifferential.Discrete.DifferentialModule.Universal
3/-!
4# Fox differential: discrete — differential module — boundary
6The principal declarations in this module are:
8- `groupRingBoundary`
9 The standard map \(G \to \mathbb{Z}[H]\), \(g \mapsto \psi(g)-1\) is viewed as a differential map.
10- `groupRingBoundaryHom`
11 The Fox boundary is itself a crossed differential.
12- `groupRingBoundary_one`
13 The Fox boundary vanishes at the identity.
14- `groupRingBoundary_eq_zero_of_mem_ker`
15 The Fox boundary is zero on elements in the kernel of \(\psi\).
16-/
18namespace FoxDifferential
20noncomputable section
22variable {H G : Type*} [Group H] [Group G]
24/--
25The standard map \(G \to \mathbb{Z}[H]\), \(g \mapsto \psi(g)-1\) is viewed as a differential
26map.
27-/
28def groupRingBoundary (ψ : G →* H) (g : G) : GroupRing H :=
29 MonoidAlgebra.of ℤ H (ψ g) - 1
31/-- The Fox boundary vanishes at the identity. -/
32@[simp]
33theorem groupRingBoundary_one (ψ : G →* H) :
34 groupRingBoundary ψ (1 : G) = 0 := by
35 simp only [groupRingBoundary, map_one, groupRing_of_one (H := H), sub_self]
37/-- The Fox boundary is zero on elements in the kernel of \(\psi\). -/
38@[simp]
39theorem groupRingBoundary_eq_zero_of_mem_ker (ψ : G →* H) {g : G} (hg : ψ g = 1) :
40 groupRingBoundary ψ g = 0 := by
41 rw [groupRingBoundary, hg, groupRing_of_one (H := H)]
42 simp only [sub_self]
44/-- The Fox boundary vanishes on the kernel subgroup of \(\psi\). -/
45@[simp]
46theorem groupRingBoundary_subtype_ker (ψ : G →* H) (g : ψ.ker) :
47 groupRingBoundary ψ g = 0 :=
48 groupRingBoundary_eq_zero_of_mem_ker (ψ := ψ) g.2
50/-- The Fox boundary is itself a crossed differential. -/
51def groupRingBoundaryHom (ψ : G →* H) : DifferentialHom ψ (GroupRing H) where
52 toFun := groupRingBoundary ψ
53 map_mul' := by
54 intro g₁ g₂
55 simp only [scalarCrossedAction_apply, groupRingBoundary, map_mul,
56 MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one, sub_eq_add_neg,
57 add_comm, groupRingScalar_apply, smul_eq_mul, mul_add, mul_neg, add_assoc,
58 add_neg_cancel_comm_assoc]
60/-- The bundled group-ring boundary homomorphism evaluates to the usual Fox boundary. -/
61@[simp]
62theorem groupRingBoundaryHom_apply (ψ : G →* H) (g : G) :
63 groupRingBoundaryHom ψ g = groupRingBoundary ψ g :=
64 rfl
66/-- Group-ring functoriality carries Fox boundaries to Fox boundaries. -/
67@[simp]
68theorem groupRingMap_groupRingBoundary {K : Type*} [Group K]
69 (φ : H →* K) (ψ : G →* H) (g : G) :
70 groupRingMap φ (groupRingBoundary ψ g) = groupRingBoundary (φ.comp ψ) g := by
71 simp only [groupRingBoundary, MonoidAlgebra.of_apply, map_sub, groupRingMap_single, map_one,
72 MonoidHom.coe_comp, Function.comp_apply]
74/--
75The universal boundary map \(A_{\psi}\ \to \mathbb{Z}[H]\), \(universalDifferential(g) \mapsto
76\psi(g) - 1\).
77-/
78def toGroupRing (ψ : G →* H) : DifferentialModule ψ →ₗ[GroupRing H] GroupRing H :=
79 differentialModuleLift (A := GroupRing H) ψ (groupRingBoundaryHom ψ)
81/-- The universal boundary sends universalDifferential g to \([\psi(g)] - 1\). -/
82theorem toGroupRing_d (ψ : G →* H) (g : G) :
83 toGroupRing ψ (universalDifferential ψ g) = groupRingBoundary ψ g := by
84 simpa only [toGroupRing, groupRingBoundaryHom_apply] using
85 differentialModuleLift_d (A := GroupRing H) ψ (groupRingBoundaryHom ψ) g
88/-- The standard group-ring generator \(h-1\) appearing in Fox boundary formulas. -/
89def augmentationGenerator (H : Type*) [Group H] (h : H) : GroupRing H :=
90 MonoidAlgebra.of Int H h - 1
92/-- The standard augmentation generator at the identity is zero. -/
93@[simp]
94theorem augmentationGenerator_one (H : Type*) [Group H] :
95 augmentationGenerator H (1 : H) = 0 := by
96 simp only [augmentationGenerator, groupRing_of_one (H := H), sub_self]
98/-- The augmentation generator is the identity-coefficient Fox boundary. -/
99@[simp]
100theorem augmentationGenerator_eq_groupRingBoundary (H : Type*) [Group H] (h : H) :
101 augmentationGenerator H h = groupRingBoundary (MonoidHom.id H) h :=
102 rfl
104/-- Group-ring functoriality carries augmentation generators to augmentation generators. -/
105@[simp]
106theorem groupRingMap_augmentationGenerator {K : Type*} [Group K]
107 (φ : H →* K) (h : H) :
108 groupRingMap φ (augmentationGenerator H h) = augmentationGenerator K (φ h) := by
109 simp only [augmentationGenerator, MonoidAlgebra.of_apply, map_sub, groupRingMap_single, map_one]
112end
114end FoxDifferential