ComparatorChallenges/ThomasonModelStructures.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

112 declarations, 2 contain sorry, 0 declared as axioms

Definitions for the Thomason model structures and their Street-nerve detection statement.

  1. structure OAI.Thomason.OmegaCategory line 12

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:12 (same declaration text).

  2. structure OAI.Thomason.OmegaCategory.Functor line 62

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:62 (same declaration text).

  3. def OAI.Thomason.OmegaCategory.Functor.id line 79

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:79 (same declaration text).

  4. def OAI.Thomason.OmegaCategory.Functor.comp line 85

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:85 (same declaration text).

  5. instance OAI.Thomason.OmegaCategory.(instance at line 107) line 107
  6. def OAI.Thomason.OmegaCategory.IsTruncated line 112

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:112 (same declaration text).

  7. def OAI.Thomason.OmegaCategory.NCategory line 114

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:114 (same declaration text).

  8. instance OAI.Thomason.OmegaCategory.(instance at line 116) line 116
  9. structure OAI.Thomason.DirectedComplex line 129

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:129 (same declaration text).

  10. structure OAI.Thomason.DirectedComplex.Hom line 148

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:148 (same declaration text).

  11. def OAI.Thomason.DirectedComplex.Hom.id line 162

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:162 (same declaration text).

  12. def OAI.Thomason.DirectedComplex.Hom.comp line 168

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:168 (same declaration text).

  13. instance OAI.Thomason.DirectedComplex.(instance at line 183) line 183
  14. structure OAI.Thomason.DirectedComplex.Table line 189

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:189 (same declaration text).

  15. def OAI.Thomason.DirectedComplex.Table.truncate line 205

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:205 (same declaration text).

  16. def OAI.Thomason.DirectedComplex.Table.comp line 235

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:235 (same declaration text).

  17. def OAI.Thomason.DirectedComplex.nu line 309

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:309 (same declaration text).

  18. def OAI.Thomason.DirectedComplex.Hom.table line 510

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:510 (same declaration text).

  19. def OAI.Thomason.DirectedComplex.Hom.nu line 521

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:521 (same declaration text).

  20. def OAI.Thomason.DirectedComplex.nuFunctor line 559

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:559 (same declaration text).

  21. abbrev OAI.Thomason.NormalizedChains.Word line 579

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:579 (same declaration text).

  22. abbrev OAI.Thomason.NormalizedChains.Chains line 582

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:582 (same declaration text).

  23. def OAI.Thomason.NormalizedChains.bracket line 584

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:584 (same declaration text).

  24. def OAI.Thomason.NormalizedChains.prepend line 588

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:588 (same declaration text).

  25. def OAI.Thomason.NormalizedChains.wordBoundary line 591

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:591 (same declaration text).

  26. def OAI.Thomason.NormalizedChains.boundary line 595

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:595 (same declaration text).

  27. def OAI.Thomason.NormalizedChains.faces line 608

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:608 (same declaration text).

  28. def OAI.Thomason.NormalizedChains.grade line 620

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:620 (same declaration text).

  29. def OAI.Thomason.NormalizedChains.emptyWord line 623

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:623 (same declaration text).

  30. def OAI.Thomason.NormalizedChains.emptyCoefficient line 625

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:625 (same declaration text).

  31. def OAI.Thomason.NormalizedChains.Positive line 627

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:627 (same declaration text).

  32. def OAI.Thomason.NormalizedChains.positiveGrade line 629

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:629 (same declaration text).

  33. def OAI.Thomason.NormalizedChains.complex line 634

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:634 (same declaration text).

  34. def OAI.Thomason.NormalizedChains.map line 835

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:835 (same declaration text).

  35. def OAI.Thomason.NormalizedChains.complexMap line 846

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:846 (same declaration text).

  36. def OAI.Thomason.NormalizedChains.simplexComplexes line 1180

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1180 (same declaration text).

  37. def OAI.Thomason.orientals line 1261

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1261 (same declaration text).

  38. def OAI.Thomason.OmegaCategory.ulift line 1272

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1272 (same declaration text).

  39. def OAI.Thomason.OmegaCategory.uliftUp line 1308

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1308 (same declaration text).

  40. def OAI.Thomason.OmegaCategory.uliftDown line 1314

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1314 (same declaration text).

  41. def OAI.Thomason.OmegaCategory.uliftFunctor line 1328

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1328 (same declaration text).

  42. def OAI.Thomason.raisedOrientals line 1340

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1340 (same declaration text).

  43. structure OAI.Thomason.OmegaCategory.Presentation line 1351

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1351 (same declaration text).

  44. structure OAI.Thomason.OmegaCategory.Presentation.Interpretation line 1364

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1364 (same declaration text).

  45. inductive OAI.Thomason.OmegaCategory.CellTerm line 1377

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1377 (same declaration text).

  46. def OAI.Thomason.OmegaCategory.CellTerm.composeOrLeft line 1391

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1391 (same declaration text).

  47. def OAI.Thomason.OmegaCategory.CellTerm.eval line 1395

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1395 (same declaration text).

  48. def OAI.Thomason.OmegaCategory.Presentation.Equiv line 1409

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1409 (same declaration text).

  49. inductive OAI.Thomason.OmegaCategory.Presentation.Valid line 1412

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1412 (same declaration text).

  50. abbrev OAI.Thomason.OmegaCategory.Presentation.ValidTerm line 1418

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1418 (same declaration text).

  51. instance OAI.Thomason.OmegaCategory.Presentation.termSetoid line 1420

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1420 (same declaration text).

  52. abbrev OAI.Thomason.OmegaCategory.Presentation.Cells line 1431

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1431 (same declaration text).

  53. def OAI.Thomason.OmegaCategory.Presentation.evaluate line 1433

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1433 (same declaration text).

  54. def OAI.Thomason.OmegaCategory.CellTerm.dimension line 1444

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1444 (same declaration text).

  55. def OAI.Thomason.OmegaCategory.Presentation.sourceTerm line 1458

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1458 (same declaration text).

  56. def OAI.Thomason.OmegaCategory.Presentation.source line 1460

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1460 (same declaration text).

  57. def OAI.Thomason.OmegaCategory.Presentation.targetTerm line 1467

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1467 (same declaration text).

  58. def OAI.Thomason.OmegaCategory.Presentation.target line 1469

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1469 (same declaration text).

  59. def OAI.Thomason.OmegaCategory.Presentation.compTerm line 1476

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1476 (same declaration text).

  60. def OAI.Thomason.OmegaCategory.Presentation.comp line 1481

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1481 (same declaration text).

  61. abbrev OAI.Thomason.OmegaCategory.Presentation.category line 1515

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1515 (same declaration text).

  62. abbrev OAI.Thomason.OmegaCategory.colimitPresentation line 1655

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1655 (same declaration text).

  63. def OAI.Thomason.OmegaCategory.Presentation.generator line 1670

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1670 (same declaration text).

  64. def OAI.Thomason.OmegaCategory.colimitInclusion line 1681

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1681 (same declaration text).

  65. def OAI.Thomason.OmegaCategory.presentedCocone line 1736

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1736 (same declaration text).

  66. def OAI.Thomason.OmegaCategory.Presentation.lift line 1767

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1767 (same declaration text).

  67. def OAI.Thomason.OmegaCategory.colimitInterpretation line 1808

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1808 (same declaration text).

  68. def OAI.Thomason.OmegaCategory.presentedCoconeIsColimit line 1816

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1816 (same declaration text).

  69. instance OAI.Thomason.OmegaCategory.hasColimits line 1865

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1865 (same declaration text).

  70. instance OAI.Thomason.omegaHasSimplicialColimits line 1876

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1876 (same declaration text).

  71. def OAI.Thomason.categorification line 1880

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1880 (same declaration text).

  72. def OAI.Thomason.thomasonLeft line 1891

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1891 (same declaration text).

  73. def OAI.Thomason.streetNerve line 1902

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1902 (same declaration text).

  74. def OAI.Thomason.streetNerveMap line 1920

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1920 (same declaration text).

  75. def OAI.Thomason.streetNerveFunctor line 1925

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1925 (same declaration text).

  76. def OAI.Thomason.thomasonRight line 1937

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1937 (same declaration text).

  77. def OAI.Thomason.streetYonedaEquiv line 1948

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1948 (same declaration text).

  78. def OAI.Thomason.streetYonedaIso line 1956

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1956 (same declaration text).

  79. def OAI.Thomason.categorificationAdjunction line 1962

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1962 (same declaration text).

  80. def OAI.Thomason.thomasonAdjunction line 1975

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1975 (same declaration text).

  81. abbrev OAI.Thomason.OmegaCategory.truncationPresentation line 1986

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1986 (same declaration text).

  82. def OAI.Thomason.OmegaCategory.truncationUnit line 1991

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:1991 (same declaration text).

  83. def OAI.Thomason.OmegaCategory.truncation line 2046

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2046 (same declaration text).

  84. def OAI.Thomason.OmegaCategory.truncationLift line 2067

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2067 (same declaration text).

  85. def OAI.Thomason.OmegaCategory.truncationFunctor line 2082

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2082 (same declaration text).

  86. def OAI.Thomason.categorificationFinite line 2143

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2143 (same declaration text).

  87. def OAI.Thomason.thomasonLeftFinite line 2154

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2154 (same declaration text).

  88. def OAI.Thomason.streetNerveFinite line 2165

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2165 (same declaration text).

  89. def OAI.Thomason.thomasonRightFinite line 2177

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2177 (same declaration text).

  90. def OAI.Thomason.OmegaCategory.nCategoryInclusion line 2188

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2188 (same declaration text).

  91. def OAI.Thomason.OmegaCategory.truncationHomEquiv line 2192

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2192 (same declaration text).

  92. def OAI.Thomason.OmegaCategory.truncationAdjunction line 2244

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2244 (same declaration text).

  93. def OAI.Thomason.categorificationFiniteAdjunction line 2305

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2305 (same declaration text).

  94. def OAI.Thomason.thomasonFiniteAdjunction line 2317

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2317 (same declaration text).

  95. def OAI.Thomason.WeakHomotopy.loopMap line 2330

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2330 (same declaration text).

  96. def OAI.Thomason.WeakHomotopy.groupMap line 2333

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2333 (same declaration text).

  97. def OAI.Thomason.WeakHomotopy.componentsMap line 2343

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2343 (same declaration text).

  98. def OAI.Thomason.WeakHomotopy.Equivalence line 2347

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2347 (same declaration text).

  99. def OAI.Thomason.simplicialWeakEquivalences line 2359

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2359 (same declaration text).

  100. def OAI.Thomason.simplicialFibrations line 2362

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2362 (same declaration text).

  101. structure OAI.Thomason.KanQuillenModel line 2372

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2372 (same declaration text).

  102. def OAI.Thomason.LeftProperFor line 2378

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2378 (same declaration text).

  103. def OAI.Thomason.RightProperFor line 2383

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2383 (same declaration text).

  104. def OAI.Thomason.FibrantFor line 2388

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2388 (same declaration text).

  105. def OAI.Thomason.boundaryImages line 2391

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2391 (same declaration text).

  106. def OAI.Thomason.hornImages line 2394

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2394 (same declaration text).

  107. structure OAI.Thomason.ExactModelEndpoint line 2397

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2397 (same declaration text).

  108. def OAI.Thomason.FullMain line 2430

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2430 (same declaration text).

  109. def OAI.Thomason.thomasonWeakEquivalences line 2445

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2445 (same declaration text).

  110. def OAI.Thomason.thomasonWeakEquivalencesFinite line 2448

    Also declared: OAI/CategoryTheory/Thomason/Definitions.lean:2448 (same declaration text).

  111. theorem OAI.Thomason.main Challenge statement: Thomason model structures in all strict higher dimensions sorry line 2460

    L4DEL explanation

    The formalization proves the higher-dimensional Thomason model-structure theorem for small strict globular $n$-categories in every positive finite dimension and in dimension $\omega$. Each category has the stated proper combinatorial model structure, Quillen equivalent to simplicial sets through the twice-subdivided categorification and twice-extended Street nerve adjunction. The selected statements also identify weak equivalences by the Street nerve in all these dimensions. Thus the constructions model the homotopy theory of spaces throughout the stated range.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.CategoryTheory.Thomason.RankedFaithfulness as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/CategoryTheory/Thomason/RankedFaithfulness.lean:683 (different declaration text). Qualify references as OAI.Thomason.main@path.

    theorem Thomason.main : OAI.Thomason.FullMain.{u} := by
…
  112. theorem OAI.Thomason.nerveDetection_allDimensions Challenge statement: Thomason model structures in all strict higher dimensions sorry line 2463

    L4DEL explanation

    The formalization proves the higher-dimensional Thomason model-structure theorem for small strict globular $n$-categories in every positive finite dimension and in dimension $\omega$. Each category has the stated proper combinatorial model structure, Quillen equivalent to simplicial sets through the twice-subdivided categorification and twice-extended Street nerve adjunction. The selected statements also identify weak equivalences by the Street nerve in all these dimensions. Thus the constructions model the homotopy theory of spaces throughout the stated range.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.CategoryTheory.Thomason.RankedFaithfulness as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/CategoryTheory/Thomason/DimensionOne.lean:516 (different declaration text). Qualify references as OAI.Thomason.nerveDetection_allDimensions@path.

    theorem Thomason.nerveDetection_allDimensions :
    OAI.Thomason.thomasonWeakEquivalences.{u} =
      OAI.Thomason.simplicialWeakEquivalences.inverseImage OAI.Thomason.streetNerveFunctor ∧
    ∀ n : ℕ, OAI.Thomason.thomasonWeakEquivalencesFinite.{u} n =
      OAI.Thomason.simplicialWeakEquivalences.inverseImage (OAI.Thomason.streetNerveFinite n) := by
…

    Mentions: OAI.Thomason.streetNerveFunctor, OAI.Thomason.streetNerveFinite