FiniteLabelledPresentation.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Ordered labels after finite reflection

Strict poset targets are already one-dimensional. Their labels therefore descend uniquely through the actual reflection unit, and their object values agree with the proved finite object equivalence.

def OAI.Thomason.Construction.FiniteReflectionInput.truncatedPoset line 24
Source documentation
A strict poset is an object of every positive finite dimension.
```
def truncatedPoset (E : Type) [Preorder E] : Truncated (n + 1) :=
…
```
def OAI.Thomason.Construction.FiniteReflectionInput.descendPosetLabel line 29
Source documentation
Descend an actual strict ordered label through finite reflection.
```
noncomputable def descendPosetLabel {X : StrictOmegaCategory.{0}} {E : Type} [Preorder E]
    (p : X ⟶ StrictPoset.category E) : (r.reflect.obj X).val ⟶ StrictPoset.category E :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.FiniteReflectionInput.descendPosetLabel_fac line 34
Source documentation
The descended label agrees with the original label on all cells.
```
theorem descendPosetLabel_fac {X : StrictOmegaCategory.{0}} {E : Type} [Preorder E]
    (p : X ⟶ StrictPoset.category E) :
    r.adjunction.unit.app X ≫ r.descendPosetLabel p = p := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category

theorem OAI.Thomason.Construction.FiniteReflectionInput.descendPosetLabel_unique line 42

Source documentation

Any two finite labels agreeing on the original category coincide.

theorem descendPosetLabel_unique {X : StrictOmegaCategory.{0}} {E : Type} [Preorder E]
    (p : X ⟶ StrictPoset.category E) (q : (r.reflect.obj X).val ⟶ StrictPoset.category E)
    (hq : r.adjunction.unit.app X ≫ q = p) : q = r.descendPosetLabel p :=
…

Mentions: OAI.Thomason.Construction.StrictPoset.category

def OAI.Thomason.Construction.FiniteReflectionInput.posetObjectsEquiv line 50
Source documentation
Poset objects retain their canonical names after finite categorification.
```
noncomputable def posetObjectsEquiv (E : Type) [PartialOrder E] :
    Objects ((r.categorification h).obj (nerve E)).val ≃ E :=
…
```
def OAI.Thomason.Construction.FiniteReflectionInput.posetEvaluation line 55
Source documentation
The actual finite-dimensional strict evaluation into ordered labels.
```
noncomputable def posetEvaluation (E : Type) [PartialOrder E] :
    ((r.categorification h).obj (nerve E)).val ⟶ StrictPoset.category E :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.FiniteReflectionInput.posetEvaluation_object line 60
Source documentation
This evaluation has the required object values after finite reflection.
```
theorem posetEvaluation_object {E : Type} [PartialOrder E]
    (x : Objects ((r.categorification h).obj (nerve E)).val) :
    (r.posetEvaluation h E).toFun x.val = StrictPoset.identity (r.posetObjectsEquiv h E x) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.identity
theorem OAI.Thomason.Construction.FiniteReflectionInput.posetEvaluation_naturality line 75
Source documentation
Evaluation of finite-dimensional poset cells is natural under monotone maps.
```
theorem posetEvaluation_naturality {E F : Type} [PartialOrder E] [PartialOrder F]
    (f : E →o F) :
    (StrictOmegaCategory.inclusion (n + 1)).map (r.reflect.map (h.posetMap f)) ≫
      r.posetEvaluation h F = r.posetEvaluation h E ≫ StrictPoset.map f := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion, OAI.Thomason.Construction.StrictPoset.map
def OAI.Thomason.Construction.FiniteReflectionInput.membershipLabel line 103
Source documentation
The sieve membership label in every positive finite dimension.
```
noncomputable def membershipLabel {E : Type} [PartialOrder E] (A : Set E) (hA : IsLowerSet A) :
    ((r.categorification h).obj (nerve E)).val ⟶ StrictPoset.category (Fin 2) :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category

theorem OAI.Thomason.Construction.FiniteReflectionInput.membershipLabel_object_zero_iff line 108

Source documentation

Finite membership labels retain the original poset's object criterion.

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

Mentions: OAI.Thomason.Construction.StrictPoset.identity

def OAI.Thomason.Construction.FiniteReflectionInput.simplexCocone line 143
Source documentation
Reflect the actual oriental presentation into the chosen finite dimension.
```
noncomputable def simplexCocone (K : SSet.{0}) :
    Cocone (CostructuredArrow.proj SSet.stdSimplex K ⋙ h.cosimplicial ⋙ r.reflect) :=
…
```
def OAI.Thomason.Construction.FiniteReflectionInput.simplexCocone_isColimit line 148
Source documentation
Its colimit property is preserved by the reflection adjunction.
```
noncomputable def simplexCocone_isColimit (K : SSet.{0}) :
    IsColimit (r.simplexCocone h K) := by
…
```

def OAI.Thomason.Construction.FiniteReflectionInput.labelledSimplexDiagram line 154

Source documentation

The simplex diagram with a fixed finite-dimensional binary label.

noncomputable def labelledSimplexDiagram {K : SSet.{0}}
    (p : (r.categorification h).obj K ⟶ finiteInterval n) :
    CostructuredArrow SSet.stdSimplex K ⥤ Over (finiteInterval n) :=
…

def OAI.Thomason.Construction.FiniteReflectionInput.labelledSimplexCocone line 161

Source documentation

This presentation lives in the finite-dimensional slice itself.

noncomputable def labelledSimplexCocone {K : SSet.{0}}
    (p : (r.categorification h).obj K ⟶ finiteInterval n) :
    Cocone (r.labelledSimplexDiagram h p) := Over.liftCocone (r.simplexCocone h K) p

def OAI.Thomason.Construction.FiniteReflectionInput.labelledSimplexCocone_isColimit line 165

def OAI.Thomason.Construction.FiniteReflectionInput.simplexFiberCocone line 171

Source documentation

Take actual finite-dimensional full endpoint fibres of the pieces.

noncomputable def simplexFiberCocone {K : SSet.{0}}
    (p : (r.categorification h).obj K ⟶ finiteInterval n) (e : Fin 2) :
    Cocone (r.labelledSimplexDiagram h p ⋙ finiteLabelFiberFunctor n e) :=
…

def OAI.Thomason.Construction.FiniteReflectionInput.simplexFiberCocone_isColimit line 177

Source documentation

Their colimit is the finite full fibre.

noncomputable def simplexFiberCocone_isColimit (f : PublishedLabelFiberInput) {K : SSet.{0}}
    (p : (r.categorification h).obj K ⟶ finiteInterval n) (e : Fin 2) :
    IsColimit (r.simplexFiberCocone h p e) := by
…

Mentions: OAI.Thomason.Construction.PublishedLabelFiberInput