OAI/CategoryTheory/Thomason/CubicalRecognition.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Cubical Recognition.

  1. def OAI.Thomason.GeometricRecognition.top_homotopy_rel_pre line 16
  2. lemma OAI.Thomason.GeometricRecognition.cubical_relative_cancel line 24
  3. structure OAI.Thomason.GeometricRecognition.CubicalPair line 47
  4. def OAI.Thomason.GeometricRecognition.CubicalPair.refine line 52
  5. lemma OAI.Thomason.GeometricRecognition.polyToRealization_natural line 78
  6. def OAI.Thomason.GeometricRecognition.polyRealize line 88
  7. lemma OAI.Thomason.GeometricRecognition.polyRealize_post line 91
  8. lemma OAI.Thomason.GeometricRecognition.polyRealize_pre line 97
  9. lemma OAI.Thomason.GeometricRecognition.polyRealize_order line 107
  10. lemma OAI.Thomason.GeometricRecognition.poly_realization_homotopy_rel line 113
  11. lemma OAI.Thomason.GeometricRecognition.map_constantOrder line 128
  12. lemma OAI.Thomason.GeometricRecognition.polyRealize_constant line 142
  13. lemma OAI.Thomason.GeometricRecognition.geometric_relative_order_cancel line 149
  14. lemma OAI.Thomason.GeometricRecognition.poly_rel_pre_pair line 198
  15. lemma OAI.Thomason.GeometricRecognition.pair_refinement_cancel line 217
  16. lemma OAI.Thomason.GeometricRecognition.finite_cubical_realization_faithful line 231
  17. lemma OAI.Thomason.GeometricRecognition.realize_const_apply line 297
  18. lemma OAI.Thomason.GeometricRecognition.polyRealize_const line 308
  19. lemma OAI.Thomason.GeometricRecognition.weak_cubical_injective line 312
  20. lemma OAI.Thomason.GeometricRecognition.cubical_relative_surject line 344
  21. lemma OAI.Thomason.GeometricRecognition.poly_realize_boundary line 362
  22. lemma OAI.Thomason.GeometricRecognition.pointed_replacement_real_vertex line 371
  23. lemma OAI.Thomason.GeometricRecognition.last_barycentric_realization_rel line 383
  24. lemma OAI.Thomason.GeometricRecognition.full_pair_home_boundary line 421
  25. lemma OAI.Thomason.GeometricRecognition.finite_cubical_geometric_representative line 431
  26. lemma OAI.Thomason.GeometricRecognition.realVertex_natural line 510
  27. lemma OAI.Thomason.GeometricRecognition.weak_cubical_surjective line 516
  28. abbrev OAI.Thomason.GeometricRecognition.cubePoset line 544
  29. abbrev OAI.Thomason.GeometricRecognition.cubeBoundary line 547
  30. abbrev OAI.Thomason.GeometricRecognition.cubeBoundaryInclusion line 550
  31. def OAI.Thomason.GeometricRecognition.actualCubicalPair line 553
  32. abbrev OAI.Thomason.GeometricRecognition.CubeMap line 578
  33. instance OAI.Thomason.GeometricRecognition.cubeBoundary_mono line 582
  34. def OAI.Thomason.GeometricRecognition.cubeMapSetoid line 585
  35. abbrev OAI.Thomason.GeometricRecognition.CubeClasses line 593
  36. def OAI.Thomason.GeometricRecognition.realizeCubeMap line 607
  37. lemma OAI.Thomason.GeometricRecognition.realizeCubeMap_homotopic line 615
  38. def OAI.Thomason.GeometricRecognition.realizeCubeClasses line 625
  39. theorem OAI.Thomason.GeometricRecognition.positive_realization_comparison line 629
  40. def OAI.Thomason.GeometricRecognition.cubeMapPost line 670
  41. def OAI.Thomason.GeometricRecognition.cubeClassesMap line 674
  42. theorem OAI.Thomason.GeometricRecognition.weak_positive_classes_bijective line 680