OAI/CategoryTheory/Thomason/Gray/DirectedGlobeUniversal.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

An upper table determines its finite atom multiset

At the largest degree a top coefficient can only come from that exact basis atom. Removing one common occurrence and repeating proves uniqueness of the complete finite multiset. This uses only the triangular top tables, not the free-gluing theorem under construction.

  1. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atom_coefficient_zero_of_ne line 24
  2. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atomSum_coefficient_pos line 41
  3. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atom_mem_of_coefficient_ne_zero line 58
  4. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.common_atom_of_upper_sum line 69
  5. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.upper_sum_perm line 98
  6. abbrev OAI.Thomason.Construction.DirectedComplex.RightCylinder.group line 164
  7. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.differential line 168
  8. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.differential_squared line 181
  9. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.augmentation line 189
  10. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.augmentation_differential line 194
  11. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.positive line 198
  12. abbrev OAI.Thomason.Construction.DirectedComplex.rightCylinder line 205

    Source documentation

    The directed chain tensor K ⊗ M[1], with the interval on the right.

    abbrev rightCylinder (K : DirectedComplex.{u}) : DirectedComplex.{u} where
…
  13. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.endpointMap line 217
  14. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.endpoint line 228

    Source documentation

    Both inclusions of K into its right chain cylinder are positive chain maps.

    def endpoint (a : Bool) : Hom K (rightCylinder K) where
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder

  15. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.projectionMap line 244
  16. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.projection line 255

    Source documentation

    Collapsing the right interval is a positive augmented chain map.

    def projection : Hom (rightCylinder K) K where
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder

  17. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.projection_endpoint line 266
  18. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.realization_projection_endpoint line 271

    Source documentation

    The endpoint–projection identity survives strict realization.

    theorem realization_projection_endpoint (a : Bool) (x : K.realization) :
    (projection K).realization ((endpoint K a).realization x) = x := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.RightCylinder.projection, OAI.Thomason.Construction.DirectedComplex.realization, OAI.Thomason.Construction.DirectedComplex.RightCylinder.endpoint

  19. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.mapMap line 279
  20. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.map line 291

    Source documentation

    Tensor a positive augmented chain map with the identity of the interval.

    def map (f : Hom K L) : Hom (rightCylinder K) (rightCylinder L) where
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder

  21. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.map_endpoint line 301
  22. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.projection_map line 305
  23. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.realization_projection_map line 311

    Source documentation

    Naturality of interval collapse holds for all positive chain maps, including maps which send basis elements to zero or sums.

    theorem realization_projection_map (f : Hom K L) (x : (rightCylinder K).realization) :
    (projection L).realization ((map f).realization x) =
      f.realization ((projection K).realization x) := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.realization, OAI.Thomason.Construction.DirectedComplex.RightCylinder.projection, OAI.Thomason.Construction.DirectedComplex.RightCylinder.map

  24. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimumMap line 340

    Source documentation

    The chain map induced by minimum on the two right interval factors.

    def minimumMap : (n : ℕ) →
    (rightCylinder (rightCylinder K)).group n →+ (rightCylinder K).group n
  | 0 => {
      toFun := fun x => (x.1.1 + x.1.2 + x.2.1, x.2.2)
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.RightCylinder.group

  25. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimumMap_differential line 357
  26. def OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimum line 369

    Source documentation

    A positive augmented chain contraction, requiring no abstract Gray input.

    def minimum : Hom (rightCylinder (rightCylinder K)) (rightCylinder K) where
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder

  27. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimum_outer_one line 389
  28. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimum_outer_zero line 396
  29. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimum_projection line 405
  30. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimum_fixed_zero line 414
  31. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimum_naturality line 425
  32. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.realization_minimum_outer_one line 434

    Source documentation

    Strict realization keeps the contraction's terminal endpoint literally.

    theorem realization_minimum_outer_one (x : (rightCylinder K).realization) :
    (minimum K).realization ((endpoint (rightCylinder K) true).realization x) = x := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.realization, OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimum, OAI.Thomason.Construction.DirectedComplex.RightCylinder.endpoint

  33. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.realization_minimum_outer_zero line 441

    Source documentation

    Its initial endpoint is the specified zero section after projection.

    theorem realization_minimum_outer_zero (x : (rightCylinder K).realization) :
    (minimum K).realization ((endpoint (rightCylinder K) false).realization x) =
      (endpoint K false).realization ((projection K).realization x) := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.realization, OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimum, OAI.Thomason.Construction.DirectedComplex.RightCylinder.endpoint, OAI.Thomason.Construction.DirectedComplex.RightCylinder.projection

  34. theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.realization_minimum_projection line 449

    Source documentation

    Collapse commutes with the actual directed contraction.

    theorem realization_minimum_projection
    (x : (rightCylinder (rightCylinder K)).realization) :
    (projection K).realization ((minimum K).realization x) =
      (projection K).realization ((projection (rightCylinder K)).realization x) := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.realization, OAI.Thomason.Construction.DirectedComplex.RightCylinder.projection, OAI.Thomason.Construction.DirectedComplex.RightCylinder.minimum

  35. inductive OAI.Thomason.Construction.StrictOmegaCategory.Globe.Cell line 472
  36. def OAI.Thomason.Construction.StrictOmegaCategory.Globe.dimension line 479
  37. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.dimension_le line 483
  38. def OAI.Thomason.Construction.StrictOmegaCategory.Globe.face line 488
  39. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.face_of_dimension_le line 492
  40. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.dimension_face line 495
  41. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.globular line 502
  42. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.matching_unit line 523

    Source documentation

    Matching faces force at least one factor to be a unit at that level.

    theorem matching_unit {m : ℕ} {x y : Cell n}
    (h : face true m x = face false m y) : dimension x ≤ m ∨ dimension y ≤ m := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.Cell, OAI.Thomason.Construction.StrictOmegaCategory.Globe.face, OAI.Thomason.Construction.StrictOmegaCategory.Globe.dimension

  43. def OAI.Thomason.Construction.StrictOmegaCategory.Globe.comp line 532
  44. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.source_comp line 534
  45. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.target_comp line 541
  46. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.face_comp line 549
  47. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.left_unit line 557
  48. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.right_unit line 561
  49. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.assoc line 567
  50. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.matching_small_iff line 571
  51. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.interchange line 578
  52. def OAI.Thomason.Construction.StrictOmegaCategory.Globe.category line 595

    Source documentation

    The strict n-globe, with its actual finite boundary cells.

    def category (n : ℕ) : StrictOmegaCategory where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory

  53. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.category_truncated line 610
  54. def OAI.Thomason.Construction.StrictOmegaCategory.Globe.evaluate line 635
  55. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.evaluate_top line 639
  56. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.evaluate_boundary line 641
  57. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.evaluate_dimension line 644
  58. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.evaluate_face line 650
  59. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.comp_of_left_unit line 668
  60. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.comp_of_right_unit line 674
  61. def OAI.Thomason.Construction.StrictOmegaCategory.Globe.lift line 681

    Source documentation

    The strict functor determined by a chosen n-dimensional cell.

    def lift (x : C) (hx : C.DimensionLE n x) : category n ⟶ C where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category

  62. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.lift_top line 699
  63. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.hom_ext line 702

    Source documentation

    Evaluation at the top cell determines a strict functor on the whole globe.

    theorem hom_ext (f g : category n ⟶ C)
    (h : f.toFun .top = g.toFun .top) : f = g := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category

  64. def OAI.Thomason.Construction.StrictOmegaCategory.Globe.homEquiv line 720

    Source documentation

    The globe represents bounded cells in the actual strict category.

    def homEquiv (n : ℕ) : (category n ⟶ C) ≃ {x : C // C.DimensionLE n x} where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category

  65. theorem OAI.Thomason.Construction.StrictOmegaCategory.Globe.homEquiv_naturality line 726
  66. abbrev OAI.Thomason.Construction.DirectedGlobeComplex.Basis line 747
  67. abbrev OAI.Thomason.Construction.DirectedGlobeComplex.Chains line 748
  68. def OAI.Thomason.Construction.DirectedGlobeComplex.weight line 750
  69. theorem OAI.Thomason.Construction.DirectedGlobeComplex.weight_single line 753
  70. def OAI.Thomason.Construction.DirectedGlobeComplex.boundary line 756
  71. theorem OAI.Thomason.Construction.DirectedGlobeComplex.weight_boundary line 761
  72. def OAI.Thomason.Construction.DirectedGlobeComplex.differential line 766
  73. theorem OAI.Thomason.Construction.DirectedGlobeComplex.differential_single line 769
  74. theorem OAI.Thomason.Construction.DirectedGlobeComplex.differential_eq_weight line 773
  75. theorem OAI.Thomason.Construction.DirectedGlobeComplex.weight_differential line 780
  76. theorem OAI.Thomason.Construction.DirectedGlobeComplex.differential_squared line 785
  77. def OAI.Thomason.Construction.DirectedGlobeComplex.positive line 790
  78. def OAI.Thomason.Construction.DirectedGlobeComplex.complex line 795
  79. theorem OAI.Thomason.Construction.DirectedGlobeComplex.chains_eq_zero_above line 803
  80. def OAI.Thomason.Construction.DirectedGlobeComplex.topTable line 807
  81. theorem OAI.Thomason.Construction.DirectedGlobeComplex.topTable_boundary line 812
  82. def OAI.Thomason.Construction.DirectedGlobeComplex.topCell line 828

    Source documentation

    The universal n-cell is the positive table of its two faces in every lower degree and the single generator at its top degree.

    noncomputable def topCell (n : ℕ) : (complex n).realization where
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex

  83. theorem OAI.Thomason.Construction.DirectedGlobeComplex.topCell_dimension line 853
  84. def OAI.Thomason.Construction.DirectedGlobeComplex.fromGlobe line 871

    Source documentation

    The actual positive-table realization of the free globe receives its canonical strict cell map, with no Gray input.

    noncomputable def fromGlobe (n : ℕ) :
    StrictOmegaCategory.Globe.category n ⟶ (complex n).realization :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.category, OAI.Thomason.Construction.DirectedGlobeComplex.complex

  85. def OAI.Thomason.Construction.DirectedGlobeComplex.cellApp line 897

    Source documentation

    Extend the table entries of a cell linearly on the globe basis.

    def cellApp (n : ℕ) (x : Cell K) (k : ℕ) : Chains n k →ₗ[ℤ] K.group k :=
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Chains

  86. theorem OAI.Thomason.Construction.DirectedGlobeComplex.cellApp_single line 900
  87. theorem OAI.Thomason.Construction.DirectedGlobeComplex.cellApp_boundary line 904
  88. theorem OAI.Thomason.Construction.DirectedGlobeComplex.cellApp_differential line 908
  89. theorem OAI.Thomason.Construction.DirectedGlobeComplex.cellApp_augmentation line 918
  90. theorem OAI.Thomason.Construction.DirectedGlobeComplex.cellApp_positive line 925
  91. def OAI.Thomason.Construction.DirectedGlobeComplex.cellMap line 937

    Source documentation

    The canonical positive globe map associated to a cell table. Its top cell is the n-source of the table, hence the table itself when bounded.

    def cellMap (n : ℕ) (x : Cell K) : Hom (complex n) K where
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex

  92. theorem OAI.Thomason.Construction.DirectedGlobeComplex.cellMap_top line 945

    Source documentation

    Realizing the associated positive chain map recovers the full bounded table, including the lower-dimensional identity extensions.

    theorem cellMap_top (n : ℕ) (x : Cell K) :
    (cellMap n x).realization.toFun (topCell n) = x.face false n := by
…

    Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.cellMap, OAI.Thomason.Construction.DirectedGlobeComplex.topCell

  93. theorem OAI.Thomason.Construction.DirectedGlobeComplex.cellMap_top_of_bounded line 957