OAI/CategoryTheory/Thomason/SimplexColimits.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Simplex Colimits.

  1. abbrev OAI.Thomason.SimplexIndex line 15
  2. abbrev OAI.Thomason.SimplexVertices line 18
  3. def OAI.Thomason.simplexVertexOrder line 21
  4. def OAI.Thomason.simplexVertexMap line 25
  5. lemma OAI.Thomason.simplexVertexOrder_natural line 29
  6. def OAI.Thomason.liftedSimplexOrder line 38
  7. lemma OAI.Thomason.isoNerve_natural line 42
  8. def OAI.Thomason.simplexCategorificationIso line 53
  9. lemma OAI.Thomason.simplexCategorificationIso_natural line 58
  10. lemma OAI.Thomason.simplexVertexOrder_nerve line 76
  11. def OAI.Thomason.posetSimplexDiagram line 83
  12. def OAI.Thomason.posetSimplexDiagramIso line 100
  13. def OAI.Thomason.posetSimplexCocone line 105
  14. lemma OAI.Thomason.posetSimplexCocone_leg line 124
  15. def OAI.Thomason.posetSimplexIsColimit line 132
  16. def OAI.Thomason.posetSimplexOverDiagram line 142
  17. def OAI.Thomason.posetSimplexOverCocone line 159
  18. def OAI.Thomason.posetSimplexOverIsColimit line 167
  19. def OAI.Thomason.posetSimplexFiberIsColimit line 171
  20. lemma OAI.Thomason.finiteFiberAssembly_natural line 181
  21. def OAI.Thomason.posetFiberInverseCocone line 225
  22. def OAI.Thomason.posetCategorificationFiberInverse line 238
  23. lemma OAI.Thomason.posetCategorificationFiberInverse_fac line 244
  24. lemma OAI.Thomason.posetCategorificationFiberInverse_map line 254
  25. def OAI.Thomason.simplexIndexMap line 271
  26. lemma OAI.Thomason.posetCategorificationFiberMap_inverse line 275
  27. def OAI.Thomason.posetCategorificationFiberIso line 315
  28. theorem OAI.Thomason.posetCategorificationFiberMap_isIso line 324
  29. theorem OAI.Thomason.posetCategorificationFiniteFiberMap_isIso line 328
  30. lemma OAI.Thomason.NormalizedChains.supportedOn_of_le_positive line 349
  31. lemma OAI.Thomason.NormalizedChains.supportedOn_of_add_positive line 357
  32. lemma OAI.Thomason.NormalizedChains.vertex_supportedOn_iff line 364
  33. lemma OAI.Thomason.NormalizedChains.edge_supportedOn_iff line 372
  34. lemma OAI.Thomason.NormalizedChains.simplexAtom_source_zero line 383
  35. lemma OAI.Thomason.NormalizedChains.simplexAtom_vertices_supported line 388
  36. lemma OAI.Thomason.NormalizedChains.table_finish_supported line 411
  37. lemma OAI.Thomason.NormalizedChains.oriental_support_of_target line 421
  38. lemma OAI.Thomason.NormalizedChains.table_support_of_target_finite line 478
  39. lemma OAI.Thomason.NormalizedChains.table_finite_support line 504
  40. lemma OAI.Thomason.NormalizedChains.table_support_of_target line 525
  41. lemma OAI.Thomason.NormalizedChains.wordBoundary_pair line 544
  42. lemma OAI.Thomason.NormalizedChains.positive_peel line 547
  43. lemma OAI.Thomason.NormalizedChains.positive_unit_flow_outgoing line 557
  44. lemma OAI.Thomason.NormalizedChains.positive_unit_flow_chain line 587
  45. lemma OAI.Thomason.NormalizedChains.table_finite_chain_support line 645
  46. lemma OAI.Thomason.NormalizedChains.table_truncate_supported line 672
  47. lemma OAI.Thomason.NormalizedChains.table_comp_supported_factors line 682