NonsingularFaceCarriers.lean`

85 declarations, 0 contain sorry, 0 declared as axioms

The concrete initial and final ordinal faces

def OAI.Thomason.Construction.SimplexComplex.initialFace line 23
Source documentation
Inclusion of an initial segment of a finite ordinal.
```
def initialFace {q m : ℕ} (hqm : q ≤ m) : Fin (q + 1) ↪o Fin (m + 1) :=
…
```
def OAI.Thomason.Construction.SimplexComplex.initialClamp line 27
Source documentation
Retraction to that initial segment, by clamping above its last vertex.
```
def initialClamp {q m : ℕ} (_hqm : q ≤ m) : Fin (m + 1) →o Fin (q + 1) where
…
```
theorem OAI.Thomason.Construction.SimplexComplex.initialClamp_retract line 31
theorem OAI.Thomason.Construction.SimplexComplex.initialFace_range line 38
def OAI.Thomason.Construction.SimplexComplex.initialFaceIso line 48
Source documentation
The full strict subcategory on an initial segment is its smaller oriental.
```
noncomputable def initialFaceIso {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {q m : ℕ} (hqm : q ≤ m) :
    h.object q ≅ vertexFullSubcategory h (Set.range (initialFace hqm)) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory, OAI.Thomason.Construction.SimplexComplex.initialFace
def OAI.Thomason.Construction.SimplexComplex.finalFace line 55
Source documentation
Inclusion of the final segment with q+1 vertices.
```
def finalFace {q m : ℕ} (hqm : q ≤ m) : Fin (q + 1) ↪o Fin (m + 1) :=
…
```
def OAI.Thomason.Construction.SimplexComplex.finalClamp line 60
Source documentation
Retraction to a final segment by clamping below its first vertex.
```
def finalClamp {q m : ℕ} (hqm : q ≤ m) : Fin (m + 1) →o Fin (q + 1) where
…
```
theorem OAI.Thomason.Construction.SimplexComplex.finalClamp_retract line 64
theorem OAI.Thomason.Construction.SimplexComplex.finalFace_range line 72
def OAI.Thomason.Construction.SimplexComplex.finalFaceIso line 87
Source documentation
The full strict subcategory on a final segment is its smaller oriental.
```
noncomputable def finalFaceIso {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {q m : ℕ} (hqm : q ≤ m) :
    h.object q ≅ vertexFullSubcategory h (Set.range (finalFace hqm)) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory, OAI.Thomason.Construction.SimplexComplex.finalFace
instance OAI.Thomason.Construction.SimplexComplex.emptyVertexFullSubcategory line 94
Source documentation
The full subcategory on no vertices has no cells.
```
instance emptyVertexFullSubcategory (h : NormalizedSimplexIdentities) (m : ℕ) :
    IsEmpty (vertexFullSubcategory h (m := m) ∅) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory
def OAI.Thomason.Construction.StrictOmegaCategory.firstLabel line 112
def OAI.Thomason.Construction.StrictOmegaCategory.lastLabel line 113
theorem OAI.Thomason.Construction.StrictOmegaCategory.label_ordered line 115
theorem OAI.Thomason.Construction.StrictOmegaCategory.firstLabel_face_zero line 118
theorem OAI.Thomason.Construction.StrictOmegaCategory.lastLabel_face_zero line 123
theorem OAI.Thomason.Construction.StrictOmegaCategory.firstLabel_face_succ line 128
theorem OAI.Thomason.Construction.StrictOmegaCategory.lastLabel_face_succ line 132
theorem OAI.Thomason.Construction.StrictOmegaCategory.firstLabel_comp line 136
theorem OAI.Thomason.Construction.StrictOmegaCategory.lastLabel_comp_zero line 144
theorem OAI.Thomason.Construction.StrictOmegaCategory.lastLabel_comp_succ line 151
theorem OAI.Thomason.Construction.StrictOmegaCategory.label_composable_zero line 158
theorem OAI.Thomason.Construction.StrictOmegaCategory.labels_composable_succ line 164
def OAI.Thomason.Construction.StrictOmegaCategory.zeroCell line 172
Source documentation
An endpoint-zero cell, as a cell of the actual full fibre.
```
def zeroCell (p : X ⟶ StrictPoset.category (Fin 2)) (x : X) (hl : lastLabel p x = 0) :
    labelFiber p 0 := ⟨x, (fullCell_label_iff p 0 x).mpr (by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.lastLabel, OAI.Thomason.Construction.StrictOmegaCategory.labelFiber, OAI.Thomason.Construction.StrictOmegaCategory.fullCell_label_iff
def OAI.Thomason.Construction.StrictOmegaCategory.zeroSource line 181
Source documentation
The source object of a cell whose source has label zero, in the zero fibre.
```
def zeroSource (p : X ⟶ StrictPoset.category (Fin 2)) (x : X) (hf : firstLabel p x = 0) :
    Objects (labelFiber p 0) :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.firstLabel, OAI.Thomason.Construction.StrictOmegaCategory.Objects, OAI.Thomason.Construction.StrictOmegaCategory.labelFiber
theorem OAI.Thomason.Construction.SimplexComplex.lowerSet_eq_Iic line 200
Source documentation
Every nonempty initial segment of a finite ordinal has a last vertex.
```
theorem lowerSet_eq_Iic {m : ℕ} {I : Set (Fin (m + 1))}
    (hI : IsLowerSet I) (hne : I.Nonempty) : ∃ i, I = Set.Iic i := by
…
```
theorem OAI.Thomason.Construction.SimplexComplex.upperSet_eq_Ici line 217
Source documentation
Every nonempty final segment of a finite ordinal has a first vertex.
```
theorem upperSet_eq_Ici {m : ℕ} {I : Set (Fin (m + 1))}
    (hI : IsUpperSet I) (hne : I.Nonempty) : ∃ i, I = Set.Ici i := by
…
```
theorem OAI.Thomason.Construction.SimplexComplex.initialSegment_oriental line 234
Source documentation
Every nonempty initial vertex segment gives the corresponding smaller oriental.
```
theorem initialSegment_oriental {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {m : ℕ} {I : Set (Fin (m + 1))} (hI : IsLowerSet I) (hne : I.Nonempty) :
    ∃ q : Fin (m + 1), Nonempty (h.object q.val ≅ vertexFullSubcategory h I) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory
theorem OAI.Thomason.Construction.SimplexComplex.finalSegment_oriental line 243
Source documentation
Every nonempty final vertex segment gives the corresponding smaller oriental.
```
theorem finalSegment_oriental {h : NormalizedSimplexIdentities} (a : SimplexAtomsInput h)
    {m : ℕ} {I : Set (Fin (m + 1))} (hI : IsUpperSet I) (hne : I.Nonempty) :
    ∃ q : Fin (m + 1), Nonempty (h.object q.val ≅ vertexFullSubcategory h I) := by
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.SimplexAtomsInput, OAI.Thomason.Construction.SimplexComplex.vertexFullSubcategory
def OAI.Thomason.Construction.hornOneIso line 279
Source documentation
A one-dimensional horn is its sole vertex.
```
noncomputable def hornOneIso (i j : Fin 2) (hji : j ≠ i) :
    (Δ[0] : SSet.{u}) ≅ Λ[1, i] where
…
```
theorem OAI.Thomason.Construction.anodyne_delta_one line 299
def OAI.Thomason.Construction.unitZeroIso line 307
theorem OAI.Thomason.Construction.anodyne_iota_zero line 310
theorem OAI.Thomason.Construction.anodyne_iota_one line 328
theorem OAI.Thomason.Construction.KanQuillenPublishedInput.anodyne_eq line 354
Source documentation
The published WFS identifies anodyne extensions with the actual monomorphisms which are realization weak equivalences.
```
theorem anodyne_eq : SSet.anodyneExtensions.{u} =
    MorphismProperty.monomorphisms SSet.{u} ⊓ realizationWeakEquivalences := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.KanQuillenPublishedInput.anodyne_weakEquivalence line 360
theorem OAI.Thomason.Construction.KanQuillenPublishedInput.cylinder_endpoint_zero line 365
theorem OAI.Thomason.Construction.KanQuillenPublishedInput.cylinder_endpoint_one line 369
theorem OAI.Thomason.Construction.KanQuillenPublishedInput.homotopy_weakEquivalence_iff line 375
Source documentation
A simplicial homotopy preserves and reflects the geometric-realization weak-equivalence property.
```
theorem homotopy_weakEquivalence_iff {X Y : SSet.{u}} {f g : X ⟶ Y}
    (H : SSet.Homotopy f g) : realizationWeakEquivalences f ↔ realizationWeakEquivalences g := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.whisker_zero_face line 416
Source documentation
The zero face of a product is its projection followed by the zero endpoint.
```
theorem whisker_zero_face (K : SSet.{u}) :
    K ◁ SSet.stdSimplex.δ (1 : Fin 2) =
      fst K (Δ[0] : SSet.{u}) ≫ SSet.ι₀ := by
…
```
def OAI.Thomason.Construction.zeroFaceSection line 435
Source documentation
The product with the terminal standard simplex has a chosen section.
```
def zeroFaceSection (K : SSet.{u}) : K ⟶ K ⊗ (Δ[0] : SSet.{u}) :=
…
```
theorem OAI.Thomason.Construction.zeroFaceSection_fst line 439
theorem OAI.Thomason.Construction.zeroFaceSection_face line 448

theorem OAI.Thomason.Construction.exists_kan_homotopy_extension line 454

Source documentation

A prescribed simplicial homotopy on any subobject extends into a Kan complex while keeping the entire initial map fixed.

theorem exists_kan_homotopy_extension {A K X : SSet.{u}}
    (i : A ⟶ K) [Mono i] [SSet.KanComplex X]
    (f : K ⟶ X) (h : A ⊗ Δ[1] ⟶ X) (h₀ : SSet.ι₀ ≫ h = i ≫ f) :
    ∃ e : K ⊗ Δ[1] ⟶ X, SSet.ι₀ ≫ e = f ∧ i ▷ Δ[1] ≫ e = h := by
…

theorem OAI.Thomason.Construction.interval_boundary_constant line 509

theorem OAI.Thomason.Construction.interval_boundary_tensor_hom_ext line 528

Source documentation

Restriction to the two endpoints detects equality even with an arbitrary simplicial parameter object.

theorem interval_boundary_tensor_hom_ext {K X : SSet.{u}}
    (f g : K ⊗ (SSet.boundary 1 : SSet.{u}) ⟶ X)
    (h₀ : K ◁ SSet.boundary.ι (1 : Fin 2) ≫ f =
      K ◁ SSet.boundary.ι (1 : Fin 2) ≫ g)
    (h₁ : K ◁ SSet.boundary.ι (0 : Fin 2) ≫ f =
      K ◁ SSet.boundary.ι (0 : Fin 2) ≫ g) : f = g := by
…

def OAI.Thomason.Construction.intervalBoundaryMap line 582
theorem OAI.Thomason.Construction.intervalBoundaryMap_zero line 606
theorem OAI.Thomason.Construction.intervalBoundaryMap_one line 620
theorem OAI.Thomason.Construction.intervalBoundaryMap_postcomp line 634
theorem OAI.Thomason.Construction.orderNerveMap_id line 666
theorem OAI.Thomason.Construction.orderNerveMap_comp line 671

def OAI.Thomason.Construction.orderInterpolate line 679

Source documentation

Interpolate between monotone maps along a monotone binary vertex label.

def orderInterpolate {P Q : Type} [PartialOrder P] [PartialOrder Q]
    (f g : P →o Q) (hfg : ∀ x, f x ≤ g x) {m : ℕ}
    (s : Fin (m + 1) →o P) (θ : Fin (m + 1) →o Fin 2) : Fin (m + 1) →o Q where
…

def OAI.Thomason.Construction.orderNerveHomotopy line 696

Source documentation

Every pointwise inequality induces a homotopy of the actual ordinary nerves.

noncomputable def orderNerveHomotopy {P Q : Type} [PartialOrder P] [PartialOrder Q]
    (f g : P →o Q) (hfg : ∀ x, f x ≤ g x) :
    SSet.Homotopy (nerveMap f.monotone.functor) (nerveMap g.monotone.functor) where
…

theorem OAI.Thomason.Construction.orderNerve_weakEquivalence_iff line 721

Source documentation

Pointwise comparable monotone maps simultaneously induce realization weak equivalences, using only the actual Kan–Quillen WFS input.

theorem orderNerve_weakEquivalence_iff (kq : KanQuillenPublishedInput.{0})
    {P Q : Type} [PartialOrder P] [PartialOrder Q]
    (f g : P →o Q) (hfg : ∀ x, f x ≤ g x) :
    realizationWeakEquivalences (nerveMap f.monotone.functor) ↔
      realizationWeakEquivalences (nerveMap g.monotone.functor) :=
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

def OAI.Thomason.Construction.NerveSubdivisionMap.vertices line 746
def OAI.Thomason.Construction.NerveSubdivisionMap.ordinalMap line 751
theorem OAI.Thomason.Construction.NerveSubdivisionMap.vertices_comp line 756
theorem OAI.Thomason.Construction.NerveSubdivisionMap.vertices_postcomp line 764
theorem OAI.Thomason.Construction.NerveSubdivisionMap.chains_comp line 772
def OAI.Thomason.Construction.NerveSubdivisionMap.chainNerveMap line 780
def OAI.Thomason.Construction.NerveSubdivisionMap.chainsOfVertices line 784
theorem OAI.Thomason.Construction.NerveSubdivisionMap.chainsOfVertices_comp line 789
theorem OAI.Thomason.Construction.NerveSubdivisionMap.chainsOfVertices_postcomp line 806
def OAI.Thomason.Construction.NerveSubdivisionMap.piece line 822
theorem OAI.Thomason.Construction.NerveSubdivisionMap.piece_naturality line 827
theorem OAI.Thomason.Construction.NerveSubdivisionMap.piece_postcomp line 842
def OAI.Thomason.Construction.NerveSubdivisionMap.targetCocone line 851
def OAI.Thomason.Construction.NerveSubdivisionMap.map line 860
theorem OAI.Thomason.Construction.NerveSubdivisionMap.map_fac line 864
theorem OAI.Thomason.Construction.NerveSubdivisionMap.map_naturality line 869
theorem OAI.Thomason.Construction.NerveSubdivisionMap.map_standard line 880
Source documentation
On an ordinal nerve this map is the actual standard subdivision isomorphism, expressed through the standard-simplex nerve isomorphism.
```
theorem map_standard (n : SimplexCategory) :
    SSet.sd.map (simplexNerveIso.hom.app n) ≫
        map (ULift.{0} (Fin (n.len+1))) = SSet.stdSimplex.sdIso.hom.app n := by
…
```
Mentions: OAI.Thomason.Construction.NerveSubdivisionMap.map
def OAI.Thomason.Construction.NonsingularLastVertex.faceUnion line 936
theorem OAI.Thomason.Construction.NonsingularLastVertex.nondegenerate_mem_faceUnion_iff line 938
theorem OAI.Thomason.Construction.NonsingularLastVertex.nondegenerate_mem_faceUnion_iff_of_lower line 948
theorem OAI.Thomason.Construction.NonsingularLastVertex.faceUnion_mono line 953
theorem OAI.Thomason.Construction.NonsingularLastVertex.faceUnion_union line 959
theorem OAI.Thomason.Construction.NonsingularLastVertex.faceUnion_inter line 969
theorem OAI.Thomason.Construction.NonsingularLastVertex.faceUnion_univ line 982
def OAI.Thomason.Construction.NonsingularLastVertex.faceInclusion line 990
theorem OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap_range_le line 993
def OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap line 1003
theorem OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap_ι line 1008
def OAI.Thomason.Construction.NonsingularLastVertex.faceSubset line 1011
theorem OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap_naturality line 1015