FoxDifferential/Completed/DifferentialModule/TargetQuotient/Fundamental.lean
1import FoxDifferential.Completed.DifferentialModule.TargetQuotient.StageMap
2import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.Fundamental
3import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.Mul
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Completed/DifferentialModule/TargetQuotient/Fundamental.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Completed differential modules
16The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
17-/
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/-- 素冪係数で定めた 群元から得られる group-like 元の写像が関手的写像が有限段階射影と両立することを述べる。 -/
36 [Fintype X]
37 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
38 [DiscreteTopology (FreeGroup X)]
39 (N : Subgroup (FreeGroup X)) [N.Normal]
40 [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
41 [IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
42 (hfinite : ∀ a : ℕ,
43 Finite (FreeGroup X ⧸
44 finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
45 (w : FreeGroup X) :
47 (ℓ := ℓ) (G := FreeGroup X)
48 (H := finiteFoxStageTargetQuotient (X := X) N)
49 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N)
50 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) - 1 =
51 ∑ i : X,
53 (ℓ := ℓ) (X := X) N hfinite i
54 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) w) *
56 (ℓ := ℓ) (G := FreeGroup X)
57 (H := finiteFoxStageTargetQuotient (X := X) N)
58 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N)
59 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X)
60 (FreeGroup.of i)) - 1) := by
64 (ℓ := ℓ) (X := X) N hfinite w
66/-- 素冪係数で定めた 群元から得られる group-like 元の写像が関手的写像が有限段階射影と両立することを述べる。 -/
68 [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
69 [DiscreteTopology (FreeGroup X)]
70 (N : Subgroup (FreeGroup X)) [N.Normal]
71 [TopologicalSpace (finiteFoxStageTargetQuotient (X := X) N)]
72 [IsTopologicalGroup (finiteFoxStageTargetQuotient (X := X) N)]
73 (hfinite : ∀ a : ℕ,
74 Finite (FreeGroup X ⧸
75 finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N (ℓ ^ a)))
76 (i : X) (u v : FreeGroup X) :
78 (ℓ := ℓ) (X := X) N hfinite i
79 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u *
80 primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v) =
82 (ℓ := ℓ) (X := X) N hfinite i
83 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u) +
85 (ℓ := ℓ) (G := FreeGroup X)
86 (H := finiteFoxStageTargetQuotient (X := X) N)
87 (finiteFoxStageTargetQuotientContinuousMonoidHom (X := X) N)
88 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) u) *
90 (ℓ := ℓ) (X := X) N hfinite i
91 (primePowerCompletedGroupAlgebraOf (ell := ℓ) (H := FreeGroup X) v) := by
96end
98end FoxDifferential