OAI/CategoryTheory/Thomason/Gray/OrderedAtomGrouping.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

The finite coefficient interface needed for ordered atom generation

This interface is shared by the normalized simplex complexes and the finite pasted-globe cylinder complexes. It records concrete basis coordinates, actual positive cells, and their disjoint ordered boundaries; generation is a theorem proved from these data, rather than a field of the interface.

  1. structure OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis line 23
  2. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.coordinate_nonnegative line 45
  3. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.positive_augmentation_zero line 49
  4. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.positive_augmentation_one line 65
  5. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.residual_sides line 100

    Source documentation

    The equality of residuals uses only the cell boundary equations.

    theorem residual_sides (X A : Cell K) (r : ℕ)
    (he : X.table false (r+1) = A.table false (r+1)) :
    X.table false r - A.table false r = X.table true r - A.table true r := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Cell

  6. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.residual_positive line 112

    Source documentation

    Disjoint atom sides make every common upper-table residual positive.

    theorem residual_positive (X : Cell K) {p : ℕ} (b : B.Index p) (r : ℕ)
    (hr : r < p) (he : X.table false (r+1) = (B.atom p b).table false (r+1)) :
    X.table false r - (B.atom p b).table false r ∈ K.positive r := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Cell

  7. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.eq_atom_of_above_zero line 125

    Source documentation

    At degree zero augmentation one eliminates the residual.

    theorem eq_atom_of_above_zero (X : Cell K) {p : ℕ} (b : B.Index p) (hp : 0 < p)
    (he : ∀ n, 0 < n → ∀ side, X.table side n = (B.atom p b).table side n) :
    X = B.atom p b := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Cell

  8. abbrev OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AtomIndex line 157
  9. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atomCell line 159
  10. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atomHeight line 161
  11. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.chainAtomIndices line 163
  12. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.chainAtomIndices_degree line 167
  13. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.coordinates_ofCells line 174
  14. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.sum_map_flatMap line 185
  15. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.chainAtomIndices_table line 193
  16. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.chainAtomIndices_above line 216
  17. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.sortAtoms line 226
  18. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.sortAtoms_perm line 229
  19. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.sortAtoms_pairwise line 232
  20. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.sortAtoms_table line 242
  21. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.split_of_disjoint line 249

    Source documentation

    Coefficientwise positivity constructs the exact binary splitting.

    theorem split_of_disjoint (X : Cell K) (A D : Cell.PositiveTable K) (r : ℕ)
    (he : ∀ n, r < n → ∀ side, X.table side n = A.table side n + D.table side n)
    (hd : ∀ b, B.coordinates r (A.table false r) b = 0 ∨
      B.coordinates r (D.table true r) b = 0) :
    ∃ (Y Z : Cell K) (hyz : Y.face true r = Z.face false r),
      Cell.comp Y Z r hyz = X ∧
      (∀ n, r < n → ∀ side, Y.table side n = A.table side n) ∧
      (∀ n, r < n → ∀ side, Z.table side n = D.table side n) := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable, OAI.Thomason.Construction.DirectedComplex.Cell.comp

  22. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.sumCells_coordinate_zero line 288
  23. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.ordered_sum_induction line 299
  24. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.AboveAtomOrZero line 330
  25. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.eq_zero_atom_of_above_zero line 335
  26. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.upper_atom_decomposition line 356
  27. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.predicate_of_upper_atom_sum line 406
  28. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.generated line 430

    Source documentation

    Actual ordered atoms composition-generate every finite positive table.

    theorem generated (P : Cell K → Prop) (hatom : ∀ p b, P (B.atom p b))
    (hcomp : ∀ n x y hxy, P x → P y → P (Cell.comp x y n hxy)) : ∀ X, P X := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.comp

  29. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.hom_ext line 453

    Source documentation

    Equality on the ordered atoms determines a strict functor out of the actual positive-table realization.

    theorem hom_ext {D : StrictOmegaCategory} (F G : K.realization ⟶ D)
    (he : ∀ p b, F.toFun (B.atom p b) = G.toFun (B.atom p b)) : F = G := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory

  30. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.aboveAtomOrZero_mono line 485
  31. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.aboveAtomOrZero_zero_iff line 496
  32. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.aboveAtomOrZero_face line 509
  33. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.ordered_list_decomposition line 534
  34. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.augmentation_nonnegative line 593
  35. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.two_atom_residual_positive line 600

    Source documentation

    A reverse-disjoint pair has an actual positive residual after removing both atom contributions from its composite.

    theorem two_atom_residual_positive {p q : ℕ} (a : B.Index p) (b : B.Index q)
    (r : ℕ) (hrp : r < p) (hrq : r < q) (Y Z : Cell K)
    (hyz : Y.face true r = Z.face false r)
    (hY : Y.table false (r+1) = (B.atom p a).table false (r+1))
    (hZ : Z.table false (r+1) = (B.atom q b).table false (r+1))
    (hdis : ∀ e, B.coordinates r ((B.atom p a).table true r) e = 0 ∨
      B.coordinates r ((B.atom q b).table false r) e = 0) :
    (Cell.comp Y Z r hyz).table false r - (B.atom p a).table false r -
      (B.atom q b).table false r ∈ K.positive r := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.comp

  36. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.two_atom_degree_positive line 624

    Source documentation

    Such a reversed pair cannot occur at degree zero: removing its two augmentation-one atoms would give a positive chain of augmentation -1.

    theorem two_atom_degree_positive {p q : ℕ} (a : B.Index p) (b : B.Index q)
    (r : ℕ) (hrp : r < p) (hrq : r < q) (Y Z : Cell K)
    (hyz : Y.face true r = Z.face false r)
    (hY : Y.table false (r+1) = (B.atom p a).table false (r+1))
    (hZ : Z.table false (r+1) = (B.atom q b).table false (r+1))
    (hdis : ∀ e, B.coordinates r ((B.atom p a).table true r) e = 0 ∨
      B.coordinates r ((B.atom q b).table false r) e = 0) : 0 < r := by
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Cell

  37. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.two_atom_upper_decomposition line 662
  38. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.two_atom_ordered_lower_decomposition line 708
  39. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.higherAtomLabels line 773
  40. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atomTable_sum_filter line 776
  41. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.related_table_sum line 792
  42. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.group_two_higher_atoms line 803
  43. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.two_atom_lowering line 864

    Source documentation

    A reverse-disjoint pair at degree s+1 is a binary composite at degree s, with the same higher atom contributions, in one of the two possible orders.

    theorem two_atom_lowering {p q : ℕ} (a : B.Index p) (b : B.Index q) (s : ℕ)
    (hrp : s+1 < p) (hrq : s+1 < q) (Y Z : Cell K)
    (hyz : Y.face true (s+1) = Z.face false (s+1))
    (hY : ∀ n, s+1 < n → ∀ side, Y.table side n = (B.atom p a).table side n)
    (hZ : ∀ n, s+1 < n → ∀ side, Z.table side n = (B.atom q b).table side n)
    (hdis : ∀ e, B.coordinates (s+1) ((B.atom p a).table true (s+1)) e = 0 ∨
      B.coordinates (s+1) ((B.atom q b).table false (s+1)) e = 0) :
    ∃ (U V : Cell K) (huv : U.face true s = V.face false s),
      Cell.comp U V s huv = Cell.comp Y Z (s+1) hyz ∧
      ((∀ n, s+1 < n → ∀ side, U.table side n = (B.atom p a).table side n) ∧
       (∀ n, s+1 < n → ∀ side, V.table side n = (B.atom q b).table side n) ∨
       (∀ n, s+1 < n → ∀ side, U.table side n = (B.atom q b).table side n) ∧
…

    Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.comp