RightCylinderPrism.lean`

85 declarations, 0 contain sorry, 0 declared as axioms

The upper atom of a one-generator expression

An expression containing exactly one atom of degree greater than r maps to that atom above r. Lower-dimensional whiskering changes no such table entry. No assumption on the expression's composition levels is needed.

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.mapped_comp_table_left_bounded line 23
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.mapped_comp_table_right_bounded line 38

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.expression_upper_atom line 55

Source documentation

The unique higher occurrence in an expression supplies its actual positive upper atom. The occurrence itself is retained in the conclusion.

theorem expression_upper_atom {C : StrictOmegaCategory.{0}}
    (g : B.AtomIndex → C) (F : C ⟶ K.realization)
    (hg : ∀ a, F.toFun (g a) = B.atomCell a)
    (hd : ∀ a, C.DimensionLE a.1 (g a))
    {x : C} (t : CompositionExpression C g x) (r : ℕ)
    (ht : highCount (fun a : B.AtomIndex => a.1) r t.labels = 1) :
    ∃ a ∈ t.labels, r < a.1 ∧
      ∀ n, r < n → ∀ side, (F.toFun x).table side n = (B.atomCell a).table side n := by
…

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.expression_aboveAtomOrZero line 100
abbrev OAI.Thomason.Construction.PastingGlobeBasis.Basis line 131
Source documentation
A canonical representative of a basis element of two n-globes pasted along a k-face. false denotes the left globe.
```
abbrev Basis (n k p : ℕ) :=
…
```
abbrev OAI.Thomason.Construction.PastingGlobeBasis.Chains line 136
def OAI.Thomason.Construction.PastingGlobeBasis.left line 139
Source documentation
The left globe supplies the chosen representatives of shared faces.
```
def left {n k p : ℕ} (b : DirectedGlobeComplex.Basis n p) : Basis n k p :=
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Basis, OAI.Thomason.Construction.PastingGlobeBasis.Basis
def OAI.Thomason.Construction.PastingGlobeBasis.right line 143
Source documentation
Normalize a right-globe face to its canonical representative.
```
def right {n k p : ℕ} (hkn : k < n) (b : DirectedGlobeComplex.Basis n p) :
    Basis n k p :=
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Basis, OAI.Thomason.Construction.PastingGlobeBasis.Basis
theorem OAI.Thomason.Construction.PastingGlobeBasis.right_below line 151
theorem OAI.Thomason.Construction.PastingGlobeBasis.right_source line 155
theorem OAI.Thomason.Construction.PastingGlobeBasis.degree_le line 161
Source documentation
The dimension bound follows from the basis itself.
```
theorem degree_le {n k p : ℕ} (b : Basis n k p) : p ≤ n := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis
theorem OAI.Thomason.Construction.PastingGlobeBasis.left_or_right line 165
Source documentation
Each canonical basis element comes from one of the two globe bases.
```
theorem left_or_right {n k p : ℕ} (hkn : k < n) (b : Basis n k p) :
    (∃ a : DirectedGlobeComplex.Basis n p, left a = b) ∨
      (∃ a : DirectedGlobeComplex.Basis n p, right hkn a = b) := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.DirectedGlobeComplex.Basis, OAI.Thomason.Construction.PastingGlobeBasis.left, OAI.Thomason.Construction.PastingGlobeBasis.right
def OAI.Thomason.Construction.PastingGlobeBasis.face line 183
Source documentation
Every positive-dimensional basis element has two canonical boundary bases.
```
def face {n k p : ℕ} (hkn : k < n) (a : Bool) (b : Basis n k (p+1)) :
    Basis n k p :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis
theorem OAI.Thomason.Construction.PastingGlobeBasis.face_globular line 189
Source documentation
Source and target of every boundary basis have the same lower faces.
```
theorem face_globular {n k p : ℕ} (hkn : k < n) (a c : Bool)
    (b : Basis n k (p+2)) :
    face hkn a (face hkn false b) = face hkn a (face hkn c b) := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.face
def OAI.Thomason.Construction.PastingGlobeBasis.boundary line 206
Source documentation
Negative and positive boundary, with no cancellation between them.
```
noncomputable def boundary {n k p : ℕ} (hkn : k < n) (b : Basis n k (p+1)) :
    Chains n k p :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.Chains
def OAI.Thomason.Construction.PastingGlobeBasis.differential line 212
Source documentation
Differential on the free abelian groups of canonical bases.
```
noncomputable def differential {n k : ℕ} (hkn : k < n) (p : ℕ) :
    Chains n k (p+1) →ₗ[ℤ] Chains n k p :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Chains
theorem OAI.Thomason.Construction.PastingGlobeBasis.differential_single line 216
theorem OAI.Thomason.Construction.PastingGlobeBasis.differential_boundary line 221
theorem OAI.Thomason.Construction.PastingGlobeBasis.differential_squared line 229
Source documentation
Globularity proves that the explicit boundary squares to zero.
```
theorem differential_squared {n k : ℕ} (hkn : k < n) (p : ℕ)
    (x : Chains n k (p+2)) :
    differential hkn p (differential hkn (p+1) x) = 0 := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Chains, OAI.Thomason.Construction.PastingGlobeBasis.differential
def OAI.Thomason.Construction.PastingGlobeBasis.weight line 237
theorem OAI.Thomason.Construction.PastingGlobeBasis.weight_single line 240
theorem OAI.Thomason.Construction.PastingGlobeBasis.weight_differential line 243
def OAI.Thomason.Construction.PastingGlobeBasis.positive line 250
def OAI.Thomason.Construction.PastingGlobeBasis.complex line 256
Source documentation
The concrete directed complex of the pasted pair, before tensoring.
```
noncomputable def complex (n k : ℕ) (hkn : k < n) : DirectedComplex where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex
def OAI.Thomason.Construction.PastingGlobeBasis.height line 265
Source documentation
A global height on all dimensions of the pasted-globe basis.
```
def height {n k p : ℕ} (b : Basis n k p) : ℤ :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis
theorem OAI.Thomason.Construction.PastingGlobeBasis.height_source_lt line 273
Source documentation
Every negative incidence strictly decreases the global height.
```
theorem height_source_lt {n k p : ℕ} (hkn : k < n) (b : Basis n k (p+1)) :
    height (face hkn false b) < height b := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.height, OAI.Thomason.Construction.PastingGlobeBasis.face
theorem OAI.Thomason.Construction.PastingGlobeBasis.height_lt_target line 282
Source documentation
Every positive incidence strictly increases the global height.
```
theorem height_lt_target {n k p : ℕ} (hkn : k < n) (b : Basis n k (p+1)) :
    height b < height (face hkn true b) := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.height, OAI.Thomason.Construction.PastingGlobeBasis.face
theorem OAI.Thomason.Construction.PastingGlobeBasis.face_ne line 291
Source documentation
Distinct signs of a boundary never overlap in this basis.
```
theorem face_ne {n k p : ℕ} (hkn : k < n) (b : Basis n k (p+1)) :
    face hkn false b ≠ face hkn true b := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.face
theorem OAI.Thomason.Construction.PastingGlobeBasis.height_lt_of_boundary_neg line 300
Source documentation
The order controls the actual negative coefficients of the boundary.
```
theorem height_lt_of_boundary_neg {n k p : ℕ} (hkn : k < n)
    (b : Basis n k (p+1)) (c : Basis n k p) (hc : boundary hkn b c < 0) :
    height c < height b := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.boundary, OAI.Thomason.Construction.PastingGlobeBasis.height
theorem OAI.Thomason.Construction.PastingGlobeBasis.height_lt_of_boundary_pos line 312
Source documentation
The order controls the actual positive coefficients of the boundary.
```
theorem height_lt_of_boundary_pos {n k p : ℕ} (hkn : k < n)
    (b : Basis n k (p+1)) (c : Basis n k p) (hc : 0 < boundary hkn b c) :
    height b < height c := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.boundary, OAI.Thomason.Construction.PastingGlobeBasis.height
def OAI.Thomason.Construction.PastingGlobeBasis.embed line 342
Source documentation
Choose the left or right inclusion of a globe basis.
```
def embed {n k p : ℕ} (hkn : k < n) (s : Bool)
    (b : DirectedGlobeComplex.Basis n p) : Basis n k p :=
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Basis, OAI.Thomason.Construction.PastingGlobeBasis.Basis
theorem OAI.Thomason.Construction.PastingGlobeBasis.face_embed line 347
Source documentation
Both inclusions preserve the two boundary faces.
```
theorem face_embed {n k p : ℕ} (hkn : k < n) (s a : Bool)
    (b : DirectedGlobeComplex.Basis n (p+1)) :
    face hkn a (embed hkn s b) =
      embed hkn s ⟨a, Or.inl (by rcases b.property with h | ⟨h, _⟩ <;> omega)⟩ := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Basis, OAI.Thomason.Construction.PastingGlobeBasis.face, OAI.Thomason.Construction.PastingGlobeBasis.embed
def OAI.Thomason.Construction.PastingGlobeBasis.embedApp line 361
Source documentation
Extend a basis inclusion linearly.
```
def embedApp {n k : ℕ} (hkn : k < n) (s : Bool) (p : ℕ) :
    DirectedGlobeComplex.Chains n p →ₗ[ℤ] Chains n k p :=
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Chains, OAI.Thomason.Construction.PastingGlobeBasis.Chains
theorem OAI.Thomason.Construction.PastingGlobeBasis.embedApp_single line 365
theorem OAI.Thomason.Construction.PastingGlobeBasis.embedApp_differential line 371
Source documentation
The free inclusions commute with the actual chain differentials.
```
theorem embedApp_differential {n k : ℕ} (hkn : k < n) (s : Bool) (p : ℕ)
    (u : DirectedGlobeComplex.Chains n (p+1)) :
    embedApp hkn s p (DirectedGlobeComplex.differential n p u) =
      differential hkn p (embedApp hkn s (p+1) u) := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Chains, OAI.Thomason.Construction.PastingGlobeBasis.embedApp, OAI.Thomason.Construction.DirectedGlobeComplex.differential, OAI.Thomason.Construction.PastingGlobeBasis.differential
theorem OAI.Thomason.Construction.PastingGlobeBasis.embedApp_augmentation line 385
Source documentation
Augmentation is unchanged by either inclusion.
```
theorem embedApp_augmentation {n k : ℕ} (hkn : k < n) (s : Bool)
    (u : DirectedGlobeComplex.Chains n 0) :
    weight n k 0 (embedApp hkn s 0 u) = DirectedGlobeComplex.weight n 0 u := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Chains, OAI.Thomason.Construction.PastingGlobeBasis.weight, OAI.Thomason.Construction.PastingGlobeBasis.embedApp, OAI.Thomason.Construction.DirectedGlobeComplex.weight
theorem OAI.Thomason.Construction.PastingGlobeBasis.embedApp_positive line 394
Source documentation
Every coefficient of an included positive chain remains nonnegative.
```
theorem embedApp_positive {n k p : ℕ} (hkn : k < n) (s : Bool)
    (u : DirectedGlobeComplex.Chains n p) (hu : u ∈ DirectedGlobeComplex.positive n p) :
    embedApp hkn s p u ∈ positive n k p := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Chains, OAI.Thomason.Construction.DirectedGlobeComplex.positive, OAI.Thomason.Construction.PastingGlobeBasis.embedApp, OAI.Thomason.Construction.PastingGlobeBasis.positive
def OAI.Thomason.Construction.PastingGlobeBasis.inclusion line 409
Source documentation
The two actual positive chain inclusions into the pasted basis complex.
```
def inclusion {n k : ℕ} (hkn : k < n) (s : Bool) :
    Hom (DirectedGlobeComplex.complex n) (complex n k hkn) where
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.complex, OAI.Thomason.Construction.PastingGlobeBasis.complex
abbrev OAI.Thomason.Construction.GridGlobeBasis.Basis line 436
abbrev OAI.Thomason.Construction.GridGlobeBasis.Chains line 440
def OAI.Thomason.Construction.GridGlobeBasis.left line 442
def OAI.Thomason.Construction.GridGlobeBasis.targetBasis line 445
def OAI.Thomason.Construction.GridGlobeBasis.embed line 449
theorem OAI.Thomason.Construction.GridGlobeBasis.degree_le line 459
theorem OAI.Thomason.Construction.GridGlobeBasis.embed_self line 462
def OAI.Thomason.Construction.GridGlobeBasis.face line 474
theorem OAI.Thomason.Construction.GridGlobeBasis.face_embed line 478
theorem OAI.Thomason.Construction.GridGlobeBasis.face_globular line 493
def OAI.Thomason.Construction.GridGlobeBasis.boundary line 502
def OAI.Thomason.Construction.GridGlobeBasis.differential line 506
theorem OAI.Thomason.Construction.GridGlobeBasis.differential_single line 510
theorem OAI.Thomason.Construction.GridGlobeBasis.differential_boundary line 515
theorem OAI.Thomason.Construction.GridGlobeBasis.differential_squared line 521
def OAI.Thomason.Construction.GridGlobeBasis.weight line 529
theorem OAI.Thomason.Construction.GridGlobeBasis.weight_single line 532
theorem OAI.Thomason.Construction.GridGlobeBasis.weight_differential line 535
def OAI.Thomason.Construction.GridGlobeBasis.positive line 542
def OAI.Thomason.Construction.GridGlobeBasis.complex line 547
def OAI.Thomason.Construction.GridGlobeBasis.height line 555
def OAI.Thomason.Construction.PastingGlobeBasis.value line 585
Source documentation
The value of a canonical basis in a pair of cell tables.
```
def value {n k p : ℕ} (x y : Cell L) (b : Basis n k p) : L.group p :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis
theorem OAI.Thomason.Construction.PastingGlobeBasis.value_embed line 589
Source documentation
Matching cell tables give the same value on every shared representative.
```
theorem value_embed {n k p : ℕ} (hkn : k < n) (x y : Cell L)
    (hxy : x.face true k = y.face false k) (s : Bool)
    (b : DirectedGlobeComplex.Basis n p) :
    value x y (embed hkn s b) = (if s then y else x).table b.val p := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Basis, OAI.Thomason.Construction.PastingGlobeBasis.value, OAI.Thomason.Construction.PastingGlobeBasis.embed
def OAI.Thomason.Construction.PastingGlobeBasis.descApp line 608
Source documentation
Extend the two cell tables linearly on canonical bases.
```
def descApp {n k : ℕ} (x y : Cell L) (p : ℕ) :
    Chains n k p →ₗ[ℤ] L.group p :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Chains
theorem OAI.Thomason.Construction.PastingGlobeBasis.descApp_single line 612
theorem OAI.Thomason.Construction.PastingGlobeBasis.descApp_embedApp line 617
Source documentation
On either globe inclusion, the universal map reads that globe's table.
```
theorem descApp_embedApp {n k : ℕ} (hkn : k < n) (x y : Cell L)
    (hxy : x.face true k = y.face false k) (s : Bool) (p : ℕ)
    (u : DirectedGlobeComplex.Chains n p) :
    descApp x y p (embedApp hkn s p u) =
      DirectedGlobeComplex.cellApp n (if s then y else x) p u := by
…
```
Mentions: OAI.Thomason.Construction.DirectedGlobeComplex.Chains, OAI.Thomason.Construction.PastingGlobeBasis.descApp, OAI.Thomason.Construction.PastingGlobeBasis.embedApp, OAI.Thomason.Construction.DirectedGlobeComplex.cellApp
theorem OAI.Thomason.Construction.PastingGlobeBasis.descApp_differential line 628
Source documentation
The universal map respects every signed boundary.
```
theorem descApp_differential {n k : ℕ} (hkn : k < n) (x y : Cell L)
    (hxy : x.face true k = y.face false k) (p : ℕ) (u : Chains n k (p+1)) :
    descApp x y p (differential hkn p u) =
      L.differential p (descApp x y (p+1) u) := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Chains, OAI.Thomason.Construction.PastingGlobeBasis.descApp, OAI.Thomason.Construction.PastingGlobeBasis.differential
theorem OAI.Thomason.Construction.PastingGlobeBasis.descApp_augmentation line 649
Source documentation
Both tables have augmentation one on every zero-dimensional basis.
```
theorem descApp_augmentation {n k : ℕ} (x y : Cell L) (u : Chains n k 0) :
    L.augmentation (descApp x y 0 u) = weight n k 0 u := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Chains, OAI.Thomason.Construction.PastingGlobeBasis.descApp, OAI.Thomason.Construction.PastingGlobeBasis.weight
theorem OAI.Thomason.Construction.PastingGlobeBasis.descApp_positive line 659
Source documentation
Positivity of each table entry gives positivity on the full free cone.
```
theorem descApp_positive {n k p : ℕ} (x y : Cell L) (u : Chains n k p)
    (hu : u ∈ positive n k p) : descApp x y p u ∈ L.positive p := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Chains, OAI.Thomason.Construction.PastingGlobeBasis.positive, OAI.Thomason.Construction.PastingGlobeBasis.descApp
def OAI.Thomason.Construction.PastingGlobeBasis.desc line 674
Source documentation
The actual positive chain map specified by two matching cell tables.
```
def desc {n k : ℕ} (hkn : k < n) (x y : Cell L)
    (hxy : x.face true k = y.face false k) : Hom (complex n k hkn) L where
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.complex
theorem OAI.Thomason.Construction.PastingGlobeBasis.inclusion_desc line 682
Source documentation
Restricting the universal map to either half recovers that half's table.
```
theorem inclusion_desc {n k : ℕ} (hkn : k < n) (x y : Cell L)
    (hxy : x.face true k = y.face false k) (s : Bool) :
    Hom.comp (inclusion hkn s) (desc hkn x y hxy) =
      DirectedGlobeComplex.cellMap n (if s then y else x) := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.inclusion, OAI.Thomason.Construction.PastingGlobeBasis.desc, OAI.Thomason.Construction.DirectedGlobeComplex.cellMap
theorem OAI.Thomason.Construction.PastingGlobeBasis.hom_ext line 691
Source documentation
The two globe inclusions jointly determine every positive chain map.
```
theorem hom_ext {n k : ℕ} (hkn : k < n) {f g : Hom (complex n k hkn) L}
    (hleft : Hom.comp (inclusion hkn false) f = Hom.comp (inclusion hkn false) g)
    (hright : Hom.comp (inclusion hkn true) f = Hom.comp (inclusion hkn true) g) : f = g := by
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.complex, OAI.Thomason.Construction.PastingGlobeBasis.inclusion

inductive OAI.Thomason.Construction.RightCylinderBasis.Basis line 739

Source documentation

The direct-sum basis of the right tensor with the oriented interval.

inductive Basis (B : ℕ → Type*) : ℕ → Type _
  | endpoint {p : ℕ} (a : Bool) (b : B p) : Basis B p
  | mixed {p : ℕ} (b : B p) : Basis B (p+1)

/-- The negative endpoint in the boundary of `b ⊗ [0,1]`. -/

def OAI.Thomason.Construction.RightCylinderBasis.sourceEndpoint line 744
Source documentation
The negative endpoint in the boundary of b ⊗ [0,1].
```
def sourceEndpoint (p : ℕ) : Bool := decide (p % 2 = 1)
```

def OAI.Thomason.Construction.RightCylinderBasis.height line 747

Source documentation

Threefold spacing keeps the endpoint offsets inside their original slot.

def height (h : ∀ p, B p → ℤ) : {p : ℕ} → Basis B p → ℤ
  | p, .endpoint a b => 3*h p b + if a = sourceEndpoint p then -1 else 1
  | p+1, .mixed b => 3*h p b

/-- Every incidence of the signed tensor differential, indexed by its sign.
`false` denotes negative and `true` denotes positive. -/

Mentions: OAI.Thomason.Construction.RightCylinderBasis.Basis, OAI.Thomason.Construction.RightCylinderBasis.sourceEndpoint

inductive OAI.Thomason.Construction.RightCylinderBasis.Incidence line 753

Source documentation

Every incidence of the signed tensor differential, indexed by its sign. false denotes negative and true denotes positive.

inductive Incidence (R : ∀ p, Bool → B p → B (p+1) → Prop) :
    (p : ℕ) → Bool → Basis B p → Basis B (p+1) → Prop
  | endpoint {p : ℕ} {s : Bool} {c : B p} {b : B (p+1)}
      (a : Bool) (hr : R p s c b) :
      Incidence R p s (.endpoint a c) (.endpoint a b)
  | mixed {p : ℕ} {s : Bool} {c : B p} {b : B (p+1)} (hr : R p s c b) :
      Incidence R (p+1) s (.mixed c) (.mixed b)
  | source {p : ℕ} (b : B p) :
      Incidence R p false (.endpoint (sourceEndpoint p) b) (.mixed b)
  | target {p : ℕ} (b : B p) :
      Incidence R p true (.endpoint (!(sourceEndpoint p)) b) (.mixed b)

Mentions: OAI.Thomason.Construction.RightCylinderBasis.Basis, OAI.Thomason.Construction.RightCylinderBasis.sourceEndpoint

theorem OAI.Thomason.Construction.RightCylinderBasis.height_incidence line 767
Source documentation
A base order compatible with negative and positive incidences extends to all signed incidences of the right-cylinder differential.
```
theorem height_incidence
    (h : ∀ p, B p → ℤ) (R : ∀ p, Bool → B p → B (p+1) → Prop)
    (hR : ∀ p s c b, R p s c b → if s then h (p+1) b < h p c else h p c < h (p+1) b)
    {p : ℕ} {s : Bool} {c : Basis B p} {b : Basis B (p+1)}
    (hi : Incidence R p s c b) :
    if s then height h b < height h c else height h c < height h b := by
…
```
Mentions: OAI.Thomason.Construction.RightCylinderBasis.Basis, OAI.Thomason.Construction.RightCylinderBasis.Incidence, OAI.Thomason.Construction.RightCylinderBasis.height
def OAI.Thomason.Construction.RightCylinderBasis.pastingIncidence line 785
Source documentation
The actual two-boundary incidence of the pasted-globe basis.
```
def pastingIncidence {n k : ℕ} (hkn : k < n) (p : ℕ) (a : Bool)
    (c : PastingGlobeBasis.Basis n k p) (b : PastingGlobeBasis.Basis n k (p+1)) : Prop :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.Basis
theorem OAI.Thomason.Construction.RightCylinderBasis.pasting_height_incidence line 790
Source documentation
The explicit pasted-globe cylinder has a strong order in every degree.
```
theorem pasting_height_incidence {n k : ℕ} (hkn : k < n)
    {p : ℕ} {s : Bool} {c : Basis (PastingGlobeBasis.Basis n k) p}
    {b : Basis (PastingGlobeBasis.Basis n k) (p+1)}
    (hi : Incidence (pastingIncidence hkn) p s c b) :
    if s then height (fun _ => PastingGlobeBasis.height) b <
        height (fun _ => PastingGlobeBasis.height) c
    else height (fun _ => PastingGlobeBasis.height) c <
        height (fun _ => PastingGlobeBasis.height) b := by
…
```
Mentions: OAI.Thomason.Construction.RightCylinderBasis.Basis, OAI.Thomason.Construction.PastingGlobeBasis.Basis, OAI.Thomason.Construction.RightCylinderBasis.Incidence, OAI.Thomason.Construction.RightCylinderBasis.pastingIncidence, OAI.Thomason.Construction.RightCylinderBasis.height, OAI.Thomason.Construction.PastingGlobeBasis.height
theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.sign_bodd line 826
Source documentation
The sign of a right mixed boundary is controlled by its degree parity.
```
theorem sign_bodd (p : ℕ) : (-1 : ℤ)^p = if p.bodd then -1 else 1 := by
…
```
def OAI.Thomason.Construction.DirectedComplex.RightCylinder.prismSide line 831
Source documentation
Which endpoint occurs in the chosen face of the prism.
```
def prismSide (p : ℕ) (a : Bool) : Bool := if a then !p.bodd else p.bodd
```
def OAI.Thomason.Construction.DirectedComplex.RightCylinder.prismTable line 835
Source documentation
A prism has one endpoint chain and the preceding mixed chain in every positive degree.
```
def prismTable (x : Cell K) (a : Bool) : (p : ℕ) → (rightCylinder K).group p
  | 0 => if a then (0, x.table true 0) else (x.table false 0, 0)
  | p+1 => if prismSide (p+1) a then (0, x.table a (p+1), x.table a p)
      else (x.table a (p+1), 0, x.table a p)

/-- The full prism table satisfies the signed chain equations. -/
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.RightCylinder.group, OAI.Thomason.Construction.DirectedComplex.RightCylinder.prismSide, OAI.Thomason.Construction.DirectedComplex.RightCylinder.prism
theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.prismTable_boundary line 841
Source documentation
The full prism table satisfies the signed chain equations.
```
theorem prismTable_boundary (x : Cell K) (a : Bool) (p : ℕ) :
    (rightCylinder K).differential p (prismTable x a (p+1)) =
      prismTable x true p - prismTable x false p := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.RightCylinder.differential, OAI.Thomason.Construction.DirectedComplex.RightCylinder.prismTable
def OAI.Thomason.Construction.DirectedComplex.RightCylinder.prism line 855
Source documentation
A natural actual cell of the right cylinder associated to every cell.
```
def prism (x : Cell K) : Cell (rightCylinder K) where
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.rightCylinder
theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.prism_dimension line 883
Source documentation
Prisms increase a finite dimension bound by one.
```
theorem prism_dimension {n : ℕ} (x : Cell K) (hx : K.realization.DimensionLE n x) :
    (rightCylinder K).realization.DimensionLE (n+1) (prism x) := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.rightCylinder, OAI.Thomason.Construction.DirectedComplex.RightCylinder.prism
theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.prism_top line 896
Source documentation
A bounded cell contributes its top chain as the literal mixed chain in the top degree of the prism.
```
theorem prism_top {n : ℕ} (x : Cell K) (hx : K.realization.DimensionLE n x) (a : Bool) :
    (prism x).table a (n+1) = (0, 0, x.table a n) := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.RightCylinder.prism
theorem OAI.Thomason.Construction.DirectedComplex.RightCylinder.prism_naturality line 901
Source documentation
Positive chain maps preserve this explicit prism construction.
```
theorem prism_naturality (f : Hom K L) (x : Cell K) :
    Cell.map (map f) (prism x) = prism (Cell.map f x) := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Hom, OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.map, OAI.Thomason.Construction.DirectedComplex.RightCylinder.map, OAI.Thomason.Construction.DirectedComplex.RightCylinder.prism