Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed.Continuous.TailExactness
ProCGroups/FoxDifferential/Completed/Continuous/TailExactness/Source

Source: ProCGroups.FoxDifferential.Completed.Continuous.TailExactness

1import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Closure
3/-!
4# Fox differential: completed — continuous — tail exactness
6The principal declarations in this module are:
8- `exact_foxBoundaryMap_zcGroupLike_sub_one_of_topologicallyGenerates`
9 If a finite family topologically generates \(H\), the corresponding completed finite Fox boundary
10 is exact at \(\mathbb{Z}_C\llbracket H\rrbracket\).
11- `exact_freeProCZCCompletedFoxBoundary_of_topologicallyGenerates`
12 In the sequence, the first map is injective, its image is the kernel of the second map, and the
13 second map is surjective.
14-/
16namespace FoxDifferential
18noncomputable section
20open scoped Topology
21open ProCGroups.Generation
23universe u v
25section TailExactness
27variable (C : ProCGroups.FiniteGroupClass.{u})
29variable {X : Type v} [Fintype X] [DecidableEq X]
30variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32omit [DecidableEq X] in
33/--
34If a finite family topologically generates \(H\), the corresponding completed finite Fox
35boundary is exact at \(\mathbb{Z}_C\llbracket H\rrbracket\).
36-/
37theorem exact_foxBoundaryMap_zcGroupLike_sub_one_of_topologicallyGenerates
39 (φ : X → H) (hφ : TopologicallyGenerates (G := H) (Set.range φ)) :
40 Function.Exact
41 (foxBoundaryMap (fun x : X => zcGroupLike C H (φ x) - 1) :
42 (X → ZCCompletedGroupAlgebra C H) → ZCCompletedGroupAlgebra C H)
43 (zcCompletedGroupAlgebraAugmentation C H :
44 ZCCompletedGroupAlgebra C H → ZCCoeff C) := by
45 classical
46 let L : (X → ZCCompletedGroupAlgebra C H) →ₗ[ZCCompletedGroupAlgebra C H]
47 ZCCompletedGroupAlgebra C H :=
48 foxBoundaryMap (fun x : X => zcGroupLike C H (φ x) - 1)
49 have hclosedRange :
50 IsClosed ((LinearMap.range L : Submodule (ZCCompletedGroupAlgebra C H)
51 (ZCCompletedGroupAlgebra C H)) : Set (ZCCompletedGroupAlgebra C H)) := by
52 change IsClosed (Set.range L)
53 have hrange :
54 Set.range L = (fun v : X → ZCCompletedGroupAlgebra C H => L v) '' Set.univ := by
55 ext y
56 constructor
57 · rintro ⟨v, rfl⟩
58 exact ⟨v, trivial, rfl⟩
59 · rintro ⟨v, _hv, rfl⟩
60 exact ⟨v, rfl⟩
61 rw [hrange]
62 simpa [L] using
63 (isCompact_univ.image (continuous_foxBoundaryMap
64 (fun x : X => zcGroupLike C H (φ x) - 1))).isClosed
65 let K : Subgroup H :=
66 { carrier := {h | zcGroupLike C H h - 1 ∈ LinearMap.range L}
67 one_mem' := by
68 change zcCompletedGroupAlgebraBoundary C (MonoidHom.id H) (1 : H) ∈
69 LinearMap.range L
70 simp only [MonoidHom.id_apply, zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker, zero_mem]
71 mul_mem' := by
72 intro a b ha hb
73 change zcCompletedGroupAlgebraBoundary C (MonoidHom.id H) (a * b) ∈
74 LinearMap.range L
75 rw [ScalarCrossedHom.map_mul
76 (zcCompletedGroupAlgebraBoundary C (MonoidHom.id H))]
77 exact (LinearMap.range L).add_mem ha ((LinearMap.range L).smul_mem _ hb)
78 inv_mem' := by
79 intro a ha
80 change zcCompletedGroupAlgebraBoundary C (MonoidHom.id H) a⁻¹ ∈
81 LinearMap.range L
82 rw [ScalarCrossedHom.map_inv
83 (zcCompletedGroupAlgebraBoundary C (MonoidHom.id H))]
84 exact (LinearMap.range L).neg_mem ((LinearMap.range L).smul_mem _ ha) }
85 have hKclosed : IsClosed ((K : Subgroup H) : Set H) := by
86 change IsClosed {h : H | zcGroupLike C H h - 1 ∈
87 (LinearMap.range L : Submodule (ZCCompletedGroupAlgebra C H)
88 (ZCCompletedGroupAlgebra C H))}
89 exact hclosedRange.preimage
90 ((continuous_zcGroupLike (C := C) (G := H)).sub continuous_const)
91 have hsub : Subgroup.closure (Set.range φ) ≤ K := by
92 rw [Subgroup.closure_le]
93 rintro h ⟨x, rfl⟩
94 change zcGroupLike C H (φ x) - 1 ∈ LinearMap.range L
95 exact ⟨Pi.single x (1 : ZCCompletedGroupAlgebra C H), by
96 simp only [foxBoundaryMap_single, L]⟩
97 have htop : (⊤ : Subgroup H) ≤ K := by
98 have hcl : (Subgroup.closure (Set.range φ)).topologicalClosure ≤ K :=
99 Subgroup.topologicalClosure_minimal _ hsub hKclosed
100 rw [TopologicallyGenerates] at hφ
101 simpa [hφ] using hcl
102 have hstandard_le_range :
103 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
104 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) ≤
105 LinearMap.range L := by
106 rw [zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span]
107 refine Submodule.span_le.2 ?_
108 rintro _ ⟨h, rfl⟩
109 simpa [K, zcCompletedGroupAlgebraBoundary] using
110 htop (show h ∈ (⊤ : Subgroup H) from by simp only [Subgroup.mem_top])
111 have hrange_le_standard :
112 LinearMap.range L ≤
113 (zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
114 Submodule (ZCCompletedGroupAlgebra C H) (ZCCompletedGroupAlgebra C H)) := by
115 rintro y ⟨v, rfl⟩
116 rw [zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_span]
117 change L v ∈ Submodule.span (ZCCompletedGroupAlgebra C H)
118 (Set.range fun h : H => zcGroupLike C H h - 1)
119 rw [show L v =
120 ∑ x : X, v x * (zcGroupLike C H (φ x) - 1) from rfl]
121 exact Submodule.sum_mem _ fun x _ =>
122 Submodule.smul_mem _ (v x)
123 (Submodule.subset_span ⟨φ x, rfl⟩)
124 have haugmentation_le_range :
125 zcCompletedGroupAlgebraAugmentationIdeal C H ≤
126 (LinearMap.range L : Submodule (ZCCompletedGroupAlgebra C H)
127 (ZCCompletedGroupAlgebra C H)) := by
128 intro z hz
129 have hzClosure :
130 z ∈ closure
131 ((zcCompletedGroupAlgebraStandardAugmentationIdeal C H :
132 Ideal (ZCCompletedGroupAlgebra C H)) : Set (ZCCompletedGroupAlgebra C H)) := by
133 rw [closure_zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_augmentationIdeal
134 (C := C) (H := H) hForm]
135 exact hz
136 exact closure_minimal
137 (by intro y hy; exact hstandard_le_range hy) hclosedRange hzClosure
138 intro z
139 constructor
140 · intro hz
141 exact haugmentation_le_range
142 ((mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
143 (C := C) (H := H) (x := z)).2 hz)
144 · rintro ⟨x, rfl⟩
145 have hstd :
146 L x ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H :=
147 hrange_le_standard ⟨x, rfl⟩
148 have haug :
149 L x ∈ zcCompletedGroupAlgebraAugmentationIdeal C H :=
150 zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal C H hstd
151 exact (mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
152 (C := C) (H := H) (x := L x)).1 haug
154variable {X₀ : Type u} [Fintype X₀] [DecidableEq X₀]
156omit [DecidableEq X₀] in
157/--
158In the sequence, the first map is injective, its image is the kernel of the second map, and the
159second map is surjective.
160-/
161theorem exact_freeProCZCCompletedFoxBoundary_of_topologicallyGenerates
163 (φ : X₀ → H) (hφ : TopologicallyGenerates (G := H) (Set.range φ)) :
164 Function.Exact
165 (freeProCZCCompletedFoxBoundary C φ :
166 (X₀ → ZCCompletedGroupAlgebra C H) → ZCCompletedGroupAlgebra C H)
167 (zcCompletedGroupAlgebraAugmentation C H :
168 ZCCompletedGroupAlgebra C H → ZCCoeff C) := by
169 simpa [freeProCZCCompletedFoxBoundary] using
170 (exact_foxBoundaryMap_zcGroupLike_sub_one_of_topologicallyGenerates
171 (C := C) (X := X₀) (H := H) hForm φ hφ)
173end TailExactness
175end
177end FoxDifferential