PosetPrismEndpoints.lean`

71 declarations, 0 contain sorry, 0 declared as axioms

From a strict Gray cylinder to a homotopy of Street nerves

The simplicial map is constructed on actual oriental-valued simplices using the explicit interval Alexander--Whitney map. Naturality includes all simplex operators, hence also degeneracies. No nerve-homotopy assertion from the new manuscript is assumed.

def OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput.simplexMap line 34
theorem OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput.simplexMap_naturality line 37
theorem OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput.simplexMap_const line 46
theorem OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput.simplexMap_projection line 55
def OAI.Thomason.Construction.RightGrayInput.diagonal line 70
theorem OAI.Thomason.Construction.RightGrayInput.diagonal_naturality line 74
theorem OAI.Thomason.Construction.RightGrayInput.diagonal_const line 94
theorem OAI.Thomason.Construction.RightGrayInput.diagonal_projection line 101
def OAI.Thomason.Construction.RightGrayInput.nerveCylinder line 115
Source documentation
The interval comparison on the Street nerve, evaluated on a simplex F : O_m → X and an ordinal map [m] → [1].
```
noncomputable def nerveCylinder (X : StrictOmegaCategory.{0}) :
    h.streetNerve.obj X ⊗ Δ[1] ⟶ h.streetNerve.obj (G.cylinder.obj X) where
…
```

theorem OAI.Thomason.Construction.RightGrayInput.nerveCylinder_endpoint line 137

Source documentation

The two simplicial endpoints are exactly the nerves of the strict endpoints.

theorem nerveCylinder_endpoint (X : StrictOmegaCategory.{0}) (a : Bool) :
    (if a then SSet.ι₁ else SSet.ι₀) ≫ G.nerveCylinder aw X =
      h.streetNerve.map ((G.endpoint a).app X) := by
…

theorem OAI.Thomason.Construction.RightGrayInput.nerveCylinder_projection line 155

Source documentation

Collapsing the Gray interval agrees with projection of simplicial sets.

theorem nerveCylinder_projection (X : StrictOmegaCategory.{0}) :
    G.nerveCylinder aw X ≫ h.streetNerve.map (G.projection.app X) =
      fst (h.streetNerve.obj X) Δ[1] := by
…

theorem OAI.Thomason.Construction.RightGrayInput.nerveCylinder_naturality line 177

Source documentation

Naturality in the strict category, needed for relative homotopies.

theorem nerveCylinder_naturality {X Y : StrictOmegaCategory.{0}} (f : X ⟶ Y) :
    h.streetNerve.map f ▷ Δ[1] ≫ G.nerveCylinder aw Y =
      G.nerveCylinder aw X ≫ h.streetNerve.map (G.cylinder.map f) := by
…

def OAI.Thomason.Construction.RightGrayInput.nerveHomotopy line 192

Source documentation

Every strict right Gray cylinder gives an actual simplicial homotopy.

noncomputable def nerveHomotopy {X Y : StrictOmegaCategory.{0}}
    (P : G.cylinder.obj X ⟶ Y) :
    SSet.Homotopy (h.streetNerve.map ((G.endpoint false).app X ≫ P))
      (h.streetNerve.map ((G.endpoint true).app X ≫ P)) where
…

theorem OAI.Thomason.Construction.RightGrayInput.nerveHomotopy_stationary line 218

Source documentation

Whole-cylinder stationarity becomes equality of whole simplicial homotopies.

theorem nerveHomotopy_stationary {A X Y : StrictOmegaCategory.{0}}
    (a : A ⟶ X) (v : A ⟶ Y) (P : G.cylinder.obj X ⟶ Y)
    (hs : G.cylinder.map a ≫ P = G.projection.app A ≫ v) :
    h.streetNerve.map a ▷ Δ[1] ≫ (G.nerveHomotopy aw P).h =
      fst (h.streetNerve.obj A) Δ[1] ≫ h.streetNerve.map v := by
…

theorem OAI.Thomason.Construction.SimplexComplex.sumCells_coefficient_zero line 247
Source documentation
Vanishing of every summand's coefficient gives vanishing of the sum.
```
theorem sumCells_coefficient_zero {h : NormalizedSimplexIdentities} {m : ℕ}
    (as : List (h.object m)) (side : Bool) (n : ℕ) (b : Basis m n)
    (hz : ∀ A ∈ as, A.table side n b = 0) :
    (Cell.PositiveTable.ofCells as).table side n b = 0 := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis

theorem OAI.Thomason.Construction.SimplexComplex.ordered_sum_induction line 259

Source documentation

A composition-closed predicate holding for the individual upper-table pieces holds for their ordered sum, with an explicit zero-table base case.

theorem ordered_sum_induction (h : NormalizedSimplexIdentities) {m : ℕ}
    (r : ℕ) (P : h.object m → Prop)
    (hzero : ∀ X : h.object m, (∀ n, r < n → ∀ side, X.table side n = 0) → P X)
    (hcomp : ∀ (Y Z : h.object m) (hyz), P Y → P Z → P ((h.object m).comp r Y Z hyz))
    (as : List (h.object m))
    (hsep : as.Pairwise (fun A B => ∀ b : Basis m r,
      A.table false r b = 0 ∨ B.table true r b = 0))
    (hone : ∀ A ∈ as, ∀ X : h.object m,
      (∀ n, r < n → ∀ side, X.table side n = A.table side n) → P X)
    (X : h.object m)
    (he : ∀ n, r < n → ∀ side,
      X.table side n = (Cell.PositiveTable.ofCells as).table side n) : P X := by
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.Basis

theorem OAI.Thomason.Construction.SimplexComplex.signedPart_positive line 305
Source documentation
A positive chain has itself as positive part and zero as negative part.
```
theorem signedPart_positive {m p : ℕ} (a : Bool) (x : Chains m p)
    (hx : x ∈ positive m p) : signedPart a x = if a then x else 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.signedPart
theorem OAI.Thomason.Construction.SimplexComplex.signedPart_neg_positive line 313
Source documentation
A negative positive-chain has only a negative part.
```
theorem signedPart_neg_positive {m p : ℕ} (a : Bool) (x : Chains m p)
    (hx : x ∈ positive m p) : signedPart a (-x) = if a then 0 else x := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.signedPart
theorem OAI.Thomason.Construction.SimplexComplex.signedPart_cone_add_prefix line 321
Source documentation
Separate the coned and old-face parts of a boundary.
```
theorem signedPart_cone_add_prefix {m p : ℕ} (a : Bool) (x : Chains m p)
    (y : Chains m (p + 1)) (hy : y ∈ positive m (p + 1)) :
    signedPart a (prism (coneInclusion m) (coneVertex m) (cone_le m) p x +
      mapChains (coneInclusion m) (p + 1) y) =
    prism (coneInclusion m) (coneVertex m) (cone_le m) p (signedPart a x) +
      if a then mapChains (coneInclusion m) (p + 1) y else 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, 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, OAI.Thomason.Construction.SimplexComplex.mapChains
theorem OAI.Thomason.Construction.SimplexComplex.signedPart_cone_sub_prefix line 331
Source documentation
The analogous separation for a negative old-face boundary term.
```
theorem signedPart_cone_sub_prefix {m p : ℕ} (a : Bool) (x : Chains m p)
    (y : Chains m (p + 1)) (hy : y ∈ positive m (p + 1)) :
    signedPart a (prism (coneInclusion m) (coneVertex m) (cone_le m) p x -
      mapChains (coneInclusion m) (p + 1) y) =
    prism (coneInclusion m) (coneVertex m) (cone_le m) p (signedPart a x) +
      if a then 0 else mapChains (coneInclusion m) (p + 1) y := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, 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, OAI.Thomason.Construction.SimplexComplex.mapChains
theorem OAI.Thomason.Construction.SimplexComplex.mapChains_coneVertex_zero line 349
Source documentation
A constant vertex map kills positive-dimensional normalized chains.
```
theorem mapChains_coneVertex_zero {m p : ℕ} (x : Chains m (p + 1)) :
    mapChains (coneVertex m) (p + 1) x = 0 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.coneVertex
theorem OAI.Thomason.Construction.SimplexComplex.coneCell_succ_table line 362
Source documentation
In positive degree the cone table is the coned boundary plus one old face.
```
theorem coneCell_succ_table (h : NormalizedSimplexIdentities) {m : ℕ}
    (x : h.object m) (a : Bool) (p : ℕ) :
    (coneCell h x).table a (p + 1) =
      prism (coneInclusion m) (coneVertex m) (cone_le m) p (x.table a p) +
        if a = decide (Even p) then mapChains (coneInclusion m) (p + 1) (x.table a (p + 1))
          else 0 := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.coneCell, 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.mapChains
theorem OAI.Thomason.Construction.SimplexComplex.coneCell_signedPart line 378
Source documentation
The downward signed-boundary recursion is preserved by coning.
```
theorem coneCell_signedPart (h : NormalizedSimplexIdentities) {m : ℕ}
    (x : h.object m) (p : ℕ)
    (hx : ∀ a, signedPart a (differential m p (x.table a (p + 1))) = x.table a p)
    (a : Bool) :
    signedPart a (differential (m + 1) (p + 1) ((coneCell h x).table a (p + 2))) =
      (coneCell h x).table a (p + 1) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.signedPart, OAI.Thomason.Construction.SimplexComplex.differential, OAI.Thomason.Construction.SimplexComplex.coneCell

theorem OAI.Thomason.Construction.SimplexComplex.map_append line 432

Source documentation

Appending an upper endpoint commutes with every monotone target map.

theorem map_append {n k p : ℕ} (b : Fin (n + 1) →o Fin (k + 1))
    (f : Fin (p + 1) →o Fin (n + 1)) (v : Fin (n + 1)) (hv : f (Fin.last p) ≤ v) :
    b.comp (append f v hv) = append (b.comp f) (b v) (b.monotone hv) := by
…

Mentions: OAI.Thomason.Construction.SimplexComplex.append

theorem OAI.Thomason.Construction.SimplexComplex.mapChains_rise line 445
theorem OAI.Thomason.Construction.SimplexComplex.prism_postcomp line 454
Source documentation
Every monotone map of target ordinals preserves the complete prism.
```
theorem prism_postcomp {m n k : ℕ} (f g : Fin (m + 1) →o Fin (n + 1))
    (hfg : ∀ i, f i ≤ g i) (b : Fin (n + 1) →o Fin (k + 1))
    (p : ℕ) (x : Chains m p) :
    mapChains b (p + 1) (prism f g hfg p x) =
      prism (b.comp f) (b.comp g) (fun i => b.monotone (hfg i)) p x := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.mapChains, OAI.Thomason.Construction.SimplexComplex.prism

theorem OAI.Thomason.Construction.SimplexComplex.strictPrism_postcomp line 478

Source documentation

The complete strict prism is independent of the chosen enclosing finite target chain. This also allows noninjective target maps.

theorem strictPrism_postcomp {k : ℕ} (b : Fin (n + 1) →o Fin (k + 1)) :
    strictPrism h hA f g hfg hagree hconstant ≫ h.map b =
      strictPrism h hA (b.comp f) (b.comp g) (fun i => b.monotone (hfg i))
        (fun i hi => congrArg b (hagree i hi))
        (fun x hx y hy => congrArg b (hconstant x hx y hy)) := by
…

Mentions: OAI.Thomason.Construction.SimplexComplex.strictPrism

theorem OAI.Thomason.Construction.SimplexComplex.lowerSet_preimage line 501
Source documentation
Pulling a lower set back along a monotone simplex operator preserves exactly the relative-prism hypotheses.
```
theorem lowerSet_preimage {l : ℕ} (a : Fin (l + 1) →o Fin (m + 1)) :
    IsLowerSet (a ⁻¹' A) := by
…
```

theorem OAI.Thomason.Construction.SimplexComplex.strictPrism_precomp line 507

Source documentation

Source naturality of the entire strict prism, not merely its top atoms.

theorem strictPrism_precomp {l : ℕ} (a : Fin (l + 1) →o Fin (m + 1)) :
    h.cylinderMap a ≫ strictPrism h hA f g hfg hagree hconstant =
      strictPrism h (lowerSet_preimage hA a) (f.comp a) (g.comp a)
        (fun i => hfg (a i)) (fun i hi => hagree (a i) hi)
        (fun x hx y hy => hconstant (a x) hx (a y) hy) := by
…

Mentions: OAI.Thomason.Construction.SimplexComplex.strictPrism, OAI.Thomason.Construction.SimplexComplex.lowerSet_preimage

theorem OAI.Thomason.Construction.RelativePrismImage.mixed_comparable line 558
Source documentation
Every lower image is comparable with every upper image in a simplex.
```
theorem mixed_comparable {m : ℕ} (s : Fin (m + 1) →o E) (i j : Fin (m + 1)) :
    f (s i) ≤ g (s j) ∨ g (s j) ≤ f (s i) := by
…
```
def OAI.Thomason.Construction.RelativePrismImage.chain line 569
Source documentation
The actual finite chain containing both endpoint vertex lists.
```
noncomputable def chain {m : ℕ} (s : Fin (m + 1) →o E) : NonemptyFiniteChains E := by
…
```
theorem OAI.Thomason.Construction.RelativePrismImage.mem_chain line 585
theorem OAI.Thomason.Construction.RelativePrismImage.chain_precomp_le line 592
Source documentation
Every simplex operator induces inclusion of the finite prism targets.
```
theorem chain_precomp_le {l m : ℕ} (s : Fin (m + 1) →o E)
    (a : Fin (l + 1) →o Fin (m + 1)) :
    chain hA f g hfg hagree hconstant (s.comp a) ≤ chain hA f g hfg hagree hconstant s := by
…
```
Mentions: OAI.Thomason.Construction.RelativePrismImage.chain
structure OAI.Thomason.Construction.ChainOrdinal line 604
Source documentation
An ordinal enumeration of a nonempty finite chain in a poset.
```
structure ChainOrdinal {E : Type} [PartialOrder E] (S : NonemptyFiniteChains E) where
…
```
def OAI.Thomason.Construction.ChainOrdinal.choose line 613
Source documentation
Every nonempty finite chain has an increasing enumeration.
```
noncomputable def choose (S : NonemptyFiniteChains E) : ChainOrdinal S := by
…
```
Mentions: OAI.Thomason.Construction.ChainOrdinal
def OAI.Thomason.Construction.ChainOrdinal.inclusion line 629
Source documentation
Inclusion of the underlying finite chains, with no re-enumeration.
```
def inclusion (hST : S ≤ T) : S.finset →o T.finset where
…
```
def OAI.Thomason.Construction.ChainOrdinal.map line 634
Source documentation
The ordinal map encoding a chain inclusion under the chosen enumerations.
```
def map (s : ChainOrdinal S) (t : ChainOrdinal T) (hST : S ≤ T) :
    Fin (s.dim + 1) →o Fin (t.dim + 1) :=
…
```
Mentions: OAI.Thomason.Construction.ChainOrdinal
theorem OAI.Thomason.Construction.ChainOrdinal.enum_map line 639
theorem OAI.Thomason.Construction.ChainOrdinal.map_comp line 646
Source documentation
The transition maps are coherent under nested target chains.
```
theorem map_comp (s : ChainOrdinal S) (t : ChainOrdinal T) (u : ChainOrdinal U)
    (hST : S ≤ T) (hTU : T ≤ U) :
    (map t u hTU).comp (map s t hST) = map s u (hST.trans hTU) := by
…
```
Mentions: OAI.Thomason.Construction.ChainOrdinal, OAI.Thomason.Construction.ChainOrdinal.map
theorem OAI.Thomason.Construction.ChainOrdinal.map_refl line 656
structure OAI.Thomason.Construction.RelativePrismData line 684
Source documentation
The poset data used by the relative prism construction.
```
structure RelativePrismData (E : Type) [PartialOrder E] where
…
```
def OAI.Thomason.Construction.RelativePrismData.image line 697
def OAI.Thomason.Construction.RelativePrismData.ordinal line 700
def OAI.Thomason.Construction.RelativePrismData.evaluate line 703
def OAI.Thomason.Construction.RelativePrismData.firstIndex line 708
def OAI.Thomason.Construction.RelativePrismData.lastIndex line 715
theorem OAI.Thomason.Construction.RelativePrismData.evaluate_firstIndex line 723
theorem OAI.Thomason.Construction.RelativePrismData.evaluate_lastIndex line 729
theorem OAI.Thomason.Construction.RelativePrismData.evaluate_injective line 734
theorem OAI.Thomason.Construction.RelativePrismData.index_le line 740
theorem OAI.Thomason.Construction.RelativePrismData.index_agree line 744
theorem OAI.Thomason.Construction.RelativePrismData.index_constant line 749
theorem OAI.Thomason.Construction.RelativePrismData.old_preimage_lower line 755
def OAI.Thomason.Construction.RelativePrismData.transition line 759
theorem OAI.Thomason.Construction.RelativePrismData.evaluate_transition line 766
theorem OAI.Thomason.Construction.RelativePrismData.transition_first line 771
theorem OAI.Thomason.Construction.RelativePrismData.transition_last line 779
def OAI.Thomason.Construction.RelativePrismData.localPrism line 788
Source documentation
The local strict prism takes values in the oriental of the finite image chain.
```
noncomputable def localPrism (h : NormalizedSimplexIdentities) {m : ℕ}
    (s : Fin (m + 1) →o E) : h.cylinderObject m ⟶ h.object (D.ordinal s).dim :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

theorem OAI.Thomason.Construction.RelativePrismData.localPrism_congr line 795

Source documentation

The relative set certifies positivity; the actual map depends only on its two endpoint lists.

theorem localPrism_congr (h : NormalizedSimplexIdentities) {m n : ℕ}
    {A B : Set (Fin (m + 1))} (hA : IsLowerSet A) (hB : IsLowerSet B)
    (f g f' g' : Fin (m + 1) →o Fin (n + 1))
    (hfg : ∀ i, f i ≤ g i) (hfg' : ∀ i, f' i ≤ g' i)
    (ha : ∀ i ∈ A, f i = g i) (ha' : ∀ i ∈ B, f' i = g' i)
    (hc : ∀ x ∉ A, ∀ y ∉ A, g x = g y)
    (hc' : ∀ x ∉ B, ∀ y ∉ B, g' x = g' y)
    (hf : f = f') (hg : g = g') :
    SimplexComplex.strictPrism h hA f g hfg ha hc =
      SimplexComplex.strictPrism h hB f' g' hfg' ha' hc' := by
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.strictPrism

theorem OAI.Thomason.Construction.RelativePrismData.localPrism_naturality line 811
Source documentation
All faces and degeneracies commute with the local strict prism, after embedding its finite target chain in the larger target chain.
```
theorem localPrism_naturality (h : NormalizedSimplexIdentities) {l m : ℕ}
    (s : Fin (m + 1) →o E) (a : Fin (l + 1) →o Fin (m + 1)) :
    h.cylinderMap a ≫ D.localPrism h s =
      D.localPrism h (s.comp a) ≫ h.map (D.transition s a) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities
def OAI.Thomason.Construction.RelativePrismData.chainPiece line 848
Source documentation
The finite local chain prism, now with values in the categorified nerve.
```
noncomputable def chainPiece {m : ℕ} (s : Fin (m + 1) →o E) :
    h.cylinderObject m ⟶ h.categorification.obj (nerve E) :=
…
```

theorem OAI.Thomason.Construction.RelativePrismData.chainPiece_naturality line 853

Source documentation

No choice of finite target is visible in the glued local maps.

theorem chainPiece_naturality {l m : ℕ} (s : Fin (m + 1) →o E)
    (a : Fin (l + 1) →o Fin (m + 1)) :
    h.cylinderMap a ≫ D.chainPiece h s = D.chainPiece h (s.comp a) := by
…

def OAI.Thomason.Construction.RelativePrismData.piece line 875

Source documentation

Transport of a local piece to the right Gray cylinder.

noncomputable def piece {m : ℕ} (s : Fin (m + 1) →o E) :
    G.cylinder.obj (h.object m) ⟶ h.categorification.obj (nerve E) :=
…

theorem OAI.Thomason.Construction.RelativePrismData.piece_naturality line 879

theorem OAI.Thomason.Construction.RelativePrismData.pieces_compatible line 896

Source documentation

The local maps form a cocone over the actual simplex presentation.

theorem pieces_compatible {i j : CostructuredArrow SSet.stdSimplex (nerve E)} (a : i ⟶ j) :
    G.cylinder.map (h.cosimplicial.map a.left) ≫
        D.piece h G (simplexOrder (SSet.yonedaEquiv j.hom)) =
      D.piece h G (simplexOrder (SSet.yonedaEquiv i.hom)) := by
…

theorem OAI.Thomason.Construction.RelativePrismData.exists_prism line 908

Source documentation

Existence and uniqueness of the assembled strict relative prism.

theorem exists_prism :
    ∃! P : G.cylinder.obj (h.categorification.obj (nerve E)) ⟶ h.categorification.obj (nerve E),
      ∀ s : CostructuredArrow SSet.stdSimplex (nerve E),
        G.cylinder.map (h.simplexLeg s.hom) ≫ P =
          D.piece h G (simplexOrder (SSet.yonedaEquiv s.hom)) := by
…

def OAI.Thomason.Construction.RelativePrismData.prism line 917
Source documentation
The strict cylinder is defined using the proved unique assembly.
```
noncomputable def prism :
    G.cylinder.obj (h.categorification.obj (nerve E)) ⟶ h.categorification.obj (nerve E) :=
…
```
theorem OAI.Thomason.Construction.RelativePrismData.prism_fac line 921

theorem OAI.Thomason.Construction.RelativePrismData.piece_endpoint line 948

Source documentation

The local endpoint equation survives passage from the finite image chain to the whole poset.

theorem piece_endpoint {m : ℕ} (s : Fin (m + 1) →o E) (a : Bool) :
    (G.endpoint a).app (h.object m) ≫ D.piece h G s =
      h.posetLeg ((if a then D.last else D.first).comp s) := by
…

theorem OAI.Thomason.Construction.RelativePrismData.prism_fac_poset line 977
Source documentation
The assembled prism restricts to the specified piece on every simplex.
```
theorem prism_fac_poset {m : ℕ} (s : Fin (m + 1) →o E) :
    G.cylinder.map (h.posetLeg s) ≫ D.prism h G = D.piece h G s := by
…
```

theorem OAI.Thomason.Construction.RelativePrismData.prism_endpoint line 985

Source documentation

Both endpoints are the actual functors induced on categorifications.

theorem prism_endpoint (a : Bool) :
    (G.endpoint a).app (h.categorification.obj (nerve E)) ≫ D.prism h G =
      h.categorification.map (nerveMap (if a then D.last else D.first).monotone.functor) := by
…