OrientalLabelFibers.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Full initial oriental faces from positive chains

The chain support proof determines every table entry from the initial segment containing its two object boundaries. No atom-generation theorem is used in this initial-face specialization.

theorem OAI.Thomason.Construction.SimplexComplex.table_zero_eq_vertex line 23
Source documentation
Degree zero of a cell is the named vertex of its object boundary.
```
theorem table_zero_eq_vertex (h : NormalizedSimplexIdentities) {m : ℕ}
    (x : h.object m) (a : Bool) :
    x.table a 0 = Finsupp.single (vertexBasis (objectIndex h a x)) 1 := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertexBasis, OAI.Thomason.Construction.SimplexComplex.objectIndex
theorem OAI.Thomason.Construction.SimplexComplex.table_support_below line 32
Source documentation
Every positive chain in the table is supported below the two endpoints.
```
theorem table_support_below (h : NormalizedSimplexIdentities) {m : ℕ}
    (x : h.object m) (q : Fin (m+1))
    (hs : objectIndex h false x ≤ q) (ht : objectIndex h true x ≤ q) :
    ∀ p a (b : Basis m p), q < b (Fin.last p) → x.table a p b = 0 := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.objectIndex, OAI.Thomason.Construction.SimplexComplex.Basis
theorem OAI.Thomason.Construction.SimplexComplex.mapBasis_eq_self_of_fixes line 55
Source documentation
A vertex map fixing the vertices of a basis simplex fixes its chain.
```
theorem mapBasis_eq_self_of_fixes {m p : ℕ} (f : Fin (m+1) →o Fin (m+1))
    (b : Basis m p) (hf : ∀ i, f (b i) = b i) :
    mapBasis f p b = Finsupp.single b 1 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.mapBasis
theorem OAI.Thomason.Construction.SimplexComplex.mapChains_eq_self_of_fixes line 68
Source documentation
A chain supported on fixed basis simplices is fixed by the induced map.
```
theorem mapChains_eq_self_of_fixes {m p : ℕ} (f : Fin (m+1) →o Fin (m+1))
    (c : Chains m p) (hf : ∀ b ∈ c.support, ∀ i, f (b i) = b i) :
    mapChains f p c = c := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.mapChains
theorem OAI.Thomason.Construction.SimplexComplex.initialClamp_fixes_cell line 83
Source documentation
Clamping to an initial segment fixes an entire cell whose endpoints already lie in that segment.
```
theorem initialClamp_fixes_cell (h : NormalizedSimplexIdentities) {q m : ℕ}
    (hqm : q ≤ m) (x : h.object m)
    (hs : (objectIndex h false x).val ≤ q) (ht : (objectIndex h true x).val ≤ q) :
    (h.map ((initialFace hqm).toOrderHom.comp (initialClamp hqm))).toFun x = x := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.objectIndex, OAI.Thomason.Construction.SimplexComplex.initialFace, OAI.Thomason.Construction.SimplexComplex.initialClamp
theorem OAI.Thomason.Construction.SimplexComplex.initialFace_full line 102
Source documentation
Every cell with both endpoints in an initial face lies in its actual image.
```
theorem initialFace_full (h : NormalizedSimplexIdentities) {q m : ℕ}
    (hqm : q ≤ m) (x : h.object m)
    (hs : (objectIndex h false x).val ≤ q) (ht : (objectIndex h true x).val ≤ q) :
    x ∈ Set.range (h.map (initialFace hqm).toOrderHom).toFun := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.objectIndex, OAI.Thomason.Construction.SimplexComplex.initialFace
theorem OAI.Thomason.Construction.SimplexComplex.table_support_above line 128
Source documentation
Every chain in the cell table is supported above both object boundaries.
```
theorem table_support_above (h : NormalizedSimplexIdentities) {m : ℕ}
    (x : h.object m) (q : Fin (m + 1))
    (hs : q ≤ objectIndex h false x) (ht : q ≤ objectIndex h true x) :
    ∀ p a (b : Basis m p), b 0 < q → x.table a p b = 0 := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.objectIndex, OAI.Thomason.Construction.SimplexComplex.Basis
theorem OAI.Thomason.Construction.SimplexComplex.finalClamp_fixes_cell line 151
Source documentation
Clamping into the final face fixes every cell whose endpoints lie there.
```
theorem finalClamp_fixes_cell (h : NormalizedSimplexIdentities) {q m : ℕ}
    (hqm : q ≤ m) (x : h.object m)
    (hs : m - q ≤ (objectIndex h false x).val) (ht : m - q ≤ (objectIndex h true x).val) :
    (h.map ((finalFace hqm).toOrderHom.comp (finalClamp hqm))).toFun x = x := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.objectIndex, OAI.Thomason.Construction.SimplexComplex.finalFace, OAI.Thomason.Construction.SimplexComplex.finalClamp
theorem OAI.Thomason.Construction.SimplexComplex.finalFace_full line 172
Source documentation
The actual final ordinal face is full on its endpoint vertices.
```
theorem finalFace_full (h : NormalizedSimplexIdentities) {q m : ℕ}
    (hqm : q ≤ m) (x : h.object m)
    (hs : m - q ≤ (objectIndex h false x).val) (ht : m - q ≤ (objectIndex h true x).val) :
    x ∈ Set.range (h.map (finalFace hqm).toOrderHom).toFun := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.objectIndex, OAI.Thomason.Construction.SimplexComplex.finalFace
def OAI.Thomason.Construction.SimplexComplex.binaryLabel line 201
Source documentation
A binary vertex label extends to a strict walking-arrow label.
```
noncomputable def binaryLabel (h : NormalizedSimplexIdentities) {m : ℕ}
    (b : Fin (m + 1) →o Fin 2) : h.object m ⟶ StrictPoset.category (Fin 2) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.SimplexComplex.binaryLabel_fullCell_iff line 206
Source documentation
On every cell, a binary fibre is detected on both object boundaries.
```
theorem binaryLabel_fullCell_iff (h : NormalizedSimplexIdentities) {m : ℕ}
    (b : Fin (m + 1) →o Fin 2) (e : Fin 2) (x : h.object m) :
    (h.object m).FullCell {z | (binaryLabel h b).toFun z = StrictPoset.identity e} x ↔
      FullOnVertices h {i | b i = e} x := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.binaryLabel, OAI.Thomason.Construction.StrictPoset.identity, OAI.Thomason.Construction.SimplexComplex.FullOnVertices
def OAI.Thomason.Construction.SimplexComplex.labelFiberToVertices line 221
Source documentation
Forget only the definitional description of fibre membership.
```
noncomputable def labelFiberToVertices (h : NormalizedSimplexIdentities) {m : ℕ}
    (b : Fin (m + 1) →o Fin 2) (e : Fin 2) :
    labelFiber (binaryLabel h b) e ⟶ vertexFullSubcategory h {i | b i = e} where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.binaryLabel, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory
def OAI.Thomason.Construction.SimplexComplex.labelFiberVerticesIso line 230
Source documentation
The label fibre is isomorphic to the actual full subcategory on its vertices.
```
noncomputable def labelFiberVerticesIso (h : NormalizedSimplexIdentities) {m : ℕ}
    (b : Fin (m + 1) →o Fin 2) (e : Fin 2) :
    labelFiber (binaryLabel h b) e ≅ vertexFullSubcategory h {i | b i = e} :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.binaryLabel, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory
theorem OAI.Thomason.Construction.SimplexComplex.labelFiberVerticesIso_inclusion line 243
Source documentation
The fibre isomorphism commutes with the given ambient inclusion.
```
theorem labelFiberVerticesIso_inclusion (h : NormalizedSimplexIdentities) {m : ℕ}
    (b : Fin (m + 1) →o Fin 2) (e : Fin 2) :
    (labelFiberVerticesIso h b e).hom ≫
      (h.object m).fullInclusion {x | objectIndex h false x ∈ {i | b i = e}} =
      labelFiberInclusion (binaryLabel h b) e := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.labelFiberVerticesIso, OAI.Thomason.Construction.SimplexComplex.objectIndex, OAI.Thomason.Construction.SimplexComplex.binaryLabel
theorem OAI.Thomason.Construction.SimplexComplex.binaryLabel_zero_initial line 252
Source documentation
The zero-labelled vertices always form an initial segment.
```
theorem binaryLabel_zero_initial {m : ℕ} (b : Fin (m + 1) →o Fin 2) :
    IsLowerSet {i | b i = 0} := by
…
```
theorem OAI.Thomason.Construction.SimplexComplex.binaryLabel_one_final line 258
Source documentation
The one-labelled vertices always form a final segment.
```
theorem binaryLabel_one_final {m : ℕ} (b : Fin (m + 1) →o Fin 2) :
    IsUpperSet {i | b i = 1} := by
…
```
theorem OAI.Thomason.Construction.SimplexComplex.zeroFiber_oriental line 266
Source documentation
Nonempty zero-fibres are precisely smaller orientals.
```
theorem zeroFiber_oriental {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {m : ℕ} (b : Fin (m + 1) →o Fin 2) (hne : Set.Nonempty {i | b i = 0}) :
    ∃ q : Fin (m + 1), Nonempty (h.object q.val ≅ labelFiber (binaryLabel h b) 0) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.binaryLabel
theorem OAI.Thomason.Construction.SimplexComplex.oneFiber_oriental line 273
Source documentation
Nonempty one-fibres are precisely smaller orientals.
```
theorem oneFiber_oriental {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {m : ℕ} (b : Fin (m + 1) →o Fin 2) (hne : Set.Nonempty {i | b i = 1}) :
    ∃ q : Fin (m + 1), Nonempty (h.object q.val ≅ labelFiber (binaryLabel h b) 1) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.binaryLabel
theorem OAI.Thomason.Construction.SimplexComplex.labelFiber_empty line 280
Source documentation
The fibre over an absent vertex label has no cells.
```
theorem labelFiber_empty (h : NormalizedSimplexIdentities) {m : ℕ}
    (b : Fin (m + 1) →o Fin 2) (e : Fin 2) (he : ¬Set.Nonempty {i | b i = e}) :
    IsEmpty (labelFiber (binaryLabel h b) e) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.binaryLabel