FoxDifferential/Completed/Continuous/Free/DiscreteGenerators.lean
1import FoxDifferential.Completed.Continuous.Free.CanonicalFormula
2import FoxDifferential.Completed.FreeProC.Uniqueness.Existence
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/Continuous/Free/DiscreteGenerators.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Continuous crossed differentials
15Crossed differentials, universal differential modules, Fox boundaries, Euler formulas, and Jacobians are the common algebraic layer used by Crowell and metabelian applications.
16-/
17namespace FoxDifferential
19noncomputable section
21open scoped BigOperators
23universe u
26variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
27variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)]
28variable (X H : Type u) [DecidableEq X]
29variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32variable {F : Type u}
33variable [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
34variable [TopologicalSpace X]
36variable [DiscreteTopology X]
38omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
39/-- Continuous completed Fox semidirect homomorphisms from a free pro-`C` source are unique for
42 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
43 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
44 (φ : X → H) :
45 ∃! f : F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
46 ∀ x : X, f (ι x) = freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x :=
48 (ProC := ProC) hι htarget φ
49 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProC) X H φ)
51omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
52/-- Componentwise continuous completed Fox semidirect homomorphisms from a free pro-`C` source
55 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
56 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
57 (φ : X → H) :
58 ∃! f : F →ₜ* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
59 (∀ x : X, (f (ι x)).left =
60 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) ∧
61 ∀ x : X, (f (ι x)).right = φ x :=
63 (ProC := ProC) hι htarget φ
64 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProC) X H φ)
66omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
67/-- Continuous completed Fox semidirect lifts from a free pro-`C` source are unique for discrete
70 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
71 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
72 (φ : X → H) :
73 ∃! f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
74 Continuous f ∧
75 ∀ x : X, f (ι x) =
76 freeProCZCCompletedFoxSemidirectGenerator (ProC := ProC) φ x :=
78 (ProC := ProC) hι htarget φ
79 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProC) X H φ)
81omit [Fact (ProCGroups.FiniteGroupClass.FiniteOnly ProC.finiteQuotientClass)] in
82/-- Componentwise continuous completed Fox semidirect lifts from a free pro-`C` source are unique
85 {ι : X → F} (hι : ProCGroups.FreeProC.IsFreeProCGroup (ProC := ProC) ι)
86 (htarget : ProC (G := ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H))
87 (φ : X → H) :
88 ∃! f : F →* ZCCompletedFoxSemidirect ProC.finiteQuotientClass X H,
89 Continuous f ∧
90 (∀ x : X, (f (ι x)).left =
91 Pi.single x (1 : ZCCompletedGroupAlgebra ProC.finiteQuotientClass H)) ∧
92 ∀ x : X, (f (ι x)).right = φ x :=
94 (ProC := ProC) hι htarget φ
95 (continuous_freeProCZCCompletedFoxSemidirectGenerator_of_discrete (ProC := ProC) X H φ)
99end
101end FoxDifferential