OAI/CategoryTheory/Thomason/HornRealization.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Horn Realization.

  1. lemma OAI.Thomason.WeakHomotopy.move_natural line 22
  2. lemma OAI.Thomason.WeakHomotopy.transport_natural line 30
  3. lemma OAI.Thomason.WeakHomotopy.groupMap_bijective_along_path line 41
  4. lemma OAI.Thomason.WeakHomotopy.groupMap_comp line 50
  5. lemma OAI.Thomason.WeakHomotopy.groupMap_id line 56
  6. lemma OAI.Thomason.WeakHomotopy.equivalence_id line 60
  7. lemma OAI.Thomason.WeakHomotopy.Equivalence.comp line 69
  8. lemma OAI.Thomason.WeakHomotopy.Equivalence.of_comp_right line 80
  9. lemma OAI.Thomason.WeakHomotopy.Equivalence.of_comp_left line 93
  10. lemma OAI.Thomason.WeakHomotopy.groupMap_homotopy line 112
  11. lemma OAI.Thomason.WeakHomotopy.Equivalence.of_homotopic line 130
  12. lemma OAI.Thomason.WeakHomotopy.bijective_of_retract line 162
  13. lemma OAI.Thomason.WeakHomotopy.basedGroupMap_bijective line 176
  14. lemma OAI.Thomason.WeakHomotopy.Equivalence.of_retract line 182
  15. def OAI.Thomason.topologicalWeakEquivalences line 240
  16. instance OAI.Thomason.topologicalWeakEquivalences_containsIdentities line 243
  17. instance OAI.Thomason.topologicalWeakEquivalences_isMultiplicative line 247
  18. instance OAI.Thomason.topologicalWeakEquivalences_hasTwoOutOfThreeProperty line 251
  19. instance OAI.Thomason.topologicalWeakEquivalences_isStableUnderRetracts line 256
  20. instance OAI.Thomason.simplicialWeakEquivalences_containsIdentities line 266
  21. instance OAI.Thomason.simplicialWeakEquivalences_isMultiplicative line 270
  22. instance OAI.Thomason.simplicialWeakEquivalences_hasTwoOutOfThreeProperty line 274
  23. instance OAI.Thomason.simplicialWeakEquivalences_isStableUnderRetracts line 278
  24. instance OAI.Thomason.thomasonWeakEquivalences_hasTwoOutOfThreeProperty line 282
  25. instance OAI.Thomason.thomasonWeakEquivalences_isStableUnderRetracts line 286
  26. instance OAI.Thomason.thomasonWeakEquivalencesFinite_hasTwoOutOfThreeProperty line 290
  27. instance OAI.Thomason.thomasonWeakEquivalencesFinite_isStableUnderRetracts line 295
  28. abbrev OAI.Thomason.TopologicalHorn.Simplex line 312
  29. def OAI.Thomason.TopologicalHorn.horn line 314
  30. def OAI.Thomason.TopologicalHorn.minimum line 317
  31. lemma OAI.Thomason.TopologicalHorn.minimum_nonneg line 320
  32. lemma OAI.Thomason.TopologicalHorn.minimum_le line 324
  33. lemma OAI.Thomason.TopologicalHorn.minimum_attained line 329
  34. lemma OAI.Thomason.TopologicalHorn.continuous_minimum line 335
  35. lemma OAI.Thomason.TopologicalHorn.minimum_eq_zero line 339
  36. def OAI.Thomason.TopologicalHorn.retractSimplex line 344
  37. lemma OAI.Thomason.TopologicalHorn.retractSimplex_zero line 374
  38. def OAI.Thomason.TopologicalHorn.retract line 381
  39. lemma OAI.Thomason.TopologicalHorn.retract_fixed line 386
  40. lemma OAI.Thomason.TopologicalHorn.map_injective_apply line 407
  41. lemma OAI.Thomason.TopologicalHorn.map_not_range line 412
  42. lemma OAI.Thomason.TopologicalHorn.map_succAbove_pivot line 417
  43. lemma OAI.Thomason.TopologicalHorn.map_succAbove_apply line 421
  44. lemma OAI.Thomason.TopologicalHorn.map_succAbove_injective line 426
  45. def OAI.Thomason.TopologicalHorn.drop line 433
  46. lemma OAI.Thomason.TopologicalHorn.map_drop line 447
  47. lemma OAI.Thomason.TopologicalHorn.drop_map line 457
  48. lemma OAI.Thomason.TopologicalHorn.double_map line 462
  49. def OAI.Thomason.TopologicalHorn.closedCoverPaste line 476
  50. lemma OAI.Thomason.TopologicalHorn.closedCoverPaste_apply line 490
  51. def OAI.Thomason.TopologicalHorn.singularValue line 511
  52. lemma OAI.Thomason.TopologicalHorn.singularValue_delta line 515
  53. lemma OAI.Thomason.TopologicalHorn.singular_faces_agree line 523
  54. def OAI.Thomason.TopologicalHorn.hornValue line 567
  55. lemma OAI.Thomason.TopologicalHorn.hornValue_face line 579
  56. theorem OAI.Thomason.TopologicalHorn.singular_kan line 589
  57. def OAI.Thomason.TopologicalHorn.simplexHomotopy line 626
  58. lemma OAI.Thomason.TopologicalHorn.simplexHomotopy_fixed line 655
  59. def OAI.Thomason.TopologicalHorn.simplexHomeoHomotopy line 662
  60. lemma OAI.Thomason.TopologicalHorn.simplexHomeoHomotopy_fixed line 669
  61. lemma OAI.Thomason.TopologicalHorn.equivalence_of_simplex_retract line 675
  62. def OAI.Thomason.TopologicalHorn.realizationHornRetraction line 684
  63. lemma OAI.Thomason.TopologicalHorn.realizationHornRetraction_comp line 693
  64. theorem OAI.Thomason.TopologicalHorn.horn_weak_equivalence line 705