OAI/CategoryTheory/Thomason/Chains/HornChainRetraction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A second-subdivision retraction into the first-subdivided horn

For a chain of faces, keep the maxima of its horn faces. If an excluded face occurs, add the distinguished horn vertex. On chains entirely in the horn this is exactly the image under the original last-vertex operation.

  1. def OAI.Thomason.Construction.HornChainRetraction.good line 22
  2. def OAI.Thomason.Construction.HornChainRetraction.bad line 25
  3. def OAI.Thomason.Construction.HornChainRetraction.imageVertices line 28
  4. theorem OAI.Thomason.Construction.HornChainRetraction.good_mem line 32
  5. theorem OAI.Thomason.Construction.HornChainRetraction.imageVertices_nonempty line 35
  6. theorem OAI.Thomason.Construction.HornChainRetraction.good_greatest line 45
  7. theorem OAI.Thomason.Construction.HornChainRetraction.imageVertices_omits line 55
  8. def OAI.Thomason.Construction.HornChainRetraction.face line 91
  9. theorem OAI.Thomason.Construction.HornChainRetraction.face_mem line 96
  10. theorem OAI.Thomason.Construction.HornChainRetraction.imageVertices_mono line 100
  11. def OAI.Thomason.Construction.HornChainRetraction.retraction line 116
  12. theorem OAI.Thomason.Construction.HornChainRetraction.retraction_old line 123

    Source documentation

    On old chains no additional vertex is inserted: the operation is precisely the finite-chain image under the original greatest-vertex map.

    theorem retraction_old (n : ℕ) (k : Fin (n+2)) (C : NonemptyFiniteChains (Faces n))
    (hC : ∀ A ∈ C.finset, A ∈ hornFaceSet n k) :
    (retraction n k C).val.val = C.map chainMaximumHom := by
…

    Mentions: OAI.Thomason.Construction.hornFaceSet, OAI.Thomason.Construction.HornChainRetraction.retraction, OAI.Thomason.Construction.chainMaximumHom