OAI/CategoryTheory/Thomason/Transfer/HornRealizationGluing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Gluing the geometric horn into its actual realization

  1. def OAI.Thomason.Construction.HornBarycentric.faceRegion line 16
  2. theorem OAI.Thomason.Construction.HornBarycentric.faceRegion_closed line 19
  3. theorem OAI.Thomason.Construction.HornBarycentric.faceRegion_cover line 24
  4. def OAI.Thomason.Construction.HornBarycentric.faceChart line 32

    Source documentation

    A continuous chart on each closed face.

    def faceChart {n : ℕ} (i : Fin (n+2)) (j : {j : Fin (n+2) // j ≠ i}) :
    C(faceRegion i j, SSet.toTop.obj (Λ[n+1, i] : SSet.{0})) where
…

    Mentions: OAI.Thomason.Construction.HornBarycentric.faceRegion

  5. theorem OAI.Thomason.Construction.HornBarycentric.faceChart_overlap line 42
  6. def OAI.Thomason.Construction.HornBarycentric.toRealization line 49

    Source documentation

    The continuous map from the geometric horn to the actual realization.

    def toRealization {n : ℕ} (i : Fin (n+2)) :
    C(horn i, SSet.toTop.obj (Λ[n+1, i] : SSet.{0})) where
…

    Mentions: OAI.Thomason.Construction.HornBarycentric.horn

  7. theorem OAI.Thomason.Construction.HornBarycentric.toRealization_face line 66