OAI/CategoryTheory/Thomason/Simplicial/AcyclicKanSimplexLifting.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

A common carrier for the prescribed boundary comparison

Both the label approximation and the exact iterated last-vertex boundary remain in the original continuous boundary carrier. The ordered homotopy between them therefore remains in that same carrier at every time.

  1. theorem OAI.Thomason.Construction.SubdivisionBarycentric.iterated_realization_boundary line 39
  2. theorem OAI.Thomason.Construction.SubdivisionBarycentric.label_boundary_carrier line 47
  3. theorem OAI.Thomason.Construction.SubdivisionBarycentric.greatest_boundary_carrier line 71
  4. def OAI.Thomason.Construction.SubdivisionBarycentric.boundaryLabelOrderMap line 87
  5. theorem OAI.Thomason.Construction.SubdivisionBarycentric.boundaryLabelOrderMap_comp line 92
  6. theorem OAI.Thomason.Construction.SubdivisionBarycentric.boundaryLabelOrderMap_le line 100
  7. theorem OAI.Thomason.Construction.SubdivisionBarycentric.boundaryLabelOrderMap_carrier line 113
  8. theorem OAI.Thomason.Construction.SubdivisionBarycentric.boundaryOrderHomotopy_carrier line 135
  9. def OAI.Thomason.Construction.SubdivisionBarycentric.boundaryBarycentricMap line 183
  10. def OAI.Thomason.Construction.SubdivisionBarycentric.boundaryApproximationHomotopy line 202
  11. theorem OAI.Thomason.Construction.SubdivisionBarycentric.boundaryApproximationHomotopy_support line 218
  12. def OAI.Thomason.Construction.SubdivisionBarycentric.boundaryLastVertexHomotopy line 241
  13. theorem OAI.Thomason.Construction.SubdivisionBarycentric.boundaryLastVertexHomotopy_support line 253
  14. def OAI.Thomason.Construction.SubdivisionBarycentric.boundaryOrderedHomotopy line 260
  15. def OAI.Thomason.Construction.SubdivisionBarycentric.boundaryApproximationTriangle line 267
  16. def OAI.Thomason.Construction.SubdivisionBarycentric.boundaryApproximationLoop line 319
  17. theorem OAI.Thomason.Construction.SubdivisionBarycentric.boundaryApproximationLoop_support line 327
  18. def OAI.Thomason.Construction.SubdivisionBarycentric.boundaryApproximationLoop_null line 339
  19. theorem OAI.Thomason.Construction.SubdivisionBarycentric.relative_kan_approximation_stage line 379
  20. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_relative_kan_approximation line 509
  21. def OAI.Thomason.Construction.SubcomplexFaceComparison.ambientFace line 589
  22. theorem OAI.Thomason.Construction.SubcomplexFaceComparison.ambientFace_simplex line 601
  23. theorem OAI.Thomason.Construction.SubcomplexFaceComparison.ambientFace_eq line 608
  24. theorem OAI.Thomason.Construction.SubcomplexFaceComparison.ambientFace_mem line 621
  25. def OAI.Thomason.Construction.SubcomplexFaceComparison.face line 632
  26. def OAI.Thomason.Construction.SubcomplexFaceComparison.forget line 641
  27. theorem OAI.Thomason.Construction.SubcomplexFaceComparison.face_ambient line 647
  28. def OAI.Thomason.Construction.SubcomplexFaceComparison.chainLastVertex line 653
  29. theorem OAI.Thomason.Construction.SubcomplexFaceComparison.ambientFace_lastVertex line 658
  30. def OAI.Thomason.Construction.SubcomplexFaceComparison.standardIntoChains line 676
  31. def OAI.Thomason.Construction.SubcomplexFaceComparison.chainInclusion line 680
  32. theorem OAI.Thomason.Construction.SubcomplexFaceComparison.chainInclusion_fac line 684
  33. theorem OAI.Thomason.Construction.SubcomplexFaceComparison.firstSubdivision_inclusion line 689
  34. def OAI.Thomason.Construction.SubcomplexFaceComparison.map line 728
  35. theorem OAI.Thomason.Construction.SubcomplexFaceComparison.map_ambient line 732
  36. theorem OAI.Thomason.Construction.SubcomplexFaceComparison.map_lastVertex line 744
  37. theorem OAI.Thomason.Construction.SubcomplexFaceComparison.map_naturality line 759
  38. abbrev OAI.Thomason.Construction.DoubleSubdivisionPairs.Faces line 795
  39. def OAI.Thomason.Construction.DoubleSubdivisionPairs.oldFaces line 797
  40. def OAI.Thomason.Construction.DoubleSubdivisionPairs.targetIso line 800
  41. def OAI.Thomason.Construction.DoubleSubdivisionPairs.orderNerveIso line 805
  42. def OAI.Thomason.Construction.DoubleSubdivisionPairs.sourceIso line 809
  43. theorem OAI.Thomason.Construction.DoubleSubdivisionPairs.inclusion line 818

    Source documentation

    The two identifications identify the actual twice-subdivided map, not just its source and target up to unrelated equivalences.

    theorem inclusion {n : ℕ} (A : (Δ[n] : SSet.{0}).Subcomplex) :
    (sourceIso A).hom ≫ nerveMap (subposetInclusion (ChainSieve.old (oldFaces A))).monotone.functor =
      SSet.sd.map (SSet.sd.map A.ι) ≫ (targetIso n).hom := by
…

    Mentions: OAI.Thomason.Construction.DoubleSubdivisionPairs.sourceIso, OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.ChainSieve.old, OAI.Thomason.Construction.DoubleSubdivisionPairs.oldFaces, OAI.Thomason.Construction.DoubleSubdivisionPairs.targetIso

  44. theorem OAI.Thomason.Construction.kan_extension_of_subcomplex_realization_extension line 877
  45. theorem OAI.Thomason.Construction.kan_extension_of_realization_boundary_extension line 895

    Source documentation

    Every continuous extension of an actual simplex boundary into a Kan realization has an exact simplicial extension of that same boundary.

    theorem kan_extension_of_realization_boundary_extension {X : SSet.{0}}
    [SSet.KanComplex X] (n : ℕ) (a : (SSet.boundary n : SSet.{0}) ⟶ X)
    (b : SSet.toTop.obj (Δ[n] : SSet.{0}) ⟶ SSet.toTop.obj X)
    (h : SSet.toTop.map (SSet.boundary n).ι ≫ b = SSet.toTop.map a) :
    ∃ d : (Δ[n] : SSet.{0}) ⟶ X, (SSet.boundary n).ι ≫ d = a := by
…
  46. theorem OAI.Thomason.Construction.acyclic_kan_simplex_boundary_lifting line 936
  47. theorem OAI.Thomason.Construction.acyclic_kan_simplex_boundary_rlp line 950