StreetWhitehead.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Recovering positive faces from strict coordinate cuts

Every face with positive mass separates its inside vertices strictly from its outside vertices. This is the uniqueness step for barycentric flags.

theorem OAI.Thomason.Construction.SubdivisionBarycentric.comparable_face_weights line 25
theorem OAI.Thomason.Construction.SubdivisionBarycentric.positive_face_strict_cut line 42
Source documentation
A positively weighted face is a strict upper-level set of the resulting geometric point. Ties can occur only within one side of its boundary.
```
theorem positive_face_strict_cut (n : ℕ)
    (z : SSet.toTop.obj (nerve (Faces n))) (A : Faces n)
    (hA : 0 < (PosetGeometry.coordinates (Faces n) z).weights A)
    (i j : Fin (n+1)) (hi : ULift.up i ∈ A.finset) (hj : ULift.up j ∉ A.finset) :
    (point n z).weights j < (point n z).weights i := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.PosetGeometry.coordinates, OAI.Thomason.Construction.SubdivisionBarycentric.point
theorem OAI.Thomason.Construction.SubdivisionBarycentric.positive_face_sorted_lower line 68
Source documentation
After sorting the resulting coordinates, every positive face is an initial segment of that same ordering. Thus the active faces share one flag.
```
theorem positive_face_sorted_lower (n : ℕ)
    (z : SSet.toTop.obj (nerve (Faces n))) (A : Faces n)
    (hA : 0 < (PosetGeometry.coordinates (Faces n) z).weights A)
    (σ : Equiv.Perm (Fin (n+1)))
    (hσ : Antitone (fun i => (point n z).weights (σ i))) :
    IsLowerSet {i : Fin (n+1) | ULift.up (σ i) ∈ A.finset} := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.PosetGeometry.coordinates, OAI.Thomason.Construction.SubdivisionBarycentric.point
theorem OAI.Thomason.Construction.SubdivisionBarycentric.positive_face_sorted_prefix line 81
Source documentation
A nonempty positive face is one full prefix of the sorted vertices, with an actual last index.
```
theorem positive_face_sorted_prefix (n : ℕ)
    (z : SSet.toTop.obj (nerve (Faces n))) (A : Faces n)
    (hA : 0 < (PosetGeometry.coordinates (Faces n) z).weights A)
    (σ : Equiv.Perm (Fin (n+1)))
    (hσ : Antitone (fun i => (point n z).weights (σ i))) :
    ∃ k : Fin (n+1), ∀ i : Fin (n+1), ULift.up (σ i) ∈ A.finset ↔ i ≤ k := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.PosetGeometry.coordinates, OAI.Thomason.Construction.SubdivisionBarycentric.point
theorem OAI.Thomason.Construction.singular_path_internalHom_weak_iff line 122
Source documentation
Singular internal-hom paths preserve and reflect the original actual weak-equivalence test, for arbitrary continuous maps.
```
theorem singular_path_internalHom_weak_iff {X Y : TopCat.{0}} (p : X ⟶ Y) :
    realizationWeakEquivalences ((ihom (Δ[1] : SSet.{0})).map (TopCat.toSSet.map p)) ↔
      IsWeakHomotopyEquivalence p.hom := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.IsWeakHomotopyEquivalence
theorem OAI.Thomason.Construction.weak_map_homotopy_fiber_weak line 130
Source documentation
Every actual homotopy fibre of a weak map is weakly contractible. The mapping-path projection and its Kan property are constructed explicitly.
```
theorem weak_map_homotopy_fiber_weak {X Y : TopCat.{0}} (p : X ⟶ Y)
    (hp : IsWeakHomotopyEquivalence p.hom) (y : Y) :
    IsWeakHomotopyEquivalence (ContinuousMap.const
      {z : mappingPathSpace p // (mappingPathProjection p).hom z = y} ()) := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.mappingPathSpace, OAI.Thomason.Construction.mappingPathProjection
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetWeak_iff_singular_realization line 143
Source documentation
The Street realization and its actual singular realization have the same weak-equivalence test, without Gray or Kan–Quillen assumptions.
```
theorem streetWeak_iff_singular_realization (h : NormalizedSimplexIdentities)
    {C D : StrictOmegaCategory.{0}} (f : C ⟶ D) :
    h.streetWeakEquivalences f ↔ realizationWeakEquivalences
      (TopCat.toSSet.map (SSet.toTop.map (h.streetNerve.map f))) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finiteStreetWeak_iff_singular_realization line 150
Source documentation
The same equivalence in every finite strict dimension.
```
theorem finiteStreetWeak_iff_singular_realization (h : NormalizedSimplexIdentities) (n : ℕ)
    {C D : StrictOmegaCategory.Truncated (n+1)} (f : C ⟶ D) :
    (realizationWeakEquivalences.inverseImage (h.finiteStreetNerve (n+1))) f ↔ realizationWeakEquivalences
      (TopCat.toSSet.map (SSet.toTop.map ((h.finiteStreetNerve (n+1)).map f))) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictOmegaCategory.Truncated, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.NormalizedSimplexIdentities.map
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetWeak_iff_singular_path_internalHom line 157
Source documentation
Actual singular path objects give the same strict Street weak test.
```
theorem streetWeak_iff_singular_path_internalHom (h : NormalizedSimplexIdentities)
    {C D : StrictOmegaCategory.{0}} (f : C ⟶ D) :
    h.streetWeakEquivalences f ↔ realizationWeakEquivalences
      ((ihom (Δ[1] : SSet.{0})).map
        (TopCat.toSSet.map (SSet.toTop.map (h.streetNerve.map f)))) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.NormalizedSimplexIdentities.map

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetWeak_iff_homotopyEquiv line 184

Source documentation

A strict higher functor is Street weak precisely when its actual realized Street nerve admits a continuous homotopy inverse.

theorem streetWeak_iff_homotopyEquiv (h : NormalizedSimplexIdentities)
    {C D : StrictOmegaCategory.{0}} (f : C ⟶ D) :
    h.streetWeakEquivalences f ↔
      ∃ e : ContinuousMap.HomotopyEquiv (SSet.toTop.obj (h.streetNerve.obj C))
          (SSet.toTop.obj (h.streetNerve.obj D)),
        e.toFun = (SSet.toTop.map (h.streetNerve.map f)).hom :=
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finiteStreetWeak_iff_homotopyEquiv line 194

Source documentation

The same actual homotopy-inverse criterion holds in every positive finite strict dimension, with the original finite Street nerve.

theorem finiteStreetWeak_iff_homotopyEquiv (h : NormalizedSimplexIdentities) (n : ℕ)
    {C D : StrictOmegaCategory.Truncated (n+1)} (f : C ⟶ D) :
    (realizationWeakEquivalences.inverseImage (h.finiteStreetNerve (n+1))) f ↔
      ∃ e : ContinuousMap.HomotopyEquiv (SSet.toTop.obj ((h.finiteStreetNerve (n+1)).obj C))
          (SSet.toTop.obj ((h.finiteStreetNerve (n+1)).obj D)),
        e.toFun = (SSet.toTop.map ((h.finiteStreetNerve (n+1)).map f)).hom :=
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictOmegaCategory.Truncated, OAI.Thomason.Construction.NormalizedSimplexIdentities.map

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullInclusion_streetWeak_deformation line 204

Source documentation

An actual full inclusion that is Street weak retracts continuously, with its complete realized full subcategory fixed throughout the deformation.

theorem fullInclusion_streetWeak_deformation (h : NormalizedSimplexIdentities)
    (C : StrictOmegaCategory.{0}) (S : Set C)
    (hw : h.streetWeakEquivalences (C.fullInclusion S)) :
    ∃ r : SSet.toTop.obj (h.streetNerve.obj C) ⟶
        SSet.toTop.obj (h.streetNerve.obj (C.fullOn S)),
      SSet.toTop.map (h.streetNerve.map (C.fullInclusion S)) ≫ r = 𝟙 _ ∧
      Nonempty ((r ≫ SSet.toTop.map (h.streetNerve.map (C.fullInclusion S))).hom.HomotopyRel
        (ContinuousMap.id _)
        (Set.range (SSet.toTop.map (h.streetNerve.map (C.fullInclusion S))).hom)) := by
…

Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities