Source: ProCGroups.FoxDifferential.Completed.Residue.Core
1import ProCGroups.FoxDifferential.Common.CrossedDifferentialModule
2import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap
4/-!
5# Fox differential: completed — residue — core
7The principal declarations in this module are:
9- `ResidueGroupRing`
10 The residue group ring \((\mathbb{Z}/n\mathbb{Z})[H]\).
11- `residueGroupRingScalar`
12 The coefficient homomorphism \(G \to (\mathbb{Z}/n\mathbb{Z})[H]\) induced by a group homomorphism
13 \(\psi: G \to H\).
14- `residueGroupRingScalar_apply`
15 The residue coefficient homomorphism sends a group element to the residue group-ring basis element
16 of its image.
17- `residueGroupRingBoundary_one`
18 The residue Fox boundary vanishes at the identity.
19-/
21namespace FoxDifferential
23noncomputable section
25open scoped BigOperators
27universe u v
29/-- The residue group ring \((\mathbb{Z}/n\mathbb{Z})[H]\). -/
30abbrev ResidueGroupRing (n : ℕ) (H : Type*) : Type _ :=
31 ModNCompletedGroupRing n H
33section Basic
35variable {G : Type u} {H : Type v} [Group G] [Group H]
37/--
38The coefficient homomorphism \(G \to (\mathbb{Z}/n\mathbb{Z})[H]\) induced by a group
39homomorphism \(\psi: G \to H\).
40-/
41def residueGroupRingScalar (n : ℕ) (ψ : G →* H) : G →* ResidueGroupRing n H :=
42 (MonoidAlgebra.of (ModNCompletedCoeff n) H).comp ψ
44/--
45The residue coefficient homomorphism sends a group element to the residue group-ring basis
46element of its image.
47-/
48@[simp]
49theorem residueGroupRingScalar_apply (n : ℕ) (ψ : G →* H) (g : G) :
50 residueGroupRingScalar n ψ g =
51 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ g) : ResidueGroupRing n H) :=
52 rfl
54/-- The residue universal differential module attached to \(\psi : G \to H\). -/
55abbrev ResidueDifferentialModule (n : ℕ) (ψ : G →* H) : Type _ :=
56 CrossedDifferentialModule (residueGroupRingScalar n ψ)
58/-- The universal residue crossed homomorphism. -/
59def residueUniversalDifferential (n : ℕ) (ψ : G →* H) :
60 ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueDifferentialModule n ψ) :=
61 universalCrossedHom (residueGroupRingScalar n ψ)
63/-- The residue Fox boundary \(g \mapsto [\psi(g)] - 1\), bundled as a crossed homomorphism. -/
64def residueGroupRingBoundary (n : ℕ) (ψ : G →* H) :
65 ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueGroupRing n H) where
66 toFun g := MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ g) - 1
67 map_mul' := by
68 intro g h
69 simp only [scalarCrossedAction_apply, map_mul, MonoidAlgebra.of_apply,
70 MonoidAlgebra.single_mul_single, mul_one, sub_eq_add_neg, add_comm,
71 residueGroupRingScalar_apply, smul_eq_mul, mul_add, mul_neg, add_assoc,
72 add_neg_cancel_comm_assoc]
74/-- The residue Fox boundary vanishes at the identity. -/
75@[simp]
76theorem residueGroupRingBoundary_one (n : ℕ) (ψ : G →* H) :
77 residueGroupRingBoundary n ψ (1 : G) = 0 := by
78 exact ScalarCrossedHom.map_one (residueGroupRingBoundary n ψ)
80section UniversalProperty
82variable (n : ℕ)
83variable {A : Type*} [AddCommGroup A] [Module (ResidueGroupRing n H) A]
85/-- The universal linear map induced by a residue crossed differential. -/
86def residueDifferentialModuleLift
87 (ψ : G →* H)
88 (delta : ScalarCrossedHom (residueGroupRingScalar n ψ) A) :
89 ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A :=
90 crossedHomModuleLift (A := A) (residueGroupRingScalar n ψ) delta
92/--
93The residue universal lift evaluates on the universal differential as the original crossed
94differential.
95-/
96@[simp]
97theorem residueDifferentialModuleLift_universal
98 (ψ : G →* H) (delta : ScalarCrossedHom (residueGroupRingScalar n ψ) A)
99 (g : G) :
100 residueDifferentialModuleLift (A := A) n ψ delta
101 (residueUniversalDifferential n ψ g) =
102 delta g := by
103 exact crossedHomModuleLift_universal
104 (A := A) (residueGroupRingScalar n ψ) delta g
106/--
107Linear maps out of the residue universal module are equal when they agree on universal residue
108differentials.
109-/
110@[ext]
111theorem residueDifferentialModuleHom_ext
112 (ψ : G →* H)
113 {f h : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A}
114 (hfh : ∀ g, f (residueUniversalDifferential n ψ g) =
115 h (residueUniversalDifferential n ψ g)) :
116 f = h := by
117 exact crossedDifferentialModuleHom_ext (A := A) (residueGroupRingScalar n ψ) hfh
119/-- Existence and uniqueness of the linear map representing a residue crossed differential. -/
120theorem existsUnique_residueDifferentialModuleLift
121 (ψ : G →* H) (delta : ScalarCrossedHom (residueGroupRingScalar n ψ) A) :
122 ∃! f : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A,
123 ∀ g, f (residueUniversalDifferential n ψ g) = delta g := by
124 exact existsUnique_crossedHomModuleLift
125 (A := A) (residueGroupRingScalar n ψ) delta
127/-- Residue crossed homomorphisms are represented by the corresponding universal residue module. -/
128def residueCrossedHomEquivLinearMap (ψ : G →* H) :
129 ScalarCrossedHom (residueGroupRingScalar n ψ) A ≃
130 (ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A) :=
131 crossedHomModuleEquivLinearMap (A := A) (residueGroupRingScalar n ψ)
133/--
134The universal residue Fox boundary map from the residue differential module to the residue group
135ring.
136-/
137def residueToGroupRing (ψ : G →* H) :
138 ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] ResidueGroupRing n H :=
139 residueDifferentialModuleLift (A := ResidueGroupRing n H) n ψ
140 (residueGroupRingBoundary n ψ)
142/-- The universal residue Fox boundary sends \(d g\) to \([\psi(g)] - 1\). -/
143@[simp]
144theorem residueToGroupRing_universal (ψ : G →* H) (g : G) :
145 residueToGroupRing n ψ (residueUniversalDifferential n ψ g) =
146 residueGroupRingBoundary n ψ g := by
147 exact residueDifferentialModuleLift_universal
148 (A := ResidueGroupRing n H) n ψ
149 (residueGroupRingBoundary n ψ) g
151/-- Existence and uniqueness of the universal residue Fox boundary map. -/
152theorem existsUnique_residueToGroupRing (ψ : G →* H) :
153 ∃! f : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] ResidueGroupRing n H,
154 ∀ g, f (residueUniversalDifferential n ψ g) =
155 residueGroupRingBoundary n ψ g := by
156 exact existsUnique_residueDifferentialModuleLift
157 (A := ResidueGroupRing n H) n ψ
158 (residueGroupRingBoundary n ψ)
160end UniversalProperty
162end Basic
164end
166end FoxDifferential