OAI/CategoryTheory/Thomason/Gray/SubdivisionPrismNaturality.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Stationarity of the subdivision comparison prism

The ordered comparison selects one of its endpoints at each vertex. A poset map identifying those endpoints therefore makes the whole prism constant. Applied to greatest vertices, this strengthens the double last-vertex comparison to an exact relative homotopy.

  1. theorem OAI.Thomason.Construction.PosetGeometry.orderedVertexHomotopy_postcompose_stationary line 23
  2. theorem OAI.Thomason.Construction.simplexDoublePrism_stationary line 43
  3. theorem OAI.Thomason.Construction.standardDoubleHomotopy_stationary line 80
  4. theorem OAI.Thomason.Construction.subdivisionLastVertexHomotopy_fac line 97
  5. theorem OAI.Thomason.Construction.subdivisionLastVertexHomotopy_stationary line 104
  6. theorem OAI.Thomason.Construction.extensionCylinder_fst line 130
  7. theorem OAI.Thomason.Construction.subdivisionUnitHomotopy_stationary line 137

    Source documentation

    The unit comparison homotopy is constant after extension of the last-vertex map. This is the exact relative identity used for descent over a prescribed base.

    theorem subdivisionUnitHomotopy_stationary (K : SSet.{0}) :
    (subdivisionUnitHomotopy K).h ≫ SSet.ex.map (lastVertex.app K) =
      fst (SSet.sd.obj K) Δ[1] ≫ lastVertex.app K ≫ canonicalExtension.app K := by
…

    Mentions: OAI.Thomason.Construction.subdivisionUnitHomotopy

  8. theorem OAI.Thomason.Construction.subdivisionLastVertexHomotopy_naturality line 190
  9. theorem OAI.Thomason.Construction.extensionCylinder_naturality line 217
  10. theorem OAI.Thomason.Construction.subdivisionUnitHomotopy_naturality line 225