OAI/CategoryTheory/Thomason/SubdivisionNerves.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Subdivision Nerves.

  1. def OAI.Thomason.Subdivision.initialFlag line 16
  2. lemma OAI.Thomason.Subdivision.chainLast_initialFlag line 32
  3. def OAI.Thomason.Subdivision.simplexLastVertexSection line 45
  4. lemma OAI.Thomason.Subdivision.simplexLastVertexSection_comp line 49
  5. def OAI.Thomason.Subdivision.lastVertexSection line 71
  6. lemma OAI.Thomason.Subdivision.lastVertexSection_comp line 75
  7. instance OAI.Thomason.Subdivision.exComparison_mono line 81
  8. def OAI.Thomason.Subdivision.simplexChain line 119
  9. lemma OAI.Thomason.Subdivision.mem_simplexChain line 133
  10. lemma OAI.Thomason.Subdivision.simplexChain_le_iff line 138
  11. def OAI.Thomason.Subdivision.chainSimplex line 172
  12. lemma OAI.Thomason.Subdivision.simplexChain_chainSimplex line 188
  13. def OAI.Thomason.Subdivision.nerveNondegenerateChains line 203
  14. lemma OAI.Thomason.Subdivision.chains_map_injective line 229
  15. lemma OAI.Thomason.Subdivision.chains_map_le_iff line 236
  16. lemma OAI.Thomason.Subdivision.chains_map_surjective_on line 246
  17. def OAI.Thomason.Subdivision.simplexVertices line 275
  18. lemma OAI.Thomason.Subdivision.simplexVertices_injective line 280
  19. def OAI.Thomason.Subdivision.simplexVerticesEmbedding line 286
  20. def OAI.Thomason.Subdivision.sdNerveLeg line 294
  21. lemma OAI.Thomason.Subdivision.sdNerveLeg_mono line 299
  22. lemma OAI.Thomason.Subdivision.sdNerveLeg_naturality line 309
  23. def OAI.Thomason.Subdivision.sdNerveCocone line 325
  24. def OAI.Thomason.Subdivision.sdNerveMap line 337
  25. lemma OAI.Thomason.Subdivision.sdNerveMap_fac line 341
  26. def OAI.Thomason.Subdivision.sdNerveInjection line 360
  27. lemma OAI.Thomason.Subdivision.sdNerveInjection_comp line 365
  28. lemma OAI.Thomason.Subdivision.sdNerveInjection_naturality line 370
  29. lemma OAI.Thomason.Subdivision.sdNerveInjection_jointly_surjective line 379
  30. lemma OAI.Thomason.Subdivision.sdNerveLeg_app_injective line 396
  31. lemma OAI.Thomason.Subdivision.sdNerveLeg_obj_le line 404
  32. lemma OAI.Thomason.Subdivision.sdNerveLeg_surjective_on line 411
  33. lemma OAI.Thomason.Subdivision.sdNerveMap_app_surjective line 435
  34. lemma OAI.Thomason.Subdivision.sdNerveMap_app_injective line 446
  35. instance OAI.Thomason.Subdivision.sdNerveMap_isIso line 479
  36. def OAI.Thomason.Subdivision.sdNerveIso line 485
  37. def OAI.Thomason.Subdivision.sdNerveSimplexLeg line 502
  38. lemma OAI.Thomason.Subdivision.sdNerveSimplexLeg_naturality line 507
  39. lemma OAI.Thomason.Subdivision.sdNerveMap_fac_any line 523
  40. lemma OAI.Thomason.Subdivision.sdNerveSimplexLeg_comp line 534
  41. lemma OAI.Thomason.Subdivision.sdNerveMap_naturality line 550
  42. def OAI.Thomason.Subdivision.subcomplexN line 578
  43. lemma OAI.Thomason.Subdivision.subcomplexN_le_iff line 581
  44. lemma OAI.Thomason.Subdivision.subcomplexN_injective line 590
  45. lemma OAI.Thomason.Subdivision.subcomplexN_downward line 595
  46. def OAI.Thomason.Subdivision.AllowedChains line 603
  47. instance OAI.Thomason.Subdivision.(instance at line 606) line 606
  48. def OAI.Thomason.Subdivision.allowedChainInclusion line 608
  49. def OAI.Thomason.Subdivision.subcomplexChain line 611
  50. lemma OAI.Thomason.Subdivision.allowedChains_downward line 614
  51. def OAI.Thomason.Subdivision.allowedChainSimplex line 622
  52. lemma OAI.Thomason.Subdivision.subcomplexChain_allowedChainSimplex line 624
  53. def OAI.Thomason.Subdivision.subcomplexNondegenerateChains line 628
  54. def OAI.Thomason.Subdivision.sdSubcomplexVertices line 652
  55. def OAI.Thomason.Subdivision.sdSubcomplexLeg line 660
  56. abbrev OAI.Thomason.Subdivision.allowedChainsForget line 664
  57. lemma OAI.Thomason.Subdivision.allowedChainsForget_app_injective line 667
  58. instance OAI.Thomason.Subdivision.(instance at line 674) line 674
  59. lemma OAI.Thomason.Subdivision.sdSubcomplexLeg_forget line 679
  60. lemma OAI.Thomason.Subdivision.subcomplexN_monoOfLE line 688
  61. lemma OAI.Thomason.Subdivision.sdSubcomplexLeg_naturality line 694
  62. def OAI.Thomason.Subdivision.sdSubcomplexCocone line 701
  63. def OAI.Thomason.Subdivision.sdSubcomplexMap line 712
  64. lemma OAI.Thomason.Subdivision.sdSubcomplexMap_fac line 715
  65. def OAI.Thomason.Subdivision.sdSubcomplexInjection line 720
  66. lemma OAI.Thomason.Subdivision.sdSubcomplexInjection_comp line 725
  67. lemma OAI.Thomason.Subdivision.sdSubcomplexInjection_naturality line 730
  68. lemma OAI.Thomason.Subdivision.sdSubcomplexInjection_jointly_surjective line 739
  69. lemma OAI.Thomason.Subdivision.sdSubcomplexLeg_app_injective line 756
  70. lemma OAI.Thomason.Subdivision.sdSubcomplexLeg_obj_le line 762
  71. lemma OAI.Thomason.Subdivision.sdSubcomplexLeg_surjective_on line 767
  72. lemma OAI.Thomason.Subdivision.sdSubcomplexMap_app_surjective line 788
  73. lemma OAI.Thomason.Subdivision.sdSubcomplexMap_app_injective line 799
  74. instance OAI.Thomason.Subdivision.sdSubcomplexMap_isIso line 834
  75. def OAI.Thomason.Subdivision.sdSubcomplexIso line 840
  76. lemma OAI.Thomason.Subdivision.sdSubcomplexMap_naturality line 843