SingularCubeNaturality.lean`

73 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of genuine simplicial internal path objects

abbrev OAI.Thomason.Construction.internalPathObject line 22
def OAI.Thomason.Construction.internalPathCylinder line 25
Source documentation
Evaluation, with the interval written as the second cylinder factor.
```
def internalPathCylinder {K X : SSet.{0}} (a : K ⟶ internalPathObject X) :
    K ⊗ Δ[1] ⟶ X := (β_ K Δ[1]).hom ≫ uncurry a
```
Mentions: OAI.Thomason.Construction.internalPathObject
theorem OAI.Thomason.Construction.internalPathCylinder_naturality line 28
def OAI.Thomason.Construction.internalPathStart line 38
theorem OAI.Thomason.Construction.internalPathCylinder_start line 41
def OAI.Thomason.Construction.internalPathTranspose line 56
Source documentation
Currying a cylinder in this order reverses evaluation exactly.
```
def internalPathTranspose {K X : SSet.{0}} (h : K ⊗ Δ[1] ⟶ X) :
    K ⟶ internalPathObject X := curry ((β_ K Δ[1]).inv ≫ h)
```
Mentions: OAI.Thomason.Construction.internalPathObject
theorem OAI.Thomason.Construction.internalPathCylinder_transpose line 59
theorem OAI.Thomason.Construction.internalPathCylinder_injective line 64
theorem OAI.Thomason.Construction.internalPathStart_mono_lifting line 73
Source documentation
Initial evaluation lifts against every monomorphism when the target is Kan. This is proved directly by relative cylinder extension.
```
theorem internalPathStart_mono_lifting (X : SSet.{0}) [SSet.KanComplex X]
    {A B : SSet.{0}} (i : A ⟶ B) [Mono i] :
    HasLiftingProperty i (internalPathStart X) := by
…
```
Mentions: OAI.Thomason.Construction.internalPathStart
theorem OAI.Thomason.Construction.internalPathStart_boundary_rlp line 87
Source documentation
The internal path start map satisfies the actual boundary lifting class, not merely the Kan fibration class.
```
theorem internalPathStart_boundary_rlp (X : SSet.{0}) [SSet.KanComplex X] :
    I.rlp (internalPathStart X) := by
…
```
Mentions: OAI.Thomason.Construction.internalPathStart
theorem OAI.Thomason.Construction.internalPathStart_weak line 94
theorem OAI.Thomason.Construction.internalPathCylinder_postcomp line 99
theorem OAI.Thomason.Construction.internalPathStart_naturality line 109
theorem OAI.Thomason.Construction.internalPathMap_weak_iff line 120
Source documentation
Internal paths preserve and reflect the actual realization weak class between Kan targets. Both evaluation maps have already been proved to lift against every boundary.
```
theorem internalPathMap_weak_iff {X Y : SSet.{0}} [SSet.KanComplex X] [SSet.KanComplex Y]
    (f : X ⟶ Y) :
    realizationWeakEquivalences ((ihom (Δ[1] : SSet.{0})).map f) ↔
      realizationWeakEquivalences f := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.internalPathEnd line 153
theorem OAI.Thomason.Construction.internalPathCylinder_end line 157
def OAI.Thomason.Construction.internalPathEvaluationHomotopy line 173
Source documentation
The internal evaluation cylinder is an actual simplicial homotopy between its two evaluation maps.
```
def internalPathEvaluationHomotopy (X : SSet.{0}) :
    SSet.Homotopy (internalPathStart X) (internalPathEnd X) where
…
```
Mentions: OAI.Thomason.Construction.internalPathStart, OAI.Thomason.Construction.internalPathEnd
def OAI.Thomason.Construction.realizedInternalPathComparison line 187
Source documentation
Realizing the evaluation cylinder and currying gives the genuine compact-open path of every realized internal path.
```
def realizedInternalPathComparison (X : SSet.{0}) :
    SSet.toTop.obj (internalPathObject X) ⟶ continuousPathSpace (SSet.toTop.obj X) :=
…
```
Mentions: OAI.Thomason.Construction.internalPathObject, OAI.Thomason.Construction.continuousPathSpace
theorem OAI.Thomason.Construction.realizedInternalPathComparison_start line 192
theorem OAI.Thomason.Construction.realizedInternalPathComparison_weak line 203
Source documentation
For a Kan target this comparison is an actual weak homotopy equivalence. The proof uses the constructed boundary-lifting property of start evaluation, without the general acyclic-Kan implication.
```
theorem realizedInternalPathComparison_weak (X : SSet.{0}) [SSet.KanComplex X] :
    topologicalWeakEquivalences (realizedInternalPathComparison X) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedInternalPathComparison
theorem OAI.Thomason.Construction.realizedInternalPathComparison_apply line 212
theorem OAI.Thomason.Construction.realizedInternalPathComparison_naturality line 221
Source documentation
The realization/path comparison commutes with every simplicial target map, including the exact point and time coordinates.
```
theorem realizedInternalPathComparison_naturality {X Y : SSet.{0}} (f : X ⟶ Y) :
    SSet.toTop.map ((ihom (Δ[1] : SSet.{0})).map f) ≫ realizedInternalPathComparison Y =
      realizedInternalPathComparison X ≫ continuousPathMap (SSet.toTop.map f) := by
…
```
Mentions: OAI.Thomason.Construction.realizedInternalPathComparison, OAI.Thomason.Construction.continuousPathMap
def OAI.Thomason.Construction.internalPathConstant line 269
theorem OAI.Thomason.Construction.internalPathConstant_start line 272
theorem OAI.Thomason.Construction.internalPathConstant_end line 277
theorem OAI.Thomason.Construction.internalPathEnd_naturality line 282
theorem OAI.Thomason.Construction.internalPathConstant_naturality line 290
theorem OAI.Thomason.Construction.realizedInternalPathComparison_end line 304
def OAI.Thomason.Construction.internalPathMinMap line 328
Source documentation
Evaluate a path at the minimum of its parameter and the contraction time.
```
def internalPathMinMap (P : SSet.{0}) :
    (P ⊗ (Δ[1] : SSet.{0})) ⊗ Δ[1] ⟶ P ⊗ Δ[1] where
…
```
def OAI.Thomason.Construction.internalPathShrinkingMap line 348
Source documentation
Internal path shrinking is obtained by transposing the actual min map.
```
def internalPathShrinkingMap (X : SSet.{0}) :
    internalPathObject X ⊗ Δ[1] ⟶ internalPathObject X :=
…
```
Mentions: OAI.Thomason.Construction.internalPathObject
theorem OAI.Thomason.Construction.internalPathMinMap_zero line 353
theorem OAI.Thomason.Construction.internalPathMinMap_one line 368
def OAI.Thomason.Construction.internalPathContraction line 384
Source documentation
The internal path object contracts to its starting constant path in all simplicial sets. This fact requires no horn fillers.
```
def internalPathContraction (X : SSet.{0}) :
    SSet.Homotopy (internalPathStart X ≫ internalPathConstant X)
      (𝟙 (internalPathObject X)) where
…
```
Mentions: OAI.Thomason.Construction.internalPathStart, OAI.Thomason.Construction.internalPathConstant, OAI.Thomason.Construction.internalPathObject
theorem OAI.Thomason.Construction.internalPathShrinkingMap_start line 415
Source documentation
The contraction fixes the initial evaluation exactly throughout time.
```
theorem internalPathShrinkingMap_start (X : SSet.{0}) :
    internalPathShrinkingMap X ≫ internalPathStart X =
      fst (internalPathObject X) Δ[1] ≫ internalPathStart X := by
…
```
Mentions: OAI.Thomason.Construction.internalPathShrinkingMap, OAI.Thomason.Construction.internalPathStart, OAI.Thomason.Construction.internalPathObject
theorem OAI.Thomason.Construction.internalPathStart_weak_unconditional line 438
Source documentation
Starting evaluation is a realization weak equivalence for every simplicial set, independently of the stronger Kan boundary-lifting claim.
```
theorem internalPathStart_weak_unconditional (X : SSet.{0}) :
    realizationWeakEquivalences (internalPathStart X) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.internalPathStart
theorem OAI.Thomason.Construction.realizedInternalPathComparison_weak_unconditional line 450
Source documentation
The continuous free-path comparison is weak for arbitrary simplicial bases, including the non-Kan bases in the main construction.
```
theorem realizedInternalPathComparison_weak_unconditional (X : SSet.{0}) :
    topologicalWeakEquivalences (realizedInternalPathComparison X) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedInternalPathComparison
theorem OAI.Thomason.Construction.internalPathMinMap_naturality line 476
Source documentation
Minimum reparametrization commutes strictly with the parameter object.
```
theorem internalPathMinMap_naturality {P Q : SSet.{0}} (f : P ⟶ Q) :
    (f ▷ (Δ[1] : SSet.{0})) ▷ Δ[1] ≫ internalPathMinMap Q =
      internalPathMinMap P ≫ f ▷ Δ[1] := by
…
```
Mentions: OAI.Thomason.Construction.internalPathMinMap
theorem OAI.Thomason.Construction.internalPathShrinkingMap_constant line 487
Source documentation
The whole contraction fixes every constant internal path, with an arbitrary simplicial parameter.
```
theorem internalPathShrinkingMap_constant (X : SSet.{0}) :
    internalPathConstant X ▷ (Δ[1] : SSet.{0}) ≫ internalPathShrinkingMap X =
      fst X Δ[1] ≫ internalPathConstant X := by
…
```
Mentions: OAI.Thomason.Construction.internalPathConstant, OAI.Thomason.Construction.internalPathShrinkingMap
theorem OAI.Thomason.Construction.internalPathConstant_anodyne line 508
Source documentation
Constant paths form an anodyne subobject without any Kan condition on X; the proof is the stationary simplicial contraction itself.
```
theorem internalPathConstant_anodyne (X : SSet.{0}) :
    SSet.anodyneExtensions (internalPathConstant X) := by
…
```
Mentions: OAI.Thomason.Construction.internalPathConstant
abbrev OAI.Thomason.Construction.simplicialMappingPath line 533
abbrev OAI.Thomason.Construction.simplicialMappingPathRetraction line 536
def OAI.Thomason.Construction.simplicialMappingPathInclusion line 539
def OAI.Thomason.Construction.simplicialMappingPathProjection line 544
theorem OAI.Thomason.Construction.simplicialMappingPath_inclusion_retraction line 548
theorem OAI.Thomason.Construction.simplicialMappingPath_factorization line 553
theorem OAI.Thomason.Construction.simplicialMappingPath_retraction_lifting line 561
Source documentation
The retraction lifts against every mono: it is a base change of the constructed acyclic initial-evaluation map.
```
theorem simplicialMappingPath_retraction_lifting {X Y A B : SSet.{0}}
    (p : X ⟶ Y) [SSet.KanComplex Y] (i : A ⟶ B) [Mono i] :
    HasLiftingProperty i (simplicialMappingPathRetraction p) := by
…
```
Mentions: OAI.Thomason.Construction.simplicialMappingPathRetraction
theorem OAI.Thomason.Construction.simplicialMappingPath_retraction_boundary_rlp line 576
theorem OAI.Thomason.Construction.simplicialMappingPath_retraction_weak line 583
theorem OAI.Thomason.Construction.simplicialMappingPath_inclusion_weak line 588
theorem OAI.Thomason.Construction.simplicialMappingPath_projection_weak_iff line 595
theorem OAI.Thomason.Construction.simplicialMappingPath_projection_lifting line 610
Source documentation
A parameter anodyne extension lifts the endpoint projection whenever its map into the first factor extends. Both path ends are fixed exactly.
```
theorem simplicialMappingPath_projection_lifting {X Y A B : SSet.{0}}
    (p : X ⟶ Y) [SSet.KanComplex Y] (i : A ⟶ B) (hi : SSet.anodyneExtensions i)
    [HasLiftingProperty i (terminal.from X)] :
    HasLiftingProperty i (simplicialMappingPathProjection p) := by
…
```
Mentions: OAI.Thomason.Construction.simplicialMappingPathProjection
theorem OAI.Thomason.Construction.simplicialMappingPath_projection_fibration line 648
Source documentation
With Kan source and target, this is an actual Kan fibration.
```
theorem simplicialMappingPath_projection_fibration {X Y : SSet.{0}}
    (p : X ⟶ Y) [SSet.KanComplex X] [SSet.KanComplex Y] :
    HomotopicalAlgebra.Fibration (simplicialMappingPathProjection p) := by
…
```
Mentions: OAI.Thomason.Construction.simplicialMappingPathProjection
theorem OAI.Thomason.Construction.realizedMappingPath_start line 675
Source documentation
The continuous path attached to a point in the realized simplicial mapping-path object starts at the image of its first coordinate.
```
theorem realizedMappingPath_start {X Y : SSet.{0}} (p : X ⟶ Y) :
    SSet.toTop.map (pullback.snd p (internalPathStart Y)) ≫
        realizedInternalPathComparison Y ≫ continuousPathStart (SSet.toTop.obj Y) =
      SSet.toTop.map (simplicialMappingPathRetraction p) ≫ SSet.toTop.map p := by
…
```
Mentions: OAI.Thomason.Construction.internalPathStart, OAI.Thomason.Construction.realizedInternalPathComparison, OAI.Thomason.Construction.continuousPathStart, OAI.Thomason.Construction.simplicialMappingPathRetraction
def OAI.Thomason.Construction.realizedMappingPathComparison line 684
Source documentation
Realization of the actual simplicial pullback maps to the actual continuous mapping-path pullback, without asserting preservation of pullbacks.
```
def realizedMappingPathComparison {X Y : SSet.{0}} (p : X ⟶ Y) :
    SSet.toTop.obj (simplicialMappingPath p) ⟶ mappingPathSpace (SSet.toTop.map p) :=
…
```
Mentions: OAI.Thomason.Construction.simplicialMappingPath, OAI.Thomason.Construction.mappingPathSpace
theorem OAI.Thomason.Construction.realizedMappingPathComparison_retraction line 700
theorem OAI.Thomason.Construction.realizedMappingPathComparison_projection line 705
theorem OAI.Thomason.Construction.realizedMappingPathComparison_weak line 718
Source documentation
The comparison is an actual weak homotopy equivalence for every map into a Kan complex. Both retractions to the source have been proved weak, so no general realization/pullback or singular-counit theorem is required.
```
theorem realizedMappingPathComparison_weak {X Y : SSet.{0}} (p : X ⟶ Y)
    [SSet.KanComplex Y] : topologicalWeakEquivalences (realizedMappingPathComparison p) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedMappingPathComparison
def OAI.Thomason.Construction.simplicialMappingPathShrinkingMap line 745
Source documentation
Shrinking the path preserves its start, so it restricts to every mapping-path pullback, even when the base is not Kan.
```
def simplicialMappingPathShrinkingMap {X Y : SSet.{0}} (p : X ⟶ Y) :
    simplicialMappingPath p ⊗ Δ[1] ⟶ simplicialMappingPath p :=
…
```
Mentions: OAI.Thomason.Construction.simplicialMappingPath
theorem OAI.Thomason.Construction.simplicialMappingPathShrinkingMap_fst line 760
theorem OAI.Thomason.Construction.simplicialMappingPathShrinkingMap_snd line 766
theorem OAI.Thomason.Construction.path_iota_zero_naturality line 771
theorem OAI.Thomason.Construction.path_iota_one_naturality line 779
def OAI.Thomason.Construction.simplicialMappingPathContraction line 789
Source documentation
The pullback contraction is an actual simplicial homotopy from the inclusion followed by retraction to the identity, over the source.
```
def simplicialMappingPathContraction {X Y : SSet.{0}} (p : X ⟶ Y) :
    SSet.Homotopy (simplicialMappingPathRetraction p ≫ simplicialMappingPathInclusion p)
      (𝟙 (simplicialMappingPath p)) where
…
```
Mentions: OAI.Thomason.Construction.simplicialMappingPathRetraction, OAI.Thomason.Construction.simplicialMappingPathInclusion, OAI.Thomason.Construction.simplicialMappingPath
theorem OAI.Thomason.Construction.simplicialMappingPath_retraction_weak_unconditional line 827
Source documentation
The retraction is weak for every map, without requiring a Kan base.
```
theorem simplicialMappingPath_retraction_weak_unconditional {X Y : SSet.{0}} (p : X ⟶ Y) :
    realizationWeakEquivalences (simplicialMappingPathRetraction p) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplicialMappingPathRetraction
theorem OAI.Thomason.Construction.realizedMappingPathComparison_weak_unconditional line 840
Source documentation
The actual comparison with continuous mapping paths is weak over every simplicial base, and still commutes exactly with the original projection.
```
theorem realizedMappingPathComparison_weak_unconditional {X Y : SSet.{0}} (p : X ⟶ Y) :
    topologicalWeakEquivalences (realizedMappingPathComparison p) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedMappingPathComparison
theorem OAI.Thomason.Construction.simplicialMappingPathShrinkingMap_stationary line 867
Source documentation
Shrinking paths in a mapping-path object fixes the original source as an entire simplicial subobject, in every parameter degree.
```
theorem simplicialMappingPathShrinkingMap_stationary {X Y : SSet.{0}} (p : X ⟶ Y) :
    (simplicialMappingPathInclusion p) ▷ (Δ[1] : SSet.{0}) ≫
        simplicialMappingPathShrinkingMap p =
      fst X Δ[1] ≫ simplicialMappingPathInclusion p := by
…
```
Mentions: OAI.Thomason.Construction.simplicialMappingPathInclusion, OAI.Thomason.Construction.simplicialMappingPathShrinkingMap
theorem OAI.Thomason.Construction.simplicialMappingPathInclusion_anodyne line 883
Source documentation
The first map in the actual mapping-path factorization is always anodyne, not merely a realization weak equivalence.
```
theorem simplicialMappingPathInclusion_anodyne {X Y : SSet.{0}} (p : X ⟶ Y) :
    SSet.anodyneExtensions (simplicialMappingPathInclusion p) := by
…
```
Mentions: OAI.Thomason.Construction.simplicialMappingPathInclusion
theorem OAI.Thomason.Construction.simplicialMappingPath_projection_weak_iff_unconditional line 893
Source documentation
The endpoint projection has exactly the weak-equivalence status of the original map over arbitrary simplicial bases.
```
theorem simplicialMappingPath_projection_weak_iff_unconditional {X Y : SSet.{0}}
    (p : X ⟶ Y) :
    realizationWeakEquivalences (simplicialMappingPathProjection p) ↔
      realizationWeakEquivalences p := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.simplicialMappingPathProjection
def OAI.Thomason.Construction.RealizedCube.insertEndpoint line 923
Source documentation
The continuous insertion of one endpoint coordinate.
```
def insertEndpoint (n : ℕ) (i : Fin (n+1)) (e : Bool) :
    C((Fin n → unitInterval), Fin (n+1) → unitInterval) :=
…
```
theorem OAI.Thomason.Construction.RealizedCube.singularMap_face_naturality line 935
Source documentation
Restriction of a singular cube agrees with the singular cube of the restricted map.
```
theorem singularMap_face_naturality {X : TopCat.{0}} (n : ℕ)
    (p : C((Fin (n+1) → unitInterval), X)) (i : Fin (n+1)) (e : Bool) :
    face n i e ≫ singularMap (n+1) p = singularMap n (p.comp (insertEndpoint n i e)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.face, OAI.Thomason.Construction.RealizedCube.singularMap, OAI.Thomason.Construction.RealizedCube.insertEndpoint

def OAI.Thomason.Construction.RealizedCube.liftMap line 948

Source documentation

The realized cubical lift of a continuous map.

def liftMap {X : TopCat.{0}} (n : ℕ) (p : C((Fin n → unitInterval), X)) :
    C((Fin n → unitInterval), SSet.toTop.obj (TopCat.toSSet.obj X)) :=
…

theorem OAI.Thomason.Construction.RealizedCube.liftMap_face line 953
Source documentation
The continuous lift also commutes exactly with every cubical face.
```
theorem liftMap_face {X : TopCat.{0}} (n : ℕ)
    (p : C((Fin (n+1) → unitInterval), X)) (i : Fin (n+1)) (e : Bool)
    (t : Fin n → unitInterval) :
    liftMap (n+1) p (Fin.insertNth i (endpoint e) t) =
      liftMap n (p.comp (insertEndpoint n i e)) t := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.liftMap, OAI.Thomason.Construction.RealizedCube.endpoint, OAI.Thomason.Construction.RealizedCube.insertEndpoint
theorem OAI.Thomason.Construction.RealizedCube.liftMap_const line 966
Source documentation
A constant topological cube has the constant lift at its singular vertex.
```
theorem liftMap_const (X : TopCat.{0}) (n : ℕ) (x : X) (t : Fin n → unitInterval) :
    liftMap n (ContinuousMap.const _ x) t = singularVertex X x := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.liftMap, OAI.Thomason.Construction.singularVertex