SimplexBasisHeight.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

The chain-cylinder functor

Positive augmentation-preserving chain maps form a category. Realization and tensoring on the right by the interval are functors, with natural endpoint inclusions and collapse.

theorem OAI.Thomason.Construction.DirectedComplex.Hom.ext_app line 25
def OAI.Thomason.Construction.DirectedComplex.Hom.id line 35
def OAI.Thomason.Construction.DirectedComplex.Hom.comp line 41
instance OAI.Thomason.Construction.DirectedComplex.(instance at line 52) line 52
def OAI.Thomason.Construction.DirectedComplex.realizationFunctor line 61
Source documentation
Strict realization of positive chain maps is a functor.
```
def realizationFunctor : DirectedComplex.{0} ⥤ StrictOmegaCategory.{0} where
…
```
def OAI.Thomason.Construction.DirectedComplex.rightCylinderFunctor line 76
Source documentation
The fixed right interval tensor, with its signed differential.
```
def rightCylinderFunctor : DirectedComplex.{0} ⥤ DirectedComplex.{0} where
…
```
def OAI.Thomason.Construction.DirectedComplex.rightEndpoint line 89
Source documentation
The endpoint chain maps are natural in the directed complex.
```
def rightEndpoint (a : Bool) : 𝟭 DirectedComplex.{0} ⟶ rightCylinderFunctor where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.rightCylinderFunctor
def OAI.Thomason.Construction.DirectedComplex.rightProjection line 97
Source documentation
The interval collapse is a natural positive chain map.
```
def rightProjection : rightCylinderFunctor ⟶ 𝟭 DirectedComplex.{0} where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.rightCylinderFunctor
theorem OAI.Thomason.Construction.DirectedComplex.rightEndpoint_projection line 104

theorem OAI.Thomason.Construction.DirectedComplex.Cell.table_zero_of_dimensionLE line 135

Source documentation

Bounded cells have zero table entries in every higher degree.

theorem table_zero_of_dimensionLE {x : K.realization} {n : ℕ}
    (hx : K.realization.DimensionLE n x) {p : ℕ} (hp : n < p) (a : Bool) :
    x.table a p = 0 := by
…

theorem OAI.Thomason.Construction.DirectedComplex.Cell.dimensionLE_of_table_zero line 143
Source documentation
Vanishing above n determines the equal top entries by the boundary equation.
```
theorem dimensionLE_of_table_zero {x : K.realization} {n : ℕ}
    (hx : ∀ p, n < p → ∀ a, x.table a p = 0) : K.realization.DimensionLE n x := by
…
```

theorem OAI.Thomason.Construction.DirectedComplex.Cell.dimensionLE_comp_factors line 165

Source documentation

Positivity rules out cancellation of higher cells in a composite.

theorem dimensionLE_comp_factors
    (hpos : ∀ p (a b : K.group p), a ∈ K.positive p → b ∈ K.positive p →
      a + b = 0 → a = 0 ∧ b = 0)
    {x y : K.realization} {k n : ℕ}
    (hxy : K.realization.target k x = K.realization.source k y)
    (hc : K.realization.DimensionLE n (K.realization.comp k x y hxy)) :
    K.realization.DimensionLE n x ∧ K.realization.DimensionLE n y := by
…

inductive OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression line 213

Source documentation

A finite, well-typed expression using generators and strict composition.

inductive CompositionExpression (C : StrictOmegaCategory.{0}) {I : Type} (g : I → C) :
    C → Type
  | generator (i : I) : CompositionExpression C g (g i)
  | comp {x y : C} (r : ℕ) (hxy : C.target r x = C.source r y)
      (tx : CompositionExpression C g x) (ty : CompositionExpression C g y) :
      CompositionExpression C g (C.comp r x y hxy)

namespace CompositionExpression

variable {C : StrictOmegaCategory.{0}} {I : Type} {g : I → C}

/-- Generator occurrences, with multiplicity and order retained. -/

def OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression.labels line 225
Source documentation
Generator occurrences, with multiplicity and order retained.
```
def labels {x : C} : CompositionExpression C g x → List I
  | .generator i => [i]
  | .comp _ _ tx ty => tx.labels ++ ty.labels
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression.labels_nonempty line 229
theorem OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression.dimensionLE line 237
Source documentation
If every occurring generator is bounded, so is the composite.
```
theorem dimensionLE {x : C} (t : CompositionExpression C g x) (d : I → ℕ)
    (hg : ∀ i, C.DimensionLE (d i) (g i)) (n : ℕ)
    (hlabels : ∀ i ∈ t.labels, d i ≤ n) : C.DimensionLE n x := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.CompositionExpression
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.positive_add_eq_zero line 260
Source documentation
Ordered-basis positivity admits no additive cancellation.
```
theorem positive_add_eq_zero (p : ℕ) (x y : K.group p)
    (hx : x ∈ K.positive p) (hy : y ∈ K.positive p) (h : x + y = 0) :
    x = 0 ∧ y = 0 := by
…
```
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.atom_degree_le line 284
Source documentation
The nonzero top chain detects the degree of a genuine basis atom.
```
theorem atom_degree_le {p n : ℕ} (b : B.Index p)
    (h : K.realization.DimensionLE n (B.atom p b)) : p ≤ n := by
…
```

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.expression_labels_bounded line 294

Source documentation

No generator above degree n can occur in an expression whose image is n-dimensional. This uses positivity rather than injectivity of the map.

theorem expression_labels_bounded {C : StrictOmegaCategory.{0}}
    (g : B.AtomIndex → C) (F : C ⟶ K.realization)
    (hg : ∀ i, F.toFun (g i) = B.atomCell i)
    {x : C} (t : CompositionExpression C g x) (n : ℕ)
    (hx : K.realization.DimensionLE n (F.toFun x)) :
    ∀ i ∈ t.labels, i.1 ≤ n := by
…

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.dimensionLE_of_expression_image line 323

Source documentation

On a composition-generated source with bounded atom lifts, the positive-table map reflects every finite dimension bound.

theorem dimensionLE_of_expression_image {C : StrictOmegaCategory.{0}}
    (g : B.AtomIndex → C) (F : C ⟶ K.realization)
    (hg : ∀ i, F.toFun (g i) = B.atomCell i)
    (hd : ∀ i, C.DimensionLE i.1 (g i))
    {x : C} (t : CompositionExpression C g x) (n : ℕ)
    (hx : K.realization.DimensionLE n (F.toFun x)) : C.DimensionLE n x :=
…

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.exists_bounded_expression line 333

Source documentation

Ordinary composition generation by atom lifts is dimensionwise: an n-cell has an expression using only the generators of degree at most n.

theorem exists_bounded_expression {C : StrictOmegaCategory.{0}}
    (g : B.AtomIndex → C) (F : C ⟶ K.realization)
    (hg : ∀ i, F.toFun (g i) = B.atomCell i)
    (hgen : ∀ x : C, Nonempty (CompositionExpression C g x))
    (n : ℕ) (x : C) (hx : C.DimensionLE n x) :
    ∃ t : CompositionExpression C g x, ∀ i ∈ t.labels, i.1 ≤ n := by
…

theorem OAI.Thomason.Construction.DirectedComplex.realization_face_eq_of_agree_through line 364

Source documentation

Low-degree agreement fixes every chosen n-face of the images.

theorem realization_face_eq_of_agree_through
    (f g : Hom K L) {n : ℕ} (hfg : ∀ k, k ≤ n → f.app k = g.app k)
    (a : Bool) (x : K.realization) :
    L.realization.face a n (f.realization x) =
      L.realization.face a n (g.realization x) := by
…

Mentions: OAI.Thomason.Construction.DirectedComplex.Hom

theorem OAI.Thomason.Construction.DirectedComplex.realization_comp_eq_of_agree_through line 385
Source documentation
Any strict functor to an n-truncated target identifies directed chain maps which agree through degree n.
```
theorem realization_comp_eq_of_agree_through
    (f g : Hom K L) {n : ℕ} (hfg : ∀ k, k ≤ n → f.app k = g.app k)
    {Y : StrictOmegaCategory.{u}} (hY : Y.IsTruncated n) (H : L.realization ⟶ Y) :
    f.realization ≫ H = g.realization ≫ H := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom
theorem OAI.Thomason.Construction.DirectedComplex.rightCylinderMap_agree_through line 399
Source documentation
Tensoring with the right interval preserves degreewise agreement through the same bound.
```
theorem rightCylinderMap_agree_through
    (f g : Hom K L) {n : ℕ} (hfg : ∀ k, k ≤ n → f.app k = g.app k) :
    ∀ k, k ≤ n → (RightCylinder.map f).app k = (RightCylinder.map g).app k := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.RightCylinder.map
theorem OAI.Thomason.Construction.DirectedComplex.rightCylinder_realization_comp_eq_of_agree_through line 415
Source documentation
The corresponding exact comparison for right-cylinder realizations.
```
theorem rightCylinder_realization_comp_eq_of_agree_through
    (f g : Hom K L) {n : ℕ} (hfg : ∀ k, k ≤ n → f.app k = g.app k)
    {Y : StrictOmegaCategory.{u}} (hY : Y.IsTruncated n)
    (H : (rightCylinder L).realization ⟶ Y) :
    (RightCylinder.map f).realization ≫ H = (RightCylinder.map g).realization ≫ H :=
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.realization, OAI.Thomason.Construction.DirectedComplex.RightCylinder.map
def OAI.Thomason.Construction.DirectedComplex.Cell.bridgeTable line 446
def OAI.Thomason.Construction.DirectedComplex.Cell.bridge line 451
Source documentation
A positive (n+1)-chain and common lower faces form a literal cell.
```
def bridge (hz : z ∈ K.positive (n+1))
    (hxy : ∀ k, k < n → ∀ a, x.table a k = y.table a k)
    (hd : K.differential n z = y.table true n - x.table false n) : Cell K where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell
theorem OAI.Thomason.Construction.DirectedComplex.Cell.bridge_source line 486
Source documentation
The new cell has exactly the prescribed source n-face.
```
theorem bridge_source (hz hxy hd) :
    (bridge x y n z hz hxy hd).face false n = x.face false n := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell.bridge, OAI.Thomason.Construction.DirectedComplex.Cell.face
theorem OAI.Thomason.Construction.DirectedComplex.Cell.bridge_target line 502
Source documentation
The new cell has exactly the prescribed target n-face.
```
theorem bridge_target (hz hxy hd) :
    (bridge x y n z hz hxy hd).face true n = y.face true n := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell.bridge, OAI.Thomason.Construction.DirectedComplex.Cell.face

theorem OAI.Thomason.Construction.DirectedComplex.realization_comp_eq_of_positive_degree_bridge line 521

Source documentation

Positive degree-(n+1) bridges suffice when the chain maps agree only strictly below n. This is stronger than agreement through degree n.

theorem realization_comp_eq_of_positive_degree_bridge
    {K L : DirectedComplex.{u}} (f g : Hom K L) {n : ℕ}
    (hfg : ∀ k, k < n → f.app k = g.app k)
    (hbridge : ∀ v : K.group n, v ∈ K.positive n →
      ∃ z : L.group (n+1), z ∈ L.positive (n+1) ∧
        L.differential n z = g.app n v - f.app n v)
    {Y : StrictOmegaCategory.{u}} (hY : Y.IsTruncated n) (H : L.realization ⟶ Y) :
    f.realization ≫ H = g.realization ≫ H := by
…

Mentions: OAI.Thomason.Construction.DirectedComplex.Hom

def OAI.Thomason.Construction.SimplexComplex.alternatingHeight line 578

Source documentation

Weights are listed in strictly decreasing order.

def alternatingHeight : List ℕ → ℤ
  | [] => 0
  | w :: ws => -(3 : ℤ)^w - alternatingHeight ws

/-- The leading ternary weight controls the entire alternating tail. -/

theorem OAI.Thomason.Construction.SimplexComplex.alternatingHeight_bounds line 583
Source documentation
The leading ternary weight controls the entire alternating tail.
```
theorem alternatingHeight_bounds {w : ℕ} {ws : List ℕ}
    (hs : (w :: ws).Pairwise (· > ·)) :
    -(3 : ℤ)^w ≤ alternatingHeight (w :: ws) ∧
      alternatingHeight (w :: ws) < 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.alternatingHeight
theorem OAI.Thomason.Construction.SimplexComplex.alternatingHeight_remove_head line 603
Source documentation
Removing the leading vertex strictly increases the height. The factor three leaves room for both copies of every remaining signed tail.
```
theorem alternatingHeight_remove_head {w : ℕ} {ws : List ℕ}
    (hs : (w :: ws).Pairwise (· > ·)) :
    0 < alternatingHeight ws - alternatingHeight (w :: ws) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.alternatingHeight
theorem OAI.Thomason.Construction.SimplexComplex.alternatingHeight_eraseIdx line 623
Source documentation
Deleting position i changes height with exactly the boundary sign (-1)^i. In particular no signed boundary relation can form a cycle.
```
theorem alternatingHeight_eraseIdx (ws : List ℕ) (hs : ws.Pairwise (· > ·))
    (i : ℕ) (hi : i < ws.length) :
    0 < (-1 : ℤ)^i * (alternatingHeight (ws.eraseIdx i) - alternatingHeight ws) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.alternatingHeight