OAI/CategoryTheory/Thomason/Gray/GrayMappingInterchangeEvaluation.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Direct Gray–Street–realization compatibility

The explicitly constructed Street-nerve prism realizes to a continuous homotopy. Consequently Gray deformations and finite relative prisms satisfy the actual semantic weak-equivalence test without a Kan–Quillen input. The right-Gray cylinder comparison is an explicit hypothesis.

  1. def OAI.Thomason.Construction.RightGrayInput.realizedHomotopy line 34

    Source documentation

    A strict Gray homotopy induces an actual continuous homotopy of realizations.

    noncomputable def realizedHomotopy {X Y : StrictOmegaCategory.{0}}
    (P : G.cylinder.obj X ⟶ Y) :
    (SSet.toTop.map (h.streetNerve.map ((G.endpoint false).app X ≫ P))).hom.Homotopy
      (SSet.toTop.map (h.streetNerve.map ((G.endpoint true).app X ≫ P))).hom :=
…
  2. theorem OAI.Thomason.Construction.RightGrayInput.cylinder_weakEquivalence_iff_direct line 41

    Source documentation

    Gray homotopies preserve the semantic Thomason weak test directly.

    theorem cylinder_weakEquivalence_iff_direct {X Y : StrictOmegaCategory.{0}}
    (P : G.cylinder.obj X ⟶ Y) :
    h.streetWeakEquivalences ((G.endpoint false).app X ≫ P) ↔
      h.streetWeakEquivalences ((G.endpoint true).app X ≫ P) :=
…
  3. theorem OAI.Thomason.Construction.RightGrayInput.deformation_retract_weakEquivalences_direct line 48

    Source documentation

    A Gray deformation retraction is weak on both maps without a model structure.

    theorem deformation_retract_weakEquivalences_direct {A X : StrictOmegaCategory.{0}}
    (i : A ⟶ X) (r : X ⟶ A) (hi : i ≫ r = 𝟙 A)
    (P : G.cylinder.obj X ⟶ X)
    (h₀ : (G.endpoint false).app X ≫ P = r ≫ i)
    (h₁ : (G.endpoint true).app X ≫ P = 𝟙 X) :
    h.streetWeakEquivalences i ∧ h.streetWeakEquivalences r := by
…
  4. theorem OAI.Thomason.Construction.RelativePrismData.finite_weakEquivalence_iff_direct line 86

    Source documentation

    The finite-dimensional relative prism bridge needs no Kan–Quillen axioms.

    theorem finite_weakEquivalence_iff_direct :
    h.streetWeakEquivalences ((StrictOmegaCategory.inclusion (n + 1)).map
      (r.reflect.map (h.posetMap D.first))) ↔
    h.streetWeakEquivalences ((StrictOmegaCategory.inclusion (n + 1)).map
      (r.reflect.map (h.posetMap D.last))) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion

  5. def OAI.Thomason.Construction.ConePrism.liftedBarycentric line 112

    Source documentation

    The barycentric cone in the universe-lifted simplex used by realization.

    noncomputable def liftedBarycentric (n : ℕ) :
    TopologicalInterval.cylinder.obj (SimplexCategory.toTop.{0}.obj (.mk n)) ⟶
      SimplexCategory.toTop.{0}.obj (.mk (n+1)) :=
…
  6. theorem OAI.Thomason.Construction.ConePrism.liftedBarycentric_naturality line 118

    Source documentation

    Naturality before descending through geometric realization.

    theorem liftedBarycentric_naturality {m n : SimplexCategory} (f : m ⟶ n) :
    TopologicalInterval.cylinder.map (SimplexCategory.toTop.{0}.map f) ≫
      liftedBarycentric n.len =
    liftedBarycentric m.len ≫
      SimplexCategory.toTop.{0}.map (SimplexCategory.Hom.mk (ordinalMap f.toOrderHom)) := by
…

    Mentions: OAI.Thomason.Construction.ConePrism.liftedBarycentric, OAI.Thomason.Construction.ConePrism.ordinalMap

  7. def OAI.Thomason.Construction.ConePrism.piece line 131

    Source documentation

    The cone piece on one original simplex of the ordinary nerve.

    noncomputable def piece (j : CostructuredArrow SSet.stdSimplex (nerve P)) :
    TopologicalInterval.cylinder.obj ((RealizationPrism.diagram (nerve P)).obj j) ⟶
      SSet.toTop.obj (nerve P) :=
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.diagram

  8. theorem OAI.Thomason.Construction.ConePrism.piece_naturality line 137

    Source documentation

    All face and degeneracy operators preserve the explicit cone pieces.

    theorem piece_naturality {j k : CostructuredArrow SSet.stdSimplex (nerve P)} (f : j ⟶ k) :
    TopologicalInterval.cylinder.map ((RealizationPrism.diagram (nerve P)).map f) ≫
      piece v hv k = piece v hv j := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.ConePrism.piece

  9. def OAI.Thomason.Construction.ConePrism.realizationCone line 147

    Source documentation

    The actual global continuous cone map, with no KQ assumption.

    noncomputable def realizationCone :
    TopologicalInterval.cylinder.obj (SSet.toTop.obj (nerve P)) ⟶ SSet.toTop.obj (nerve P) :=
…
  10. def OAI.Thomason.Construction.intervalMin line 173

    Source documentation

    Pointwise minimum of two simplices of the ordered interval.

    def intervalMin {n : SimplexCategoryᵒᵖ} (a b : (Δ[1] : SSet.{0}).obj n) :
    (Δ[1] : SSet.{0}).obj n :=
…
  11. def OAI.Thomason.Construction.intervalMax line 183

    Source documentation

    Pointwise maximum of two simplices of the ordered interval.

    def intervalMax {n : SimplexCategoryᵒᵖ} (a b : (Δ[1] : SSet.{0}).obj n) :
    (Δ[1] : SSet.{0}).obj n :=
…
  12. def OAI.Thomason.Construction.cylinderMinHomotopy line 193

    Source documentation

    Contract the simplicial cylinder to its zero endpoint.

    def cylinderMinHomotopy (X : SSet.{0}) :
    SSet.Homotopy (fst X Δ[1] ≫ SSet.ι₀) (𝟙 (X ⊗ Δ[1])) where
…
  13. def OAI.Thomason.Construction.cylinderMaxHomotopy line 235

    Source documentation

    Contract the simplicial cylinder to its one endpoint.

    def cylinderMaxHomotopy (X : SSet.{0}) :
    SSet.Homotopy (𝟙 (X ⊗ Δ[1])) (fst X Δ[1] ≫ SSet.ι₁) where
…
  14. theorem OAI.Thomason.Construction.cylinder_projection_weak line 276

    Source documentation

    The actual simplicial cylinder projection satisfies the semantic weak test.

    theorem cylinder_projection_weak (X : SSet.{0}) :
    realizationWeakEquivalences (fst X Δ[1]) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  15. theorem OAI.Thomason.Construction.cylinder_endpoint_zero_weak line 289

    Source documentation

    The zero endpoint is weak in actual geometric realization.

    theorem cylinder_endpoint_zero_weak (X : SSet.{0}) :
    realizationWeakEquivalences (SSet.ι₀ (X := X)) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  16. theorem OAI.Thomason.Construction.cylinder_endpoint_one_weak line 295

    Source documentation

    The one endpoint is weak in actual geometric realization.

    theorem cylinder_endpoint_one_weak (X : SSet.{0}) :
    realizationWeakEquivalences (SSet.ι₁ (X := X)) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  17. theorem OAI.Thomason.Construction.boundary_rlp_weak line 301

    Source documentation

    Every boundary-lifting map is an actual realization weak equivalence.

    theorem boundary_rlp_weak {X Y : SSet.{0}} (f : X ⟶ Y) (hf : I.rlp f) :
    realizationWeakEquivalences f :=
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  18. theorem OAI.Thomason.Construction.RealizedCylinder.comparison_leg line 323
  19. theorem OAI.Thomason.Construction.RealizedCylinder.comparison_first line 331

    Source documentation

    The global prism preserves the original realization point.

    theorem comparison_first (K : SSet.{0}) (x : SSet.toTop.obj K) (t : unitInterval) :
    (SSet.toTop.map (fst K Δ[1])).hom ((comparison K).hom (x, t)) = x := by
…

    Mentions: OAI.Thomason.Construction.RealizedCylinder.comparison

  20. theorem OAI.Thomason.Construction.RealizedCylinder.comparison_time line 350

    Source documentation

    The global prism preserves the ordinary interval parameter.

    theorem comparison_time (K : SSet.{0}) (x : SSet.toTop.obj K) (t : unitInterval) :
    PrismBarycentric.realizationTime.hom
      ((SSet.toTop.map (snd K Δ[1])).hom ((comparison K).hom (x, t))) = t := by
…

    Mentions: OAI.Thomason.Construction.RealizedCylinder.comparison

  21. theorem OAI.Thomason.Construction.RealizedCylinder.comparison_weak line 362

    Source documentation

    The comparison itself satisfies the full, actual weak homotopy test.

    theorem comparison_weak (K : SSet.{0}) : topologicalWeakEquivalences (comparison K) := by
…

    Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.RealizedCylinder.comparison

  22. theorem OAI.Thomason.Construction.RealizedCylinder.comparison_naturality line 392

    Source documentation

    The comparison is natural in every simplicial map.

    theorem comparison_naturality {K L : SSet.{0}} (f : K ⟶ L) :
    TopologicalInterval.cylinder.map (SSet.toTop.map f) ≫ comparison L =
      comparison K ≫ SSet.toTop.map (f ▷ Δ[1]) := by
…

    Mentions: OAI.Thomason.Construction.RealizedCylinder.comparison

  23. theorem OAI.Thomason.Construction.RealizedCylinder.comparison_zero line 417

    Source documentation

    The exact zero endpoint on the global comparison.

    theorem comparison_zero (K : SSet.{0}) (x : SSet.toTop.obj K) :
    (comparison K).hom (x, 0) = (SSet.toTop.map SSet.ι₀).hom x := by
…

    Mentions: OAI.Thomason.Construction.RealizedCylinder.comparison

  24. theorem OAI.Thomason.Construction.RealizedCylinder.comparison_one line 424

    Source documentation

    The exact one endpoint on the global comparison.

    theorem comparison_one (K : SSet.{0}) (x : SSet.toTop.obj K) :
    (comparison K).hom (x, 1) = (SSet.toTop.map SSet.ι₁).hom x := by
…

    Mentions: OAI.Thomason.Construction.RealizedCylinder.comparison

  25. def OAI.Thomason.Construction.TripleGlobeBasis.value line 448
  26. theorem OAI.Thomason.Construction.TripleGlobeBasis.tables_below line 451
  27. theorem OAI.Thomason.Construction.TripleGlobeBasis.value_embed line 460
  28. def OAI.Thomason.Construction.TripleGlobeBasis.descApp line 476
  29. theorem OAI.Thomason.Construction.TripleGlobeBasis.descApp_single line 480
  30. theorem OAI.Thomason.Construction.TripleGlobeBasis.descApp_embedApp line 484
  31. theorem OAI.Thomason.Construction.TripleGlobeBasis.descApp_differential line 493
  32. theorem OAI.Thomason.Construction.TripleGlobeBasis.descApp_augmentation line 509
  33. theorem OAI.Thomason.Construction.TripleGlobeBasis.descApp_positive line 516
  34. def OAI.Thomason.Construction.TripleGlobeBasis.desc line 526
  35. theorem OAI.Thomason.Construction.TripleGlobeBasis.inclusion_desc line 534
  36. theorem OAI.Thomason.Construction.TripleGlobeBasis.hom_ext line 542
  37. abbrev OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.bridge line 579
  38. abbrev OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.category line 582
  39. abbrev OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.pair line 585
  40. abbrev OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.inclusion line 588
  41. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.cell line 593
  42. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.adjacent_matching line 596
  43. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.cell_dimension line 610
  44. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.hom_ext line 614
  45. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.desc_condition line 624
  46. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.desc line 640
  47. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.desc_cell line 647
  48. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.firstComposite line 689
  49. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.lastComposite line 692
  50. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.firstComposite_dimension line 695
  51. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.lastComposite_dimension line 698
  52. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.firstComposite_matching line 701
  53. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.lastComposite_matching line 705
  54. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.rightPair line 710

    Source documentation

    The inclusion of the second and third globe.

    def rightPair : PastingGlobe.category n n k ⟶ category n k :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.category

  55. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.rightPair_left line 714
  56. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.rightPair_right line 719
  57. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.pair_composite line 724
  58. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.rightPair_composite line 728
  59. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.leftBracket line 733

    Source documentation

    The outer pair of the left-associated composite.

    def leftBracket : PastingGlobe.category n n k ⟶ category n k :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.category

  60. def OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.rightBracket line 738

    Source documentation

    The outer pair of the right-associated composite.

    def rightBracket : PastingGlobe.category n n k ⟶ category n k :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.category

  61. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.leftBracket_left line 742
  62. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.leftBracket_right line 748
  63. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.rightBracket_left line 753
  64. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.rightBracket_right line 758
  65. theorem OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.associativity_diagram line 765

    Source documentation

    Equality of the two actual universal composite maps.

    theorem associativity_diagram :
    GrayMapping.compositionGlobe n k hk ≫ leftBracket n k hk =
      GrayMapping.compositionGlobe n k hk ≫ rightBracket n k hk := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.compositionGlobe, OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.leftBracket, OAI.Thomason.Construction.StrictOmegaCategory.TripleGlobe.rightBracket

  66. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_congr line 797
  67. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite_evaluation_of_legs line 807

    Source documentation

    Evaluate any binary parameter when its two legs have already been identified.

    theorem composite_evaluation_of_legs {C : StrictOmegaCategory.{0}} (hk : k < n)
    (p : PastingGlobe.category n n k ⟶ C) (u : model.obj C ⟶ D)
    (f g : model.obj (Globe.category n) ⟶ D)
    (hf : model.map (PastingGlobe.left n n k ≫ p) ≫ u = f)
    (hg : model.map (PastingGlobe.right n n k ≫ p) ≫ u = g)
    (h : model.map (Globe.faceMap true k n) ≫ f =
      model.map (Globe.faceMap false k n) ≫ g) :
    composite hk f g h = model.map (compositionGlobe n k hk ≫ p) ≫ u :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.left, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.right, OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.compositionGlobe

  68. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.tripleEvaluation line 818
  69. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.triple_first_composite line 821
  70. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.triple_last_composite line 829
  71. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.triple_associativity line 843
  72. abbrev OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.gridEvaluation line 899
  73. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.grid_row_composite line 902
  74. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.grid_column_composite line 910
  75. theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.grid_interchange line 921

    Source documentation

    Any actual map from the grid cylinder respects strict interchange.

    theorem grid_interchange (hln : l < n)
    (u : model.obj (GridGlobe.category n k l hkl) ⟶ D)
    (ht : model.map (Globe.faceMap true k n) ≫ gridEvaluation u false false =
      model.map (Globe.faceMap false k n) ≫ gridEvaluation u false true)
    (hb : model.map (Globe.faceMap true k n) ≫ gridEvaluation u true false =
      model.map (Globe.faceMap false k n) ≫ gridEvaluation u true true)
    (hl : model.map (Globe.faceMap true l n) ≫ gridEvaluation u false false =
      model.map (Globe.faceMap false l n) ≫ gridEvaluation u true false)
    (hr : model.map (Globe.faceMap true l n) ≫ gridEvaluation u false true =
      model.map (Globe.faceMap false l n) ≫ gridEvaluation u true true)
    (hv : model.map (Globe.faceMap true l n) ≫
        composite (hkl.trans hln) (gridEvaluation u false false) (gridEvaluation u false true) ht =
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GridGlobe.category, OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.gridEvaluation, OAI.Thomason.Construction.StrictOmegaCategory.GrayMapping.composite