FinalPositiveSimplexSupport.lean`

71 declarations, 0 contain sorry, 0 declared as axioms

Realizing directed complexes as strict omega-categories

The finite positive tables form a strict omega-category. Composition adds the higher chains and uses the exterior source and target chains. The globular, unit, associative and interchange laws are proved on tables.

theorem OAI.Thomason.Construction.DirectedComplex.Cell.source_comp line 28
theorem OAI.Thomason.Construction.DirectedComplex.Cell.target_comp line 34
theorem OAI.Thomason.Construction.DirectedComplex.Cell.left_unit line 43
theorem OAI.Thomason.Construction.DirectedComplex.Cell.right_unit line 53
theorem OAI.Thomason.Construction.DirectedComplex.Cell.assoc line 63
theorem OAI.Thomason.Construction.DirectedComplex.Cell.face_comp line 70
theorem OAI.Thomason.Construction.DirectedComplex.Cell.interchange line 77
theorem OAI.Thomason.Construction.DirectedComplex.Cell.finite_dimension line 88
Source documentation
Finite support supplies a dimension bound: the top positive and negative chains coincide because the next chain vanishes.
```
theorem finite_dimension (x : Cell K) : ∃ n, x.face false n = x ∧ x.face true n = x := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell
def OAI.Thomason.Construction.DirectedComplex.realization line 108
Source documentation
Steiner's positive-table construction as a strict omega-category.
```
def realization (K : DirectedComplex.{u}) : StrictOmegaCategory.{u} where
…
```
def OAI.Thomason.Construction.DirectedComplex.Hom.realization line 124
Source documentation
A positive augmentation-preserving chain map gives a strict functor.
```
def Hom.realization {K L : DirectedComplex.{u}} (f : Hom K L) :
    StrictOmegaCategory.Hom K.realization L.realization where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.StrictOmegaCategory.Hom
theorem OAI.Thomason.Construction.DirectedComplex.Cell.dimensionLE_iff_zero_above line 146
structure OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable line 192
Source documentation
A finite positive table with a common augmentation on its two sides. Sums of atoms have this form even when their augmentation exceeds one.
```
structure PositiveTable (K : DirectedComplex.{u}) where
…
```
def OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable.ofCell line 203
Source documentation
Globular cells are the augmentation-one positive tables.
```
def ofCell (x : Cell K) : PositiveTable K where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable
instance OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable.(instance at line 210) line 210
def OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable.add line 213
Source documentation
Positive tables add without an artificial augmentation-one restriction.
```
def add (A B : PositiveTable K) : PositiveTable K where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable
def OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable.zero line 226
def OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable.ofCells line 234
Source documentation
Finite sums of atoms are positive tables.
```
def ofCells : List (Cell K) → PositiveTable K
  | [] => zero
  | A :: as => add (ofCell A) (ofCells as)
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable, OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable.zero, OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable.add, OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable.ofCell
theorem OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable.ofCells_table line 238
def OAI.Thomason.Construction.DirectedComplex.Cell.replacementTable line 249
Source documentation
Replace the upper part of X by A and retain one chosen r-boundary of X.
```
def replacementTable (X : Cell K) (A : PositiveTable K) (r : ℕ) (side a : Bool) (n : ℕ) : K.group n :=
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable
def OAI.Thomason.Construction.DirectedComplex.Cell.replacement line 255
Source documentation
A positive middle boundary suffices to make the replacement a strict globular cell, with every lower boundary equation retained.
```
def replacement (X : Cell K) (A : PositiveTable K) (r : ℕ) (side : Bool)
    (hpos : ∀ a, X.table side r + A.table a r - A.table side r ∈ K.positive r) :
    Cell K where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable
theorem OAI.Thomason.Construction.DirectedComplex.Cell.replacement_table line 301
theorem OAI.Thomason.Construction.DirectedComplex.Cell.boundary_add_of_above line 308
Source documentation
The difference of the two r-boundaries is additive whenever the next table is additive.
```
theorem boundary_add_of_above (X : Cell K) (A B : PositiveTable K) (r : ℕ)
    (he : X.table false (r+1) = A.table false (r+1) + B.table false (r+1)) :
    X.table true r - X.table false r =
      (A.table true r - A.table false r) + (B.table true r - B.table false r) := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.PositiveTable

theorem OAI.Thomason.Construction.DirectedComplex.Cell.replacement_middle_eq line 316

Source documentation

The two formulas for the joining chain agree.

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

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

theorem OAI.Thomason.Construction.DirectedComplex.Cell.exists_comp_of_positive_middle line 328

Source documentation

Binary table decomposition with an explicitly positive joining chain.

theorem exists_comp_of_positive_middle (X : Cell K) (A B : PositiveTable K) (r : ℕ)
    (he : ∀ n, r < n → ∀ a, X.table a n = A.table a n + B.table a n)
    (hm : X.table false r + A.table true r - A.table false r ∈ K.positive r) :
    ∃ (Y Z : Cell K) (hyz : Y.face true r = Z.face false r),
      comp Y Z r hyz = X ∧
      (∀ n, r < n → ∀ a, Y.table a n = A.table a n) ∧
      (∀ n, r < n → ∀ a, Z.table a n = B.table a n) := by
…

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

theorem OAI.Thomason.Construction.DirectedComplex.Cell.factors_unique_of_above line 407
Source documentation
Two r-compositions with the same total and the same upper left factor have identical factors, including all lower boundary data.
```
theorem factors_unique_of_above (Y Z Y' Z' : Cell K) (r : ℕ)
    (hyz : Y.face true r = Z.face false r)
    (hyz' : Y'.face true r = Z'.face false r)
    (he : comp Y Z r hyz = comp Y' Z' r hyz')
    (hupper : ∀ n, r < n → ∀ side, Y.table side n = Y'.table side n) :
    Y = Y' ∧ Z = Z' := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.comp
theorem OAI.Thomason.Construction.DirectedComplex.Cell.compositeList_table line 469
Source documentation
Above the composition degree, the table of a string is the sum of its factor tables.
```
theorem compositeList_table {xs : List (Cell K)} {x : Cell K}
    (h : CompositeList K.realization r xs x) (n : ℕ) (hn : r < n) (side : Bool) :
    x.table side n = (xs.map (fun y => y.table side n)).sum := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell
theorem OAI.Thomason.Construction.DirectedComplex.Cell.compositeList_factors_unique line 484
abbrev OAI.Thomason.Construction.SimplexComplex.Basis line 537
abbrev OAI.Thomason.Construction.SimplexComplex.Chains line 538
def OAI.Thomason.Construction.SimplexComplex.deleteVertex line 540
def OAI.Thomason.Construction.SimplexComplex.differentialBasis line 543
def OAI.Thomason.Construction.SimplexComplex.differential line 546
def OAI.Thomason.Construction.SimplexComplex.augmentation line 549
theorem OAI.Thomason.Construction.SimplexComplex.augmentation_single line 553
theorem OAI.Thomason.Construction.SimplexComplex.differential_single line 558
theorem OAI.Thomason.Construction.SimplexComplex.augmentation_differentialBasis line 562
theorem OAI.Thomason.Construction.SimplexComplex.augmentation_differential line 566
def OAI.Thomason.Construction.SimplexComplex.positive line 573
def OAI.Thomason.Construction.SimplexComplex.BoundarySquared line 579
Source documentation
The usual differential identity on these concrete normalized chains.
```
def BoundarySquared (m : ℕ) : Prop :=
…
```
abbrev OAI.Thomason.Construction.SimplexComplex.directedComplex line 583
Source documentation
The augmented directed simplex complex with its differential identity.
```
noncomputable abbrev directedComplex (m : ℕ) (hsq : BoundarySquared m) : DirectedComplex where
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.BoundarySquared, OAI.Thomason.Construction.DirectedComplex
def OAI.Thomason.Construction.SimplexComplex.oriental line 593
Source documentation
The m-th oriental is the strict realization of the normalized directed simplex.
```
noncomputable def oriental (m : ℕ) (hsq : BoundarySquared m) : StrictOmegaCategory :=
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.BoundarySquared, OAI.Thomason.Construction.StrictOmegaCategory
def OAI.Thomason.Construction.SimplexComplex.mapBasis line 598
Source documentation
A monotone vertex map takes a nondegenerate simplex to its image if that image is nondegenerate, and to zero otherwise.
```
noncomputable def mapBasis {m n : ℕ} (f : Fin (m + 1) →o Fin (n + 1))
    (p : ℕ) (s : Basis m p) : Chains n p := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.Chains
def OAI.Thomason.Construction.SimplexComplex.mapChains line 604
theorem OAI.Thomason.Construction.SimplexComplex.mapChains_single line 609
theorem OAI.Thomason.Construction.SimplexComplex.mapBasis_nonneg line 613
theorem OAI.Thomason.Construction.SimplexComplex.mapChains_positive line 622
theorem OAI.Thomason.Construction.SimplexComplex.augmentation_mapBasis line 630
theorem OAI.Thomason.Construction.SimplexComplex.augmentation_mapChains line 638
theorem OAI.Thomason.Construction.SimplexComplex.mapBasis_id line 646
theorem OAI.Thomason.Construction.SimplexComplex.mapChains_id line 655
theorem OAI.Thomason.Construction.SimplexComplex.mapBasis_comp line 662
theorem OAI.Thomason.Construction.SimplexComplex.mapChains_comp line 683
def OAI.Thomason.Construction.SimplexComplex.BoundaryNaturality line 694
Source documentation
The classical naturality identity for alternating normalized chains. This is the normalized simplex chain-map assertion of Steiner (2007), Section 4.
```
def BoundaryNaturality {m n : ℕ} (f : Fin (m + 1) →o Fin (n + 1)) : Prop :=
…
```
def OAI.Thomason.Construction.SimplexComplex.directedMap line 698
def OAI.Thomason.Construction.SimplexComplex.swapDeletion line 724
Source documentation
Swap the order of two vertex deletions, accounting for the index shift.
```
def swapDeletion {p : ℕ} (ij : Fin (p + 3) × Fin (p + 2)) :
    Fin (p + 3) × Fin (p + 2) :=
…
```
theorem OAI.Thomason.Construction.SimplexComplex.swapDeletion_involutive line 729
Source documentation
Swapping the two deleted original vertices twice restores both indices.
```
theorem swapDeletion_involutive {p : ℕ} : Function.Involutive (@swapDeletion p) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.swapDeletion
theorem OAI.Thomason.Construction.SimplexComplex.deleteVertex_swap line 735
Source documentation
The paired deletion order gives exactly the same basis simplex.
```
theorem deleteVertex_swap {m p : ℕ} (s : Basis m (p + 2))
    (i : Fin (p + 3)) (j : Fin (p + 2)) :
    deleteVertex (deleteVertex s (i.succAbove j)) (j.predAbove i) =
      deleteVertex (deleteVertex s i) j := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.deleteVertex

theorem OAI.Thomason.Construction.SimplexComplex.deletion_sign line 744

Source documentation

Exactly one index changes by one when the order of deletion is exchanged.

theorem deletion_sign {p : ℕ} (i : Fin (p + 3)) (j : Fin (p + 2)) :
    (-1 : ℤ) ^ ((i.succAbove j).val + (j.predAbove i).val) =
      -((-1 : ℤ) ^ (i.val + j.val)) := by
…

theorem OAI.Thomason.Construction.SimplexComplex.differential_squared_basis line 763
Source documentation
Alternating double deletion vanishes on each nondegenerate simplex.
```
theorem differential_squared_basis {m p : ℕ} (s : Basis m (p + 2)) :
    differential m p (differentialBasis m (p + 1) s) = 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.differentialBasis
theorem OAI.Thomason.Construction.SimplexComplex.boundarySquared line 788
Source documentation
The concrete normalized differential squares to zero, without hypotheses.
```
theorem boundarySquared (m : ℕ) : BoundarySquared m := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.BoundarySquared
theorem OAI.Thomason.Construction.SimplexComplex.deleteVertex_first_of_ne_zero line 813
Source documentation
Deleting a non-first vertex leaves the first vertex unchanged.
```
theorem deleteVertex_first_of_ne_zero {m p : ℕ} (s : Basis m (p + 1))
    (i : Fin (p + 2)) (hi : i ≠ 0) : deleteVertex s i 0 = s 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.deleteVertex
theorem OAI.Thomason.Construction.SimplexComplex.deleteVertex_last_le line 819
Source documentation
No vertex of a face lies above the original final vertex.
```
theorem deleteVertex_last_le {m p : ℕ} (s : Basis m (p + 1)) (i : Fin (p + 2)) :
    deleteVertex s i (Fin.last p) ≤ s (Fin.last (p + 1)) :=
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.deleteVertex
theorem OAI.Thomason.Construction.SimplexComplex.differentialBasis_at_first_face line 825
Source documentation
At the face obtained by deleting the first vertex of b, only the first face of a simplex starting no later than b can contribute.
```
theorem differentialBasis_at_first_face {m p : ℕ} (s b : Basis m (p + 1))
    (hs : s 0 ≤ b 0) :
    differentialBasis m p s (deleteVertex b 0) =
      Finsupp.single (deleteVertex s 0) (1 : ℤ) (deleteVertex b 0) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differentialBasis, OAI.Thomason.Construction.SimplexComplex.deleteVertex
theorem OAI.Thomason.Construction.SimplexComplex.differentialBasis_zero_above line 847
Source documentation
A face of a simplex lying below q also lies below q.
```
theorem differentialBasis_zero_above {m p : ℕ} (s : Basis m (p + 1))
    (t : Basis m p) (q : Fin (m + 1))
    (hs : s (Fin.last (p+1)) ≤ q) (ht : q < t (Fin.last p)) :
    differentialBasis m p s t = 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differentialBasis
theorem OAI.Thomason.Construction.SimplexComplex.positive_support_below_of_boundary line 864
Source documentation
Support in an initial segment is detected by the differential on positive chains of positive degree.
```
theorem positive_support_below_of_boundary {m p : ℕ} (q : Fin (m + 1))
    (c : Chains m (p + 1)) (hc : c ∈ positive m (p + 1))
    (hd : ∀ t : Basis m p, q < t (Fin.last p) → differential m p c t = 0) :
    ∀ b : Basis m (p + 1), q < b (Fin.last (p + 1)) → c b = 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differential
theorem OAI.Thomason.Construction.SimplexComplex.deleteVertex_last_of_ne_last line 917
Source documentation
Deleting a non-last vertex leaves the last vertex unchanged.
```
theorem deleteVertex_last_of_ne_last {m p : ℕ} (s : Basis m (p + 1))
    (i : Fin (p + 2)) (hi : i ≠ Fin.last (p + 1)) :
    deleteVertex s i (Fin.last p) = s (Fin.last (p + 1)) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.deleteVertex
theorem OAI.Thomason.Construction.SimplexComplex.deleteVertex_first_ge line 923
theorem OAI.Thomason.Construction.SimplexComplex.differentialBasis_at_last_face line 927
Source documentation
At an extremal last face, all other face coefficients vanish.
```
theorem differentialBasis_at_last_face {m p : ℕ} (s b : Basis m (p + 1))
    (hs : b (Fin.last (p + 1)) ≤ s (Fin.last (p + 1))) :
    differentialBasis m p s (deleteVertex b (Fin.last (p + 1))) =
      Finsupp.single (deleteVertex s (Fin.last (p + 1))) ((-1 : ℤ) ^ (p + 1))
        (deleteVertex b (Fin.last (p + 1))) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differentialBasis, OAI.Thomason.Construction.SimplexComplex.deleteVertex
theorem OAI.Thomason.Construction.SimplexComplex.differentialBasis_zero_below line 952
Source documentation
A simplex in a final segment has no boundary below the segment.
```
theorem differentialBasis_zero_below {m p : ℕ} (s : Basis m (p + 1))
    (t : Basis m p) (q : Fin (m + 1)) (hs : q ≤ s 0) (ht : t 0 < q) :
    differentialBasis m p s t = 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differentialBasis
theorem OAI.Thomason.Construction.SimplexComplex.sign_square line 966
theorem OAI.Thomason.Construction.SimplexComplex.positive_support_above_of_boundary line 971
Source documentation
The boundary detects final support of every positive chain.
```
theorem positive_support_above_of_boundary {m p : ℕ} (q : Fin (m + 1))
    (c : Chains m (p + 1)) (hc : c ∈ positive m (p + 1))
    (hd : ∀ t : Basis m p, t 0 < q → differential m p c t = 0) :
    ∀ b : Basis m (p + 1), b 0 < q → c b = 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differential