FoxDifferential/Completed/Continuous/TailExactness.lean
1import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Closure
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/Continuous/TailExactness.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Continuous crossed differentials
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 Topology
21open ProCGroups.Generation
23universe u v
25section TailExactness
27variable (C : ProCGroups.FiniteGroupClass.{u})
28variable [Fact (ProCGroups.FiniteGroupClass.FiniteOnly C)]
30variable {X : Type v} [Fintype X] [DecidableEq X]
31variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33/-- If a finite family topologically generates `H`, the corresponding completed finite Fox
34boundary is exact at `Z_C[[H]]`. -/
36 (hForm : ProCGroups.FiniteGroupClass.Formation C)
37 (φ : X → H) (hφ : TopologicallyGenerates (G := H) (Set.range φ)) :
38 Function.Exact
39 (foxBoundaryMap (fun x : X => zcGroupLike C H (φ x) - 1) :
40 (X → ZCCompletedGroupAlgebra C H) → ZCCompletedGroupAlgebra C H)
42 ZCCompletedGroupAlgebra C H → ZCCoeff C) := by
43 let L : (X → ZCCompletedGroupAlgebra C H) →ₗ[ZCCompletedGroupAlgebra C H]
44 ZCCompletedGroupAlgebra C H :=
45 foxBoundaryMap (fun x : X => zcGroupLike C H (φ x) - 1)
46 have hclosedRange :
47 IsClosed ((LinearMap.range L : Submodule (ZCCompletedGroupAlgebra C H)
48 (ZCCompletedGroupAlgebra C H)) : Set (ZCCompletedGroupAlgebra C H)) := by
49 change IsClosed (Set.range L)
50 have hrange :
51 Set.range L = (fun v : X → ZCCompletedGroupAlgebra C H => L v) '' Set.univ := by
52 ext y
53 constructor
54 · rintro ⟨v, rfl⟩
55 exact ⟨v, trivial, rfl⟩
56 · rintro ⟨v, _hv, rfl⟩
57 exact ⟨v, rfl⟩
58 rw [hrange]
59 simpa [L] using
60 (isCompact_univ.image (continuous_foxBoundaryMap
61 (fun x : X => zcGroupLike C H (φ x) - 1))).isClosed
62 let K : Subgroup H :=
63 { carrier := {h | zcGroupLike C H h - 1 ∈ LinearMap.range L}
64 one_mem' := by
65 change zcCompletedGroupAlgebraBoundary C (MonoidHom.id H) (1 : H) ∈
66 LinearMap.range L
67 simp only [MonoidHom.id_apply, zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker, zero_mem]
68 mul_mem' := by
69 intro a b ha hb
70 change zcCompletedGroupAlgebraBoundary C (MonoidHom.id H) (a * b) ∈
71 LinearMap.range L
73 exact (LinearMap.range L).add_mem ha ((LinearMap.range L).smul_mem _ hb)
74 inv_mem' := by
75 intro a ha
76 change zcCompletedGroupAlgebraBoundary C (MonoidHom.id H) a⁻¹ ∈
77 LinearMap.range L
79 exact (LinearMap.range L).neg_mem ((LinearMap.range L).smul_mem _ ha) }
80 have hKclosed : IsClosed ((K : Subgroup H) : Set H) := by
81 change IsClosed {h : H | zcGroupLike C H h - 1 ∈
82 (LinearMap.range L : Submodule (ZCCompletedGroupAlgebra C H)
83 (ZCCompletedGroupAlgebra C H))}
84 exact hclosedRange.preimage
85 ((continuous_zcGroupLike (C := C) (G := H)).sub continuous_const)
86 have hsub : Subgroup.closure (Set.range φ) ≤ K := by
87 rw [Subgroup.closure_le]
88 rintro h ⟨x, rfl⟩
89 change zcGroupLike C H (φ x) - 1 ∈ LinearMap.range L
90 exact ⟨Pi.single x (1 : ZCCompletedGroupAlgebra C H), by
91 simp only [foxBoundaryMap_single, L]⟩
92 have htop : (⊤ : Subgroup H) ≤ K := by
93 have hcl : (Subgroup.closure (Set.range φ)).topologicalClosure ≤ K :=
94 Subgroup.topologicalClosure_minimal _ hsub hKclosed
95 rw [TopologicallyGenerates] at hφ
96 simpa [hφ] using hcl
97 have hstandard_le_range :
99 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) ≤
100 LinearMap.range L := by
102 refine Submodule.span_le.2 ?_
103 rintro _ ⟨h, rfl⟩
104 simpa [K, zcCompletedGroupAlgebraBoundary] using
105 htop (show h ∈ (⊤ : Subgroup H) from by simp only [Subgroup.mem_top])
106 have hrange_le_standard :
107 LinearMap.range L ≤
109 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) := by
110 rintro y ⟨v, rfl⟩
112 change L v ∈ Submodule.span (ZCCompletedGroupAlgebra C H)
113 (Set.range fun h : H => zcGroupLike C H h - 1)
114 rw [show L v =
115 ∑ x : X, v x * (zcGroupLike C H (φ x) - 1) from rfl]
116 exact Submodule.sum_mem _ fun x _ =>
117 Submodule.smul_mem _ (v x)
118 (Submodule.subset_span ⟨φ x, rfl⟩)
119 have haugmentation_le_range :
121 (LinearMap.range L : Submodule (ZCCompletedGroupAlgebra C H)
122 (ZCCompletedGroupAlgebra C H)) := by
123 intro z hz
124 have hzClosure :
125 z ∈ closure
127 Ideal (ZCCompletedGroupAlgebra C H)) : Set (ZCCompletedGroupAlgebra C H)) := by
129 (C := C) (H := H) hForm]
130 exact hz
131 exact closure_minimal
132 (by intro y hy; exact hstandard_le_range hy) hclosedRange hzClosure
133 intro z
134 constructor
135 · intro hz
136 exact haugmentation_le_range
138 (C := C) (H := H) (x := z)).2 hz)
139 · rintro ⟨x, rfl⟩
140 have hstd :
141 L x ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H :=
142 hrange_le_standard ⟨x, rfl⟩
143 have haug :
144 L x ∈ zcCompletedGroupAlgebraAugmentationIdeal C H :=
147 (C := C) (H := H) (x := L x)).1 haug
149variable {X₀ : Type u} [Fintype X₀] [DecidableEq X₀]
151/-- Source-shaped version of
154 (hForm : ProCGroups.FiniteGroupClass.Formation C)
155 (φ : X₀ → H) (hφ : TopologicallyGenerates (G := H) (Set.range φ)) :
156 Function.Exact
158 (X₀ → ZCCompletedGroupAlgebra C H) → ZCCompletedGroupAlgebra C H)
160 ZCCompletedGroupAlgebra C H → ZCCoeff C) := by
161 simpa [freeProCZCCompletedFoxBoundary] using
163 (C := C) (X := X₀) (H := H) hForm φ hφ)
165end TailExactness
167end
169end FoxDifferential