Source: ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Boundary
1import ProCGroups.FoxDifferential.Common.FoxBoundary
2import ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Basic
4/-!
5# Fox differential: completed — residue — free group — boundary
7The principal declarations in this module are:
9- `residueFreeGroupFoxBoundary`
10 The residue Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\).
11- `residueFreeGroupFoxBoundary_apply`
12 The residue free-group Fox boundary is evaluated on the canonical generators and then extended
13 linearly to the residue coordinate module.
14- `residueFreeGroupFoxBoundary_single`
15 The residue Fox boundary sends a coordinate basis vector to the corresponding augmentation
16 generator.
17-/
19namespace FoxDifferential
21noncomputable section
23open scoped BigOperators
25universe u v
28variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
30section FiniteBasis
32variable [Fintype X]
34/-- The residue Fox boundary/Euler map \(v \mapsto \sum_i v_i * ([\psi(x_i)]-1)\). -/
35def residueFreeGroupFoxBoundary (n : ℕ) (ψ : FreeGroup X →* H) :
36 ResidueFreeFoxCoordinates n H X →ₗ[ResidueGroupRing n H] ResidueGroupRing n H where
37 toFun v :=
38 ∑ i : X,
39 v i *
40 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1)
41 map_add' := by
42 intro v w
43 simp only [Pi.add_apply, MonoidAlgebra.of_apply, add_mul, Finset.sum_add_distrib]
44 map_smul' := by
45 intro r v
46 simp only [Pi.smul_apply, smul_eq_mul, MonoidAlgebra.of_apply, mul_assoc, RingHom.id_apply,
47 Finset.mul_sum]
49omit [DecidableEq X] in
50/--
51The residue free-group Fox boundary is evaluated on the canonical generators and then extended
52linearly to the residue coordinate module.
53-/
54theorem residueFreeGroupFoxBoundary_apply
55 (n : ℕ) (ψ : FreeGroup X →* H) (v : ResidueFreeFoxCoordinates n H X) :
56 residueFreeGroupFoxBoundary n ψ v =
57 ∑ i : X,
58 v i *
59 (MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ (FreeGroup.of i)) - 1) :=
60 rfl
62/--
63The residue Fox boundary sends a coordinate basis vector to the corresponding augmentation
64generator.
65-/
66@[simp]
67theorem residueFreeGroupFoxBoundary_single (n : ℕ) (ψ : FreeGroup X →* H) (i : X) :
68 residueFreeGroupFoxBoundary n ψ
69 (Pi.single i (1 : ResidueGroupRing n H)) =
70 residueGroupRingBoundary n ψ (FreeGroup.of i) := by
71 rw [residueFreeGroupFoxBoundary_apply]
72 rw [Finset.sum_eq_single i]
73 · simp only [Pi.single_eq_same, MonoidAlgebra.of_apply, one_mul, residueGroupRingBoundary]
74 rfl
75 · intro j _ hji
76 simp only [Pi.single_eq_of_ne hji, MonoidAlgebra.of_apply, zero_mul]
77 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, MonoidAlgebra.of_apply,
78 one_mul,
79 IsEmpty.forall_iff]
81end FiniteBasis
84end
86end FoxDifferential