SingularPathSpaceAdjunction.lean`

49 declarations, 0 contain sorry, 0 declared as axioms

Constructed oriental comparison and actual cylinder weak equivalence

Finite positive-chain decomposition gives the atom-generation property for the oriental comparison. The normalized chain identities hold for the simplex complexes.

def OAI.Thomason.Construction.NormalizedSimplexIdentities.orientalAbelianizationIso line 32
Source documentation
The actual orientals abelianize naturally to the normalized simplex complexes, without a separate published generation premise.
```
def orientalAbelianizationIso (h : NormalizedSimplexIdentities) :
    h.cosimplicial ⋙ StrictOmegaCategory.Abelianization.functor ≅
      h.chainCosimplicial :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.functor
def OAI.Thomason.Construction.NormalizedSimplexIdentities.constructedChainModelComparison line 39
Source documentation
The simplex comparison with the global chain model follows from normalized simplex identities.
```
def constructedChainModelComparison (h : NormalizedSimplexIdentities) :
    h.cylinderCosimplicial ≅
      h.cosimplicial ⋙ StrictOmegaCategory.GrayChainExtension.model :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.model
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.constructedChainModelComparison_endpoint line 44
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.chainCylinder_projection_weak line 53
Source documentation
Projection from every concrete positive-chain cylinder is an actual Street-nerve realization weak equivalence, with no Gray or model-structure input and no atom-generation assumption.
```
theorem chainCylinder_projection_weak (h : NormalizedSimplexIdentities)
    (K : DirectedComplex.{0}) :
    h.streetWeakEquivalences (RightCylinder.projection K).realization :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

theorem OAI.Thomason.Construction.realization_homotopy_extension line 81

Source documentation

Every realized simplicial monomorphism has the homotopy extension property, with the prescribed homotopy retained pointwise on the entire subobject.

theorem realization_homotopy_extension {A K : SSet.{0}} {X : TopCat.{0}}
    (i : A ⟶ K) [Mono i] (f : SSet.toTop.obj K ⟶ X)
    {g : SSet.toTop.obj A ⟶ X}
    (H : (SSet.toTop.map i ≫ f).hom.Homotopy g.hom) :
    ∃ F : C(unitInterval × SSet.toTop.obj K, X),
      (∀ x, F (0, x) = f.hom x) ∧
      ∀ t x, F (t, (SSet.toTop.map i).hom x) = H (t, x) := by
…

theorem OAI.Thomason.Construction.realization_homotopy_extension_endpoint line 108

Source documentation

The extension may be packaged as a continuous homotopy with its endpoint.

theorem realization_homotopy_extension_endpoint {A K : SSet.{0}} {X : TopCat.{0}}
    (i : A ⟶ K) [Mono i] (f : SSet.toTop.obj K ⟶ X)
    {g : SSet.toTop.obj A ⟶ X}
    (H : (SSet.toTop.map i ≫ f).hom.Homotopy g.hom) :
    ∃ (g' : SSet.toTop.obj K ⟶ X) (H' : f.hom.Homotopy g'.hom),
      ∀ t x, H' (t, (SSet.toTop.map i).hom x) = H (t, x) := by
…

def OAI.Thomason.Construction.RealizedCube.oppositeFaces line 141
Source documentation
The two faces perpendicular to the first coordinate.
```
def oppositeFaces (n : ℕ) : (obj (n+1)).Subcomplex :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.oppositeFaces_le_boundary line 144
def OAI.Thomason.Construction.RealizedCube.oppositeFacesInclusion line 149
instance OAI.Thomason.Construction.RealizedCube.oppositeFacesInclusion_mono line 153
theorem OAI.Thomason.Construction.RealizedCube.oppositeFaces_coordinate line 157
def OAI.Thomason.Construction.RealizedCube.oppositeFacesContraction line 177
Source documentation
Contract the remaining coordinates without leaving either opposite face.
```
def oppositeFacesContraction (n : ℕ) :
    C(unitInterval × SSet.toTop.obj (oppositeFaces n : SSet.{0}),
      SSet.toTop.obj (boundary n : SSet.{0})) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.oppositeFaces, OAI.Thomason.Construction.RealizedCube.boundary
theorem OAI.Thomason.Construction.RealizedCube.oppositeFacesContraction_zero line 188
def OAI.Thomason.Construction.RealizedCube.boundaryFacePoint line 215
Source documentation
The literal face point in the full cube boundary.
```
def boundaryFacePoint (n : ℕ) (e : Bool) (u : Fin n → unitInterval) :
    Cube.boundary (Fin (n+1)) :=
…
```
theorem OAI.Thomason.Construction.RealizedCube.boundaryFacePoint_mem_oppositeFaces line 219
theorem OAI.Thomason.Construction.RealizedCube.oppositeFacesContraction_one line 245

theorem OAI.Thomason.Construction.RealizedCube.boundary_normalization line 290

Source documentation

Any boundary map can be homotoped so that each of its two opposite faces is constant. The two constants are its original corner values.

theorem boundary_normalization {X : TopCat.{0}} (n : ℕ)
    (a : C(Cube.boundary (Fin (n+1)), X)) :
    ∃ F : C(unitInterval × Cube.boundary (Fin (n+1)), X),
      (∀ x, F (0, x) = a x) ∧
      ∀ (e : Bool) (u : Fin n → unitInterval),
        F (1, boundaryFacePoint n e u) =
          a (boundaryFacePoint n e (fun _ => 0)) := by
…

Mentions: OAI.Thomason.Construction.RealizedCube.boundaryFacePoint

theorem OAI.Thomason.Construction.RealizedCube.boundary_square_normalization line 328

Source documentation

Normalize a complete lifting square while retaining a homotopy of the base cube compatible with the prescribed boundary at every time.

theorem boundary_square_normalization {X Y : TopCat.{0}} (p : X ⟶ Y) (n : ℕ)
    (a : C(Cube.boundary (Fin (n+1)), X))
    (b : C(Fin (n+1) → unitInterval, Y))
    (hab : ∀ z, p.hom (a z) = b z.val) :
    ∃ (F : C(unitInterval × Cube.boundary (Fin (n+1)), X))
      (B : C(unitInterval × (Fin (n+1) → unitInterval), Y)),
      (∀ z, F (0, z) = a z) ∧ (∀ z, B (0, z) = b z) ∧
      (∀ t z, p.hom (F (t, z)) = B (t, z.val)) ∧
      ∀ (e : Bool) (u : Fin n → unitInterval),
        F (1, boundaryFacePoint n e u) =
          a (boundaryFacePoint n e (fun _ => 0)) := by
…

Mentions: OAI.Thomason.Construction.RealizedCube.boundaryFacePoint

theorem OAI.Thomason.Construction.singularCylinderMap_realizedHomotopy line 383
Source documentation
Realizing a simplicial homotopy and then taking its singular cylinder adjoint agrees exactly with postcomposing the original homotopy by the unit.
```
theorem singularCylinderMap_realizedHomotopy {K L : SSet.{0}} {f g : K ⟶ L}
    (H : SSet.Homotopy f g) :
    singularCylinderMap (RealizedCylinder.homotopy H).toContinuousMap =
      H.h ≫ sSetTopAdj.unit.app L := by
…
```
Mentions: OAI.Thomason.Construction.singularCylinderMap, OAI.Thomason.Construction.RealizedCylinder.homotopy

def OAI.Thomason.Construction.adjointRealizationHomotopy line 422

Source documentation

An arbitrary continuous homotopy on a realization has a simplicial adjoint, with its two specified adjoint endpoint maps.

def adjointRealizationHomotopy {K : SSet.{0}} {X : TopCat.{0}}
    {f g : SSet.toTop.obj K ⟶ X} (H : f.hom.Homotopy g.hom) :
    SSet.Homotopy (sSetTopAdj.homEquiv K X f) (sSetTopAdj.homEquiv K X g) where
…

theorem OAI.Thomason.Construction.evaluateSingularCylinder_constant line 453

Source documentation

A constant cylinder is adjoint to the constant simplicial cylinder, including all higher simplices.

theorem evaluateSingularCylinder_constant {K : SSet.{0}} {X : TopCat.{0}}
    (f : K ⟶ TopCat.toSSet.obj X) (t : unitInterval) (x : SSet.toTop.obj K) :
    evaluateSingularCylinder (fst K (Δ[1] : SSet.{0}) ≫ f) (t, x) =
      ((sSetTopAdj.homEquiv K X).symm f).hom x := by
…

Mentions: OAI.Thomason.Construction.evaluateSingularCylinder

theorem OAI.Thomason.Construction.adjointRealizationHomotopy_stationary line 467

Source documentation

Stationarity on the entire realized image is retained exactly by the adjoint cylinder. No monomorphism or weak equivalence hypothesis is needed.

theorem adjointRealizationHomotopy_stationary {A K : SSet.{0}} {X : TopCat.{0}}
    (i : A ⟶ K) {f g : SSet.toTop.obj K ⟶ X}
    (H : f.hom.HomotopyRel g.hom (Set.range (SSet.toTop.map i).hom)) :
    i ▷ Δ[1] ≫ (adjointRealizationHomotopy H.toHomotopy).h =
      fst A Δ[1] ≫ i ≫ sSetTopAdj.homEquiv K X f := by
…

Mentions: OAI.Thomason.Construction.adjointRealizationHomotopy

theorem OAI.Thomason.Construction.adjoint_realized_map line 487
Source documentation
The adjoint of a realized map is its original map followed by the actual realization/singular unit.
```
theorem adjoint_realized_map {A X : SSet.{0}} (a : A ⟶ X) :
    sSetTopAdj.homEquiv A (SSet.toTop.obj X) (SSet.toTop.map a) =
      a ≫ sSetTopAdj.unit.app X := by
…
```

theorem OAI.Thomason.Construction.adjoint_relative_extension line 496

Source documentation

An exact continuous relative extension gives an exact singular relative extension. The original simplicial boundary is preserved after the unit.

theorem adjoint_relative_extension {A K X : SSet.{0}} (i : A ⟶ K) (a : A ⟶ X)
    (c : SSet.toTop.obj K ⟶ SSet.toTop.obj X)
    (hc : SSet.toTop.map i ≫ c = SSet.toTop.map a) :
    i ≫ sSetTopAdj.homEquiv K (SSet.toTop.obj X) c = a ≫ sSetTopAdj.unit.app X := by
…

theorem OAI.Thomason.Construction.realizedCube_finite line 520
Source documentation
The actual triangulated cube is finite in every dimension.
```
theorem realizedCube_finite (n : ℕ) : (RealizedCube.obj n).Finite := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj

theorem OAI.Thomason.Construction.singularCubeProductEquiv_relative line 530

Source documentation

A continuous higher family whose whole boundary is simplicial gives an exact singular family with that entire boundary, followed by the unit.

theorem singularCubeProductEquiv_relative {K X : SSet.{0}} (n : ℕ)
    (a : K ⊗ (RealizedCube.boundary n).toSSet ⟶ X)
    (H : TopCat.of (SSet.toTop.obj K × SSet.toTop.obj (RealizedCube.obj (n+1))) ⟶
      SSet.toTop.obj X)
    (hH : SSet.toTop.map (K ◁ (RealizedCube.boundary n).ι) ≫
      realizationProductComparison K (RealizedCube.obj (n+1)) ≫ H = SSet.toTop.map a) :
    K ◁ (RealizedCube.boundary n).ι ≫ singularCubeProductEquiv K (n+1) (SSet.toTop.obj X) H =
      a ≫ sSetTopAdj.unit.app X := by
…

Mentions: OAI.Thomason.Construction.RealizedCube.boundary, OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.singularCubeProductEquiv

theorem OAI.Thomason.Construction.finite_singular_cube_family line 547

Source documentation

One finite singular carrier contains the entire higher cubical family and its exact original boundary. The carrier retains the full continuous evaluation, not just the two endpoint maps.

theorem finite_singular_cube_family {K X : SSet.{0}} [K.Finite] (n : ℕ)
    (a : K ⊗ (RealizedCube.boundary n).toSSet ⟶ X)
    (H : TopCat.of (SSet.toTop.obj K × SSet.toTop.obj (RealizedCube.obj (n+1))) ⟶
      SSet.toTop.obj X)
    (hH : SSet.toTop.map (K ◁ (RealizedCube.boundary n).ι) ≫
      realizationProductComparison K (RealizedCube.obj (n+1)) ≫ H = SSet.toTop.map a) :
    ∃ (S : (TopCat.toSSet.obj (SSet.toTop.obj X)).Subcomplex) (_ : SSet.Finite S.toSSet)
      (d : K ⊗ RealizedCube.obj (n+1) ⟶ S.toSSet)
      (aS : K ⊗ (RealizedCube.boundary n).toSSet ⟶ S.toSSet),
      aS ≫ S.ι = a ≫ sSetTopAdj.unit.app X ∧
      K ◁ (RealizedCube.boundary n).ι ≫ d = aS ∧
      (realizationCubeProductIso K (n+1)).inv ≫
…

theorem OAI.Thomason.Construction.singularFiniteProductEquiv_parameter line 593
Source documentation
Changing the family parameter commutes with the actual product adjunction. Both sides represent the same full continuous family.
```
theorem singularFiniteProductEquiv_parameter {L K P : SSet.{0}} [P.Finite]
    (f : L ⟶ K) (X : TopCat.{0})
    (H : TopCat.of (SSet.toTop.obj K × SSet.toTop.obj P) ⟶ X) :
    letI := realizationProductComparison_finite_isIso K P
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison_finite_isIso
theorem OAI.Thomason.Construction.singularFiniteProductEquiv_relative line 612
Source documentation
Restriction to an arbitrary prescribed simplicial parameter subspace is exact under the singular adjunction. The parameter need only be finite; it need not already be presented as a triangulated cube.
```
theorem singularFiniteProductEquiv_relative {K A P X : SSet.{0}} [P.Finite]
    (i : A ⟶ P) (a : K ⊗ A ⟶ X)
    (H : TopCat.of (SSet.toTop.obj K × SSet.toTop.obj P) ⟶ SSet.toTop.obj X)
    (hH : SSet.toTop.map (K ◁ i) ≫ realizationProductComparison K P ≫ H =
      SSet.toTop.map a) :
    letI := realizationProductComparison_finite_isIso K P
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.realizationProductComparison_finite_isIso
theorem OAI.Thomason.Construction.finite_singular_parameter_family line 627
Source documentation
A whole continuous family and its entire prescribed subfamily fit in one finite singular carrier. Evaluation recovers the original family at every point of the actual product realization.
```
theorem finite_singular_parameter_family {K A P X : SSet.{0}} [K.Finite] [P.Finite]
    (i : A ⟶ P) (a : K ⊗ A ⟶ X)
    (H : TopCat.of (SSet.toTop.obj K × SSet.toTop.obj P) ⟶ SSet.toTop.obj X)
    (hH : SSet.toTop.map (K ◁ i) ≫ realizationProductComparison K P ≫ H =
      SSet.toTop.map a) :
    letI := realizationProductComparison_finite_isIso K P
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.realizationProductComparison_finite_isIso

theorem OAI.Thomason.Construction.singular_fibration_relative_homotopy_lifting line 676

Source documentation

If the actual singular map is a Kan fibration, it lifts any continuous homotopy on a realization while respecting a prescribed subcomplex homotopy.

theorem singular_fibration_relative_homotopy_lifting
    {A K : SSet.{0}} {X Y : TopCat.{0}} (i : A ⟶ K) [Mono i]
    (p : X ⟶ Y) [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (f : SSet.toTop.obj K ⟶ X)
    (a : C(unitInterval × SSet.toTop.obj A, X))
    (H : C(unitInterval × SSet.toTop.obj K, Y))
    (ha₀ : ∀ x, a (0, x) = f.hom ((SSet.toTop.map i).hom x))
    (hap : ∀ t x, p.hom (a (t, x)) = H (t, (SSet.toTop.map i).hom x))
    (hf₀ : ∀ x, p.hom (f.hom x) = H (0, x)) :
    ∃ F : C(unitInterval × SSet.toTop.obj K, X),
      (∀ x, F (0, x) = f.hom x) ∧
      (∀ t x, F (t, (SSet.toTop.map i).hom x) = a (t, x)) ∧
…

theorem OAI.Thomason.Construction.RealizedCube.singular_fibration_cube_lifting line 744

Source documentation

The relative homotopy lifting property for an ordinary cube and its entire boundary follows from the Kan fibration property of the actual singular map.

theorem singular_fibration_cube_lifting {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)] (n : ℕ)
    (f : C(Fin (n+1) → unitInterval, X))
    (a : C(unitInterval × Cube.boundary (Fin (n+1)), X))
    (H : C(unitInterval × (Fin (n+1) → unitInterval), Y))
    (ha₀ : ∀ x : Cube.boundary (Fin (n+1)), a (0, x) = f x.val)
    (hap : ∀ t (x : Cube.boundary (Fin (n+1))), p.hom (a (t, x)) = H (t, x.val))
    (hf₀ : ∀ x, p.hom (f x) = H (0, x)) :
    ∃ F : C(unitInterval × (Fin (n+1) → unitInterval), X),
      (∀ x, F (0, x) = f x) ∧
      (∀ t (x : Cube.boundary (Fin (n+1))), F (t, x.val) = a (t, x)) ∧
      ∀ t x, p.hom (F (t, x)) = H (t, x) := by
…

theorem OAI.Thomason.Construction.singular_fibration_homotopy_lifting line 814

Source documentation

Singular Kan fibrations lift continuous homotopies on any realization with the given initial lift fixed exactly.

theorem singular_fibration_homotopy_lifting {K : SSet.{0}} {X Y : TopCat.{0}}
    (p : X ⟶ Y) [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (f : SSet.toTop.obj K ⟶ X) (H : C(unitInterval × SSet.toTop.obj K, Y))
    (h₀ : ∀ x, p.hom (f.hom x) = H (0, x)) :
    ∃ F : C(unitInterval × SSet.toTop.obj K, X),
      (∀ x, F (0, x) = f.hom x) ∧ ∀ t x, p.hom (F (t, x)) = H (t, x) := by
…

theorem OAI.Thomason.Construction.singular_fibration_path_lifting line 840

Source documentation

Every path in the base of a singular Kan fibration has a continuous lift from any specified point over its source.

theorem singular_fibration_path_lifting {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    {x : X} {y : Y} (γ : Path (p.hom x) y) :
    ∃ q : C(unitInterval, X), q 0 = x ∧ ∀ t, p.hom (q t) = γ t := by
…

theorem OAI.Thomason.Construction.singular_fibration_surjective_of_components line 856
Source documentation
Surjectivity on path components becomes strict surjectivity on points when the actual singular map is a Kan fibration.
```
theorem singular_fibration_surjective_of_components {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : Function.Surjective (HomotopyMaps.componentsMap p.hom)) :
    Function.Surjective p.hom := by
…
```
Mentions: OAI.Thomason.Construction.HomotopyMaps.componentsMap
theorem OAI.Thomason.Construction.singular_fibration_surjective_of_weak line 870
Source documentation
The degree-zero lifting consequence of a weak singular fibration, proved for the actual topological weak-equivalence test.
```
theorem singular_fibration_surjective_of_weak {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) : Function.Surjective p.hom :=
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence
def OAI.Thomason.Construction.continuousPathSpace line 897
Source documentation
The ordinary compact-open space of all paths, with unrestricted ends.
```
def continuousPathSpace (X : TopCat.{0}) : TopCat.{0} :=
…
```
def OAI.Thomason.Construction.continuousPathFamilyEquiv line 902
Source documentation
Exponential adjunction with the compact interval, in the order used by the realization cylinder. No local compactness of the parameter space is needed.
```
def continuousPathFamilyEquiv (K : SSet.{0}) (X : TopCat.{0}) :
    (SSet.toTop.obj K ⟶ continuousPathSpace X) ≃
      C(unitInterval × SSet.toTop.obj K, X) where
…
```
Mentions: OAI.Thomason.Construction.continuousPathSpace
def OAI.Thomason.Construction.singularPathCylinderEquiv line 920
Source documentation
Singular path families are exactly singular-valued simplicial cylinders.
```
def singularPathCylinderEquiv (K : SSet.{0}) (X : TopCat.{0}) :
    (K ⟶ TopCat.toSSet.obj (continuousPathSpace X)) ≃
      (K ⊗ Δ[1] ⟶ TopCat.toSSet.obj X) :=
…
```
Mentions: OAI.Thomason.Construction.continuousPathSpace
theorem OAI.Thomason.Construction.singularPathCylinderEquiv_naturality line 927
Source documentation
The cylinder correspondence respects every simplicial parameter change.
```
theorem singularPathCylinderEquiv_naturality {A K : SSet.{0}} (i : A ⟶ K)
    (X : TopCat.{0}) (f : K ⟶ TopCat.toSSet.obj (continuousPathSpace X)) :
    singularPathCylinderEquiv A X (i ≫ f) =
      i ▷ Δ[1] ≫ singularPathCylinderEquiv K X f := by
…
```
Mentions: OAI.Thomason.Construction.continuousPathSpace, OAI.Thomason.Construction.singularPathCylinderEquiv
def OAI.Thomason.Construction.swapCylinderEquiv line 943
Source documentation
Braiding identifies the two orders of the simplicial cylinder.
```
def swapCylinderEquiv (K : SSet.{0}) (X : SSet.{0}) :
    (K ⊗ Δ[1] ⟶ X) ≃ (Δ[1] ⊗ K ⟶ X) :=
…
```
def OAI.Thomason.Construction.singularPathInternalEquiv line 948
Source documentation
The hom-set form of the path-space/internal-hom identification.
```
def singularPathInternalEquiv (K : SSet.{0}) (X : TopCat.{0}) :
    (K ⟶ TopCat.toSSet.obj (continuousPathSpace X)) ≃
      (K ⟶ (ihom (Δ[1] : SSet.{0})).obj (TopCat.toSSet.obj X)) :=
…
```
Mentions: OAI.Thomason.Construction.continuousPathSpace
theorem OAI.Thomason.Construction.singularPathInternalEquiv_naturality line 954
def OAI.Thomason.Construction.singularPathSpaceIso line 965
Source documentation
The actual compact-open path space and the simplicial internal hom have isomorphic singular complexes.
```
def singularPathSpaceIso (X : TopCat.{0}) :
    TopCat.toSSet.obj (continuousPathSpace X) ≅
      (ihom (Δ[1] : SSet.{0})).obj (TopCat.toSSet.obj X) :=
…
```
Mentions: OAI.Thomason.Construction.continuousPathSpace
def OAI.Thomason.Construction.continuousPathMap line 974
Source documentation
Postcomposition on actual compact-open path spaces.
```
def continuousPathMap {X Y : TopCat.{0}} (p : X ⟶ Y) :
    continuousPathSpace X ⟶ continuousPathSpace Y :=
…
```
Mentions: OAI.Thomason.Construction.continuousPathSpace
theorem OAI.Thomason.Construction.singularPathCylinderEquiv_postcomp line 978
theorem OAI.Thomason.Construction.singularPathInternalEquiv_postcomp line 996
theorem OAI.Thomason.Construction.singularPathSpaceIso_naturality line 1008
Source documentation
The internal-hom comparison is natural in the target space.
```
theorem singularPathSpaceIso_naturality {X Y : TopCat.{0}} (p : X ⟶ Y) :
    TopCat.toSSet.map (continuousPathMap p) ≫ (singularPathSpaceIso Y).hom =
      (singularPathSpaceIso X).hom ≫ (ihom Δ[1]).map (TopCat.toSSet.map p) := by
…
```
Mentions: OAI.Thomason.Construction.continuousPathMap, OAI.Thomason.Construction.singularPathSpaceIso
def OAI.Thomason.Construction.singularPathMapArrowIso line 1020
Source documentation
Naturality gives an isomorphism of the actual induced path-map arrows.
```
def singularPathMapArrowIso {X Y : TopCat.{0}} (p : X ⟶ Y) :
    Arrow.mk (TopCat.toSSet.map (continuousPathMap p)) ≅
      Arrow.mk ((ihom Δ[1]).map (TopCat.toSSet.map p)) :=
…
```
Mentions: OAI.Thomason.Construction.continuousPathMap