OAI/CategoryTheory/Thomason/Chains/NormalizedCubicalLifting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reduce a cube with constant opposite faces to a path-space lifting problem

  1. def OAI.Thomason.Construction.RealizedCube.boundarySide line 16
  2. theorem OAI.Thomason.Construction.RealizedCube.normalized_cube_lift line 24

    Source documentation

    Currying a normalized boundary square reduces its dimension by one, with the fixed-endpoint path map as the right-hand arrow.

    theorem normalized_cube_lift {X Y : TopCat.{0}} (p : X ⟶ Y) (n : ℕ)
    {x₀ x₁ : X}
    (hp : HasLiftingProperty (boundaryInclusion n)
      (TopCat.ofHom (PathSpace.map p.hom (x := x₀) (y := x₁))))
…

    Mentions: OAI.Thomason.Construction.RealizedCube.boundaryInclusion, OAI.Thomason.Construction.PathSpace.map