SubdivisionFaceImages.lean`

61 declarations, 0 contain sorry, 0 declared as axioms

Singular simplices carry continuous homotopies to simplicial homotopies

The interval coordinate of an ordered simplex is its affine barycentric coordinate. Its compatibility includes every face and degeneracy.

def OAI.Thomason.Construction.singularSimplexTime line 31

Source documentation

The affine time coordinate of a simplex of the simplicial interval.

def singularSimplexTime {n : SimplexCategoryᵒᵖ} (u : (Δ[1] : SSet.{0}).obj n) :
    C(StdSimplex ℝ (Fin (n.unop.len+1)), unitInterval) where
…

theorem OAI.Thomason.Construction.singularSimplexTime_naturality line 37

Source documentation

The affine time is natural even when the ordinal map merges vertices.

theorem singularSimplexTime_naturality {m n : SimplexCategory} (f : m ⟶ n)
    (u : (Δ[1] : SSet.{0}).obj (.op n)) (x : StdSimplex ℝ (Fin (m.len+1))) :
    singularSimplexTime ((Δ[1] : SSet.{0}).map f.op u) x =
      singularSimplexTime u (StdSimplex.map f.toOrderHom x) := by
…

Mentions: OAI.Thomason.Construction.singularSimplexTime

def OAI.Thomason.Construction.singularHomotopy line 47

Source documentation

A continuous homotopy applied simplexwise, with the affine interval coordinate.

def singularHomotopy {X Y : TopCat.{0}} {f g : X ⟶ Y} (H : f.hom.Homotopy g.hom) :
    SSet.Homotopy (TopCat.toSSet.map f) (TopCat.toSSet.map g) where
…

theorem OAI.Thomason.Construction.singular_weakEquivalence_iff line 97
Source documentation
After singularization, continuous homotopies preserve the actual realization weak test.
```
theorem singular_weakEquivalence_iff {X Y : TopCat.{0}} {f g : X ⟶ Y}
    (H : f.hom.Homotopy g.hom) :
    realizationWeakEquivalences (TopCat.toSSet.map f) ↔
      realizationWeakEquivalences (TopCat.toSSet.map g) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.singular_counit_simplex line 121

Source documentation

The counit on a represented singular simplex is its defining continuous map.

theorem singular_counit_simplex (X : TopCat.{0}) (n : SimplexCategory)
    (s : (TopCat.toSSet.obj X).obj (.op n)) :
    (SSet.toTopSimplex.inv.app n ≫ SSet.toTop.map (SSet.yonedaEquiv.symm s)) ≫
      sSetTopAdj.counit.app X = s.down := by
…

theorem OAI.Thomason.Construction.singular_counit_leg line 133

Source documentation

Pointwise evaluation formula for every simplex in the realization colimit.

theorem singular_counit_leg (X : TopCat.{0})
    (j : CostructuredArrow SSet.stdSimplex (TopCat.toSSet.obj X))
    (p : (RealizationPrism.diagram (TopCat.toSSet.obj X)).obj j) :
    (sSetTopAdj.counit.app X).hom ((RealizationPrism.leg (TopCat.toSSet.obj X) j).hom p) =
      (TopCat.toSSetObjEquiv X (.op j.left) (SSet.yonedaEquiv j.hom)) p.down := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.RealizationPrism.leg

theorem OAI.Thomason.Construction.realizationTime_simplex line 143

Source documentation

Evaluation of a simplicial-interval simplex is its affine time function.

theorem realizationTime_simplex (n : SimplexCategory)
    (u : (Δ[1] : SSet.{0}).obj (.op n)) (p : StdSimplex ℝ (Fin (n.len+1))) :
    PrismBarycentric.realizationTime.hom
      ((RealizationPrism.leg (Δ[1] : SSet.{0})
        (CostructuredArrow.mk (SSet.yonedaEquiv.symm u))).hom (ULift.up p)) =
      singularSimplexTime u p := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.singularSimplexTime

theorem OAI.Thomason.Construction.singular_counit_map_leg line 161

Source documentation

Evaluation commutes with a simplicial map into the singular set, simplexwise.

theorem singular_counit_map_leg {K : SSet.{0}} (X : TopCat.{0})
    (f : K ⟶ TopCat.toSSet.obj X) (j : CostructuredArrow SSet.stdSimplex K)
    (p : (RealizationPrism.diagram K).obj j) :
    (sSetTopAdj.counit.app X).hom
      ((SSet.toTop.map f).hom ((RealizationPrism.leg K j).hom p)) =
      (TopCat.toSSetObjEquiv X (.op j.left)
        (f.app (.op j.left) (SSet.yonedaEquiv j.hom))) p.down := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.RealizationPrism.leg

theorem OAI.Thomason.Construction.realizationTime_map_leg line 175

Source documentation

The same simplexwise naturality for the interval coordinate.

theorem realizationTime_map_leg {K : SSet.{0}} (f : K ⟶ (Δ[1] : SSet.{0}))
    (j : CostructuredArrow SSet.stdSimplex K) (p : (RealizationPrism.diagram K).obj j) :
    PrismBarycentric.realizationTime.hom
      ((SSet.toTop.map f).hom ((RealizationPrism.leg K j).hom p)) =
      singularSimplexTime (f.app (.op j.left) (SSet.yonedaEquiv j.hom)) p.down := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.singularSimplexTime

def OAI.Thomason.Construction.realizationHomotopyEquiv line 209

Source documentation

Simplicial homotopy inverses give actual topological homotopy inverses.

def realizationHomotopyEquiv {X Y : SSet.{0}} (f : X ⟶ Y) (g : Y ⟶ X)
    (hX : SSet.Homotopy (f ≫ g) (𝟙 X)) (hY : SSet.Homotopy (g ≫ f) (𝟙 Y)) :
    ContinuousMap.HomotopyEquiv (SSet.toTop.obj X) (SSet.toTop.obj Y) where
…

theorem OAI.Thomason.Construction.simplicial_homotopy_inverse_weak line 220
Source documentation
The semantic weak test for a simplicial map with actual homotopy inverse.
```
theorem simplicial_homotopy_inverse_weak {X Y : SSet.{0}} (f : X ⟶ Y) (g : Y ⟶ X)
    (hX : SSet.Homotopy (f ≫ g) (𝟙 X)) (hY : SSet.Homotopy (g ≫ f) (𝟙 Y)) :
    realizationWeakEquivalences f :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.singular_homotopy_equivalence_weak line 227
Source documentation
Singularization of a continuous homotopy equivalence satisfies the actual realization weak-equivalence test, without using the counit weak theorem.
```
theorem singular_homotopy_equivalence_weak {X Y : TopCat.{0}}
    (e : ContinuousMap.HomotopyEquiv X Y) :
    realizationWeakEquivalences (TopCat.toSSet.map (TopCat.ofHom e.toFun)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.singular_deformation_weak line 242
Source documentation
In particular, every stationary topological deformation remains weak after singularization and realization.
```
theorem singular_deformation_weak {X Y : TopCat.{0}} {f : X ⟶ Y}
    (d : TopologicalDeformation.Data f) :
    realizationWeakEquivalences (TopCat.toSSet.map f) := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data, OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.realizedPointIsTerminal line 272
Source documentation
The realization of the zero simplex is an actual terminal topological space.
```
def realizedPointIsTerminal : IsTerminal (SSet.toTop.obj (Δ[0] : SSet.{0})) := by
…
```
def OAI.Thomason.Construction.singularRealizedPointIso line 284
Source documentation
The singular simplicial set of this point is the actual zero simplex.
```
def singularRealizedPointIso :
    TopCat.toSSet.obj (SSet.toTop.obj (Δ[0] : SSet.{0})) ≅ (Δ[0] : SSet.{0}) :=
…
```
instance OAI.Thomason.Construction.counit_realized_point_isIso line 290
Source documentation
At a point, the evaluation counit is an isomorphism.
```
instance counit_realized_point_isIso :
    IsIso (sSetTopAdj.counit.app (SSet.toTop.obj (Δ[0] : SSet.{0}))) := by
…
```

theorem OAI.Thomason.Construction.singular_counit_weak_of_homotopyEquiv line 302

Source documentation

The counit weak-equivalence test transports along actual homotopy equivalences.

theorem singular_counit_weak_of_homotopyEquiv {X Y : TopCat.{0}}
    (e : ContinuousMap.HomotopyEquiv X Y)
    (hY : topologicalWeakEquivalences (sSetTopAdj.counit.app Y)) :
    topologicalWeakEquivalences (sSetTopAdj.counit.app X) := by
…

Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences

theorem OAI.Thomason.Construction.singular_counit_weak_contractible line 317
Source documentation
Contractibility suffices for the actual counit weak-equivalence theorem.
```
theorem singular_counit_weak_contractible (X : TopCat.{0}) [ContractibleSpace X] :
    topologicalWeakEquivalences (sSetTopAdj.counit.app X) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences

theorem OAI.Thomason.Construction.singularHomotopy_counit line 341

Source documentation

Evaluation of a singular homotopy is the original homotopy on both coordinates.

theorem singularHomotopy_counit {X Y : TopCat.{0}} {f g : X ⟶ Y}
    (H : f.hom.Homotopy g.hom)
    (z : SSet.toTop.obj (TopCat.toSSet.obj X ⊗ Δ[1])) :
    (sSetTopAdj.counit.app Y).hom ((SSet.toTop.map (singularHomotopy H).h).hom z) =
      H (PrismBarycentric.realizationTime.hom
          ((SSet.toTop.map (snd (TopCat.toSSet.obj X) Δ[1])).hom z),
        (sSetTopAdj.counit.app X).hom
          ((SSet.toTop.map (fst (TopCat.toSSet.obj X) Δ[1])).hom z)) := by
…

Mentions: OAI.Thomason.Construction.singularHomotopy

theorem OAI.Thomason.Construction.realizedHomotopy_apply line 354
Source documentation
The realized simplicial homotopy is given by the same assembled comparison.
```
theorem realizedHomotopy_apply {K L : SSet.{0}} {f g : K ⟶ L}
    (H : SSet.Homotopy f g) (t : unitInterval) (x : SSet.toTop.obj K) :
    RealizedCylinder.homotopy H (t, x) =
      (SSet.toTop.map H.h).hom ((RealizedCylinder.comparison K).hom (x, t)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCylinder.homotopy, OAI.Thomason.Construction.RealizedCylinder.comparison
theorem OAI.Thomason.Construction.realizedSingularHomotopy_counit line 367
Source documentation
Realizing a singular homotopy and then evaluating recovers the continuous homotopy at every point, not merely its homotopy class.
```
theorem realizedSingularHomotopy_counit {X Y : TopCat.{0}} {f g : X ⟶ Y}
    (H : f.hom.Homotopy g.hom) (t : unitInterval)
    (x : SSet.toTop.obj (TopCat.toSSet.obj X)) :
    (sSetTopAdj.counit.app Y).hom (RealizedCylinder.homotopy (singularHomotopy H) (t, x)) =
      H (t, (sSetTopAdj.counit.app X).hom x) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCylinder.homotopy, OAI.Thomason.Construction.singularHomotopy

theorem OAI.Thomason.Construction.RealizedCylinder.homotopy_stationary line 396

Source documentation

A stationary simplicial cylinder is stationary at every point of the actual realized image, not just at its vertices.

theorem homotopy_stationary (H : SSet.Homotopy f g) (i : A ⟶ K)
    (hi : i ▷ Δ[1] ≫ H.h = fst A Δ[1] ≫ i ≫ f)
    (t : unitInterval) (x : SSet.toTop.obj A) :
    homotopy H (t, (SSet.toTop.map i).hom x) =
      (SSet.toTop.map f).hom ((SSet.toTop.map i).hom x) := by
…

Mentions: OAI.Thomason.Construction.RealizedCylinder.homotopy

def OAI.Thomason.Construction.RealizedCylinder.homotopyRelOfStationary line 415

Source documentation

The realized homotopy is relative to the entire image of the specified simplicial map; no embedding hypothesis is needed.

def homotopyRelOfStationary (H : SSet.Homotopy f g) (i : A ⟶ K)
    (hi : i ▷ Δ[1] ≫ H.h = fst A Δ[1] ≫ i ≫ f) :
    (SSet.toTop.map f).hom.HomotopyRel (SSet.toTop.map g).hom
      (Set.range (SSet.toTop.map i).hom) where
…

theorem OAI.Thomason.Construction.exists_kan_relative_homotopy line 444

Source documentation

Lift a homotopy through a Kan fibration, preserving a prescribed homotopy on any simplicial subobject. The endpoint commutes strictly with the fibration.

theorem exists_kan_relative_homotopy {A K E B : SSet.{0}}
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (f : K ⟶ E) {a : A ⟶ E} (HA : SSet.Homotopy (i ≫ f) a)
    {g : K ⟶ B} (HB : SSet.Homotopy (f ≫ p) g)
    (hc : HA.h ≫ p = i ▷ Δ[1] ≫ HB.h) :
    ∃ (g' : K ⟶ E) (H : SSet.Homotopy f g'),
      i ▷ Δ[1] ≫ H.h = HA.h ∧ H.h ≫ p = HB.h ∧ g' ≫ p = g := by
…

theorem OAI.Thomason.Construction.exists_kan_relative_homotopy_weak line 468

Source documentation

The new endpoint in a relative Kan lift has exactly the same actual realization weak-equivalence status as the initial map.

theorem exists_kan_relative_homotopy_weak {A K E B : SSet.{0}}
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (f : K ⟶ E) {a : A ⟶ E} (HA : SSet.Homotopy (i ≫ f) a)
    {g : K ⟶ B} (HB : SSet.Homotopy (f ≫ p) g)
    (hc : HA.h ≫ p = i ▷ Δ[1] ≫ HB.h) :
    ∃ (g' : K ⟶ E) (H : SSet.Homotopy f g'),
      i ▷ Δ[1] ≫ H.h = HA.h ∧ H.h ≫ p = HB.h ∧ g' ≫ p = g ∧
      (realizationWeakEquivalences f ↔ realizationWeakEquivalences g') := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.exists_kan_stationary_lift line 481

Source documentation

If the prescribed cylinder is stationary, the lift is stationary on the entire realized subobject, as an actual relative continuous homotopy.

theorem exists_kan_stationary_lift {A K E B : SSet.{0}}
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (f : K ⟶ E) {g : K ⟶ B} (HB : SSet.Homotopy (f ≫ p) g)
    (hc : i ▷ Δ[1] ≫ HB.h = fst A Δ[1] ≫ i ≫ f ≫ p) :
    ∃ (g' : K ⟶ E) (H : SSet.Homotopy f g'),
      g' ≫ p = g ∧ i ▷ Δ[1] ≫ H.h = fst A Δ[1] ≫ i ≫ f ∧
      Nonempty ((SSet.toTop.map f).hom.HomotopyRel (SSet.toTop.map g').hom
        (Set.range (SSet.toTop.map i).hom)) ∧
      (realizationWeakEquivalences f ↔ realizationWeakEquivalences g') := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.exactify_simplicial_relative_lift line 526

Source documentation

Once a relative approximation is simplicial, the Kan cylinder lifting property makes its projection exact while retaining the original boundary.

theorem exactify_simplicial_relative_lift {A K E B : SSet.{0}}
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (a : A ⟶ E) (b : K ⟶ B) (d : K ⟶ E) (hd : i ≫ d = a)
    (H : SSet.Homotopy (d ≫ p) b)
    (hH : i ▷ Δ[1] ≫ H.h = fst A Δ[1] ≫ a ≫ p) :
    ∃ l : K ⟶ E, i ≫ l = a ∧ l ≫ p = b := by
…

theorem OAI.Thomason.Construction.realized_homotopy_square line 571
theorem OAI.Thomason.Construction.homotopy_trans_pointwise line 588
def OAI.Thomason.Construction.singularProductEquiv line 622
Source documentation
Product realization gives an exact singular adjunction for a whole parameterized family, using the actual canonical product comparison.
```
def singularProductEquiv (K A : SSet.{0}) (X : TopCat.{0})
    [IsIso (realizationProductComparison K A)] :
    (TopCat.of (SSet.toTop.obj K × SSet.toTop.obj A) ⟶ X) ≃
      (K ⊗ A ⟶ TopCat.toSSet.obj X) :=
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison

theorem OAI.Thomason.Construction.singularProductEquiv_apply line 630

Source documentation

The forward adjunction is evaluation after the canonical projections.

theorem singularProductEquiv_apply (K A : SSet.{0}) (X : TopCat.{0})
    [IsIso (realizationProductComparison K A)]
    (H : TopCat.of (SSet.toTop.obj K × SSet.toTop.obj A) ⟶ X) :
    singularProductEquiv K A X H =
      sSetTopAdj.homEquiv _ X (realizationProductComparison K A ≫ H) := by
…

Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.singularProductEquiv

theorem OAI.Thomason.Construction.singularProductEquiv_restrict line 641
Source documentation
Restriction in the higher parameter commutes exactly with the singular adjunction, including restriction to the entire parameter boundary.
```
theorem singularProductEquiv_restrict (K : SSet.{0}) {A C : SSet.{0}}
    (i : C ⟶ A) (X : TopCat.{0})
    [IsIso (realizationProductComparison K A)] [IsIso (realizationProductComparison K C)]
    (H : TopCat.of (SSet.toTop.obj K × SSet.toTop.obj A) ⟶ X) :
    K ◁ i ≫ singularProductEquiv K A X H =
      singularProductEquiv K C X (realizationProductRightMap K i ≫ H) := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.singularProductEquiv, OAI.Thomason.Construction.realizationProductRightMap

theorem OAI.Thomason.Construction.singularProductEquiv_postcomp line 652

Source documentation

Postcomposition also commutes exactly with the full singular family.

theorem singularProductEquiv_postcomp (K A : SSet.{0}) {X Y : TopCat.{0}}
    [IsIso (realizationProductComparison K A)] (p : X ⟶ Y)
    (H : TopCat.of (SSet.toTop.obj K × SSet.toTop.obj A) ⟶ X) :
    singularProductEquiv K A X H ≫ TopCat.toSSet.map p =
      singularProductEquiv K A Y (H ≫ p) := by
…

Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.singularProductEquiv

theorem OAI.Thomason.Construction.singularProductEquiv_evaluate line 662

Source documentation

Recovering a singular family by actual realization and evaluation is exact on every point of its entire parameter space.

theorem singularProductEquiv_evaluate (K A : SSet.{0}) (X : TopCat.{0})
    [IsIso (realizationProductComparison K A)]
    (H : TopCat.of (SSet.toTop.obj K × SSet.toTop.obj A) ⟶ X) :
    inv (realizationProductComparison K A) ≫
      SSet.toTop.map (singularProductEquiv K A X H) ≫ sSetTopAdj.counit.app X = H := by
…

Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.singularProductEquiv

def OAI.Thomason.Construction.singularCubeProductEquiv line 675
Source documentation
Higher cubes with arbitrary simplicial parameter spaces admit the exact adjunction; the inverse retains all continuous family coordinates.
```
def singularCubeProductEquiv (K : SSet.{0}) (n : ℕ) (X : TopCat.{0}) :
    (TopCat.of (SSet.toTop.obj K × SSet.toTop.obj (RealizedCube.obj n)) ⟶ X) ≃
      (K ⊗ RealizedCube.obj n ⟶ TopCat.toSSet.obj X) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj

def OAI.Thomason.Construction.singularCubeBoundaryProductEquiv line 682

Source documentation

The same exact adjunction holds for the COMPLETE cube boundary.

def singularCubeBoundaryProductEquiv (K : SSet.{0}) (n : ℕ) (X : TopCat.{0}) :
    (TopCat.of (SSet.toTop.obj K × SSet.toTop.obj (RealizedCube.boundary n).toSSet) ⟶ X) ≃
      (K ⊗ (RealizedCube.boundary n).toSSet ⟶ TopCat.toSSet.obj X) := by
…

Mentions: OAI.Thomason.Construction.RealizedCube.boundary

theorem OAI.Thomason.Construction.singularCubeProductEquiv_boundary line 690
Source documentation
Restriction from the cube to its complete boundary is exactly the ordinary continuous boundary restriction under these equivalences.
```
theorem singularCubeProductEquiv_boundary (K : SSet.{0}) (n : ℕ) (X : TopCat.{0})
    (H : TopCat.of (SSet.toTop.obj K × SSet.toTop.obj (RealizedCube.obj (n+1))) ⟶ X) :
    K ◁ (RealizedCube.boundary n).ι ≫ singularCubeProductEquiv K (n+1) X H =
      singularCubeBoundaryProductEquiv K n X
        (realizationProductRightMap K (RealizedCube.boundary n).ι ≫ H) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.RealizedCube.boundary, OAI.Thomason.Construction.singularCubeProductEquiv, OAI.Thomason.Construction.singularCubeBoundaryProductEquiv, OAI.Thomason.Construction.realizationProductRightMap
theorem OAI.Thomason.Construction.greatest_poset_realization_contractible line 717
Source documentation
The existing explicit greatest-vertex contraction gives contractibility.
```
theorem greatest_poset_realization_contractible {P : Type} [PartialOrder P]
    (v : P) (hv : ∀ x, x ≤ v) : ContractibleSpace (SSet.toTop.obj (nerve P)) :=
…
```
theorem OAI.Thomason.Construction.standard_simplex_realization_contractible line 723
Source documentation
Contractibility of each actual realized standard simplex.
```
theorem standard_simplex_realization_contractible (n : ℕ) :
    ContractibleSpace (SSet.toTop.obj (Δ[n] : SSet.{0})) := by
…
```
theorem OAI.Thomason.Construction.singular_unit_weak_of_counit line 731
Source documentation
The adjunction triangle turns a counit weak equivalence into the corresponding unit test.
```
theorem singular_unit_weak_of_counit {K : SSet.{0}}
    (h : topologicalWeakEquivalences (sSetTopAdj.counit.app (SSet.toTop.obj K))) :
    realizationWeakEquivalences (sSetTopAdj.unit.app K) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.singular_unit_weak_contractible line 740
Source documentation
The unit is weak whenever the actual realization is contractible.
```
theorem singular_unit_weak_contractible (K : SSet.{0})
    [ContractibleSpace (SSet.toTop.obj K)] :
    realizationWeakEquivalences (sSetTopAdj.unit.app K) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.singular_unit_standard_simplex_weak line 746
Source documentation
The genuine singular unit of every standard simplex is weak.
```
theorem singular_unit_standard_simplex_weak (n : ℕ) :
    realizationWeakEquivalences (sSetTopAdj.unit.app (Δ[n] : SSet.{0})) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.singular_unit_greatest_poset_weak line 752
Source documentation
The same unit test holds on every greatest-element poset nerve used by the main induction.
```
theorem singular_unit_greatest_poset_weak {P : Type} [PartialOrder P]
    (v : P) (hv : ∀ x, x ≤ v) :
    realizationWeakEquivalences (sSetTopAdj.unit.app (nerve P)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.totalVertexChain line 776
Source documentation
The full vertex set is the greatest vertex in a subdivided simplex.
```
def totalVertexChain (n : ℕ) : NonemptyFiniteChains (ULift.{0} (Fin (n+1))) where
…
```
theorem OAI.Thomason.Construction.le_totalVertexChain line 781
theorem OAI.Thomason.Construction.standard_simplex_hom_weak line 785
Source documentation
Every actual simplicial map between two standard simplices is weak.
```
theorem standard_simplex_hom_weak {m n : SimplexCategory}
    (f : SSet.stdSimplex.{0}.obj m ⟶ SSet.stdSimplex.obj n) :
    realizationWeakEquivalences f := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.simplexLastVertex_weak line 793
Source documentation
On each standard simplex, last vertex is weak by the actual contraction of its finite-chain nerve onto its greatest vertex.
```
theorem simplexLastVertex_weak (n : SimplexCategory) :
    realizationWeakEquivalences (simplexLastVertex.{0}.app n) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.lastVertex_standard_weak line 802
Source documentation
The same result expressed using the original subdivision functor.
```
theorem lastVertex_standard_weak (n : SimplexCategory) :
    realizationWeakEquivalences (lastVertex.app (SSet.stdSimplex.{0}.obj n)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.finiteChain_map_injective line 810

Source documentation

Injective vertex maps remain injective on finite nonempty chains.

theorem finiteChain_map_injective {P Q : Type} [PartialOrder P] [PartialOrder Q]
    (f : P →o Q) (hf : Function.Injective f) :
    Function.Injective (NonemptyFiniteChains.orderHomMap f) := by
…

theorem OAI.Thomason.Construction.simplexSubdivision_map_mono line 819
Source documentation
The finite-chain nerve of a simplex preserves every face embedding.
```
theorem simplexSubdivision_map_mono {m n : SimplexCategory} (f : m ⟶ n) [Mono f] :
    Mono (SimplexCategory.sd.{0}.map f) := by
…
```
theorem OAI.Thomason.Construction.subdivision_standard_map_mono line 838
Source documentation
On the original left-Kan-extension subdivision functor, every standard face inclusion is still an actual simplicial monomorphism.
```
theorem subdivision_standard_map_mono {m n : SimplexCategory} (f : m ⟶ n) [Mono f] :
    Mono (SSet.sd.map (SSet.stdSimplex.{0}.map f)) := by
…
```
def OAI.Thomason.Construction.chainsSupported line 868
Source documentation
Chains whose original vertices all belong to a specified set.
```
def chainsSupported (A : Set P) : Set (NonemptyFiniteChains P) :=
…
```
theorem OAI.Thomason.Construction.chainsSupported_isLowerSet line 871
theorem OAI.Thomason.Construction.chainsSupported_inter line 874
def OAI.Thomason.Construction.finiteChainPreimage line 881
Source documentation
Pull a supported finite chain back through its original order embedding.
```
def finiteChainPreimage (f : P ↪o Q) (s : NonemptyFiniteChains Q)
    (hs : s ∈ chainsSupported (Set.range f)) : NonemptyFiniteChains P where
…
```
Mentions: OAI.Thomason.Construction.chainsSupported
theorem OAI.Thomason.Construction.finiteChainPreimage_map line 894
theorem OAI.Thomason.Construction.finiteChainPreimage_mono line 910
theorem OAI.Thomason.Construction.finiteChain_map_supported line 920
theorem OAI.Thomason.Construction.finiteChain_nerve_range line 927
Source documentation
Exact image of the nerve map on finite chains, not merely its vertices.
```
theorem finiteChain_nerve_range (f : P ↪o Q) :
    SSet.Subcomplex.range
      (nerveMap (NonemptyFiniteChains.orderHomMap f.toOrderHom).monotone.functor) =
      fullSubposetComplex (chainsSupported (Set.range f)) := by
…
```
Mentions: OAI.Thomason.Construction.fullSubposetComplex, OAI.Thomason.Construction.chainsSupported

theorem OAI.Thomason.Construction.finiteChain_nerve_range_inter line 946

Source documentation

The chain nerve preserves intersections of original vertex images.

theorem finiteChain_nerve_range_inter {R : Type} [PartialOrder R]
    (f : P ↪o Q) (g : R ↪o Q) :
    SSet.Subcomplex.range
        (nerveMap (NonemptyFiniteChains.orderHomMap f.toOrderHom).monotone.functor) ⊓
      SSet.Subcomplex.range
        (nerveMap (NonemptyFiniteChains.orderHomMap g.toOrderHom).monotone.functor) =
      fullSubposetComplex (chainsSupported (Set.range f ∩ Set.range g)) := by
…

Mentions: OAI.Thomason.Construction.fullSubposetComplex, OAI.Thomason.Construction.chainsSupported

theorem OAI.Thomason.Construction.simplexSubdivision_map_range line 957

Source documentation

The exact face-image description for the actual simplex subdivision.

theorem simplexSubdivision_map_range {m n : SimplexCategory} (f : m ⟶ n) [Mono f] :
    SSet.Subcomplex.range (SimplexCategory.sd.{0}.map f) =
      fullSubposetComplex (chainsSupported
        (Set.range (fun x : ULift.{0} (Fin (m.len + 1)) =>
          (ULift.up (f.toOrderHom x.down) : ULift.{0} (Fin (n.len + 1)))))) := by
…

Mentions: OAI.Thomason.Construction.fullSubposetComplex, OAI.Thomason.Construction.chainsSupported