FoxDifferential/Completed/DifferentialModule/TargetQuotient/MulProjection.lean
1import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/DifferentialModule/TargetQuotient/MulProjection.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed differential modules
14The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
15-/
16namespace FoxDifferential
18noncomputable section
20open ProCGroups
21open ProCGroups.ProC
23universe u v
25variable (ℓ : ℕ)
26variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
27variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30variable {X : Type u} [DecidableEq X]
32/-- 素冪係数で定めた 標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
34 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
35 [DiscreteTopology (FreeGroup X)]
36 (N : Subgroup (FreeGroup X)) [N.Normal]
37 [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
38 [IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
39 (hfinite : ∀ a : ℕ,
40 Finite (FreeGroup X ⧸
41 finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
42 (i : X) (x y : PrimePowerCompletedGroupAlgebra ℓ (FreeGroup X))
44 (finiteFoxStageTargetQuotient (X := X) N)) :
46 (ℓ := ℓ) (G := finiteFoxStageTargetQuotient (X := X) N) j
48 (ℓ := ℓ) (X := X) N hfinite i (x * y)) =
49 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := FreeGroup X)
51 (ℓ := ℓ) (X := X) N hfinite j.1)
53 (ℓ := ℓ) (G := FreeGroup X) y) •
55 (ℓ := ℓ) (G := finiteFoxStageTargetQuotient (X := X) N) j
57 (ℓ := ℓ) (X := X) N hfinite i x) +
59 (ℓ := ℓ) (G := finiteFoxStageTargetQuotient (X := X) N) j
61 (ℓ := ℓ) (G := FreeGroup X)
62 (H := finiteFoxStageTargetQuotient (X := X) N)
63 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) x) *
65 (ℓ := ℓ) (G := finiteFoxStageTargetQuotient (X := X) N) j
67 (ℓ := ℓ) (X := X) N hfinite i y) := by
70 change
71 modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
72 (finiteFoxStageTargetQuotient (X := X) N) j.2
73 (finiteFoxStageGroupAlgebraDerivative (X := X) N (ℓ ^ j.1) i
74 ((primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
76 (ℓ := ℓ) (X := X) N hfinite j.1) x) *
77 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
79 (ℓ := ℓ) (X := X) N hfinite j.1) y))) =
80 _
83 rw [show
84 modNCompletedGroupAlgebraStageMap (ℓ ^ j.1)
85 (finiteFoxStageTargetQuotient (X := X) N) j.2
87 (F := FreeGroup X) N (ℓ ^ j.1)
88 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := FreeGroup X)
90 (ℓ := ℓ) (X := X) N hfinite j.1) x)) =
92 (ℓ := ℓ) (G := finiteFoxStageTargetQuotient (X := X) N) j
94 (ℓ := ℓ) (G := FreeGroup X)
95 (H := finiteFoxStageTargetQuotient (X := X) N)
96 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N) x) by
101 (ℓ := ℓ) (X := X) N hfinite y j.1]
102 rw [Algebra.smul_def, map_mul, modNCompletedGroupAlgebraStageMap_algebraMap,
103 ← Algebra.smul_def]
106end
108end FoxDifferential