Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental
1import ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.StageMap
2import ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.Fundamental
3import ProCGroups.FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.Mul
5/-!
6# Fox differential: completed — differential module — target quotient — fundamental
8The principal declarations in this module are:
10- `ppCompletedGAFoxDerivToTarget_of_fundFormula_map`
11 The completed Fox derivative satisfies the fundamental formula after passage to the target
12 quotient.
13- `ppCompletedGAFoxDerivToTarget_of_mul_product_map`
14 The completed Fox derivative of a product is computed by the crossed product rule after passage to
15 the target quotient.
16-/
18namespace FoxDifferential
20noncomputable section
22open ProCGroups
23open ProCGroups.ProC
25universe u v
27variable (ℓ : ℕ)
28variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
29variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32variable {X : Type u} [DecidableEq X]
34/--
35The completed Fox derivative satisfies the fundamental formula after passage to the target
36quotient.
37-/
38theorem ppCompletedGAFoxDerivToTarget_of_fundFormula_map
39 [Fintype X]
40 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
41 [DiscreteTopology (FreeGroup X)]
42 (N : Subgroup (FreeGroup X)) [N.Normal]
43 [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
44 [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
45 (hfinite : ∀ a : ℕ,
46 Finite (FreeGroup X ⧸
47 foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
48 (w : FreeGroup X) :
49 primePowerCompletedGroupAlgebraMap
50 (ℓ := ℓ) (G := FreeGroup X)
51 (H := foxAlgebraicStageTargetQuotient (X := X) N)
52 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
53 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) - 1 =
54 ∑ i : X,
55 primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
56 (ℓ := ℓ) (X := X) N hfinite i
57 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) *
58 (primePowerCompletedGroupAlgebraMap
59 (ℓ := ℓ) (G := FreeGroup X)
60 (H := foxAlgebraicStageTargetQuotient (X := X) N)
61 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
62 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X)
63 (FreeGroup.of i)) - 1) := by
64 rw [primePowerCompletedGroupAlgebraMap_targetQuotient_of]
65 simp_rw [primePowerCompletedGroupAlgebraMap_targetQuotient_of]
66 exact ppCompletedGAFoxDerivToTarget_of_fundFormula
67 (ℓ := ℓ) (X := X) N hfinite w
69/--
70The completed Fox derivative of a product is computed by the crossed product rule after passage
71to the target quotient.
72-/
73theorem ppCompletedGAFoxDerivToTarget_of_mul_product_map
74 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
75 [DiscreteTopology (FreeGroup X)]
76 (N : Subgroup (FreeGroup X)) [N.Normal]
77 [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
78 [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
79 (hfinite : ∀ a : ℕ,
80 Finite (FreeGroup X ⧸
81 foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
82 (i : X) (u v : FreeGroup X) :
83 primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
84 (ℓ := ℓ) (X := X) N hfinite i
85 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u *
86 primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v) =
87 primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
88 (ℓ := ℓ) (X := X) N hfinite i
89 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u) +
90 primePowerCompletedGroupAlgebraMap
91 (ℓ := ℓ) (G := FreeGroup X)
92 (H := foxAlgebraicStageTargetQuotient (X := X) N)
93 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N)
94 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u) *
95 primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
96 (ℓ := ℓ) (X := X) N hfinite i
97 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v) := by
98 rw [primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_of_mul_product,
99 primePowerCompletedGroupAlgebraMap_targetQuotient_of]
102end
104end FoxDifferential