OAI/CategoryTheory/Thomason/SimplexAtoms.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Simplex Atoms.

  1. def OAI.Thomason.OmegaCategory.Functor.onCells line 16
  2. lemma OAI.Thomason.OmegaCategory.Functor.onCells_source line 19
  3. lemma OAI.Thomason.OmegaCategory.Functor.onCells_target line 23
  4. lemma OAI.Thomason.OmegaCategory.Functor.onCells_comp line 27
  5. def OAI.Thomason.OmegaCategory.Functor.lambdaRawMap line 33
  6. lemma OAI.Thomason.OmegaCategory.Functor.lambdaRawMap_single line 36
  7. lemma OAI.Thomason.OmegaCategory.Functor.lambdaRawMap_relations line 40
  8. def OAI.Thomason.OmegaCategory.Functor.lambdaMap line 55
  9. lemma OAI.Thomason.OmegaCategory.Functor.lambdaMap_gen line 58
  10. lemma OAI.Thomason.OmegaCategory.Functor.lambdaMap_d line 62
  11. lemma OAI.Thomason.OmegaCategory.Functor.lambdaMap_aug line 84
  12. lemma OAI.Thomason.OmegaCategory.Functor.lambdaMap_positive line 91
  13. def OAI.Thomason.OmegaCategory.Functor.linearization line 100
  14. lemma OAI.Thomason.OmegaCategory.Functor.lambdaMap_id line 106
  15. lemma OAI.Thomason.OmegaCategory.Functor.lambdaMap_comp line 113
  16. def OAI.Thomason.OmegaCategory.linearizationFunctor line 131
  17. lemma OAI.Thomason.OmegaCategory.lambda_add_ext line 150
  18. lemma OAI.Thomason.DirectedComplex.Table.truncate_top_row line 168
  19. lemma OAI.Thomason.DirectedComplex.Table.row_above_fixed line 172
  20. lemma OAI.Thomason.DirectedComplex.Table.row_top_fixed line 177
  21. def OAI.Thomason.DirectedComplex.lambdaCounitRaw line 186
  22. lemma OAI.Thomason.DirectedComplex.lambdaCounitRaw_single line 189
  23. lemma OAI.Thomason.DirectedComplex.lambdaCounitRaw_relations line 193
  24. def OAI.Thomason.DirectedComplex.lambdaCounitMap line 206
  25. lemma OAI.Thomason.DirectedComplex.lambdaCounitMap_gen line 209
  26. lemma OAI.Thomason.DirectedComplex.lambdaCounitMap_d line 213
  27. lemma OAI.Thomason.DirectedComplex.lambdaCounitMap_aug line 227
  28. lemma OAI.Thomason.DirectedComplex.lambdaCounitMap_positive line 235
  29. def OAI.Thomason.DirectedComplex.lambdaCounit line 244
  30. def OAI.Thomason.lambdaNuForward line 260
  31. def OAI.Thomason.lambdaNuBackward line 264
  32. lemma OAI.Thomason.lambdaNuBackward_gen line 268
  33. lemma OAI.Thomason.lambdaNu_left_inv line 274
  34. lemma OAI.Thomason.lambdaNu_right_inv line 288
  35. def OAI.Thomason.lambdaNuHomEquiv line 309
  36. lemma OAI.Thomason.lambdaNu_backward_natural line 328
  37. lemma OAI.Thomason.lambdaNu_forward_natural line 342
  38. def OAI.Thomason.lambdaNuAdjunction line 351
  39. lemma OAI.Thomason.NormalizedChains.boundary_prepend_supported line 371
  40. lemma OAI.Thomason.NormalizedChains.prepend_positive line 387
  41. lemma OAI.Thomason.NormalizedChains.prepend_mem_supportedOn line 390
  42. lemma OAI.Thomason.NormalizedChains.grade_zero_eq_empty line 403
  43. lemma OAI.Thomason.NormalizedChains.boundary_prepend_zero line 418
  44. def OAI.Thomason.NormalizedChains.coneTable line 425
  45. lemma OAI.Thomason.NormalizedChains.coneTable_row_zero line 496
  46. lemma OAI.Thomason.NormalizedChains.coneTable_row_succ line 501
  47. lemma OAI.Thomason.NormalizedChains.coneTable_supported line 508
  48. lemma OAI.Thomason.NormalizedChains.coneTable_dimension line 523
  49. lemma OAI.Thomason.NormalizedChains.supportedOn_mono line 569
  50. structure OAI.Thomason.NormalizedChains.SimplexAtomData line 574
  51. def OAI.Thomason.NormalizedChains.SimplexAtomData.singleton line 582
  52. def OAI.Thomason.NormalizedChains.SimplexAtomData.cone line 591
  53. def OAI.Thomason.NormalizedChains.simplexAtom line 621
  54. lemma OAI.Thomason.NormalizedChains.basis_has_atom line 627
  55. lemma OAI.Thomason.NormalizedChains.normalized_lambdaCounit_surjective line 644
  56. lemma OAI.Thomason.NormalizedChains.positive_cycle_zero line 705
  57. lemma OAI.Thomason.NormalizedChains.table_endomorphism_identity line 719
  58. lemma OAI.Thomason.NormalizedChains.table_source_le_target line 751
  59. lemma OAI.Thomason.NormalizedChains.coneTable_one_source line 781
  60. lemma OAI.Thomason.NormalizedChains.coneTable_one_target line 802