Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.MulProjection
1import ProCGroups.FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental
3/-!
4# Fox differential: completed — differential module — target quotient — mul projection
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_mul_projection`
9 The finite-stage projection of the prime-power completed target derivative satisfies the Fox
10 product rule.
11-/
13namespace FoxDifferential
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
20universe u v
22variable (ℓ : ℕ)
23variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
24variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
27variable {X : Type u} [DecidableEq X]
29/--
30The finite-stage projection of the prime-power completed target derivative satisfies the Fox
31product rule.
32-/
33theorem primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_mul_projection
34 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
35 [DiscreteTopology (FreeGroup X)]
36 (N : Subgroup (FreeGroup X)) [N.Normal]
37 [TopologicalSpace (foxAlgebraicStageTargetQuotient (X := X) N)]
38 [IsTopologicalGroup (foxAlgebraicStageTargetQuotient (X := X) N)]
39 (hfinite : ∀ a : ℕ,
40 Finite (FreeGroup X ⧸
41 foxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
42 (i : X) (x y : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X))
43 (j : PrimePowerCompletedGroupAlgebraIndex
44 (foxAlgebraicStageTargetQuotient (X := X) N)) :
45 primePowerCompletedGroupAlgebraProjection
46 (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
47 (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
48 (ℓ := ℓ) (X := X) N hfinite i (x * y)) =
49 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := FreeGroup X)
50 (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex
51 (ℓ := ℓ) (X := X) N hfinite j.1)
52 (primePowerCompletedGroupAlgebraAugmentation
53 (ℓ := ℓ) (G := FreeGroup X) y) •
54 primePowerCompletedGroupAlgebraProjection
55 (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
56 (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
57 (ℓ := ℓ) (X := X) N hfinite i x) +
58 primePowerCompletedGroupAlgebraProjection
59 (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
60 (primePowerCompletedGroupAlgebraMap
61 (ℓ := ℓ) (G := FreeGroup X)
62 (H := foxAlgebraicStageTargetQuotient (X := X) N)
63 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N) x) *
64 primePowerCompletedGroupAlgebraProjection
65 (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
66 (primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget
67 (ℓ := ℓ) (X := X) N hfinite i y) := by
68 rw [primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_projection,
69 primePowerCompletedGroupAlgebraProjection_mul]
70 change
71 modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
72 (foxAlgebraicStageTargetQuotient (X := X) N) j.2
73 (foxAlgebraicStageGroupAlgebraDerivative (X := X) N (ℓ ^ j.1) i
74 ((show foxAlgebraicStageSourceGroupAlgebra (X := X) N (ℓ ^ j.1) from
75 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
76 (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex
77 (ℓ := ℓ) (X := X) N hfinite j.1) x) *
78 (show foxAlgebraicStageSourceGroupAlgebra (X := X) N (ℓ ^ j.1) from
79 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
80 (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex
81 (ℓ := ℓ) (X := X) N hfinite j.1) y))) =
82 _
83 rw [foxAlgebraicStageGroupAlgebraDerivative_mul]
84 rw [map_add, map_mul]
85 rw [show
86 modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
87 (foxAlgebraicStageTargetQuotient (X := X) N) j.2
88 (foxCommutatorPowerGroupAlgebraMap
89 (F := FreeGroup X) N (ℓ ^ j.1)
90 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
91 (j.1, foxAlgebraicStagePrimePowerSourceCompletedIndex
92 (ℓ := ℓ) (X := X) N hfinite j.1) x)) =
93 primePowerCompletedGroupAlgebraProjection
94 (ℓ := ℓ) (G := foxAlgebraicStageTargetQuotient (X := X) N) j
95 (primePowerCompletedGroupAlgebraMap
96 (ℓ := ℓ) (G := FreeGroup X)
97 (H := foxAlgebraicStageTargetQuotient (X := X) N)
98 (foxAlgebraicStageTargetQuotientContinuousMonoidHom (X := X) N) x) by
99 rw [primePowerCompletedGAProj_map_targetQuotient_eq_freeDerivativeSource]]
100 rw [primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_projection,
101 primePowerCompletedGroupAlgebraFreeFoxDerivativeToCompletedTarget_projection]
102 rw [foxCommutatorPowerSourceGroupAlgebraAugmentation_projection_eq_completed
103 (ℓ := ℓ) (X := X) N hfinite y j.1]
104 rw [Algebra.smul_def, map_mul, modNCompletedGroupAlgebraStageMap_algebraMap,
105 ← Algebra.smul_def]
108end
110end FoxDifferential