GraySingularPathComparison.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Barycentric lifting tests for the actual Gray--Street comparison

These are consequences of the constructed topological lifting bridge. They add no hypothesis to the main theorem and do not assert that an arbitrary Gray projection has the displayed lifting property.

theorem OAI.Thomason.Construction.weak_and_singular_weak_of_singular_boundary_rlp line 28
Source documentation
Singular boundary lifting forces the weak test both before and after singularization, without requiring the singular counit to be weak.
```
theorem weak_and_singular_weak_of_singular_boundary_rlp {X Y : TopCat.{0}} (f : X ⟶ Y)
    (hf : SSet.modelCategoryQuillen.I.rlp (TopCat.toSSet.map f)) :
    topologicalWeakEquivalences f ∧ realizationWeakEquivalences (TopCat.toSSet.map f) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.RightGrayInput.nerveCylinder_weak_of_boundary_lifting line 42
Source documentation
The concrete boundary lifting test on a realized strict Gray projection suffices for the actual simplicial Gray--Street comparison to be weak.
```
theorem nerveCylinder_weak_of_boundary_lifting (X : StrictOmegaCategory.{0})
    (hp : ∀ n, HasLiftingProperty (RealizationPrism.boundaryInclusion n)
      (SSet.toTop.map (h.streetNerve.map (G.projection.app X)))) :
    realizationWeakEquivalences (G.nerveCylinder aw X) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.RightGrayInput.realizedCylinderComparison_weak_of_boundary_lifting line 51
Source documentation
The same lifting test controls the original continuous comparison map, including all basepoints and positive homotopy groups.
```
theorem realizedCylinderComparison_weak_of_boundary_lifting (X : StrictOmegaCategory.{0})
    (hp : ∀ n, HasLiftingProperty (RealizationPrism.boundaryInclusion n)
      (SSet.toTop.map (h.streetNerve.map (G.projection.app X)))) :
    topologicalWeakEquivalences (G.realizedCylinderComparison aw X) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.boundaryInclusion, OAI.Thomason.Construction.topologicalWeakEquivalences
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullInclusion_weak_of_boundary_lifting line 63
Source documentation
For strict full inclusions the lifting test implies precisely the Street weak test, using the actual closed subspace realization.
```
theorem fullInclusion_weak_of_boundary_lifting (h : NormalizedSimplexIdentities)
    (C : StrictOmegaCategory.{0}) (S : Set C)
    (hp : ∀ n, HasLiftingProperty (RealizationPrism.boundaryInclusion n)
      (SSet.toTop.map (h.streetNerve.map (C.fullInclusion S)))) :
    h.streetWeakEquivalences (C.fullInclusion S) :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.RealizationPrism.boundaryInclusion
def OAI.Thomason.Construction.RightGrayInput.singularPathTranspose line 96
Source documentation
The strict Gray homotopy transposed into the actual compact-open path space of the Street realization.
```
def singularPathTranspose {X Y : StrictOmegaCategory.{0}} (P : G.cylinder.obj X ⟶ Y) :
    h.streetNerve.obj X ⟶ TopCat.toSSet.obj
      (continuousPathSpace (SSet.toTop.obj (h.streetNerve.obj Y))) :=
…
```
Mentions: OAI.Thomason.Construction.continuousPathSpace
theorem OAI.Thomason.Construction.RightGrayInput.singularPathTranspose_cylinder line 104
Source documentation
The path-space transpose recovers the original Street-nerve cylinder followed by the actual realization/singular unit.
```
theorem singularPathTranspose_cylinder {X Y : StrictOmegaCategory.{0}}
    (P : G.cylinder.obj X ⟶ Y) :
    singularPathCylinderEquiv _ _ (G.singularPathTranspose aw P) =
      (G.nerveHomotopy aw P).h ≫ sSetTopAdj.unit.app (h.streetNerve.obj Y) := by
…
```
Mentions: OAI.Thomason.Construction.singularPathCylinderEquiv
theorem OAI.Thomason.Construction.RightGrayInput.singularPathTranspose_zero line 119
theorem OAI.Thomason.Construction.RightGrayInput.singularPathTranspose_one line 126
theorem OAI.Thomason.Construction.weak_of_singular_path_internalHom line 137
Source documentation
Weak equivalence of the actual singular internal-hom path map reflects the original topological weak test, with no singular-counit assumption.
```
theorem weak_of_singular_path_internalHom {X Y : TopCat.{0}} (p : X ⟶ Y)
    (hp : 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.NormalizedSimplexIdentities.streetWeak_of_singular_path_internalHom line 149
Source documentation
The same exact reflection applies to the implemented strict Street nerve.
```
theorem streetWeak_of_singular_path_internalHom (h : NormalizedSimplexIdentities)
    {X Y : StrictOmegaCategory.{0}} (f : X ⟶ Y)
    (hf : realizationWeakEquivalences ((ihom (Δ[1] : SSet.{0})).map
      (TopCat.toSSet.map (SSet.toTop.map (h.streetNerve.map f))))) :
    h.streetWeakEquivalences f :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.NormalizedSimplexIdentities.map