SimplexChainHeight.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Support separation for simplex cones

The old simplex basis and the coned basis have disjoint images: their last vertices are respectively before, and equal to, the new final vertex. Consequently taking positive or negative parts commutes with the two basis embeddings and with sums across these two images.

def OAI.Thomason.Construction.SimplexComplex.prefixBasis line 20
Source documentation
Embed a basis simplex into the old face.
```
def prefixBasis {m p : ℕ} (s : Basis m p) : Basis (m + 1) p :=
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis
def OAI.Thomason.Construction.SimplexComplex.coneBasis line 24
Source documentation
Append the new final vertex to a basis simplex.
```
def coneBasis {m p : ℕ} (s : Basis m p) : Basis (m + 1) (p + 1) :=
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis
theorem OAI.Thomason.Construction.SimplexComplex.coneBasis_castSucc line 35
theorem OAI.Thomason.Construction.SimplexComplex.coneBasis_last line 41
theorem OAI.Thomason.Construction.SimplexComplex.prefixBasis_injective line 47
Source documentation
Both changes of basis are injective.
```
theorem prefixBasis_injective (m p : ℕ) : Function.Injective (@prefixBasis m p) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.prefixBasis
theorem OAI.Thomason.Construction.SimplexComplex.coneBasis_injective line 53
def OAI.Thomason.Construction.SimplexComplex.prefixBasisEmbedding line 62
def OAI.Thomason.Construction.SimplexComplex.coneBasisEmbedding line 65
theorem OAI.Thomason.Construction.SimplexComplex.mapChains_coneInclusion line 69
Source documentation
The old-face chain map is precisely extension along the basis embedding.
```
theorem mapChains_coneInclusion {m p : ℕ} (x : Chains m p) :
    mapChains (coneInclusion m) p x = Finsupp.embDomain (prefixBasisEmbedding m p) x := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.coneInclusion, OAI.Thomason.Construction.SimplexComplex.prefixBasisEmbedding
theorem OAI.Thomason.Construction.SimplexComplex.prismBasis_cone line 85
Source documentation
A cone prism is a single basis embedding, without cancellations.
```
theorem prismBasis_cone {m p : ℕ} (s : Basis m p) :
    prismBasis (coneInclusion m) (coneVertex m) (cone_le m) p s =
      Finsupp.single (coneBasis s) 1 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.prismBasis, OAI.Thomason.Construction.SimplexComplex.coneInclusion, OAI.Thomason.Construction.SimplexComplex.coneVertex, OAI.Thomason.Construction.SimplexComplex.cone_le, OAI.Thomason.Construction.SimplexComplex.coneBasis
theorem OAI.Thomason.Construction.SimplexComplex.prism_cone line 107
Source documentation
The cone operator is extension along the coned-basis embedding.
```
theorem prism_cone {m p : ℕ} (x : Chains m p) :
    prism (coneInclusion m) (coneVertex m) (cone_le m) p x =
      Finsupp.embDomain (coneBasisEmbedding m p) x := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.prism, OAI.Thomason.Construction.SimplexComplex.coneInclusion, OAI.Thomason.Construction.SimplexComplex.coneVertex, OAI.Thomason.Construction.SimplexComplex.cone_le, OAI.Thomason.Construction.SimplexComplex.coneBasisEmbedding
theorem OAI.Thomason.Construction.SimplexComplex.signedPart_prefix line 118
Source documentation
Positive and negative parts commute with embedding a chain in the old face.
```
theorem signedPart_prefix {m p : ℕ} (a : Bool) (x : Chains m p) :
    signedPart a (mapChains (coneInclusion m) p x) =
      mapChains (coneInclusion m) p (signedPart a x) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.signedPart, OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.coneInclusion
theorem OAI.Thomason.Construction.SimplexComplex.signedPart_cone line 125
Source documentation
Positive and negative parts commute with coning a chain.
```
theorem signedPart_cone {m p : ℕ} (a : Bool) (x : Chains m p) :
    signedPart a (prism (coneInclusion m) (coneVertex m) (cone_le m) p x) =
      prism (coneInclusion m) (coneVertex m) (cone_le m) p (signedPart a x) := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.signedPart, OAI.Thomason.Construction.SimplexComplex.prism, OAI.Thomason.Construction.SimplexComplex.coneInclusion, OAI.Thomason.Construction.SimplexComplex.coneVertex, OAI.Thomason.Construction.SimplexComplex.cone_le
theorem OAI.Thomason.Construction.SimplexComplex.prefixBasis_ne_coneBasis line 132
Source documentation
An old-face basis simplex cannot contain the new final vertex.
```
theorem prefixBasis_ne_coneBasis {m p : ℕ} (s : Basis m (p + 1)) (t : Basis m p) :
    prefixBasis s ≠ coneBasis t := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.prefixBasis, OAI.Thomason.Construction.SimplexComplex.coneBasis
theorem OAI.Thomason.Construction.SimplexComplex.prefix_cone_disjoint line 141
Source documentation
The two chain operators have disjoint coefficient support.
```
theorem prefix_cone_disjoint {m p : ℕ} (x : Chains m (p + 1)) (y : Chains m p)
    (b : Basis (m + 1) (p + 1)) :
    mapChains (coneInclusion m) (p + 1) x b = 0 ∨
      prism (coneInclusion m) (coneVertex m) (cone_le m) p y b = 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.coneInclusion, OAI.Thomason.Construction.SimplexComplex.prism, OAI.Thomason.Construction.SimplexComplex.coneVertex, OAI.Thomason.Construction.SimplexComplex.cone_le
theorem OAI.Thomason.Construction.SimplexComplex.signedPart_add_of_disjoint line 158
Source documentation
Disjoint supports allow positive and negative parts to distribute.
```
theorem signedPart_add_of_disjoint {m p : ℕ} (a : Bool) (x y : Chains m p)
    (hxy : ∀ b, x b = 0 ∨ y b = 0) :
    signedPart a (x + y) = signedPart a x + signedPart a y := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.signedPart
theorem OAI.Thomason.Construction.SimplexComplex.differential_coefficient_sum line 184
theorem OAI.Thomason.Construction.SimplexComplex.negative_boundary_witness line 190
Source documentation
Negative boundary support comes from a negative basis incidence.
```
theorem negative_boundary_witness {m p : ℕ} (x : Chains m (p+1))
    (hx : x ∈ positive m (p+1)) (b : Basis m p)
    (hb : differential m p x b < 0) :
    ∃ c ∈ x.support, differentialBasis m p 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, OAI.Thomason.Construction.SimplexComplex.differentialBasis
theorem OAI.Thomason.Construction.SimplexComplex.positive_boundary_witness line 205
Source documentation
Positive boundary support comes from a positive basis incidence.
```
theorem positive_boundary_witness {m p : ℕ} (x : Chains m (p+1))
    (hx : x ∈ positive m (p+1)) (b : Basis m p)
    (hb : 0 < differential m p x b) :
    ∃ c ∈ x.support, 0 < differentialBasis m p c b := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.differentialBasis
theorem OAI.Thomason.Construction.SimplexComplex.negative_part_height line 220
Source documentation
Taking a negative signed boundary lowers all supporting basis heights.
```
theorem negative_part_height {m p : ℕ} (x : Chains m (p+1))
    (hx : x ∈ positive m (p+1)) (R : ℤ)
    (hr : ∀ c ∈ x.support, basisHeight c ≤ R) (b : Basis m p)
    (hb : b ∈ (signedPart false (differential m p x)).support) : basisHeight b < R := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.basisHeight, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.signedPart, OAI.Thomason.Construction.SimplexComplex.differential
theorem OAI.Thomason.Construction.SimplexComplex.positive_part_height line 232
Source documentation
Taking a positive signed boundary raises all supporting basis heights.
```
theorem positive_part_height {m p : ℕ} (x : Chains m (p+1))
    (hx : x ∈ positive m (p+1)) (R : ℤ)
    (hr : ∀ c ∈ x.support, R ≤ basisHeight c) (b : Basis m p)
    (hb : b ∈ (signedPart true (differential m p x)).support) : R < basisHeight b := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.basisHeight, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.signedPart, OAI.Thomason.Construction.SimplexComplex.differential
theorem OAI.Thomason.Construction.SimplexComplex.basisAtom_side_bounds line 245
Source documentation
The two entire iterated sides of a basis atom remain on their specified side of its height.
```
theorem basisAtom_side_bounds {h : NormalizedSimplexIdentities} {m p : ℕ}
    {b : Basis m p} {x : h.object m} (hx : IsBasisAtom h b x)
    (side : Bool) (n : ℕ) (hn : n ≤ p) (c : Basis m n) (hc : c ∈ (x.table side n).support) :
    if side then basisHeight b ≤ basisHeight c else basisHeight c ≤ basisHeight b := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.IsBasisAtom, OAI.Thomason.Construction.SimplexComplex.basisHeight
theorem OAI.Thomason.Construction.SimplexComplex.basisAtom_side_height line 269
Source documentation
Below the atom's dimension the height inequalities are strict.
```
theorem basisAtom_side_height {h : NormalizedSimplexIdentities} {m p : ℕ}
    {b : Basis m p} {x : h.object m} (hx : IsBasisAtom h b x)
    (side : Bool) (n : ℕ) (hn : n < p) (c : Basis m n) (hc : c ∈ (x.table side n).support) :
    if side then basisHeight b < basisHeight c else basisHeight c < basisHeight b := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.IsBasisAtom, OAI.Thomason.Construction.SimplexComplex.basisHeight
theorem OAI.Thomason.Construction.SimplexComplex.ordered_basisAtoms_disjoint line 284
Source documentation
Increasingly ordered atoms have precisely the disjoint boundary supports required by the positive binary splitting construction.
```
theorem ordered_basisAtoms_disjoint {h : NormalizedSimplexIdentities} {m p q r : ℕ}
    {a : Basis m p} {b : Basis m q} {A B : h.object m}
    (hA : IsBasisAtom h a A) (hB : IsBasisAtom h b B)
    (hp : r < p) (hq : r < q) (hab : basisHeight a ≤ basisHeight b) (c : Basis m r) :
    A.table false r c = 0 ∨ B.table true r c = 0 := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.IsBasisAtom, OAI.Thomason.Construction.SimplexComplex.basisHeight