StrictTerminalConeFunctor.lean`

82 declarations, 0 contain sorry, 0 declared as axioms

Constructed ordered vertex maps of strict oriental functors

The explicitly constructed interval cell supplies a cell between any two ordered vertices. No composition-generation theorem is needed. Consequently a strict functor from an oriental to a poset is precisely its monotone vertex map. This will detect full sieve fibres at the last vertex.

def OAI.Thomason.Construction.NormalizedSimplexIdentities.edgeOrder line 27
Source documentation
The ordinal map selecting a possibly degenerate edge.
```
def edgeOrder {m : ℕ} (i j : Fin (m + 1)) (hij : i ≤ j) : Fin 2 →o Fin (m + 1) where
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.edge line 40
Source documentation
An actual oriental cell from i to j.
```
noncomputable def edge {m : ℕ} (i j : Fin (m + 1)) (hij : i ≤ j) : h.object m :=
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.edge_source line 43
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.edge_target line 49
def OAI.Thomason.Construction.NormalizedSimplexIdentities.vertexOrder line 58
Source documentation
Read the monotone vertex function of a strict functor into a poset.
```
noncomputable def vertexOrder (f : h.object m ⟶ StrictPoset.category E) :
    Fin (m + 1) →o E where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.vertexOrder_label line 74
Source documentation
The label of a vertex is its identity cell, not just its first endpoint.
```
theorem vertexOrder_label (f : h.object m ⟶ StrictPoset.category E)
    (i : Fin (m + 1)) :
    f.toFun (SimplexComplex.vertex h i) = StrictPoset.identity (h.vertexOrder f i) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.SimplexComplex.vertex, OAI.Thomason.Construction.StrictPoset.identity
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.eq_ordinalLabel_vertexOrder line 82
Source documentation
Every strict poset label of an oriental factors through its ordinal label.
```
theorem eq_ordinalLabel_vertexOrder (f : h.object m ⟶ StrictPoset.category E) :
    f = h.ordinalLabel m ≫ StrictPoset.map (h.vertexOrder f) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.map
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.label_zero_iff_last line 94
Source documentation
A binary strict label vanishes on every cell exactly when it vanishes at the last vertex.
```
theorem label_zero_iff_last (f : h.object m ⟶ StrictPoset.category (Fin 2)) :
    (∀ x, f.toFun x = StrictPoset.identity 0) ↔
      f.toFun (SimplexComplex.vertex h (Fin.last m)) = StrictPoset.identity 0 := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.identity, OAI.Thomason.Construction.SimplexComplex.vertex
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.label_one_iff_first line 109
Source documentation
Dually the initial vertex detects the entire one-fibre.
```
theorem label_one_iff_first (f : h.object m ⟶ StrictPoset.category (Fin 2)) :
    (∀ x, f.toFun x = StrictPoset.identity 1) ↔
      f.toFun (SimplexComplex.vertex h 0) = StrictPoset.identity 1 := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.identity, OAI.Thomason.Construction.SimplexComplex.vertex
structure OAI.Thomason.Construction.FiniteReflectionInput line 148
Source documentation
Intelligent truncation into positive finite dimension.
```
structure FiniteReflectionInput (n : ℕ) where
…
```
structure OAI.Thomason.Construction.GrayTruncationInput line 153
Source documentation
Right-interval internal hom preserves the finite dimension bound.
```
structure GrayTruncationInput {h : NormalizedSimplexIdentities} (G : RightGrayInput h) : Prop where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.RightGrayInput
def OAI.Thomason.Construction.FiniteReflectionInput.categorification line 162
def OAI.Thomason.Construction.FiniteReflectionInput.categorificationAdjunction line 165
def OAI.Thomason.Construction.FiniteReflectionInput.thomasonLeft line 169
def OAI.Thomason.Construction.FiniteReflectionInput.thomasonAdjunction line 172
def OAI.Thomason.Construction.RightGrayInput.cylinderRestrictionEquiv line 185
Source documentation
The adjunction chain giving restriction of cylinders along the reflection unit. Its target is an actual finite-dimensional strict category.
```
noncomputable def cylinderRestrictionEquiv (X : StrictOmegaCategory.{0})
    (Y : StrictOmegaCategory.Truncated.{0} (n + 1)) :
    (G.cylinder.obj (r.reflect.obj X).val ⟶ Y.val) ≃ (G.cylinder.obj X ⟶ Y.val) :=
…
```

theorem OAI.Thomason.Construction.RightGrayInput.cylinderRestrictionEquiv_apply line 194

Source documentation

The abstract adjunction bijection is precisely precomposition with q_X ⊗ id, not a different unidentified equivalence.

theorem cylinderRestrictionEquiv_apply (X : StrictOmegaCategory.{0})
    (Y : StrictOmegaCategory.Truncated.{0} (n + 1))
    (P : G.cylinder.obj (r.reflect.obj X).val ⟶ Y.val) :
    G.cylinderRestrictionEquiv t r X Y P = G.cylinder.map (r.adjunction.unit.app X) ≫ P := by
…

theorem OAI.Thomason.Construction.RightGrayInput.factor_cylinder line 215

Source documentation

Every cylinder into a finite-dimensional target descends uniquely through finite reflection in its first factor.

theorem factor_cylinder (X : StrictOmegaCategory.{0})
    (Y : StrictOmegaCategory.Truncated.{0} (n + 1)) (P : G.cylinder.obj X ⟶ Y.val) :
    ∃! Q : G.cylinder.obj (r.reflect.obj X).val ⟶ Y.val,
      G.cylinder.map (r.adjunction.unit.app X) ≫ Q = P := by
…

theorem OAI.Thomason.Construction.RightGrayInput.factor_cylinder_endpoint line 229

Source documentation

Descent identifies both strict endpoints after reflection restriction.

theorem factor_cylinder_endpoint (X : StrictOmegaCategory.{0})
    (Y : StrictOmegaCategory.Truncated.{0} (n + 1))
    (P : G.cylinder.obj X ⟶ Y.val) (Q : G.cylinder.obj (r.reflect.obj X).val ⟶ Y.val)
    (hQ : G.cylinder.map (r.adjunction.unit.app X) ≫ Q = P) (a : Bool) :
    r.adjunction.unit.app X ≫ ((G.endpoint a).app (r.reflect.obj X).val ≫ Q) =
      (G.endpoint a).app X ≫ P := by
…

def OAI.Thomason.Construction.FiniteReflectionInput.finiteCodiscrete line 267
Source documentation
The codiscrete target used to test object sets is already a finite category.
```
def finiteCodiscrete (E : Type) : Truncated (n + 1) :=
…
```
def OAI.Thomason.Construction.FiniteReflectionInput.objectLabelsEquiv line 272
Source documentation
The explicit object/codiscrete bijection, without bundling functions as arrows.
```
def objectLabelsEquiv (C : StrictOmegaCategory.{0}) (E : Type) :
    (Objects C → E) ≃ (C ⟶ codiscrete E) where
…
```
def OAI.Thomason.Construction.FiniteReflectionInput.unitLabelsEquiv line 280
Source documentation
The unit induces a bijection on Boolean object labels.
```
noncomputable def unitLabelsEquiv (X : StrictOmegaCategory.{0}) :
    (Objects (r.reflect.obj X).val → Bool) ≃ (Objects X → Bool) :=
…
```

theorem OAI.Thomason.Construction.FiniteReflectionInput.unitLabelsEquiv_apply line 287

Source documentation

This bijection is actual precomposition with the object map of the unit.

theorem unitLabelsEquiv_apply (X : StrictOmegaCategory.{0})
    (f : Objects (r.reflect.obj X).val → Bool) :
    r.unitLabelsEquiv X f = f ∘ (r.adjunction.unit.app X).toOneFunctor.obj := by
…

theorem OAI.Thomason.Construction.FiniteReflectionInput.unit_objects_bijective line 305
Source documentation
Intelligent truncation preserves and reflects every object, as a consequence of its adjunction alone.
```
theorem unit_objects_bijective (X : StrictOmegaCategory.{0}) :
    Function.Bijective (r.adjunction.unit.app X).toOneFunctor.obj := by
…
```
def OAI.Thomason.Construction.FiniteReflectionInput.unitObjectsEquiv line 319
Source documentation
The resulting canonical equivalence of object sets.
```
noncomputable def unitObjectsEquiv (X : StrictOmegaCategory.{0}) :
    Objects X ≃ Objects (r.reflect.obj X).val :=
…
```

theorem OAI.Thomason.Construction.FiniteReflectionInput.unitObjectsEquiv_naturality line 324

Source documentation

The object equivalence commutes with every strict functor.

theorem unitObjectsEquiv_naturality {X Y : StrictOmegaCategory.{0}} (f : X ⟶ Y)
    (x : Objects X) :
    r.unitObjectsEquiv Y (f.toOneFunctor.obj x) =
      (r.reflect.map f).toOneFunctor.obj (r.unitObjectsEquiv X x) := by
…

def OAI.Thomason.Construction.FiniteReflectionInput.categorificationObjectsEquiv line 334
Source documentation
The objects of finite-dimensional categorification are the original vertices.
```
noncomputable def categorificationObjectsEquiv (K : SSet.{0}) :
    Objects ((r.categorification h).obj K).val ≃ K.obj (.op (.mk 0)) :=
…
```

theorem OAI.Thomason.Construction.FiniteReflectionInput.categorificationObjectsEquiv_naturality line 339

Source documentation

The finite-dimensional vertex identification is natural.

theorem categorificationObjectsEquiv_naturality {K L : SSet.{0}} (f : K ⟶ L)
    (x : Objects ((r.categorification h).obj K).val) :
    r.categorificationObjectsEquiv h L (((r.categorification h).map f).toOneFunctor.obj x) =
      f.app _ (r.categorificationObjectsEquiv h K x) := by
…

def OAI.Thomason.Construction.SimplexComplex.objectIndex line 372
Source documentation
The vertex index of either object boundary of an oriental cell.
```
noncomputable def objectIndex (h : NormalizedSimplexIdentities) {m : ℕ}
    (a : Bool) (x : h.object m) : Fin (m + 1) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities
theorem OAI.Thomason.Construction.SimplexComplex.objectIndex_face_zero line 377
theorem OAI.Thomason.Construction.SimplexComplex.objectIndex_face_succ line 385
theorem OAI.Thomason.Construction.SimplexComplex.objectIndex_comp_zero line 393
theorem OAI.Thomason.Construction.SimplexComplex.objectIndex_comp_succ line 404
def OAI.Thomason.Construction.SimplexComplex.FullOnVertices line 412
Source documentation
An actual cell whose two object boundaries are in the selected vertices.
```
def FullOnVertices (h : NormalizedSimplexIdentities) {m : ℕ}
    (I : Set (Fin (m + 1))) (x : h.object m) : Prop :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities
theorem OAI.Thomason.Construction.SimplexComplex.fullOnVertices_comp_factors line 418
Source documentation
Both factors of a cell supported on a convex vertex set remain supported on that set. This is the key step in induction on a composition expression.
```
theorem fullOnVertices_comp_factors (h : NormalizedSimplexIdentities) {m : ℕ}
    {I : Set (Fin (m + 1))} (hI : Set.OrdConnected I)
    (n : ℕ) (x y : h.object m) (hxy : (h.object m).target n x = (h.object m).source n y)
    (hc : FullOnVertices h I ((h.object m).comp n x y hxy)) :
    FullOnVertices h I x ∧ FullOnVertices h I y := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.FullOnVertices
theorem OAI.Thomason.Construction.SimplexComplex.objectIndex_atom_source line 445
Source documentation
The source index of a simplex atom is its first tuple entry.
```
theorem objectIndex_atom_source {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {m p : ℕ} (b : Basis m p) : objectIndex h false (a.atom b) = b 0 := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.objectIndex
theorem OAI.Thomason.Construction.SimplexComplex.objectIndex_atom_target line 452
Source documentation
The target index of a simplex atom is its last tuple entry.
```
theorem objectIndex_atom_target {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {m p : ℕ} (b : Basis m p) : objectIndex h true (a.atom b) = b (Fin.last p) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.Basis, OAI.Thomason.Construction.SimplexComplex.objectIndex

theorem OAI.Thomason.Construction.SimplexComplex.map_injective_of_retraction line 459

Source documentation

A split ordinal embedding gives an injective map on all oriental cells.

theorem map_injective_of_retraction (h : NormalizedSimplexIdentities) {q m : ℕ}
    (e : Fin (q + 1) →o Fin (m + 1)) (r : Fin (m + 1) →o Fin (q + 1))
    (hre : r.comp e = OrderHom.id) : Function.Injective (h.map e).toFun := by
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

theorem OAI.Thomason.Construction.SimplexComplex.hom_range_comp line 470

Source documentation

The cell image of an injective strict functor is closed under composition.

theorem hom_range_comp {C D : StrictOmegaCategory.{0}} (f : C ⟶ D)
    (hf : Function.Injective f.toFun) (n : ℕ) {x y : D}
    (hxy : D.target n x = D.source n y)
    (hx : x ∈ Set.range f.toFun) (hy : y ∈ Set.range f.toFun) :
    D.comp n x y hxy ∈ Set.range f.toFun := by
…

def OAI.Thomason.Construction.SimplexComplex.factorThroughFace line 482
Source documentation
A tuple whose entries lie in an ordinal face factors monotonically through it.
```
noncomputable def factorThroughFace {q m p : ℕ} (e : Fin (q + 1) ↪o Fin (m + 1))
    (b : Basis m p) (hb : ∀ i, b i ∈ Set.range e) : Fin (p + 1) →o Fin (q + 1) where
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis
theorem OAI.Thomason.Construction.SimplexComplex.factorThroughFace_fac line 492
theorem OAI.Thomason.Construction.SimplexComplex.full_convex_face line 502
Source documentation
Atom generation implies the full-cell assertion for any convex ordinal face with a monotone retraction. This is the needed initial/final-segment statement at the level of actual cells.
```
theorem full_convex_face {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {q m : ℕ} (e : Fin (q + 1) ↪o Fin (m + 1))
    (r : Fin (m + 1) →o Fin (q + 1)) (hre : r.comp e.toOrderHom = OrderHom.id)
    (he : Set.OrdConnected (Set.range e)) :
    ∀ x : h.object m, FullOnVertices h (Set.range e) x →
      x ∈ Set.range (h.map e.toOrderHom).toFun := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.FullOnVertices
theorem OAI.Thomason.Construction.SimplexComplex.objectIndex_map line 526
Source documentation
The endpoint index is natural for all monotone ordinal maps.
```
theorem objectIndex_map (h : NormalizedSimplexIdentities) {q m : ℕ}
    (f : Fin (q + 1) →o Fin (m + 1)) (a : Bool) (x : h.object q) :
    objectIndex h a ((h.map f).toFun x) = f (objectIndex h a x) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.objectIndex
def OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory line 554
Source documentation
The full strict subcategory on the specified oriental vertices.
```
noncomputable def vertexFullSubcategory (h : NormalizedSimplexIdentities) {m : ℕ}
    (I : Set (Fin (m + 1))) : StrictOmegaCategory.{0} :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities
theorem OAI.Thomason.Construction.SimplexComplex.fullCell_vertices_iff line 559
Source documentation
Its all-cell membership is precisely membership of both object endpoints.
```
theorem fullCell_vertices_iff (h : NormalizedSimplexIdentities) {m : ℕ}
    (I : Set (Fin (m + 1))) (x : h.object m) :
    (h.object m).FullCell {x | objectIndex h false x ∈ I} x ↔ FullOnVertices h I x := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.objectIndex, OAI.Thomason.Construction.SimplexComplex.FullOnVertices
def OAI.Thomason.Construction.SimplexComplex.fullFaceMap line 567
Source documentation
Any ordinal face lands in the actual full subcategory on its image vertices.
```
noncomputable def fullFaceMap (h : NormalizedSimplexIdentities) {q m : ℕ}
    (e : Fin (q + 1) ↪o Fin (m + 1)) :
    h.object q ⟶ vertexFullSubcategory h (Set.range e) where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory

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

Source documentation

The smaller oriental is the full strict subcategory on a convex split face.

noncomputable def fullFaceIso {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {q m : ℕ} (e : Fin (q + 1) ↪o Fin (m + 1))
    (r : Fin (m + 1) →o Fin (q + 1)) (hre : r.comp e.toOrderHom = OrderHom.id)
    (he : Set.OrdConnected (Set.range e)) :
    h.object q ≅ vertexFullSubcategory h (Set.range e) :=
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory

theorem OAI.Thomason.Construction.SimplexComplex.fullFaceIso_hom_inclusion line 592

Source documentation

The isomorphism realizes the given ordinal face, not merely an abstract copy.

theorem fullFaceIso_hom_inclusion {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {q m : ℕ} (e : Fin (q + 1) ↪o Fin (m + 1))
    (r : Fin (m + 1) →o Fin (q + 1)) (hre : r.comp e.toOrderHom = OrderHom.id)
    (he : Set.OrdConnected (Set.range e)) :
    (fullFaceIso a e r hre he).hom ≫
      (h.object m).fullInclusion {x | objectIndex h false x ∈ Set.range e} = h.map e.toOrderHom := by
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.fullFaceIso, OAI.Thomason.Construction.SimplexComplex.objectIndex

def OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexPosetLabel line 622
Source documentation
The ordered label on one oriental in the nerve of a poset.
```
noncomputable def simplexPosetLabel {E : Type} [PartialOrder E] {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ nerve E) : h.object m.len ⟶ StrictPoset.category E :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexPosetLabel_precomp line 628

Source documentation

Every simplex operator respects the ordered labels.

theorem simplexPosetLabel_precomp {E : Type} [PartialOrder E] {m n : SimplexCategory}
    (s : SSet.stdSimplex.obj n ⟶ nerve E) (a : m ⟶ n) :
    h.cosimplicial.map a ≫ h.simplexPosetLabel s =
      h.simplexPosetLabel (SSet.stdSimplex.map a ≫ s) := by
…

def OAI.Thomason.Construction.NormalizedSimplexIdentities.posetLabelCocone line 643
Source documentation
The compatible ordered labels form a cocone on the oriental presentation.
```
noncomputable def posetLabelCocone (E : Type) [PartialOrder E] :
    Cocone (CostructuredArrow.proj SSet.stdSimplex (nerve E) ⋙ h.cosimplicial) where
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.posetEvaluation line 655
Source documentation
Evaluation of categorified poset cells in their underlying ordered labels.
```
noncomputable def posetEvaluation (E : Type) [PartialOrder E] :
    h.categorification.obj (nerve E) ⟶ StrictPoset.category E :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetEvaluation_fac line 660

Source documentation

Evaluation on each actual colimit leg is the constructed ordered label.

theorem posetEvaluation_fac {E : Type} [PartialOrder E] {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ nerve E) :
    h.simplexLeg s ≫ h.posetEvaluation E = h.simplexPosetLabel s :=
…

def OAI.Thomason.Construction.NormalizedSimplexIdentities.posetNerveZeroEquiv line 666
Source documentation
In degree zero the ordinary nerve of a poset is its set of elements.
```
def posetNerveZeroEquiv (E : Type) [PartialOrder E] :
    (nerve E).obj (op (.mk 0)) ≃ E where
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.posetObjectsEquiv line 680
Source documentation
The object set of the actual categorified poset nerve is the original poset.
```
noncomputable def posetObjectsEquiv (E : Type) [PartialOrder E] :
    Objects (h.categorification.obj (nerve E)) ≃ E :=
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetEvaluation_object line 685
Source documentation
The ordered evaluation agrees with this object identification.
```
theorem posetEvaluation_object {E : Type} [PartialOrder E]
    (x : Objects (h.categorification.obj (nerve E))) :
    (h.posetEvaluation E).toFun x.val = StrictPoset.identity (h.posetObjectsEquiv E x) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.identity

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetObjectsEquiv_naturality line 703

Source documentation

The poset object identification is natural for monotone maps.

theorem posetObjectsEquiv_naturality {E F : Type} [PartialOrder E] [PartialOrder F]
    (f : E →o F) (x : Objects (h.categorification.obj (nerve E))) :
    h.posetObjectsEquiv F ((h.posetMap f).toOneFunctor.obj x) =
      f (h.posetObjectsEquiv E x) := by
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetEvaluation_naturality line 711
Source documentation
Strict evaluation of ordered labels is natural, on all cells.
```
theorem posetEvaluation_naturality {E F : Type} [PartialOrder E] [PartialOrder F]
    (f : E →o F) :
    h.posetMap f ≫ h.posetEvaluation F = h.posetEvaluation E ≫ StrictPoset.map f := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.map
def OAI.Thomason.Construction.sieveCharacteristic line 743
Source documentation
The monotone zero/one characteristic map of a downward-closed subset.
```
noncomputable def sieveCharacteristic {E : Type} [PartialOrder E]
    (A : Set E) (hA : IsLowerSet A) : E →o Fin 2 := by
…
```
theorem OAI.Thomason.Construction.sieveCharacteristic_zero_iff line 755
def OAI.Thomason.Construction.NormalizedSimplexIdentities.membershipLabel line 766
Source documentation
The actual strict walking-arrow label associated to a poset sieve.
```
noncomputable def membershipLabel {E : Type} [PartialOrder E] (A : Set E) (hA : IsLowerSet A) :
    h.categorification.obj (nerve E) ⟶ StrictPoset.category (Fin 2) :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.membershipLabel_object line 771
Source documentation
Membership labelling on objects is the original poset characteristic map.
```
theorem membershipLabel_object {E : Type} [PartialOrder E] (A : Set E) (hA : IsLowerSet A)
    (x : Objects (h.categorification.obj (nerve E))) :
    (h.membershipLabel A hA).toFun x.val =
      StrictPoset.identity (sieveCharacteristic A hA (h.posetObjectsEquiv E x)) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.identity, OAI.Thomason.Construction.sieveCharacteristic

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.membershipLabel_object_zero_iff line 780

Source documentation

An object lies over zero precisely when its original vertex is in the sieve.

theorem membershipLabel_object_zero_iff {E : Type} [PartialOrder E]
    (A : Set E) (hA : IsLowerSet A) (x : Objects (h.categorification.obj (nerve E))) :
    (h.membershipLabel A hA).toFun x.val = StrictPoset.identity 0 ↔
      h.posetObjectsEquiv E x ∈ A := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.identity

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.membershipLabel_zero_iff line 793

Source documentation

The zero-fiber includes precisely all cells between sieve-labelled objects.

theorem membershipLabel_zero_iff {E : Type} [PartialOrder E]
    (A : Set E) (hA : IsLowerSet A) (x : h.categorification.obj (nerve E)) :
    (h.membershipLabel A hA).toFun x = StrictPoset.identity 0 ↔
      h.posetObjectsEquiv E ((h.categorification.obj (nerve E)).boundaryObject false x) ∈ A ∧
      h.posetObjectsEquiv E ((h.categorification.obj (nerve E)).boundaryObject true x) ∈ A := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.identity

def OAI.Thomason.Construction.NormalizedSimplexIdentities.fiberStreetSubcomplex line 827
Source documentation
The actual full-fibre Street subcomplex of a binary strict label.
```
def fiberStreetSubcomplex (p : C ⟶ StrictPoset.category (Fin 2)) (e : Fin 2) :
    (h.streetNerve.obj C).Subcomplex :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.mem_fiberStreetSubcomplex line 831
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.mem_fiberStreetSubcomplex_zero_iff_last line 838
Source documentation
The last vertex detects membership in every full zero-fibre.
```
theorem mem_fiberStreetSubcomplex_zero_iff_last
    (p : C ⟶ StrictPoset.category (Fin 2)) {m : SimplexCategory}
    (f : h.object m.len ⟶ C) :
    f ∈ (h.fiberStreetSubcomplex p 0).obj (op m) ↔
      p.toFun (f.toFun (SimplexComplex.vertex h (Fin.last m.len))) = StrictPoset.identity 0 :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.SimplexComplex.vertex, OAI.Thomason.Construction.StrictPoset.identity
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.mem_fiberStreetSubcomplex_one_iff_first line 846
Source documentation
The first vertex detects membership in every full one-fibre.
```
theorem mem_fiberStreetSubcomplex_one_iff_first
    (p : C ⟶ StrictPoset.category (Fin 2)) {m : SimplexCategory}
    (f : h.object m.len ⟶ C) :
    f ∈ (h.fiberStreetSubcomplex p 1).obj (op m) ↔
      p.toFun (f.toFun (SimplexComplex.vertex h 0)) = StrictPoset.identity 1 :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.SimplexComplex.vertex, OAI.Thomason.Construction.StrictPoset.identity
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.sieve_street_cover line 854
Source documentation
A cover of the objects by full sieves gives a cover of the actual Street nerve.
```
theorem sieve_street_cover
    (p q : C ⟶ StrictPoset.category (Fin 2))
    (hc : ∀ x : Objects C, p.toFun x.val = StrictPoset.identity 0 ∨
      q.toFun x.val = StrictPoset.identity 0) :
    h.fiberStreetSubcomplex p 0 ⊔ h.fiberStreetSubcomplex q 0 = ⊤ := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.identity

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.cosieve_street_cover line 869

Source documentation

The dual assertion for full cosieves uses the initial vertex.

theorem cosieve_street_cover
    (p q : C ⟶ StrictPoset.category (Fin 2))
    (hc : ∀ x : Objects C, p.toFun x.val = StrictPoset.identity 1 ∨
      q.toFun x.val = StrictPoset.identity 1) :
    h.fiberStreetSubcomplex p 1 ⊔ h.fiberStreetSubcomplex q 1 = ⊤ := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.identity

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.sieve_street_isPushout line 885

Source documentation

The resulting sieve-cover square is an ordinary simplicial pushout, with the intersection formed on the original object labels.

theorem sieve_street_isPushout
    (p q : C ⟶ StrictPoset.category (Fin 2))
    (hc : ∀ x : Objects C, p.toFun x.val = StrictPoset.identity 0 ∨
      q.toFun x.val = StrictPoset.identity 0) :
    IsPushout
      (SSet.Subcomplex.homOfLE (show h.fullStreetSubcomplex C
        ({x | p.toFun x = StrictPoset.identity 0} ∩ {x | q.toFun x = StrictPoset.identity 0}) ≤
        h.fiberStreetSubcomplex p 0 from fun _ _ hf x => ⟨(hf x).1.1, (hf x).2.1⟩))
      (SSet.Subcomplex.homOfLE (show h.fullStreetSubcomplex C
        ({x | p.toFun x = StrictPoset.identity 0} ∩ {x | q.toFun x = StrictPoset.identity 0}) ≤
        h.fiberStreetSubcomplex q 0 from fun _ _ hf x => ⟨(hf x).1.2, (hf x).2.2⟩))
      (h.fiberStreetSubcomplex p 0).ι (h.fiberStreetSubcomplex q 0).ι :=
…

Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.identity

def OAI.Thomason.Construction.NormalizedSimplexIdentities.strictPosetSimplexEquiv line 918
def OAI.Thomason.Construction.NormalizedSimplexIdentities.strictPosetNerveMap line 931
instance OAI.Thomason.Construction.NormalizedSimplexIdentities.strictPosetNerveMap_isIso line 942
def OAI.Thomason.Construction.NormalizedSimplexIdentities.strictPosetNerveIso line 950
Source documentation
The canonical comparison is an isomorphism on the Street nerve, including every degenerate simplex and every ordinal map.
```
def strictPosetNerveIso : h.streetNerve.obj (StrictPoset.category P) ≅ nerve P :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.map_boundaryObject line 969
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.mapCell line 973
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.map line 978
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.map_id line 994
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.map_comp line 999
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.map_label line 1004
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.overFunctor line 1010
Source documentation
The cone construction as a functor to the actual slice over [1].
```
def overFunctor : StrictOmegaCategory.{0} ⥤ Over (StrictPoset.category (Fin 2)) where
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category