IndisputableMonolith.Foundation.CircleH1Computation
IndisputableMonolith/Foundation/CircleH1Computation.lean · 546 lines · 54 declarations
show as:
view math explainer →
1import Mathlib.Algebra.Homology.SingleHomology
2import Mathlib.Algebra.Category.ModuleCat.Basic
3import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
4import Mathlib.Algebra.Homology.QuasiIso
5import Mathlib.AlgebraicTopology.SingularHomology.Basic
6import Mathlib.Topology.Category.TopCat.Sphere
7import IndisputableMonolith.Foundation.CircleParam
8import IndisputableMonolith.Foundation.CircleFundamentalSimplex
9import IndisputableMonolith.Foundation.MathlibCohomologyBridge
10
11/-!
12# Circle H₁ Computation Workbench
13
14This module is the local Mathlib-style workbench for the missing computation
15`H₁(S¹; ℤ) ≅ ℤ`. It does not replace `TopCat.sphere 1` and does not feed the
16strict T8 bridge until a real equivalence to Mathlib's imported singular
17homology object is proved.
18
19The first proved atom is the algebraic core of the finite circle chain model:
20a chain complex supported by `ℤ` in degree `1` has degree-`1` homology `ℤ`.
21-/
22
23namespace IndisputableMonolith
24namespace Foundation
25namespace CircleH1Computation
26
27open CategoryTheory CategoryTheory.Limits ZeroObject Opposite
28
29noncomputable section
30
31/-- The integer chain complex supported in degree `1`. This is the algebraic
32core of the finite circle model before the topological transport to
33`TopCat.sphere 1` is supplied. -/
34abbrev singleDegreeOneIntComplex :
35 HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ) :=
36 (HomologicalComplex.single (ModuleCat ℤ) (ComplexShape.down ℕ) 1).obj
37 (ModuleCat.of ℤ ℤ)
38
39/-- Degree-`1` homology of the single-supported integer chain complex is the
40integer module. -/
41def singleDegreeOneIntComplexHomologyOneIsoInt :
42 (((HomologicalComplex.single (ModuleCat ℤ) (ComplexShape.down ℕ) 1).obj
43 (ModuleCat.of ℤ ℤ)).homology 1) ≅ ModuleCat.of ℤ ℤ :=
44 HomologicalComplex.singleObjHomologySelfIso (ComplexShape.down ℕ) 1
45 (ModuleCat.of ℤ ℤ)
46
47/-- Proposition-facing form of `singleDegreeOneIntComplexHomologyOneIsoInt`,
48matching the `circleH1ZIsoInt` pattern used by the strict T8 bridge. -/
49theorem singleDegreeOneIntComplexHomologyOneNonemptyIsoInt :
50 Nonempty
51 ((((HomologicalComplex.single (ModuleCat ℤ) (ComplexShape.down ℕ) 1).obj
52 (ModuleCat.of ℤ ℤ)).homology 1) ≅ ModuleCat.of ℤ ℤ) :=
53 ⟨singleDegreeOneIntComplexHomologyOneIsoInt⟩
54
55/-- Any chain complex isomorphic to the degree-`1` single-supported integer
56complex has degree-`1` homology `ℤ`. This is the transport lemma needed once a
57finite circle chain model is identified with the single degree-`1` reduced
58model. -/
59def homologyOneIsoIntOfIsoSingleDegreeOneIntComplex
60 {K : HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ)}
61 (e : K ≅ singleDegreeOneIntComplex) :
62 ((HomologicalComplex.homologyFunctor
63 (ModuleCat ℤ) (ComplexShape.down ℕ) 1).obj K) ≅ ModuleCat.of ℤ ℤ :=
64 ((HomologicalComplex.homologyFunctor
65 (ModuleCat ℤ) (ComplexShape.down ℕ) 1).mapIso e) ≪≫
66 singleDegreeOneIntComplexHomologyOneIsoInt
67
68/-- Proposition-facing form of
69`homologyOneIsoIntOfIsoSingleDegreeOneIntComplex`. -/
70theorem homologyOneNonemptyIsoIntOfIsoSingleDegreeOneIntComplex
71 {K : HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ)}
72 (e : K ≅ singleDegreeOneIntComplex) :
73 Nonempty
74 (((HomologicalComplex.homologyFunctor
75 (ModuleCat ℤ) (ComplexShape.down ℕ) 1).obj K) ≅ ModuleCat.of ℤ ℤ) :=
76 ⟨homologyOneIsoIntOfIsoSingleDegreeOneIntComplex e⟩
77
78/-- Degree-local quasi-isomorphism transport: if a chain complex maps by a
79quasi-isomorphism in degree `1` to the single-supported integer complex, then
80its degree-`1` homology is `ℤ`. -/
81def homologyOneIsoIntOfQuasiIsoAtSingleDegreeOneIntComplex
82 {K : HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ)}
83 (f : K ⟶ singleDegreeOneIntComplex)
84 [K.HasHomology 1] [QuasiIsoAt f 1] :
85 K.homology 1 ≅ ModuleCat.of ℤ ℤ :=
86 isoOfQuasiIsoAt f 1 ≪≫
87 singleDegreeOneIntComplexHomologyOneIsoInt
88
89/-- Proposition-facing form of the degree-local quasi-isomorphism transport. -/
90theorem homologyOneNonemptyIsoIntOfQuasiIsoAtSingleDegreeOneIntComplex
91 {K : HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ)}
92 (f : K ⟶ singleDegreeOneIntComplex)
93 [K.HasHomology 1] [QuasiIsoAt f 1] :
94 Nonempty (K.homology 1 ≅ ModuleCat.of ℤ ℤ) :=
95 ⟨homologyOneIsoIntOfQuasiIsoAtSingleDegreeOneIntComplex f⟩
96
97/-- Global quasi-isomorphism transport, for the common case where the finite
98circle chain model is proved quasi-isomorphic to the single-supported reduced
99model in every degree. -/
100def homologyOneIsoIntOfQuasiIsoSingleDegreeOneIntComplex
101 {K : HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ)}
102 (f : K ⟶ singleDegreeOneIntComplex)
103 [∀ i, K.HasHomology i] [QuasiIso f] :
104 K.homology 1 ≅ ModuleCat.of ℤ ℤ :=
105 homologyOneIsoIntOfQuasiIsoAtSingleDegreeOneIntComplex f
106
107/-- Proposition-facing form of the global quasi-isomorphism transport. -/
108theorem homologyOneNonemptyIsoIntOfQuasiIsoSingleDegreeOneIntComplex
109 {K : HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ)}
110 (f : K ⟶ singleDegreeOneIntComplex)
111 [∀ i, K.HasHomology i] [QuasiIso f] :
112 Nonempty (K.homology 1 ≅ ModuleCat.of ℤ ℤ) :=
113 ⟨homologyOneIsoIntOfQuasiIsoSingleDegreeOneIntComplex f⟩
114
115/-- The reduced cellular chain model of the circle: one integer generator in
116degree `1` and zero elsewhere. This is a finite chain model target, not a
117replacement for `TopCat.sphere 1`. -/
118abbrev reducedCellularCircleChainModel :
119 HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ) :=
120 singleDegreeOneIntComplex
121
122/-- The reduced cellular circle model has chain group `ℤ` in degree `1`. -/
123def reducedCellularCircleChainModelXOneIsoInt :
124 reducedCellularCircleChainModel.X 1 ≅ ModuleCat.of ℤ ℤ :=
125 HomologicalComplex.singleObjXSelf (ComplexShape.down ℕ) 1
126 (ModuleCat.of ℤ ℤ)
127
128/-- The reduced cellular circle model has zero chain group in degree `0`. -/
129theorem reducedCellularCircleChainModelXZeroIsZero :
130 CategoryTheory.Limits.IsZero (reducedCellularCircleChainModel.X 0) :=
131 HomologicalComplex.isZero_single_obj_X (ComplexShape.down ℕ) 1
132 (ModuleCat.of ℤ ℤ) 0 (by norm_num)
133
134/-- The reduced cellular circle model has zero chain groups above degree `1`. -/
135theorem reducedCellularCircleChainModelXSuccSuccIsZero (n : ℕ) :
136 CategoryTheory.Limits.IsZero (reducedCellularCircleChainModel.X (n + 2)) :=
137 HomologicalComplex.isZero_single_obj_X (ComplexShape.down ℕ) 1
138 (ModuleCat.of ℤ ℤ) (n + 2) (by omega)
139
140/-- All differentials in the reduced cellular circle model are zero. -/
141theorem reducedCellularCircleChainModel_d_eq_zero (i j : ℕ) :
142 reducedCellularCircleChainModel.d i j = 0 :=
143 HomologicalComplex.single_obj_d (ComplexShape.down ℕ) 1
144 (ModuleCat.of ℤ ℤ) i j
145
146/-- The reduced cellular circle model has first homology `ℤ`. -/
147def reducedCellularCircleChainModelH1IsoInt :
148 reducedCellularCircleChainModel.homology 1 ≅ ModuleCat.of ℤ ℤ :=
149 singleDegreeOneIntComplexHomologyOneIsoInt
150
151/-- Proposition-facing form of
152`reducedCellularCircleChainModelH1IsoInt`. -/
153theorem reducedCellularCircleChainModelH1NonemptyIsoInt :
154 Nonempty (reducedCellularCircleChainModel.homology 1 ≅ ModuleCat.of ℤ ℤ) :=
155 ⟨reducedCellularCircleChainModelH1IsoInt⟩
156
157/-- The ordinary two-cell cellular chain model of the circle: one integer
158generator in degree `0`, one integer generator in degree `1`, no higher chain
159groups, and zero boundary. This remains an algebraic finite-chain model until
160a later theorem connects it to Mathlib's `TopCat.sphere 1`. -/
161def ordinaryCellularCircleChainModel :
162 HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ) where
163 X n := if n = 0 then ModuleCat.of ℤ ℤ
164 else if n = 1 then ModuleCat.of ℤ ℤ
165 else 0
166 d _ _ := 0
167
168/-- The ordinary cellular circle model has chain group `ℤ` in degree `0`. -/
169def ordinaryCellularCircleChainModelXZeroIsoInt :
170 ordinaryCellularCircleChainModel.X 0 ≅ ModuleCat.of ℤ ℤ :=
171 eqToIso (by simp [ordinaryCellularCircleChainModel])
172
173/-- The ordinary cellular circle model has chain group `ℤ` in degree `1`. -/
174def ordinaryCellularCircleChainModelXOneIsoInt :
175 ordinaryCellularCircleChainModel.X 1 ≅ ModuleCat.of ℤ ℤ :=
176 eqToIso (by simp [ordinaryCellularCircleChainModel])
177
178/-- The ordinary cellular circle model has zero chain groups above degree `1`. -/
179theorem ordinaryCellularCircleChainModelXSuccSuccIsZero (n : ℕ) :
180 CategoryTheory.Limits.IsZero (ordinaryCellularCircleChainModel.X (n + 2)) := by
181 dsimp [ordinaryCellularCircleChainModel]
182 exact isZero_zero (C := ModuleCat ℤ)
183
184/-- All differentials in the ordinary cellular circle model are zero. -/
185theorem ordinaryCellularCircleChainModel_d_eq_zero (i j : ℕ) :
186 ordinaryCellularCircleChainModel.d i j = 0 :=
187 rfl
188
189/-- Since the outgoing degree-`1` boundary is zero, the degree-`1` cycles in the
190ordinary cellular circle model are the whole degree-`1` chain group, hence
191`ℤ`. -/
192def ordinaryCellularCircleChainModelCyclesOneIsoInt :
193 ordinaryCellularCircleChainModel.cycles 1 ≅ ModuleCat.of ℤ ℤ :=
194 ordinaryCellularCircleChainModel.iCyclesIso 1 0 (by norm_num)
195 (ordinaryCellularCircleChainModel_d_eq_zero 1 0) ≪≫
196 ordinaryCellularCircleChainModelXOneIsoInt
197
198/-- The ordinary two-cell cellular circle model has first homology `ℤ`. -/
199def ordinaryCellularCircleChainModelH1IsoInt :
200 ordinaryCellularCircleChainModel.homology 1 ≅ ModuleCat.of ℤ ℤ :=
201 (ordinaryCellularCircleChainModel.isoHomologyπ 2 1 (by norm_num)
202 (ordinaryCellularCircleChainModel_d_eq_zero 2 1)).symm ≪≫
203 ordinaryCellularCircleChainModelCyclesOneIsoInt
204
205/-- Proposition-facing form of `ordinaryCellularCircleChainModelH1IsoInt`. -/
206theorem ordinaryCellularCircleChainModelH1NonemptyIsoInt :
207 Nonempty (ordinaryCellularCircleChainModel.homology 1 ≅ ModuleCat.of ℤ ℤ) :=
208 ⟨ordinaryCellularCircleChainModelH1IsoInt⟩
209
210/-- The ordinary two-cell cellular circle model and the reduced one have the
211same first homology. This is an algebraic comparison of the two finite chain
212models, independent of any topological claim about `TopCat.sphere 1`. -/
213def ordinaryCellularCircleChainModelH1IsoReducedCellularH1 :
214 ordinaryCellularCircleChainModel.homology 1 ≅
215 reducedCellularCircleChainModel.homology 1 :=
216 ordinaryCellularCircleChainModelH1IsoInt ≪≫
217 reducedCellularCircleChainModelH1IsoInt.symm
218
219/-- Proposition-facing form of
220`ordinaryCellularCircleChainModelH1IsoReducedCellularH1`. -/
221theorem ordinaryCellularCircleChainModelH1NonemptyIsoReducedCellularH1 :
222 Nonempty
223 (ordinaryCellularCircleChainModel.homology 1 ≅
224 reducedCellularCircleChainModel.homology 1) :=
225 ⟨ordinaryCellularCircleChainModelH1IsoReducedCellularH1⟩
226
227/-- Chain map collapsing the degree-`0` cellular generator and retaining the
228degree-`1` circle generator. -/
229def ordinaryCellularToReducedChainMap :
230 ordinaryCellularCircleChainModel ⟶ reducedCellularCircleChainModel :=
231 HomologicalComplex.mkHomToSingle
232 ordinaryCellularCircleChainModelXOneIsoInt.hom
233 (by
234 intro i _hi
235 simp [ordinaryCellularCircleChainModel_d_eq_zero])
236
237/-- In degree `1`, `ordinaryCellularToReducedChainMap` is the identity on the
238chosen integer generator, modulo the definitional single-complex isomorphism. -/
239theorem ordinaryCellularToReducedChainMap_f_one :
240 ordinaryCellularToReducedChainMap.f 1 =
241 ordinaryCellularCircleChainModelXOneIsoInt.hom ≫
242 (HomologicalComplex.singleObjXSelf
243 (ComplexShape.down ℕ) 1 (ModuleCat.of ℤ ℤ)).inv := by
244 simp [ordinaryCellularToReducedChainMap]
245
246/-- Chain map including the reduced degree-`1` model into the ordinary two-cell
247cellular circle model. -/
248def reducedCellularToOrdinaryChainMap :
249 reducedCellularCircleChainModel ⟶ ordinaryCellularCircleChainModel :=
250 HomologicalComplex.mkHomFromSingle
251 ordinaryCellularCircleChainModelXOneIsoInt.inv
252 (by
253 intro k _hk
254 simp [ordinaryCellularCircleChainModel_d_eq_zero])
255
256/-- In degree `1`, `reducedCellularToOrdinaryChainMap` is the inverse of the
257chosen integer-generator identification, modulo the definitional
258single-complex isomorphism. -/
259theorem reducedCellularToOrdinaryChainMap_f_one :
260 reducedCellularToOrdinaryChainMap.f 1 =
261 (HomologicalComplex.singleObjXSelf
262 (ComplexShape.down ℕ) 1 (ModuleCat.of ℤ ℤ)).hom ≫
263 ordinaryCellularCircleChainModelXOneIsoInt.inv := by
264 simp [reducedCellularToOrdinaryChainMap]
265
266/-- The reduced model is a retract of the ordinary cellular model at the chain
267level: include the degree-`1` generator and then collapse degree `0`, and the
268reduced complex is unchanged. -/
269theorem reducedCellularToOrdinary_comp_ordinaryCellularToReduced :
270 reducedCellularToOrdinaryChainMap ≫ ordinaryCellularToReducedChainMap =
271 𝟙 reducedCellularCircleChainModel := by
272 apply HomologicalComplex.from_single_hom_ext
273 simp [reducedCellularToOrdinaryChainMap_f_one,
274 ordinaryCellularToReducedChainMap_f_one]
275
276/-- The other composite need not be the identity on the ordinary two-cell
277complex, because the ordinary model has an additional degree-`0` generator.
278It is, however, the identity in degree `1`, the degree relevant to the circle
279homology computation. -/
280theorem ordinaryCellularToReduced_comp_reducedCellularToOrdinary_f_one :
281 (ordinaryCellularToReducedChainMap ≫ reducedCellularToOrdinaryChainMap).f 1 =
282 𝟙 (ordinaryCellularCircleChainModel.X 1) := by
283 simp [ordinaryCellularToReducedChainMap_f_one,
284 reducedCellularToOrdinaryChainMap_f_one]
285
286/-- The collapse from the ordinary two-cell cellular circle model to the reduced
287degree-`1` model is a quasi-isomorphism in degree `1`.
288
289The proof uses Mathlib's zero-differential short-complex criterion: in degree
290`1`, both relevant short complexes have zero differentials, and the middle
291component of the collapse map is an isomorphism on the chosen integer
292generator. -/
293theorem ordinaryCellularToReducedChainMap_quasiIsoAt_one :
294 QuasiIsoAt ordinaryCellularToReducedChainMap 1 := by
295 rw [quasiIsoAt_iff]
296 rw [ShortComplex.quasiIso_iff_isIso_liftCycles _ (by
297 simp [ordinaryCellularCircleChainModel_d_eq_zero]) (by
298 simp [ordinaryCellularCircleChainModel_d_eq_zero]) (by
299 simp)]
300 let S₂ :=
301 (HomologicalComplex.shortComplexFunctor (ModuleCat ℤ) (ComplexShape.down ℕ) 1).obj
302 reducedCellularCircleChainModel
303 let φ :=
304 ((HomologicalComplex.shortComplexFunctor (ModuleCat ℤ) (ComplexShape.down ℕ) 1).map
305 ordinaryCellularToReducedChainMap)
306 let w : φ.τ₂ ≫ S₂.g = 0 := by
307 dsimp [S₂, φ]
308 simp
309 change IsIso (S₂.liftCycles φ.τ₂ w)
310 haveI : IsIso S₂.iCycles := S₂.isIso_iCycles (by
311 dsimp [S₂])
312 haveI : IsIso (S₂.liftCycles φ.τ₂ w ≫ S₂.iCycles) := by
313 rw [ShortComplex.liftCycles_i]
314 dsimp [S₂, φ]
315 rw [ordinaryCellularToReducedChainMap_f_one]
316 infer_instance
317 exact IsIso.of_isIso_comp_right (S₂.liftCycles φ.τ₂ w) S₂.iCycles
318
319/-- The finite cellular algebraic part of the circle-H1 computation is closed:
320the reduced and ordinary cellular models have H₁ ≅ ℤ, the ordinary model
321collapses to the reduced model in degree `1`, and the reduced model is a chain
322retract of the ordinary one. The remaining Phase 5 gap is only the geometric
323transport from Mathlib's singular chains on `TopCat.sphere 1` to this cellular
324model. -/
325structure CellularCircleAlgebraicH1Certificate : Prop where
326 reduced_h1_iso_int :
327 Nonempty (reducedCellularCircleChainModel.homology 1 ≅ ModuleCat.of ℤ ℤ)
328 ordinary_h1_iso_int :
329 Nonempty (ordinaryCellularCircleChainModel.homology 1 ≅ ModuleCat.of ℤ ℤ)
330 ordinary_h1_iso_reduced_h1 :
331 Nonempty
332 (ordinaryCellularCircleChainModel.homology 1 ≅
333 reducedCellularCircleChainModel.homology 1)
334 reduced_is_retract :
335 reducedCellularToOrdinaryChainMap ≫ ordinaryCellularToReducedChainMap =
336 𝟙 reducedCellularCircleChainModel
337 collapse_quasiIsoAt_one :
338 QuasiIsoAt ordinaryCellularToReducedChainMap 1
339
340/-- Checked certificate for the finite cellular algebraic part of the
341circle-H1 computation. -/
342theorem cellularCircleAlgebraicH1Certificate :
343 CellularCircleAlgebraicH1Certificate where
344 reduced_h1_iso_int :=
345 reducedCellularCircleChainModelH1NonemptyIsoInt
346 ordinary_h1_iso_int :=
347 ordinaryCellularCircleChainModelH1NonemptyIsoInt
348 ordinary_h1_iso_reduced_h1 :=
349 ordinaryCellularCircleChainModelH1NonemptyIsoReducedCellularH1
350 reduced_is_retract :=
351 reducedCellularToOrdinary_comp_ordinaryCellularToReduced
352 collapse_quasiIsoAt_one :=
353 ordinaryCellularToReducedChainMap_quasiIsoAt_one
354
355/-- The imported Mathlib singular chain complex of `TopCat.sphere 1` with
356integer coefficients. This is the exact chain-level object whose degree-`1`
357homology is the final strict T8 target. -/
358abbrev sphereOneSingularIntChainComplex : ChainComplex (ModuleCat ℤ) ℕ :=
359 ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj
360 (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere 1)
361
362/-- The degree-`1` singular chain selecting the once-around fundamental
363singular 1-simplex of `TopCat.sphere 1`. It is the coproduct summand inclusion
364corresponding to `fundamentalSphereOneSingularOneSimplex`. -/
365noncomputable def fundamentalSphereOneSingularOneChain :
366 ModuleCat.of ℤ ℤ ⟶ sphereOneSingularIntChainComplex.X 1 :=
367 Sigma.ι
368 (fun _ : (TopCat.toSSet.obj (TopCat.sphere 1)).obj (op (SimplexCategory.mk 1)) =>
369 ModuleCat.of ℤ ℤ)
370 CircleFundamentalSimplex.fundamentalSphereOneSingularOneSimplex
371
372/-- The fundamental singular 1-chain has zero boundary. This is the
373chain-level form of the equal-faces theorem for the once-around singular
3741-simplex. -/
375theorem fundamentalSphereOneSingularOneChain_boundary_zero :
376 fundamentalSphereOneSingularOneChain ≫ sphereOneSingularIntChainComplex.d 1 0 = 0 := by
377 dsimp [fundamentalSphereOneSingularOneChain, sphereOneSingularIntChainComplex,
378 AlgebraicTopology.singularChainComplexFunctor,
379 AlgebraicTopology.SSet.singularChainComplexFunctor,
380 AlgebraicTopology.alternatingFaceMapComplex,
381 sigmaConst]
382 rw [AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq]
383 dsimp [AlgebraicTopology.AlternatingFaceMapComplex.objD]
384 simp only [Fin.sum_univ_two, Fin.val_zero, pow_zero, one_zsmul, Fin.val_one, pow_one,
385 neg_zsmul, one_zsmul, Preadditive.comp_add, Preadditive.comp_neg]
386 simp only [CategoryTheory.SimplicialObject.δ]
387 dsimp [sigmaConst]
388 simp only [Sigma.ι_comp_map', Category.id_comp]
389 change Sigma.ι (fun x => ModuleCat.of ℤ ℤ)
390 ((TopCat.toSSet.obj (TopCat.sphere 1)).δ (0 : Fin 2)
391 CircleFundamentalSimplex.fundamentalSphereOneSingularOneSimplex) +
392 -Sigma.ι (fun x => ModuleCat.of ℤ ℤ)
393 ((TopCat.toSSet.obj (TopCat.sphere 1)).δ (1 : Fin 2)
394 CircleFundamentalSimplex.fundamentalSphereOneSingularOneSimplex) =
395 0
396 rw [CircleFundamentalSimplex.fundamentalSphereOneSingularOneSimplex_faces_eq]
397 simp
398
399/-- Mathlib's homology infrastructure supplies the degree-`1` homology object
400for the imported singular chain complex. -/
401theorem sphereOneSingularIntChainComplexHasHomologyOne :
402 sphereOneSingularIntChainComplex.HasHomology 1 :=
403 inferInstance
404
405/-- The final strict T8 singular-homology target is definitionally the degree-`1`
406homology of the imported singular chain complex. -/
407theorem singularHomologyFunctorSphereOneInt_eq_homologyOne :
408 (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
409 (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere 1)) =
410 sphereOneSingularIntChainComplex.homology 1 :=
411 rfl
412
413/-- Isomorphism form of `singularHomologyFunctorSphereOneInt_eq_homologyOne`. -/
414def singularHomologyFunctorSphereOneIntIsoHomologyOne :
415 (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
416 (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere 1)) ≅
417 sphereOneSingularIntChainComplex.homology 1 :=
418 Iso.refl _
419
420/-- A degree-`1` quasi-isomorphism from Mathlib's singular chains on
421`TopCat.sphere 1` to the ordinary cellular circle model computes the exact
422`singularHomologyFunctor` target as `ℤ`.
423
424This is not the missing geometric theorem itself; it isolates it as the single
425remaining chain-level bridge `QuasiIsoAt f 1`. -/
426def singularHomologyFunctorSphereOneIntIsoOfQuasiIsoAtOrdinaryCellular
427 (f : sphereOneSingularIntChainComplex ⟶ ordinaryCellularCircleChainModel)
428 [sphereOneSingularIntChainComplex.HasHomology 1] [QuasiIsoAt f 1] :
429 (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
430 (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere 1)) ≅ ModuleCat.of ℤ ℤ :=
431 isoOfQuasiIsoAt f 1 ≪≫ ordinaryCellularCircleChainModelH1IsoInt
432
433/-- Proposition-facing form of
434`singularHomologyFunctorSphereOneIntIsoOfQuasiIsoAtOrdinaryCellular`. -/
435theorem singularHomologyFunctorSphereOneIntNonemptyIsoOfQuasiIsoAtOrdinaryCellular
436 (f : sphereOneSingularIntChainComplex ⟶ ordinaryCellularCircleChainModel)
437 [sphereOneSingularIntChainComplex.HasHomology 1] [QuasiIsoAt f 1] :
438 Nonempty
439 ((((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
440 (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere 1)) ≅ ModuleCat.of ℤ ℤ) :=
441 ⟨singularHomologyFunctorSphereOneIntIsoOfQuasiIsoAtOrdinaryCellular f⟩
442
443/-- The same conditional bridge stated in the exact proposition shape used by
444`MathlibCohomologyBridge`. The bridge file stays untouched until the
445chain-level quasi-isomorphism is proved unconditionally. -/
446theorem circleH1ZIsoIntOfQuasiIsoAtOrdinaryCellular
447 (f : sphereOneSingularIntChainComplex ⟶ ordinaryCellularCircleChainModel)
448 [sphereOneSingularIntChainComplex.HasHomology 1] [QuasiIsoAt f 1] :
449 MathlibCohomologyBridge.circleH1ZIsoInt :=
450 singularHomologyFunctorSphereOneIntNonemptyIsoOfQuasiIsoAtOrdinaryCellular f
451
452/-- A degree-local chain homotopy equivalence between Mathlib's singular chains
453on `TopCat.sphere 1` and the ordinary cellular circle model computes the exact
454singular homology target as `ℤ`. This is weaker in hypotheses than the global
455quasi-isomorphism route: it only requires degree-`1` homology for the singular
456chain complex. -/
457def singularHomologyFunctorSphereOneIntIsoOfHomotopyEquivOrdinaryCellularAtOne
458 (e : HomotopyEquiv sphereOneSingularIntChainComplex ordinaryCellularCircleChainModel)
459 [sphereOneSingularIntChainComplex.HasHomology 1] :
460 (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
461 (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere 1)) ≅ ModuleCat.of ℤ ℤ :=
462 e.toHomologyIso 1 ≪≫ ordinaryCellularCircleChainModelH1IsoInt
463
464/-- The degree-local homotopy-equivalence bridge stated in the exact proposition
465shape used by `MathlibCohomologyBridge`. -/
466theorem circleH1ZIsoIntOfHomotopyEquivOrdinaryCellularAtOne
467 (e : HomotopyEquiv sphereOneSingularIntChainComplex ordinaryCellularCircleChainModel)
468 [sphereOneSingularIntChainComplex.HasHomology 1] :
469 MathlibCohomologyBridge.circleH1ZIsoInt :=
470 ⟨singularHomologyFunctorSphereOneIntIsoOfHomotopyEquivOrdinaryCellularAtOne e⟩
471
472/-- Proposition-facing closure target: it is enough to produce a chain homotopy
473equivalence between Mathlib's singular chains on `TopCat.sphere 1` and the
474ordinary cellular circle model. -/
475theorem circleH1ZIsoIntOfNonemptyHomotopyEquivOrdinaryCellularAtOne
476 (h : Nonempty
477 (HomotopyEquiv sphereOneSingularIntChainComplex ordinaryCellularCircleChainModel))
478 [sphereOneSingularIntChainComplex.HasHomology 1] :
479 MathlibCohomologyBridge.circleH1ZIsoInt := by
480 rcases h with ⟨e⟩
481 exact circleH1ZIsoIntOfHomotopyEquivOrdinaryCellularAtOne e
482
483/-- The remaining geometric chain-level bridge for the strict T8 circle-H1
484closure: Mathlib's singular chain complex for `TopCat.sphere 1` is chain
485homotopy equivalent to the ordinary two-cell cellular circle model. -/
486def circleH1GeometricBridge : Prop :=
487 Nonempty
488 (HomotopyEquiv sphereOneSingularIntChainComplex ordinaryCellularCircleChainModel)
489
490/-- The geometric bridge immediately computes the exact imported Mathlib
491singular-H1 object as `ℤ`. -/
492theorem singularHomologyFunctorSphereOneIntNonemptyIsoOfGeometricBridge
493 (h : circleH1GeometricBridge) :
494 Nonempty
495 ((((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
496 (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere 1)) ≅ ModuleCat.of ℤ ℤ) := by
497 rcases h with ⟨e⟩
498 exact ⟨singularHomologyFunctorSphereOneIntIsoOfHomotopyEquivOrdinaryCellularAtOne e⟩
499
500/-- The geometric bridge immediately closes the exact proposition used by
501`MathlibCohomologyBridge`. -/
502theorem circleH1ZIsoIntOfGeometricBridge
503 (h : circleH1GeometricBridge) :
504 MathlibCohomologyBridge.circleH1ZIsoInt := by
505 rcases h with ⟨e⟩
506 exact circleH1ZIsoIntOfHomotopyEquivOrdinaryCellularAtOne e
507
508/-- The geometric bridge fills the Mathlib computation certificate used by the
509strict T8 handoff. -/
510theorem circleH1MathlibComputationOfGeometricBridge
511 (h : circleH1GeometricBridge) :
512 MathlibCohomologyBridge.CircleH1MathlibComputation :=
513 MathlibCohomologyBridge.circleH1MathlibComputation_of_iso_int
514 (circleH1ZIsoIntOfGeometricBridge h)
515
516/-- The geometric bridge also builds the Mathlib circle-linking backend object. -/
517theorem mathlibCircleLinkingBackendOfGeometricBridge
518 (h : circleH1GeometricBridge) :
519 Nonempty MathlibCohomologyBridge.MathlibCircleLinkingBackend :=
520 MathlibCohomologyBridge.mathlibCircleLinkingBackend_of_circleH1ZIsoInt
521 (circleH1ZIsoIntOfGeometricBridge h)
522
523/-- A chain homotopy equivalence between Mathlib's singular chains on
524`TopCat.sphere 1` and the ordinary cellular circle model is enough to compute
525the exact singular homology target as `ℤ`. -/
526def singularHomologyFunctorSphereOneIntIsoOfHomotopyEquivOrdinaryCellular
527 (e : HomotopyEquiv sphereOneSingularIntChainComplex ordinaryCellularCircleChainModel)
528 [∀ i, sphereOneSingularIntChainComplex.HasHomology i] :
529 (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj
530 (ModuleCat.of ℤ ℤ)).obj (TopCat.sphere 1)) ≅ ModuleCat.of ℤ ℤ :=
531 singularHomologyFunctorSphereOneIntIsoOfQuasiIsoAtOrdinaryCellular e.hom
532
533/-- The same homotopy-equivalence bridge stated in the exact proposition shape
534used by `MathlibCohomologyBridge`. -/
535theorem circleH1ZIsoIntOfHomotopyEquivOrdinaryCellular
536 (e : HomotopyEquiv sphereOneSingularIntChainComplex ordinaryCellularCircleChainModel)
537 [∀ i, sphereOneSingularIntChainComplex.HasHomology i] :
538 MathlibCohomologyBridge.circleH1ZIsoInt :=
539 circleH1ZIsoIntOfQuasiIsoAtOrdinaryCellular e.hom
540
541end
542
543end CircleH1Computation
544end Foundation
545end IndisputableMonolith
546