SingularCylinderEquivalence.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

The actual realization weak equivalence of positive-chain cylinders

The explicit minimum contraction gives a homotopy inverse on Street nerves. This bridge uses the existing published simplex-generation premise, but no right Gray adjunction, transfer, localization or Kan lifting premise.

theorem OAI.Thomason.Construction.SimplexAtomsInput.chainCylinder_projection_weak line 30
Source documentation
The projection of an actual chain cylinder is a weak equivalence for the prescribed topological realization of the Street nerve.
```
theorem chainCylinder_projection_weak (K : DirectedComplex.{0}) :
    h.streetWeakEquivalences (RightCylinder.projection K).realization := by
…
```

def OAI.Thomason.Construction.RightGrayInput.realizedCylinderComparison line 83

Source documentation

The continuous comparison from the ordinary cylinder to the realized Gray cylinder.

def realizedCylinderComparison (X : StrictOmegaCategory.{0}) :
    TopologicalInterval.cylinder.obj (SSet.toTop.obj (h.streetNerve.obj X)) ⟶
      SSet.toTop.obj (h.streetNerve.obj (G.cylinder.obj X)) :=
…

theorem OAI.Thomason.Construction.RightGrayInput.realizedCylinderComparison_naturality line 90

Source documentation

The geometric Gray comparison is natural in actual strict functors.

theorem realizedCylinderComparison_naturality {X Y : StrictOmegaCategory.{0}}
    (f : X ⟶ Y) :
    TopologicalInterval.cylinder.map (SSet.toTop.map (h.streetNerve.map f)) ≫
      G.realizedCylinderComparison aw Y =
    G.realizedCylinderComparison aw X ≫
      SSet.toTop.map (h.streetNerve.map (G.cylinder.map f)) := by
…

theorem OAI.Thomason.Construction.RightGrayInput.nerveCylinder_weak_iff line 101
Source documentation
Preceding the nerve comparison by the explicit prism does not change its weak test.
```
theorem nerveCylinder_weak_iff (X : StrictOmegaCategory.{0}) :
    realizationWeakEquivalences (G.nerveCylinder aw X) ↔
      topologicalWeakEquivalences (G.realizedCylinderComparison aw X) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.topologicalWeakEquivalences

theorem OAI.Thomason.Construction.RightGrayInput.realizedCylinderComparison_projection line 115

Source documentation

Collapsing the Gray interval recovers the original realization point exactly.

theorem realizedCylinderComparison_projection (X : StrictOmegaCategory.{0}) :
    G.realizedCylinderComparison aw X ≫
      SSet.toTop.map (h.streetNerve.map (G.projection.app X)) =
        TopologicalInterval.projection (SSet.toTop.obj (h.streetNerve.obj X)) := by
…

Mentions: OAI.Thomason.Construction.TopologicalInterval.projection

theorem OAI.Thomason.Construction.RightGrayInput.realizedCylinderComparison_weak_iff line 128
Source documentation
The geometric Gray-cylinder comparison is weak exactly when its strict projection satisfies the actual Street-nerve weak-equivalence test.
```
theorem realizedCylinderComparison_weak_iff (X : StrictOmegaCategory.{0}) :
    topologicalWeakEquivalences (G.realizedCylinderComparison aw X) ↔
      h.streetWeakEquivalences (G.projection.app X) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences
theorem OAI.Thomason.Construction.RightGrayInput.nerveCylinder_weak_iff_projection line 143
Source documentation
The actual simplicial Gray–Street comparison and the strict cylinder projection have exactly the same semantic weak-equivalence obligation.
```
theorem nerveCylinder_weak_iff_projection (X : StrictOmegaCategory.{0}) :
    realizationWeakEquivalences (G.nerveCylinder aw X) ↔
      h.streetWeakEquivalences (G.projection.app X) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.RightGrayInput.realizedHomotopy_singular_counit line 149

Source documentation

Singularizing and realizing a strict Gray homotopy commutes pointwise with evaluation.

theorem realizedHomotopy_singular_counit {X Y : StrictOmegaCategory.{0}}
    (P : G.cylinder.obj X ⟶ Y) (t : unitInterval)
    (x : SSet.toTop.obj (TopCat.toSSet.obj (SSet.toTop.obj (h.streetNerve.obj X)))) :
    (sSetTopAdj.counit.app (SSet.toTop.obj (h.streetNerve.obj Y))).hom
      (RealizedCylinder.homotopy (singularHomotopy (G.realizedHomotopy aw P)) (t, x)) =
        G.realizedHomotopy aw P (t,
          (sSetTopAdj.counit.app (SSet.toTop.obj (h.streetNerve.obj X))).hom x) :=
…

Mentions: OAI.Thomason.Construction.RealizedCylinder.homotopy, OAI.Thomason.Construction.singularHomotopy

def OAI.Thomason.Construction.evaluateSingularCylinder line 176

Source documentation

A singular-valued simplicial cylinder gives an actual continuous cylinder.

def evaluateSingularCylinder {K : SSet.{0}} {X : TopCat.{0}}
    (e : K ⊗ Δ[1] ⟶ TopCat.toSSet.obj X) :
    C(unitInterval × SSet.toTop.obj K, X) where
…

theorem OAI.Thomason.Construction.evaluateSingularCylinder_naturality line 186

Source documentation

Evaluation commutes exactly with restriction along a simplicial map.

theorem evaluateSingularCylinder_naturality {A K : SSet.{0}} {X : TopCat.{0}}
    (i : A ⟶ K) (e : K ⊗ Δ[1] ⟶ TopCat.toSSet.obj X)
    (t : unitInterval) (x : SSet.toTop.obj A) :
    evaluateSingularCylinder e (t, (SSet.toTop.map i).hom x) =
      evaluateSingularCylinder (i ▷ Δ[1] ≫ e) (t, x) := by
…

Mentions: OAI.Thomason.Construction.evaluateSingularCylinder

theorem OAI.Thomason.Construction.evaluateSingularCylinder_postcomp line 199

Source documentation

Evaluation commutes with postcomposition by an actual continuous map.

theorem evaluateSingularCylinder_postcomp {K : SSet.{0}} {X Y : TopCat.{0}}
    (e : K ⊗ Δ[1] ⟶ TopCat.toSSet.obj X) (p : X ⟶ Y)
    (t : unitInterval) (x : SSet.toTop.obj K) :
    evaluateSingularCylinder (e ≫ TopCat.toSSet.map p) (t, x) =
      p.hom (evaluateSingularCylinder e (t, x)) := by
…

Mentions: OAI.Thomason.Construction.evaluateSingularCylinder

theorem OAI.Thomason.Construction.evaluateSingularCylinder_zero line 212

Source documentation

The zero endpoint is the actual adjoint of the zero face.

theorem evaluateSingularCylinder_zero {K : SSet.{0}} {X : TopCat.{0}}
    (e : K ⊗ Δ[1] ⟶ TopCat.toSSet.obj X) (x : SSet.toTop.obj K) :
    evaluateSingularCylinder e (0, x) =
      ((sSetTopAdj.homEquiv K X).symm (SSet.ι₀ ≫ e)).hom x := by
…

Mentions: OAI.Thomason.Construction.evaluateSingularCylinder

theorem OAI.Thomason.Construction.evaluateSingularCylinder_one line 224

Source documentation

The one endpoint is the actual adjoint of the one face.

theorem evaluateSingularCylinder_one {K : SSet.{0}} {X : TopCat.{0}}
    (e : K ⊗ Δ[1] ⟶ TopCat.toSSet.obj X) (x : SSet.toTop.obj K) :
    evaluateSingularCylinder e (1, x) =
      ((sSetTopAdj.homEquiv K X).symm (SSet.ι₁ ≫ e)).hom x := by
…

Mentions: OAI.Thomason.Construction.evaluateSingularCylinder

theorem OAI.Thomason.Construction.evaluateSingularCylinder_unit line 237
Source documentation
Singularizing a continuous homotopy and restricting by the unit recovers that same homotopy at every time and point.
```
theorem evaluateSingularCylinder_unit {K : SSet.{0}} {X : TopCat.{0}}
    {f g : SSet.toTop.obj K ⟶ X} (H : f.hom.Homotopy g.hom)
    (t : unitInterval) (x : SSet.toTop.obj K) :
    evaluateSingularCylinder
      (sSetTopAdj.unit.app K ▷ Δ[1] ≫ (singularHomotopy H).h) (t, x) = H (t, x) := by
…
```
Mentions: OAI.Thomason.Construction.evaluateSingularCylinder, OAI.Thomason.Construction.singularHomotopy

def OAI.Thomason.Construction.cylinderRealizationMap line 275

Source documentation

Pull a continuous cylinder back along the actual realized projections.

def cylinderRealizationMap {K : SSet.{0}} {X : TopCat.{0}}
    (H : C(unitInterval × SSet.toTop.obj K, X)) : SSet.toTop.obj (K ⊗ Δ[1]) ⟶ X :=
…

def OAI.Thomason.Construction.singularCylinderMap line 286

Source documentation

The simplicial adjoint of an arbitrary continuous cylinder.

def singularCylinderMap {K : SSet.{0}} {X : TopCat.{0}}
    (H : C(unitInterval × SSet.toTop.obj K, X)) : K ⊗ Δ[1] ⟶ TopCat.toSSet.obj X :=
…

theorem OAI.Thomason.Construction.evaluate_singularCylinderMap line 291
Source documentation
The original continuous cylinder is recovered exactly by evaluation.
```
theorem evaluate_singularCylinderMap {K : SSet.{0}} {X : TopCat.{0}}
    (H : C(unitInterval × SSet.toTop.obj K, X)) (t : unitInterval)
    (x : SSet.toTop.obj K) :
    evaluateSingularCylinder (singularCylinderMap H) (t, x) = H (t, x) := by
…
```
Mentions: OAI.Thomason.Construction.evaluateSingularCylinder, OAI.Thomason.Construction.singularCylinderMap

theorem OAI.Thomason.Construction.cylinderRealizationMap_naturality line 305

Source documentation

The actual projections of a realized simplicial cylinder are natural.

theorem cylinderRealizationMap_naturality {A K : SSet.{0}} {X : TopCat.{0}}
    (i : A ⟶ K) (H : C(unitInterval × SSet.toTop.obj K, X)) :
    SSet.toTop.map (i ▷ Δ[1]) ≫ cylinderRealizationMap H =
      cylinderRealizationMap
        (H.comp ⟨fun z => (z.1, (SSet.toTop.map i).hom z.2),
          continuous_fst.prodMk ((SSet.toTop.map i).hom.continuous.comp continuous_snd)⟩) := by
…

Mentions: OAI.Thomason.Construction.cylinderRealizationMap

theorem OAI.Thomason.Construction.singularCylinderMap_zero line 328

Source documentation

The zero face of the adjoint cylinder is the adjoint of its zero endpoint.

theorem singularCylinderMap_zero {K : SSet.{0}} {X : TopCat.{0}}
    (H : C(unitInterval × SSet.toTop.obj K, X)) :
    SSet.ι₀ ≫ singularCylinderMap H =
      sSetTopAdj.homEquiv K X
        (TopCat.ofHom ⟨fun x => H (0, x), H.continuous.comp (by fun_prop)⟩) := by
…

Mentions: OAI.Thomason.Construction.singularCylinderMap

theorem OAI.Thomason.Construction.singularCylinderMap_naturality line 345

Source documentation

Restriction of the continuous cylinder commutes with its simplicial adjoint.

theorem singularCylinderMap_naturality {A K : SSet.{0}} {X : TopCat.{0}}
    (i : A ⟶ K) (H : C(unitInterval × SSet.toTop.obj K, X)) :
    i ▷ Δ[1] ≫ singularCylinderMap H =
      singularCylinderMap
        (H.comp ⟨fun z => (z.1, (SSet.toTop.map i).hom z.2),
          continuous_fst.prodMk ((SSet.toTop.map i).hom.continuous.comp continuous_snd)⟩) := by
…

Mentions: OAI.Thomason.Construction.singularCylinderMap

theorem OAI.Thomason.Construction.singularCylinderMap_postcomp line 356

Source documentation

Postcomposition commutes with the adjoint cylinder, before realization.

theorem singularCylinderMap_postcomp {K : SSet.{0}} {X Y : TopCat.{0}}
    (H : C(unitInterval × SSet.toTop.obj K, X)) (p : X ⟶ Y) :
    singularCylinderMap H ≫ TopCat.toSSet.map p = singularCylinderMap (p.hom.comp H) := by
…

Mentions: OAI.Thomason.Construction.singularCylinderMap

theorem OAI.Thomason.Construction.singularCylinderMap_evaluate line 381
Source documentation
Applying the explicit cylinder adjunction to an evaluated singular map returns the original map in every simplicial degree.
```
theorem singularCylinderMap_evaluate {K : SSet.{0}} {X : TopCat.{0}}
    (e : K ⊗ Δ[1] ⟶ TopCat.toSSet.obj X) :
    singularCylinderMap (evaluateSingularCylinder e) = e := by
…
```
Mentions: OAI.Thomason.Construction.singularCylinderMap, OAI.Thomason.Construction.evaluateSingularCylinder
def OAI.Thomason.Construction.singularCylinderEquiv line 397
Source documentation
Continuous cylinders and singular-valued simplicial cylinders are exactly equivalent, with the constructed evaluation formula as inverse.
```
def singularCylinderEquiv (K : SSet.{0}) (X : TopCat.{0}) :
    C(unitInterval × SSet.toTop.obj K, X) ≃ (K ⊗ Δ[1] ⟶ TopCat.toSSet.obj X) where
…
```
theorem OAI.Thomason.Construction.evaluateSingularCylinder_injective line 409
Source documentation
Equality of evaluated continuous cylinders detects equality of the actual singular-valued simplicial maps.
```
theorem evaluateSingularCylinder_injective {K : SSet.{0}} {X : TopCat.{0}} :
    Function.Injective (evaluateSingularCylinder (K := K) (X := X)) :=
…
```
Mentions: OAI.Thomason.Construction.evaluateSingularCylinder