FoxDifferential/Completed/Comparison/SourceProjection.lean
1import FoxDifferential.Completed.Continuous.Naturality
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Comparison/SourceProjection.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Discrete-completed comparison
14Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
15-/
16namespace FoxDifferential
18noncomputable section
20open scoped BigOperators
22universe u
24section SourceBoundaryProjection
26variable (C : ProCGroups.FiniteGroupClass.{u})
27variable {X H : Type u} [Fintype X]
28variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
30/-- Finite-stage projection of the source-shaped completed Fox boundary map. -/
32 (φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H))
33 (j : ZCCompletedGroupAlgebraIndex C H) :
35 (freeProCZCCompletedFoxBoundary C φ v) =
36 ∑ x : X,
37 zcCompletedGroupAlgebraProjection C H j (v x) *
38 zcCompletedGroupAlgebraProjection C H j (zcGroupLike C H (φ x) - 1) := by
40 apply Finset.sum_congr rfl
41 intro x _
43 zcCompletedGroupAlgebraProjection_sub, zcCompletedGroupAlgebraProjection_groupLike, MonoidAlgebra.of_apply,
46/-- Finite-stage projection of the source-shaped completed Fox boundary map, with generator
49 (φ : X → H) (v : ZCFreeFoxCoordinates C (X := X) (H := H))
50 (j : ZCCompletedGroupAlgebraIndex C H) :
52 (freeProCZCCompletedFoxBoundary C φ v) =
53 ∑ x : X,
54 zcCompletedGroupAlgebraProjection C H j (v x) *
55 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
56 (CompletedGroupAlgebraQuotientInClass H C j.2)
57 (QuotientGroup.mk (φ x)) - 1) := by
58 simpa [zcCompletedGroupAlgebraProjection] using
60 (C := C) (X := X) (H := H) φ v j
62end SourceBoundaryProjection
64section TargetProjectionNaturality
66variable (C : ProCGroups.FiniteGroupClass.{u})
67variable (hC : ProCGroups.FiniteGroupClass.Hereditary C)
68variable {X H K : Type u} [Fintype X]
69variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
70variable [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
72omit [Fintype X] in
73/-- Componentwise finite-stage projection formula for target maps on completed Fox coordinates. -/
75 (η : H →ₜ* K)
76 (v : ZCFreeFoxCoordinates C (X := X) (H := H))
77 (j : ZCCompletedGroupAlgebraIndex C K) (x : X) :
79 (zcFreeFoxCoordinatesMap (X := X) C hC η v x) =
80 zcCompletedGroupAlgebraMapStage C hC η j
82 (j.1, completedGroupAlgebraComapIndexInClass
83 (G := H) (H := K) C hC η j.2) (v x)) := by
86/-- Finite-stage projection of target naturality for source-shaped completed Fox boundary maps. -/
88 (η : H →ₜ* K) (φ : X → H)
89 (v : ZCFreeFoxCoordinates C (X := X) (H := H))
90 (j : ZCCompletedGroupAlgebraIndex C K) :
92 (zcCompletedGroupAlgebraMap C hC η (freeProCZCCompletedFoxBoundary C φ v)) =
93 ∑ x : X,
94 zcCompletedGroupAlgebraMapStage C hC η j
96 (j.1, completedGroupAlgebraComapIndexInClass
97 (G := H) (H := K) C hC η j.2) (v x)) *
98 (MonoidAlgebra.of (ModNCompletedCoeff j.1.modulus)
99 (CompletedGroupAlgebraQuotientInClass K C j.2)
100 (QuotientGroup.mk (η (φ x))) - 1) := by
103 apply Finset.sum_congr rfl
104 intro x _
107end TargetProjectionNaturality
109end
111end FoxDifferential