StrictTerminalConeCategory.lean`

79 declarations, 0 contain sorry, 0 declared as axioms

Objects of strict categories preserve colimits

The codiscrete strict category on a set is a right adjoint to the object functor. The adjunction identifies the objects of simplex colimits.

def OAI.Thomason.Construction.StrictOmegaCategory.objectFunctor line 28
Source documentation
The actual zero-dimensional objects of a strict category.
```
def objectFunctor : StrictOmegaCategory.{u} ⥤ Type u := underlyingCategory ⋙ Cat.objects
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.underlyingCategory
def OAI.Thomason.Construction.StrictOmegaCategory.Indiscrete line 31
Source documentation
A type endowed with the indiscrete preorder, used only for endpoint labels.
```
def Indiscrete (E : Type u) := E
```
instance OAI.Thomason.Construction.StrictOmegaCategory.(instance at line 33) line 33
def OAI.Thomason.Construction.StrictOmegaCategory.codiscrete line 40
Source documentation
There is a unique cell between each pair of labels, and only identities above dimension one.
```
def codiscrete (E : Type u) : StrictOmegaCategory.{u} := StrictPoset.category (Indiscrete E)
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.Indiscrete
def OAI.Thomason.Construction.StrictOmegaCategory.boundaryObject line 43
Source documentation
The object at either end of a cell.
```
def boundaryObject (C : StrictOmegaCategory.{u}) (a : Bool) (x : C) : Objects C :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Objects
theorem OAI.Thomason.Construction.StrictOmegaCategory.boundaryObject_of_object line 47
def OAI.Thomason.Construction.StrictOmegaCategory.codiscreteLift line 55
Source documentation
Any assignment of object labels extends to the codiscrete strict category.
```
def codiscreteLift {C : StrictOmegaCategory.{u}} {E : Type u} (f : Objects C → E) :
    C ⟶ codiscrete E where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Objects, OAI.Thomason.Construction.StrictOmegaCategory.codiscrete
def OAI.Thomason.Construction.StrictOmegaCategory.codiscreteLabel line 91
Source documentation
Read the label of a zero-cell in a codiscrete target.
```
def codiscreteLabel {C : StrictOmegaCategory.{u}} {E : Type u} (f : C ⟶ codiscrete E) :
    Objects C → E := fun x => (f.toFun x.val).first
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.codiscrete, OAI.Thomason.Construction.StrictOmegaCategory.Objects
theorem OAI.Thomason.Construction.StrictOmegaCategory.codiscreteLabel_lift line 95
theorem OAI.Thomason.Construction.StrictOmegaCategory.codiscreteLift_label line 102
Source documentation
A functor into a codiscrete category is determined by its object labels.
```
theorem codiscreteLift_label {C : StrictOmegaCategory.{u}} {E : Type u}
    (f : C ⟶ codiscrete E) : codiscreteLift (codiscreteLabel f) = f := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.codiscrete, OAI.Thomason.Construction.StrictOmegaCategory.codiscreteLift, OAI.Thomason.Construction.StrictOmegaCategory.codiscreteLabel
def OAI.Thomason.Construction.StrictOmegaCategory.codiscreteFunctor line 115
Source documentation
Relabelling codiscrete categories is functorial.
```
def codiscreteFunctor : Type u ⥤ StrictOmegaCategory.{u} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.objectAdjunction line 122
Source documentation
The object/codiscrete adjunction, proved from the explicit endpoint formula.
```
def objectAdjunction : objectFunctor.{u} ⊣ codiscreteFunctor.{u} :=
…
```
instance OAI.Thomason.Construction.StrictOmegaCategory.objectFunctor_preservesColimits line 140
Source documentation
Object sets of arbitrary strict-category colimits are their set colimits.
```
instance objectFunctor_preservesColimits : PreservesColimitsOfSize.{u, u} objectFunctor.{u} :=
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.finiteObjectFunctor line 160
Source documentation
The actual object functor on positive finite strict categories.
```
def finiteObjectFunctor (n : ℕ) : Truncated.{0} (n + 1) ⥤ Type :=
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.finiteCodiscreteFunctor line 164
Source documentation
Codiscrete categories already satisfy every positive dimension bound.
```
def finiteCodiscreteFunctor (n : ℕ) : Type ⥤ Truncated.{0} (n + 1) where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.finiteObjectAdjunction line 172
Source documentation
The direct adjunction in the actual finite category.
```
def finiteObjectAdjunction (n : ℕ) : finiteObjectFunctor n ⊣ finiteCodiscreteFunctor n :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.finiteObjectFunctor, OAI.Thomason.Construction.StrictOmegaCategory.finiteCodiscreteFunctor
instance OAI.Thomason.Construction.StrictOmegaCategory.finiteObjectFunctor_preservesColimits line 189

theorem OAI.Thomason.Construction.StrictOmegaCategory.finite_pushout_objects_covered line 194

Source documentation

Every object of a finite-dimensional pushout comes from a summand.

theorem finite_pushout_objects_covered {n : ℕ} {A B X Y : Truncated.{0} (n + 1)}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) (y : Objects Y.val) :
    (∃ x : Objects B.val, b.toOneFunctor.obj x = y) ∨
      ∃ x : Objects X.val, j.toOneFunctor.obj x = y :=
…

Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Objects

def OAI.Thomason.Construction.SimplexComplex.vertexBasis line 220
Source documentation
The zero-simplex at a specified vertex.
```
def vertexBasis {m : ℕ} (i : Fin (m + 1)) : Basis m 0 :=
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis
theorem OAI.Thomason.Construction.SimplexComplex.vertexBasis_apply line 228
theorem OAI.Thomason.Construction.SimplexComplex.basis_zero_eq_vertex line 230
theorem OAI.Thomason.Construction.SimplexComplex.positive_augmentation_one line 238
Source documentation
Positivity and augmentation force a degree-zero chain to be one vertex.
```
theorem positive_augmentation_one {m : ℕ} (x : Chains m 0)
    (hx : x ∈ positive m 0) (haug : augmentation m x = 1) :
    ∃ i : Fin (m + 1), x = Finsupp.single (vertexBasis i) 1 := by
…
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Chains, OAI.Thomason.Construction.SimplexComplex.positive, OAI.Thomason.Construction.SimplexComplex.augmentation, OAI.Thomason.Construction.SimplexComplex.vertexBasis
def OAI.Thomason.Construction.SimplexComplex.vertex line 275
Source documentation
The strict zero-cell at a vertex, as a full positive globular table.
```
noncomputable def vertex (h : NormalizedSimplexIdentities) {m : ℕ} (i : Fin (m + 1)) : h.object m where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities
theorem OAI.Thomason.Construction.SimplexComplex.vertex_dimensionLE line 293
Source documentation
The constructed vertex is zero-dimensional.
```
theorem vertex_dimensionLE (h : NormalizedSimplexIdentities) {m : ℕ} (i : Fin (m + 1)) :
    (h.object m).DimensionLE 0 (vertex h i) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertex
theorem OAI.Thomason.Construction.SimplexComplex.eq_vertex_of_dimensionLE line 299
Source documentation
Every zero-dimensional cell of an oriental is a vertex.
```
theorem eq_vertex_of_dimensionLE (h : NormalizedSimplexIdentities) {m : ℕ}
    (x : h.object m) (hx : (h.object m).DimensionLE 0 x) :
    ∃ i : Fin (m + 1), x = vertex h i := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertex
theorem OAI.Thomason.Construction.SimplexComplex.vertex_injective line 313
Source documentation
Distinct vertices define distinct strict cells.
```
theorem vertex_injective (h : NormalizedSimplexIdentities) {m : ℕ} :
    Function.Injective (vertex h (m := m)) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertex
theorem OAI.Thomason.Construction.SimplexComplex.map_vertex line 326
Source documentation
Normalized ordinal maps preserve the explicitly constructed vertices.
```
theorem map_vertex (h : NormalizedSimplexIdentities) {m n : ℕ}
    (f : Fin (m + 1) →o Fin (n + 1)) (i : Fin (m + 1)) :
    (h.map f).toFun (vertex h i) = vertex h (f i) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertex
def OAI.Thomason.Construction.SimplexComplex.objectsEquiv line 348
Source documentation
The objects of the concrete oriental are canonically its ordered vertices.
```
noncomputable def objectsEquiv (h : NormalizedSimplexIdentities) (m : ℕ) :
    StrictOmegaCategory.Objects (h.object m) ≃ Fin (m + 1) where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictOmegaCategory.Objects
theorem OAI.Thomason.Construction.SimplexComplex.objectsEquiv_symm_val line 357
theorem OAI.Thomason.Construction.SimplexComplex.objectsEquiv_map line 361
Source documentation
The vertex classification is natural for every ordinal operator.
```
theorem objectsEquiv_map (h : NormalizedSimplexIdentities) {m n : ℕ}
    (f : Fin (m + 1) →o Fin (n + 1)) (x : StrictOmegaCategory.Objects (h.object m)) :
    objectsEquiv h n ((h.map f).toOneFunctor.obj x) = f (objectsEquiv h m x) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictOmegaCategory.Objects, OAI.Thomason.Construction.SimplexComplex.objectsEquiv
def OAI.Thomason.Construction.NormalizedSimplexIdentities.vertexObject line 395
Source documentation
A vertex of a simplicial set gives an object in its categorification.
```
noncomputable def vertexObject (K : SSet.{0}) (v : K _⦋0⦌) :
    Objects (h.categorification.obj K) :=
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexLeg_vertex line 402

Source documentation

The image of any oriental vertex is already represented by its zero-simplex in the simplicial set.

theorem simplexLeg_vertex {K : SSet.{0}} {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ K) (i : Fin (m.len + 1)) :
    (h.simplexLeg s).toFun (SimplexComplex.vertex h i) =
      (h.vertexObject K (K.map (SimplexCategory.const (.mk 0) m i).op
        (SSet.yonedaEquiv s))).val := by
…

Mentions: OAI.Thomason.Construction.SimplexComplex.vertex

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.vertexObject_surjective line 421
Source documentation
Every object of categorification is represented by an original vertex.
```
theorem vertexObject_surjective (K : SSet.{0}) : Function.Surjective (h.vertexObject K) := by
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.vertexObject_naturality line 435

Source documentation

The vertex representation commutes with every simplicial map.

theorem vertexObject_naturality {K L : SSet.{0}} (f : K ⟶ L) (v : K _⦋0⦌) :
    (h.categorification.map f).toOneFunctor.obj (h.vertexObject K v) =
      h.vertexObject L (f.app _ v) := by
…

def OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexVertex line 447
Source documentation
Read the original vertex carried by an object of one presentation simplex.
```
noncomputable def simplexVertex {K : SSet.{0}} {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ K) (x : Objects (h.object m.len)) : K _⦋0⦌ :=
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.simplexVertex_precomp line 454

Source documentation

Vertex readings respect every map in the simplex presentation.

theorem simplexVertex_precomp {K : SSet.{0}} {m n : SimplexCategory}
    (s : SSet.stdSimplex.obj n ⟶ K) (a : m ⟶ n) (x : Objects (h.object m.len)) :
    h.simplexVertex (SSet.stdSimplex.map a ≫ s) x =
      h.simplexVertex s ((h.map a.toOrderHom).toOneFunctor.obj x) := by
…

def OAI.Thomason.Construction.NormalizedSimplexIdentities.vertexCocone line 466

Source documentation

The compatible vertex readings form a cocone of sets.

noncomputable def vertexCocone (K : SSet.{0}) :
    Cocone ((CostructuredArrow.proj SSet.stdSimplex K ⋙ h.cosimplicial) ⋙ objectFunctor) where
…

def OAI.Thomason.Construction.NormalizedSimplexIdentities.readVertex line 482
Source documentation
The inverse reading of the vertices of categorification.
```
noncomputable def readVertex (K : SSet.{0}) : Objects (h.categorification.obj K) → K _⦋0⦌ :=
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.readVertex_simplexLeg line 486

Source documentation

Reading a vertex on a presentation leg returns that simplex's vertex.

theorem readVertex_simplexLeg {K : SSet.{0}} {m : SimplexCategory}
    (s : SSet.stdSimplex.obj m ⟶ K) (x : Objects (h.object m.len)) :
    h.readVertex K ((h.simplexLeg s).toOneFunctor.obj x) = h.simplexVertex s x := by
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.readVertex_vertexObject line 494
def OAI.Thomason.Construction.NormalizedSimplexIdentities.categorificationObjectsEquiv line 508
Source documentation
Objects of categorification are exactly the original vertices.
```
noncomputable def categorificationObjectsEquiv (K : SSet.{0}) :
    Objects (h.categorification.obj K) ≃ K _⦋0⦌ where
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.categorificationObjectsEquiv_naturality line 518

Source documentation

Reading vertices is natural for arbitrary simplicial maps.

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

def OAI.Thomason.Construction.SimplexComplex.intervalEdge line 547
Source documentation
The unique top-dimensional basis edge of the first simplex.
```
def intervalEdge : Basis 1 1 := OrderEmbedding.ofStrictMono id strictMono_id
```
Mentions: OAI.Thomason.Construction.SimplexComplex.Basis
theorem OAI.Thomason.Construction.SimplexComplex.interval_basis_eq line 549
theorem OAI.Thomason.Construction.SimplexComplex.interval_chain_eq line 560
theorem OAI.Thomason.Construction.SimplexComplex.interval_differential line 565
theorem OAI.Thomason.Construction.SimplexComplex.interval_no_backward line 584
Source documentation
Positivity rules out a cell from vertex one to vertex zero in O[1].
```
theorem interval_no_backward (h : NormalizedSimplexIdentities) (x : h.object 1)
    (hs : (h.object 1).source 0 x = vertex h 1)
    (ht : (h.object 1).target 0 x = vertex h 0) : False := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertex
theorem OAI.Thomason.Construction.SimplexComplex.endpoints_ordered line 604
Source documentation
Any oriental cell has nondecreasing zero-dimensional endpoints.
```
theorem endpoints_ordered (h : NormalizedSimplexIdentities) {m : ℕ} (x : h.object m) :
    objectsEquiv h m ((h.object m).boundaryObject false x) ≤
      objectsEquiv h m ((h.object m).boundaryObject true x) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.objectsEquiv
abbrev OAI.Thomason.Construction.StrictOmegaCategory.ColimitGeneration.Index line 655
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitGeneration.generators line 657
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitGeneration.generators_face line 659
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitGeneration.generated line 670
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitGeneration.inclusion line 695
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitGeneration.leg line 700
def OAI.Thomason.Construction.StrictOmegaCategory.ColimitGeneration.cocone line 707
theorem OAI.Thomason.Construction.StrictOmegaCategory.ColimitGeneration.generated_by_pieces line 717
inductive OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.Cell line 751
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.face line 758
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.object_face line 765
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.globular line 771
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.comp line 782
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.source_comp line 788
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.target_comp line 793
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.left_unit line 798
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.right_unit line 803
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.boundaryObject_face_succ line 821
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.boundaryObject_comp line 827
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.face_comp line 834
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.assoc line 846
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.interchange line 857
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.category line 891
Source documentation
Adjoin a terminal vertex and one arrow from each original object.
```
def category (C : StrictOmegaCategory.{0}) : StrictOmegaCategory.{0} where
…
```
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.inclusion line 911
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.labelCell line 918
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.label line 924
Source documentation
The cone is canonically a strict category over the walking arrow.
```
def label (C : StrictOmegaCategory.{0}) : category C ⟶ StrictPoset.category (Fin 2) where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.category, OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.inclusion_label line 933
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.zeroFiberInclusion line 937
Source documentation
The old category is the actual full zero-fibre of the cone label.
```
def zeroFiberInclusion (C : StrictOmegaCategory.{0}) : C ⟶ labelFiber (label C) 0 where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.labelFiber, OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.label
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.zeroFiberInclusion_bijective line 942
def OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.zeroFiberIso line 959
theorem OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.isTruncated line 963
Source documentation
Positive finite dimension is preserved by adjoining the terminal cone.
```
theorem isTruncated {n : ℕ} (hn : 1 ≤ n) (hC : C.IsTruncated n) :
    (category C).IsTruncated n := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.TerminalCone.category, OAI.Thomason.Construction.StrictOmegaCategory.IsTruncated