OAI/CategoryTheory/Thomason/DimensionOne.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Dimension One.

  1. lemma OAI.Thomason.transferred_right_proper line 14
  2. lemma OAI.Thomason.left_preserves_cofibrations line 22
  3. lemma OAI.Thomason.leftOne_preserves_weak line 35
  4. structure OAI.Thomason.BoundaryProperness.PosetAttachment line 58
  5. abbrev OAI.Thomason.BoundaryProperness.PosetAttachment.arrow line 68
  6. def OAI.Thomason.BoundaryProperness.Admissible line 70
  7. instance OAI.Thomason.BoundaryProperness.(instance at line 73) line 73
  8. lemma OAI.Thomason.BoundaryProperness.boundary_admissible line 78
  9. def OAI.Thomason.BoundaryProperness.sumData line 97
  10. def OAI.Thomason.BoundaryProperness.posetCoprodIso line 105
  11. def OAI.Thomason.BoundaryProperness.oldCoprodIso line 110
  12. lemma OAI.Thomason.BoundaryProperness.posetCoprodIso_ι line 114
  13. lemma OAI.Thomason.BoundaryProperness.oldCoprodIso_ι line 121
  14. lemma OAI.Thomason.BoundaryProperness.coprod_inc line 133
  15. instance OAI.Thomason.BoundaryProperness.admissible_coproducts line 159
  16. instance OAI.Thomason.BoundaryProperness.(instance at line 182) line 182
  17. lemma OAI.Thomason.BoundaryProperness.poset_attachment_invariance line 184
  18. lemma OAI.Thomason.BoundaryProperness.admissible_pushout_mono line 239
  19. lemma OAI.Thomason.BoundaryProperness.admissible_pushout_weak line 256
  20. lemma OAI.Thomason.BoundaryProperness.coproduct_boundary_pushout_mono line 276
  21. lemma OAI.Thomason.BoundaryProperness.coproduct_boundary_pushout_weak line 284
  22. abbrev OAI.Thomason.BoundaryProperness.Cells line 306
  23. lemma OAI.Thomason.BoundaryProperness.weak_iso line 309
  24. lemma OAI.Thomason.BoundaryProperness.sequential_pushout_weak line 314
  25. lemma OAI.Thomason.BoundaryProperness.cofibration_pushout_weak line 417
  26. theorem OAI.Thomason.BoundaryProperness.one line 466
  27. def OAI.Thomason.exactEndpointOne line 483
  28. theorem OAI.Thomason.endpointOne line 504
  29. theorem OAI.Thomason.nerveDetection_allDimensions line 516

    Distinct definitions of this name: ComparatorChallenges/ThomasonModelStructures.lean:2463 (different declaration text). Qualify references as OAI.Thomason.nerveDetection_allDimensions@path.

  30. theorem OAI.Thomason.rightProper_allDimensions line 528
  31. theorem OAI.Thomason.boundaryGenerators_allDimensions line 535
  32. theorem OAI.Thomason.hornGenerators_allDimensions line 543
  33. theorem OAI.Thomason.secondWFS_allDimensions line 550
  34. structure OAI.Thomason.RightIntervalExtension line 568
  35. def OAI.Thomason.RightIntervalExtensionExists line 600
  36. def OAI.Thomason.GlobeComplex.tableRowMap line 613
  37. lemma OAI.Thomason.GlobeComplex.tableRowMap_d line 628
  38. lemma OAI.Thomason.GlobeComplex.tableRowMap_positive line 642
  39. def OAI.Thomason.GlobeComplex.tableMap line 652
  40. lemma OAI.Thomason.GlobeComplex.tableMap_nu_top line 662
  41. lemma OAI.Thomason.GlobeComplex.tableMap_nu line 678
  42. def OAI.Thomason.GlobeComplex.faceMap line 684
  43. lemma OAI.Thomason.GlobeComplex.faceMap_nu line 687
  44. lemma OAI.Thomason.GlobeComplex.chain_eq_topRows line 694
  45. lemma OAI.Thomason.GlobeComplex.hom_ext line 716
  46. def OAI.Thomason.GlobeComplex.homCellEquiv line 728
  47. lemma OAI.Thomason.GlobeComplex.faceMap_top line 743
  48. lemma OAI.Thomason.GlobeComplex.faceMap_self line 747
  49. lemma OAI.Thomason.GlobeComplex.faceMap_faceMap line 755
  50. def OAI.Thomason.GlobeComplex.counitInverse line 765
  51. lemma OAI.Thomason.GlobeComplex.counitInverse_nu line 768
  52. lemma OAI.Thomason.GlobeComplex.counitInverse_counit line 778
  53. lemma OAI.Thomason.GlobeComplex.counit_counitInverse line 787
  54. def OAI.Thomason.GlobeComplex.counitIso line 796