OAI/CategoryTheory/Thomason/GlobularComplexes.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Globular Complexes.

  1. def OAI.Thomason.Subdivision.chainsSubtypeOrderIso line 19
  2. def OAI.Thomason.Subdivision.sdTwiceSubcomplexIso line 73
  3. def OAI.Thomason.Subdivision.sdTwiceNerveIso line 78
  4. lemma OAI.Thomason.Subdivision.sdTwiceSubcomplexIso_naturality line 83
  5. def OAI.Thomason.Subdivision.orderedSimplexSubcomplex line 98
  6. def OAI.Thomason.Subdivision.orderedSimplexSubcomplexIso line 102
  7. def OAI.Thomason.Subdivision.sdTwiceSimplexSubcomplexIso line 115
  8. def OAI.Thomason.Subdivision.sdTwiceSimplexIso line 122
  9. lemma OAI.Thomason.Subdivision.sdTwiceSimplexSubcomplexIso_naturality line 127
  10. def OAI.Thomason.GlobeComplex.chainModule line 153
  11. abbrev OAI.Thomason.GlobeComplex.Chain line 159
  12. def OAI.Thomason.GlobeComplex.mass line 161
  13. lemma OAI.Thomason.GlobeComplex.chain_zero line 166
  14. lemma OAI.Thomason.GlobeComplex.top_target_zero line 171
  15. def OAI.Thomason.GlobeComplex.delta line 174
  16. lemma OAI.Thomason.GlobeComplex.mass_delta line 179
  17. def OAI.Thomason.GlobeComplex.differential line 182
  18. lemma OAI.Thomason.GlobeComplex.differential_coordinate line 187
  19. def OAI.Thomason.GlobeComplex.positive line 195
  20. def OAI.Thomason.GlobeComplex.complex line 200
  21. lemma OAI.Thomason.GlobeComplex.complex_d_coordinate line 213
  22. lemma OAI.Thomason.GlobeComplex.mass_nonneg line 217
  23. lemma OAI.Thomason.GlobeComplex.coordinate_le_mass line 221
  24. lemma OAI.Thomason.GlobeComplex.mass_eq_zero_iff line 228
  25. def OAI.Thomason.GlobeComplex.basis line 240
  26. lemma OAI.Thomason.GlobeComplex.basis_coordinate line 254
  27. lemma OAI.Thomason.GlobeComplex.mass_basis line 258
  28. lemma OAI.Thomason.GlobeComplex.basis_positive line 262
  29. lemma OAI.Thomason.GlobeComplex.differential_basis line 268
  30. def OAI.Thomason.GlobeComplex.topRow line 293
  31. lemma OAI.Thomason.GlobeComplex.topRow_lt line 297
  32. lemma OAI.Thomason.GlobeComplex.topRow_eq line 300
  33. lemma OAI.Thomason.GlobeComplex.topRow_gt line 303
  34. def OAI.Thomason.GlobeComplex.topTable line 306
  35. lemma OAI.Thomason.GlobeComplex.topTable_bounded line 333
  36. lemma OAI.Thomason.GlobeComplex.table_boundary_coordinate line 344
  37. lemma OAI.Thomason.GlobeComplex.table_mass_eq line 351
  38. lemma OAI.Thomason.GlobeComplex.table_mass_zero line 357
  39. lemma OAI.Thomason.GlobeComplex.table_mass_step line 359
  40. lemma OAI.Thomason.GlobeComplex.table_mass_le_one line 367
  41. lemma OAI.Thomason.GlobeComplex.table_mass_antitone line 372
  42. lemma OAI.Thomason.GlobeComplex.positive_mass_one line 377
  43. lemma OAI.Thomason.GlobeComplex.table_has_top line 410
  44. lemma OAI.Thomason.GlobeComplex.table_lower_row line 439
  45. lemma OAI.Thomason.GlobeComplex.topRow_basis line 457
  46. lemma OAI.Thomason.GlobeComplex.table_classification line 463
  47. def OAI.Thomason.OmegaCategory.face line 506
  48. lemma OAI.Thomason.OmegaCategory.face_face line 509
  49. lemma OAI.Thomason.OmegaCategory.face_of_fixed line 524
  50. lemma OAI.Thomason.OmegaCategory.Functor.map_face line 530
  51. lemma OAI.Thomason.GlobeComplex.face_nu line 549
  52. lemma OAI.Thomason.GlobeComplex.top_face_mass line 552
  53. lemma OAI.Thomason.GlobeComplex.top_face_dimension line 561
  54. lemma OAI.Thomason.GlobeComplex.top_face_sign line 573
  55. lemma OAI.Thomason.GlobeComplex.face_evaluation_well_defined line 585
  56. def OAI.Thomason.GlobeComplex.evaluate line 596
  57. lemma OAI.Thomason.GlobeComplex.evaluate_face line 602
  58. lemma OAI.Thomason.GlobeComplex.evaluate_top line 618
  59. lemma OAI.Thomason.GlobeComplex.evaluate_truncate line 623
  60. lemma OAI.Thomason.GlobeComplex.composable_has_identity line 630
  61. def OAI.Thomason.GlobeComplex.lift line 643
  62. lemma OAI.Thomason.GlobeComplex.lift_top line 666
  63. lemma OAI.Thomason.GlobeComplex.functor_ext line 670
  64. def OAI.Thomason.GlobeComplex.globeIso line 679
  65. lemma OAI.Thomason.NormalizedChains.basisLambda_positive line 707
  66. lemma OAI.Thomason.NormalizedChains.atomCounitInverse_positive line 718
  67. lemma OAI.Thomason.NormalizedChains.oriental_lambdaCounit_rightInverse line 731
  68. lemma OAI.Thomason.NormalizedChains.counit_atomInverse line 739
  69. def OAI.Thomason.NormalizedChains.simplexCounitInverse line 743
  70. lemma OAI.Thomason.NormalizedChains.simplexCounitInverse_counit line 761
  71. lemma OAI.Thomason.NormalizedChains.counit_simplexCounitInverse line 767
  72. def OAI.Thomason.NormalizedChains.simplexCounitIso line 773