OAI/CategoryTheory/Thomason/Gray/TripleGlobeAtoms.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

Street homotopies from concrete positive-chain cylinders

No global Gray functor or adjunction is needed here: the chain map of each actual Street simplex is extracted from the normalized oriental presentation. The construction uses composition generation of the simplex atoms.

  1. abbrev OAI.Thomason.Construction.SimplexAtomsInput.normalizedAWMap line 32

    Source documentation

    Typed form of the explicit normalized AW map.

    abbrev normalizedAWMap (h : NormalizedSimplexIdentities) {m : ℕ}
    (θ : Fin (m+1) →o Fin 2) :
    directedComplex m (h.squared m) ⟶ rightCylinder (directedComplex m (h.squared m)) :=
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

  2. abbrev OAI.Thomason.Construction.SimplexAtomsInput.simplexChainMap line 37
  3. abbrev OAI.Thomason.Construction.SimplexAtomsInput.chainCylinderMap line 42
  4. abbrev OAI.Thomason.Construction.SimplexAtomsInput.chainEndpoint line 45
  5. abbrev OAI.Thomason.Construction.SimplexAtomsInput.chainProjection line 48
  6. theorem OAI.Thomason.Construction.SimplexAtomsInput.aw_naturality line 52

    Source documentation

    The concrete AW map, viewed before strict realization, is natural.

    theorem aw_naturality {l m : ℕ} (f : Fin (l+1) →o Fin (m+1))
    (θ : Fin (m+1) →o Fin 2) :
    simplexChainMap h f ≫
        (normalizedAWMap h θ) =
      (normalizedAWMap h (θ.comp f)) ≫
        chainCylinderMap (simplexChainMap h f) := by
…

    Mentions: OAI.Thomason.Construction.SimplexAtomsInput.simplexChainMap, OAI.Thomason.Construction.SimplexAtomsInput.normalizedAWMap, OAI.Thomason.Construction.SimplexAtomsInput.chainCylinderMap

  7. def OAI.Thomason.Construction.SimplexAtomsInput.chainNerveCylinder line 64

    Source documentation

    An actual simplicial cylinder map for the realization of every directed complex. Its simplices are positive chain maps, including degenerate ones.

    def chainNerveCylinder (K : DirectedComplex.{0}) :
    h.streetNerve.obj K.realization ⊗ Δ[1] ⟶
      h.streetNerve.obj (rightCylinder K).realization where
…
  8. theorem OAI.Thomason.Construction.SimplexAtomsInput.chainNerveCylinder_endpoint line 94

    Source documentation

    The simplicial cylinder has the two actual strict chain endpoints.

    theorem chainNerveCylinder_endpoint (K : DirectedComplex.{0}) (side : Bool) :
    (if side then SSet.ι₁ else SSet.ι₀) ≫ a.chainNerveCylinder K =
      h.streetNerve.map (chainEndpoint K side).realization := by
…

    Mentions: OAI.Thomason.Construction.SimplexAtomsInput.chainEndpoint

  9. theorem OAI.Thomason.Construction.SimplexAtomsInput.chainNerveCylinder_projection line 125

    Source documentation

    The concrete chain projection is the simplicial cylinder projection.

    theorem chainNerveCylinder_projection (K : DirectedComplex.{0}) :
    a.chainNerveCylinder K ≫ h.streetNerve.map (chainProjection K).realization =
      fst (h.streetNerve.obj K.realization) Δ[1] := by
…

    Mentions: OAI.Thomason.Construction.SimplexAtomsInput.chainProjection

  10. def OAI.Thomason.Construction.SimplexAtomsInput.chainNerveHomotopy line 149

    Source documentation

    Every strict map from the concrete chain cylinder determines an actual homotopy of Street nerves, with no Gray model-structure premise.

    def chainNerveHomotopy {K : DirectedComplex.{0}} {Y : StrictOmegaCategory.{0}}
    (P : (rightCylinder K).realization ⟶ Y) :
    SSet.Homotopy (h.streetNerve.map ((RightCylinder.endpoint K false).realization ≫ P))
      (h.streetNerve.map ((RightCylinder.endpoint K true).realization ≫ P)) where
…
  11. def OAI.Thomason.Construction.PrismBarycentric.lowerFiberMass line 192

    Source documentation

    Source mass before the cut that is identified with the cut vertex.

    def lowerFiberMass {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (x : StdSimplex ℝ (Fin (m+1))) (j : Fin (m+1)) : ℝ :=
…
  12. theorem OAI.Thomason.Construction.PrismBarycentric.cumulative_map_decomposition line 197

    Source documentation

    Cumulative source mass separates into strict target mass and merged cut mass.

    theorem cumulative_map_decomposition {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (x : StdSimplex ℝ (Fin (m+1))) (j : Fin (m+1)) :
    cumulative x j.val = cumulative (StdSimplex.map f x) (f j).val + lowerFiberMass f x j := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.cumulative, OAI.Thomason.Construction.PrismBarycentric.lowerFiberMass

  13. theorem OAI.Thomason.Construction.PrismBarycentric.cutMass_map line 219

    Source documentation

    The target cut coordinate includes precisely the mass merged from below.

    theorem cutMass_map {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (j : Fin (m+1)) (p : StdSimplex ℝ (Fin (m+1)) × unitInterval) :
    cutMass (f j) (StdSimplex.map f p.1, p.2) = cutMass j p + lowerFiberMass f p.1 j := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.cutMass, OAI.Thomason.Construction.PrismBarycentric.lowerFiberMass

  14. theorem OAI.Thomason.Construction.PrismBarycentric.prismOrdinal_succAbove line 228

    Source documentation

    On an original vertex, the prism ordinal map selects the correct copy.

    theorem prismOrdinal_succAbove {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (j i : Fin (m+1)) :
    prismOrdinal f j (j.castSucc.succAbove i) =
      if i < j then (f i).castSucc else (f i).succ := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.prismOrdinal

  15. theorem OAI.Thomason.Construction.PrismBarycentric.prismOrdinal_lower line 246
  16. theorem OAI.Thomason.Construction.PrismBarycentric.prismOrdinal_upper line 251
  17. def OAI.Thomason.Construction.PrismBarycentric.sideMap line 278

    Source documentation

    The image of an original vertex under the cut prism map.

    def sideMap {m n : ℕ} (f : Fin (m+1) →o Fin (n+1)) (j i : Fin (m+1)) :
    Fin (n+2) := if i < j then (f i).castSucc else (f i).succ
  18. theorem OAI.Thomason.Construction.PrismBarycentric.sideMap_single line 282

    Source documentation

    Only vertices merged with the cut require a correction.

    theorem sideMap_single {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (j i : Fin (m+1)) (a : ℝ) :
    Finsupp.single (sideMap f j i) a =
      Finsupp.single ((f j).castSucc.succAbove (f i)) a +
      Finsupp.single (f j).castSucc (if i < j ∧ f i = f j then a else 0) -
      Finsupp.single (f j).succ (if i < j ∧ f i = f j then a else 0) := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.sideMap

  19. theorem OAI.Thomason.Construction.PrismBarycentric.sideMap_weights line 301

    Source documentation

    Summing the vertex correction gives the merged lower mass.

    theorem sideMap_weights {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (x : StdSimplex ℝ (Fin (m+1))) (j : Fin (m+1)) :
    x.weights.mapDomain (sideMap f j) =
      (x.weights.mapDomain f).mapDomain (f j).castSucc.succAbove +
      Finsupp.single (f j).castSucc (lowerFiberMass f x j) -
      Finsupp.single (f j).succ (lowerFiberMass f x j) := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.sideMap, OAI.Thomason.Construction.PrismBarycentric.lowerFiberMass

  20. theorem OAI.Thomason.Construction.PrismBarycentric.splitWeights_map line 316

    Source documentation

    Splitting and mapping commute, with exactly the merged cut mass.

    theorem splitWeights_map {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (x : StdSimplex ℝ (Fin (m+1))) (j : Fin (m+1)) (a : ℝ) :
    (splitWeights x j a).mapDomain (prismOrdinal f j) =
      splitWeights (StdSimplex.map f x) (f j) (a + lowerFiberMass f x j) := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.splitWeights, OAI.Thomason.Construction.PrismBarycentric.prismOrdinal, OAI.Thomason.Construction.PrismBarycentric.lowerFiberMass

  21. theorem OAI.Thomason.Construction.PrismBarycentric.chart_naturality line 337

    Source documentation

    Full chart naturality, valid for every ordinal map.

    theorem chart_naturality {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (j : Fin (m+1)) (p : region j) :
    StdSimplex.map (prismOrdinal f j) (chart j p) =
      chart (f j) ⟨(StdSimplex.map f p.val.1, p.val.2), region_map f j p⟩ := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.prismOrdinal, OAI.Thomason.Construction.PrismBarycentric.chart, OAI.Thomason.Construction.PrismBarycentric.region_map

  22. theorem OAI.Thomason.Construction.PrismBarycentric.realizedChart_naturality line 365

    Source documentation

    Naturality on each closed barycentric chart.

    theorem realizedChart_naturality {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (j : Fin (m+1)) (p : region j) :
    (SSet.toTop.map (SSet.stdSimplex.map (SimplexCategory.Hom.mk f) ▷ Δ[1])).hom
      (realizedChart j p) =
    realizedChart (f j) ⟨(StdSimplex.map f p.val.1, p.val.2), region_map f j p⟩ := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.realizedChart, OAI.Thomason.Construction.PrismBarycentric.region_map

  23. theorem OAI.Thomason.Construction.PrismBarycentric.standardPrism_naturality line 383

    Source documentation

    The glued standard prism is natural under every face and degeneracy.

    theorem standardPrism_naturality {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (p : StdSimplex ℝ (Fin (m+1)) × unitInterval) :
    (SSet.toTop.map (SSet.stdSimplex.map (SimplexCategory.Hom.mk f) ▷ Δ[1])).hom
      (standardPrism m p) = standardPrism n (StdSimplex.map f p.1, p.2) := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.standardPrism

  24. theorem OAI.Thomason.Construction.PrismBarycentric.liftedStandardPrism_naturality line 394

    Source documentation

    Naturality in the exact simplex convention of the realization colimit.

    theorem liftedStandardPrism_naturality {m n : SimplexCategory} (f : m ⟶ n) :
    TopologicalInterval.cylinder.map (SimplexCategory.toTop.{0}.map f) ≫
      liftedStandardPrism n.len =
    liftedStandardPrism m.len ≫ SSet.toTop.map (SSet.stdSimplex.map f ▷ Δ[1]) := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.liftedStandardPrism

  25. theorem OAI.Thomason.Construction.PrismBarycentric.chart_zero_time line 421

    Source documentation

    On a zero-dimensional base the barycentric chart has exactly its given time.

    theorem chart_zero_time (p : region (0 : Fin 1)) :
    StdSimplex.homeomorphI (chart 0 p) = p.val.2 := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.chart

  26. def OAI.Thomason.Construction.PrismBarycentric.timeOrdinal line 429

    Source documentation

    The ordinal map recording which side of the prism cut a vertex lies on.

    def timeOrdinal {n : ℕ} (j : Fin (n+1)) : Fin (n+2) →o Fin 2 :=
…
  27. theorem OAI.Thomason.Construction.PrismBarycentric.chart_time line 433

    Source documentation

    Collapsing the base of a barycentric prism preserves its time coordinate.

    theorem chart_time {n : ℕ} (j : Fin (n+1)) (p : region j) :
    StdSimplex.homeomorphI (StdSimplex.map (timeOrdinal j) (chart j p)) = p.val.2 := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.timeOrdinal, OAI.Thomason.Construction.PrismBarycentric.chart

  28. def OAI.Thomason.Construction.PrismBarycentric.secondProjectionMap line 440

    Source documentation

    The second simplicial projection records the time ordinal of each chart.

    def secondProjectionMap {n : ℕ} (j : Fin (n+1)) :
    (CostructuredArrow.map (snd (Δ[n] : SSet.{0}) Δ[1])).obj (simplexIndex j) ⟶
      baseIndex 1 :=
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.simplexIndex, OAI.Thomason.Construction.PrismBarycentric.baseIndex

  29. def OAI.Thomason.Construction.PrismBarycentric.realizationTime line 461

    Source documentation

    The usual affine coordinate on the realization of the simplicial interval.

    def realizationTime : SSet.toTop.obj (Δ[1] : SSet.{0}) ⟶ TopCat.of unitInterval :=
…
  30. theorem OAI.Thomason.Construction.PrismBarycentric.realizationTime_base line 465
  31. theorem OAI.Thomason.Construction.PrismBarycentric.realizedChart_time line 477

    Source documentation

    On every chart the realized second projection is exactly the supplied time.

    theorem realizedChart_time {n : ℕ} (j : Fin (n+1)) (p : region j) :
    realizationTime.hom ((SSet.toTop.map (snd (Δ[n] : SSet.{0}) Δ[1])).hom
      (realizedChart j p)) = p.val.2 := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.realizedChart

  32. theorem OAI.Thomason.Construction.PrismBarycentric.standardPrism_time line 494

    Source documentation

    The glued standard prism preserves the interval coordinate.

    theorem standardPrism_time (n : ℕ)
    (p : StdSimplex ℝ (Fin (n+1)) × unitInterval) :
    realizationTime.hom ((SSet.toTop.map (snd (Δ[n] : SSet.{0}) Δ[1])).hom
      (standardPrism n p)) = p.2 := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.standardPrism

  33. theorem OAI.Thomason.Construction.PrismBarycentric.splitWeights_recover line 520

    Source documentation

    Removing the first copy of the cut vertex reverses the split weights.

    theorem splitWeights_recover {n : ℕ} (j : Fin (n+1))
    (u : StdSimplex ℝ (Fin (n+2))) :
    splitWeights (StdSimplex.map j.predAbove u) j (u.weights j.castSucc) = u.weights := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.splitWeights

  34. theorem OAI.Thomason.Construction.PrismBarycentric.removedMass_le line 550

    Source documentation

    The removed mass lies between zero and the mass of the collapsed vertex.

    theorem removedMass_le {n : ℕ} (j : Fin (n+1))
    (u : StdSimplex ℝ (Fin (n+2))) :
    u.weights j.castSucc ≤ (StdSimplex.map j.predAbove u).weights j := by
…
  35. theorem OAI.Thomason.Construction.PrismBarycentric.chart_surjective line 570

    Source documentation

    Every barycentric point of a maximal prism simplex is attained by its chart.

    theorem chart_surjective {n : ℕ} (j : Fin (n+1))
    (u : StdSimplex ℝ (Fin (n+2))) : ∃ p : region j, chart j p = u := by
…

    Mentions: OAI.Thomason.Construction.PrismBarycentric.region, OAI.Thomason.Construction.PrismBarycentric.chart

  36. abbrev OAI.Thomason.Construction.TripleGlobeBasis.Basis line 619
  37. abbrev OAI.Thomason.Construction.TripleGlobeBasis.Chains line 624
  38. def OAI.Thomason.Construction.TripleGlobeBasis.predecessor line 626
  39. def OAI.Thomason.Construction.TripleGlobeBasis.embed line 629

    Source documentation

    Normalize the source of a later globe to the preceding target.

    def embed {n k p : ℕ} (hkn : k < n) (i : Fin 3)
    (b : DirectedGlobeComplex.Basis n p) : Basis n k p := by
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Basis, OAI.Thomason.Construction.TripleGlobeBasis.Basis

  40. theorem OAI.Thomason.Construction.TripleGlobeBasis.degree_le line 644
  41. theorem OAI.Thomason.Construction.TripleGlobeBasis.embed_self line 647
  42. def OAI.Thomason.Construction.TripleGlobeBasis.face line 665
  43. theorem OAI.Thomason.Construction.TripleGlobeBasis.face_globular line 669
  44. def OAI.Thomason.Construction.TripleGlobeBasis.boundary line 682
  45. def OAI.Thomason.Construction.TripleGlobeBasis.differential line 686
  46. theorem OAI.Thomason.Construction.TripleGlobeBasis.differential_single line 690
  47. theorem OAI.Thomason.Construction.TripleGlobeBasis.differential_boundary line 695
  48. theorem OAI.Thomason.Construction.TripleGlobeBasis.differential_squared line 702
  49. def OAI.Thomason.Construction.TripleGlobeBasis.weight line 709
  50. theorem OAI.Thomason.Construction.TripleGlobeBasis.weight_single line 712
  51. theorem OAI.Thomason.Construction.TripleGlobeBasis.weight_differential line 715
  52. def OAI.Thomason.Construction.TripleGlobeBasis.positive line 722
  53. def OAI.Thomason.Construction.TripleGlobeBasis.complex line 727
  54. def OAI.Thomason.Construction.TripleGlobeBasis.height line 736

    Source documentation

    The three successive intervals are placed consecutively in the height order.

    def height {n k p : ℕ} (b : Basis n k p) : ℤ :=
…

    Mentions: OAI.Thomason.Construction.TripleGlobeBasis.Basis

  55. theorem OAI.Thomason.Construction.TripleGlobeBasis.height_source_lt line 742
  56. theorem OAI.Thomason.Construction.TripleGlobeBasis.height_lt_target line 750
  57. theorem OAI.Thomason.Construction.TripleGlobeBasis.face_ne line 758
  58. theorem OAI.Thomason.Construction.TripleGlobeBasis.face_embed line 780
  59. def OAI.Thomason.Construction.TripleGlobeBasis.embedApp line 790
  60. theorem OAI.Thomason.Construction.TripleGlobeBasis.embedApp_single line 794
  61. theorem OAI.Thomason.Construction.TripleGlobeBasis.embedApp_differential line 799
  62. theorem OAI.Thomason.Construction.TripleGlobeBasis.embedApp_augmentation line 812
  63. theorem OAI.Thomason.Construction.TripleGlobeBasis.embedApp_positive line 820
  64. def OAI.Thomason.Construction.TripleGlobeBasis.inclusion line 834
  65. def OAI.Thomason.Construction.TripleGlobeBasis.atom line 856
  66. theorem OAI.Thomason.Construction.TripleGlobeBasis.atom_top line 860
  67. theorem OAI.Thomason.Construction.TripleGlobeBasis.atom_above line 866
  68. theorem OAI.Thomason.Construction.TripleGlobeBasis.atom_below line 873
  69. theorem OAI.Thomason.Construction.TripleGlobeBasis.height_lower line 881
  70. theorem OAI.Thomason.Construction.TripleGlobeBasis.atom_sideHeight line 893
  71. def OAI.Thomason.Construction.TripleGlobeBasis.orderedAtomBasis line 904
  72. theorem OAI.Thomason.Construction.TripleGlobeBasis.orderedAtomBasis_sideHeight line 926
  73. def OAI.Thomason.Construction.TripleGlobeBasis.cylinderOrderedAtomBasis line 930