OAI/CategoryTheory/Thomason/Gray/TripleGlobeCylinderSource.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thomason.Construction.CubeGrid.cell line 22
2. theorem OAI.Thomason.Construction.CubeGrid.cell_isClosed line 27
3. theorem OAI.Thomason.Construction.CubeGrid.cell_nonempty line 40
4. theorem OAI.Thomason.Construction.CubeGrid.interval_mem line 49
5. theorem OAI.Thomason.Construction.CubeGrid.cover line 70

   Source documentation

   The finite closed grid covers the entire cube.

   theorem cover (n m : ℕ) : ⋃ k, cell n m k = Set.univ := by
   …

   Mentions: OAI.Thomason.Construction.CubeGrid.cell

6. theorem OAI.Thomason.Construction.CubeGrid.cell_diam line 78

   Source documentation

   In the product metric every grid cell has mesh at most 1/(m+1).

   theorem cell_diam (n m : ℕ) (k : Fin n → Fin (m+1)) :
       Metric.diam (cell n m k) ≤ 1 / ((m : ℝ)+1) := by
   …

   Mentions: OAI.Thomason.Construction.CubeGrid.cell

7. theorem OAI.Thomason.Construction.PrismBarycentric.exists_maximal_prism_simplex line 110

   Source documentation

   The maximal simplices cover the actual realization of the standard prism.

   theorem exists_maximal_prism_simplex (n : ℕ) (x : SSet.toTop.obj (prism n)) :
       ∃ (j : Fin (n+1)) (u : StdSimplex ℝ (Fin (n+2))),
         (RealizationPrism.leg (prism n) (simplexIndex j)).hom (ULift.up u) = x := by
   …

   Mentions: OAI.Thomason.Construction.PrismBarycentric.prism, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.PrismBarycentric.simplexIndex

8. theorem OAI.Thomason.Construction.PrismBarycentric.standardPrism_surjective line 143

   Source documentation

   Every point of the standard simplicial prism is obtained by the constructed continuous prism map, including points on degenerate and shared faces.

   theorem standardPrism_surjective (n : ℕ) : Function.Surjective (standardPrism n) := by
   …

   Mentions: OAI.Thomason.Construction.PrismBarycentric.standardPrism

9. theorem OAI.Thomason.Construction.RealizedCylinder.comparison_surjective line 175

   Source documentation

   The comparison covers every point of the actual simplicial cylinder.

   theorem comparison_surjective (K : SSet.{0}) : Function.Surjective (comparison K).hom := by
   …

   Mentions: OAI.Thomason.Construction.RealizedCylinder.comparison

10. def OAI.Thomason.Construction.RealizedCylinder.coordinates line 200

    Source documentation

    The two actual realized cylinder coordinates.

    def coordinates (K : SSet.{0}) :
        SSet.toTop.obj (K ⊗ Δ[1]) ⟶ TopologicalInterval.cylinder.obj (SSet.toTop.obj K) :=
    …

11. theorem OAI.Thomason.Construction.RealizedCylinder.coordinates_comparison line 210

    Source documentation

    The explicit coordinate map is a left inverse to the comparison.

    theorem coordinates_comparison (K : SSet.{0}) :
        Function.LeftInverse (coordinates K).hom (comparison K).hom := by
    …

    Mentions: OAI.Thomason.Construction.RealizedCylinder.coordinates, OAI.Thomason.Construction.RealizedCylinder.comparison

12. theorem OAI.Thomason.Construction.RealizedCylinder.comparison_coordinates line 218

    Source documentation

    Surjectivity gives the other inverse equation for the same explicit map.

    theorem comparison_coordinates (K : SSet.{0}) :
        Function.RightInverse (coordinates K).hom (comparison K).hom :=
    …

    Mentions: OAI.Thomason.Construction.RealizedCylinder.coordinates, OAI.Thomason.Construction.RealizedCylinder.comparison

13. def OAI.Thomason.Construction.RealizedCylinder.cylinderHomeomorph line 224

    Source documentation

    The natural comparison is an actual homeomorphism, with the proved coordinate formulas as its inverse.

    def cylinderHomeomorph (K : SSet.{0}) :
        TopologicalInterval.cylinder.obj (SSet.toTop.obj K) ≃ₜ SSet.toTop.obj (K ⊗ Δ[1]) where
    …

14. def OAI.Thomason.Construction.RealizedCylinder.cylinderIso line 234

    Source documentation

    The same cylinder comparison as an isomorphism of actual topological spaces.

    def cylinderIso (K : SSet.{0}) :
        TopologicalInterval.cylinder.obj (SSet.toTop.obj K) ≅ SSet.toTop.obj (K ⊗ Δ[1]) :=
    …

15. theorem OAI.Thomason.Construction.TripleGlobeBasis.cylinderAtom_in_globe line 252
16. abbrev OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.model line 286
17. abbrev OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.Source line 287
18. abbrev OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.PieceCells line 288
19. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.comparison line 291
20. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.inl_comparison line 297
21. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.inr_comparison line 303
22. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.basisComparison line 309
23. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.comparison_imageCell line 313
24. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.globeChoice line 320
25. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.globeMap line 325
26. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.globeChoice_image line 330
27. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.globeMap_comparison line 334
28. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.globeMap_basisComparison line 345
29. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.imageCell_eq_of_basisComparison line 351
30. abbrev OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.atomBasis line 369
31. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.representativeIndex line 371
32. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.representativeCell line 374
33. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.representative_spec line 378
34. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.atomChoice line 385
35. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.atomLift line 389
36. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.atomLift_dimension line 392
37. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobeCylinder.atomLift_image line 401