SingularKanComplex.lean`

76 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite vertex-star control for maps from cubes

theorem OAI.Thomason.Construction.RealizationPrism.cube_grid_vertexStar_refinement line 27
Source documentation
Any continuous cube in a realization admits a finite closed grid whose individual cell images lie in individual vertex stars.
```
theorem cube_grid_vertexStar_refinement (K : SSet.{0}) (n : ℕ)
    (f : C((Fin n → unitInterval), SSet.toTop.obj K)) :
    ∃ m : ℕ, ∀ k : Fin n → Fin (m+1), ∃ v : K.obj (.op (.mk 0)),
      ∀ x ∈ CubeGrid.cell n m k, f x ∈ vertexStar K v := by
…
```
Mentions: OAI.Thomason.Construction.CubeGrid.cell, OAI.Thomason.Construction.RealizationPrism.vertexStar

theorem OAI.Thomason.Construction.RealizationPrism.cube_grid_supported_vertex line 45

Source documentation

The selected star controls positive support in every simplex representation of every image point, including degenerate ones.

theorem cube_grid_supported_vertex (K : SSet.{0}) (n : ℕ)
    (f : C((Fin n → unitInterval), SSet.toTop.obj K)) :
    ∃ m : ℕ, ∀ k : Fin n → Fin (m+1), ∃ v : K.obj (.op (.mk 0)),
      ∀ x ∈ CubeGrid.cell n m k, ∀ (d : ℕ) (s : K.obj (.op (.mk d)))
        (p : StdSimplex ℝ (Fin (d+1))), simplexPoint K s p = f x →
          ∃ i, 0 < p.weights i ∧ simplexVertex K s i = v := by
…

Mentions: OAI.Thomason.Construction.CubeGrid.cell, OAI.Thomason.Construction.RealizationPrism.simplexPoint, OAI.Thomason.Construction.RealizationPrism.simplexVertex

def OAI.Thomason.Construction.realizationProductComparison line 76
Source documentation
The canonical comparison uses the two actual realized projections.
```
def realizationProductComparison (X Y : SSet.{0}) :
    SSet.toTop.obj (X ⊗ Y) ⟶ TopCat.of (SSet.toTop.obj X × SSet.toTop.obj Y) :=
…
```

def OAI.Thomason.Construction.realizationProductRightMap line 84

Source documentation

The right-factor map on the product of actual realizations.

def realizationProductRightMap (X : SSet.{0}) {Y Z : SSet.{0}} (f : Y ⟶ Z) :
    TopCat.of (SSet.toTop.obj X × SSet.toTop.obj Y) ⟶
      TopCat.of (SSet.toTop.obj X × SSet.toTop.obj Z) :=
…

theorem OAI.Thomason.Construction.realizationProductComparison_naturality_right line 92
Source documentation
The canonical product comparison is natural in its right factor.
```
theorem realizationProductComparison_naturality_right (X : SSet.{0})
    {Y Z : SSet.{0}} (f : Y ⟶ Z) :
    SSet.toTop.map (X ◁ f) ≫ realizationProductComparison X Z =
      realizationProductComparison X Y ≫ realizationProductRightMap X f := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.realizationProductRightMap
theorem OAI.Thomason.Construction.realizationProductRightMap_comp line 107
theorem OAI.Thomason.Construction.realizationProductRightMap_id line 118
theorem OAI.Thomason.Construction.realizationProductComparison_isIso_of_retract line 129
Source documentation
If the product comparison is an isomorphism for a larger factor, it is also an isomorphism for any specified simplicial retract.
```
theorem realizationProductComparison_isIso_of_retract (X : SSet.{0})
    {Y Z : SSet.{0}} (i : Y ⟶ Z) (r : Z ⟶ Y) (hir : i ≫ r = 𝟙 Y)
    [IsIso (realizationProductComparison X Z)] :
    IsIso (realizationProductComparison X Y) := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison
theorem OAI.Thomason.Construction.RealizedCube.section_coordinates line 165
Source documentation
The actual cubical section is also a right inverse, in every dimension.
```
theorem section_coordinates (n : ℕ) (x : SSet.toTop.obj (obj n)) :
    sectionMap n (coordinates n x) = x := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.RealizedCube.sectionMap, OAI.Thomason.Construction.RealizedCube.coordinates
def OAI.Thomason.Construction.RealizedCube.cubeHomeomorph line 180
Source documentation
A finite simplicial cube realizes to the ordinary topological cube, with the original constructed cubical section as its inverse coordinates.
```
def cubeHomeomorph (n : ℕ) :
    (Fin n → unitInterval) ≃ₜ SSet.toTop.obj (obj n) where
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.boundarySection_coordinates line 191
Source documentation
The section identifies the entire topological boundary with the actual realization of the simplicial boundary, not merely a retract of it.
```
theorem boundarySection_coordinates (n : ℕ)
    (x : SSet.toTop.obj (boundary n : SSet.{0})) :
    boundarySection n (boundaryCoordinates n x) = x := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.boundary, OAI.Thomason.Construction.RealizedCube.boundarySection, OAI.Thomason.Construction.RealizedCube.boundaryCoordinates
def OAI.Thomason.Construction.RealizedCube.boundaryHomeomorph line 199
Source documentation
The exact boundary homeomorphism is compatible with the ambient cube.
```
def boundaryHomeomorph (n : ℕ) :
    Cube.boundary (Fin (n+1)) ≃ₜ SSet.toTop.obj (boundary n : SSet.{0}) where
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.boundary
def OAI.Thomason.Construction.RealizedCube.boundaryArrowIso line 209
Source documentation
An isomorphism of the complete boundary-inclusion arrows.
```
def boundaryArrowIso (n : ℕ) :
    Arrow.mk (boundaryInclusion n) ≅ Arrow.mk (SSet.toTop.map (boundary n).ι) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.boundaryInclusion, OAI.Thomason.Construction.RealizedCube.boundary
theorem OAI.Thomason.Construction.RealizedCube.boundary_lifting_iff line 220
Source documentation
Ordinary cube-boundary lifting and lifting of the corresponding realized simplicial boundary are exactly equivalent.
```
theorem boundary_lifting_iff {X Y : TopCat.{0}} (p : X ⟶ Y) (n : ℕ) :
    HasLiftingProperty (boundaryInclusion n) p ↔
      HasLiftingProperty (SSet.toTop.map (boundary n).ι) p :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.boundaryInclusion, OAI.Thomason.Construction.RealizedCube.boundary
def OAI.Thomason.Construction.realizationCubeProductHomeomorph line 244
Source documentation
Iterated cylinder coordinates give an actual product homeomorphism when the right simplicial factor is a finite cube.
```
def realizationCubeProductHomeomorph (X : SSet.{0}) (n : ℕ) :
    SSet.toTop.obj (X ⊗ RealizedCube.obj n) ≃ₜ
      (SSet.toTop.obj X × SSet.toTop.obj (RealizedCube.obj n)) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.realizationCubeProductHomeomorph_fst line 259
Source documentation
The homeomorphism's first coordinate is the actual realized projection.
```
theorem realizationCubeProductHomeomorph_fst (X : SSet.{0}) (n : ℕ)
    (z : SSet.toTop.obj (X ⊗ RealizedCube.obj n)) :
    (realizationCubeProductHomeomorph X n z).1 =
      (SSet.toTop.map (fst X (RealizedCube.obj n))).hom z := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationCubeProductHomeomorph
theorem OAI.Thomason.Construction.realizationCubeProductHomeomorph_snd line 281
Source documentation
Its second coordinate is likewise the actual projection, so the homeomorphism is exactly the canonical comparison.
```
theorem realizationCubeProductHomeomorph_snd (X : SSet.{0}) (n : ℕ)
    (z : SSet.toTop.obj (X ⊗ RealizedCube.obj n)) :
    (realizationCubeProductHomeomorph X n z).2 =
      (SSet.toTop.map (snd X (RealizedCube.obj n))).hom z := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationCubeProductHomeomorph
theorem OAI.Thomason.Construction.realizationProductComparison_cube_isIso line 320
Source documentation
The canonical realization comparison for products with finite cubes is an isomorphism of topological spaces.
```
theorem realizationProductComparison_cube_isIso (X : SSet.{0}) (n : ℕ) :
    IsIso (realizationProductComparison X (RealizedCube.obj n)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.RealizedCube.obj
def OAI.Thomason.Construction.realizationCubeProductIso line 333
Source documentation
The canonical cube product comparison as an explicit isomorphism.
```
def realizationCubeProductIso (X : SSet.{0}) (n : ℕ) :
    SSet.toTop.obj (X ⊗ RealizedCube.obj n) ≅
      TopCat.of (SSet.toTop.obj X × SSet.toTop.obj (RealizedCube.obj n)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.realizationProductComparison_simplex_isIso line 341
Source documentation
The actual canonical comparison for an arbitrary simplicial set and a standard simplex is a homeomorphism, by its explicit cube retraction.
```
theorem realizationProductComparison_simplex_isIso (X : SSet.{0}) (n : ℕ) :
    IsIso (realizationProductComparison X (Δ[n] : SSet.{0})) := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison

def OAI.Thomason.Construction.realizationSimplexProductHomeomorph line 348

Source documentation

Product realization with a simplex, with the actual two projections.

def realizationSimplexProductHomeomorph (X : SSet.{0}) (n : ℕ) :
    SSet.toTop.obj (X ⊗ (Δ[n] : SSet.{0})) ≃ₜ
      (SSet.toTop.obj X × SSet.toTop.obj (Δ[n] : SSet.{0})) := by
…

theorem OAI.Thomason.Construction.realizationProductComparison_naturality_left line 372

Source documentation

The canonical comparison is natural also in its first factor.

theorem realizationProductComparison_naturality_left {X X' : SSet.{0}}
    (f : X ⟶ X') (Y : SSet.{0}) :
    SSet.toTop.map (f ▷ Y) ≫ realizationProductComparison X' Y =
      realizationProductComparison X Y ≫ (SSet.toTop.map f ▷ SSet.toTop.obj Y) := by
…

Mentions: OAI.Thomason.Construction.realizationProductComparison

def OAI.Thomason.Construction.realizationProductRightComparison line 388
Source documentation
Regard the actual product comparison as a map of colimit diagrams.
```
def realizationProductRightComparison (Y : SSet.{0}) :
    tensorRight Y ⋙ SSet.toTop ⟶ SSet.toTop ⋙ tensorRight (SSet.toTop.obj Y) where
…
```
theorem OAI.Thomason.Construction.realizationProductComparison_simplex_left_isIso line 395
Source documentation
Symmetry reduces a standard simplex in the left factor to the already constructed right-simplex product homeomorphism.
```
theorem realizationProductComparison_simplex_left_isIso (n : ℕ) (Y : SSet.{0}) :
    IsIso (realizationProductComparison (Δ[n] : SSet.{0}) Y) := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison
theorem OAI.Thomason.Construction.realizationProductComparison_isIso_of_locallyCompact line 427
Source documentation
A locally compact realization in the fixed factor lets the comparison pass from standard simplices to the actual simplex colimit.
```
theorem realizationProductComparison_isIso_of_locallyCompact (X Y : SSet.{0})
    [LocallyCompactSpace (SSet.toTop.obj Y)] :
    IsIso (realizationProductComparison X Y) := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison
theorem OAI.Thomason.Construction.realizationProductComparison_finite_isIso line 441
Source documentation
Every finite simplicial parameter has a compact Hausdorff realization, so its product with any actual realization has the canonical topology.
```
theorem realizationProductComparison_finite_isIso (X Y : SSet.{0}) [Y.Finite] :
    IsIso (realizationProductComparison X Y) := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison
def OAI.Thomason.Construction.realizationFiniteProductHomeomorph line 449
Source documentation
The homeomorphism for finite parameter spaces retains both actual realized projections, by construction from the canonical comparison.
```
def realizationFiniteProductHomeomorph (X Y : SSet.{0}) [Y.Finite] :
    SSet.toTop.obj (X ⊗ Y) ≃ₜ (SSet.toTop.obj X × SSet.toTop.obj Y) := by
…
```
def OAI.Thomason.Construction.productSubcomplexIso line 473
Source documentation
A product with a subcomplex is exactly the inverse image under the second simplicial projection, including all degenerate simplices.
```
def productSubcomplexIso (X Y : SSet.{0}) (A : Y.Subcomplex) :
    X ⊗ A.toSSet ≅ (A.preimage (snd X Y)).toSSet where
…
```
theorem OAI.Thomason.Construction.productSubcomplexIso_hom_ι line 484
def OAI.Thomason.Construction.productSubspaceHomeomorph line 489
Source documentation
The subspace selected by the second coordinate is the ordinary product with the selected subspace.
```
def productSubspaceHomeomorph (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y]
    (A : Set Y) : {z : X × Y // z.2 ∈ A} ≃ₜ (X × A) where
…
```
def OAI.Thomason.Construction.realizationProductSubcomplexHomeomorph line 500
Source documentation
Any established product comparison restricts to an actual product homeomorphism on every subcomplex of its right factor.
```
def realizationProductSubcomplexHomeomorph (X Y : SSet.{0}) (A : Y.Subcomplex)
    [IsIso (realizationProductComparison X Y)] :
    SSet.toTop.obj (X ⊗ A.toSSet) ≃ₜ
      (SSet.toTop.obj X × SSet.toTop.obj A.toSSet) :=
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison
theorem OAI.Thomason.Construction.realizationProductSubcomplexHomeomorph_fst line 514
Source documentation
Its first coordinate is the original realized projection.
```
theorem realizationProductSubcomplexHomeomorph_fst (X Y : SSet.{0}) (A : Y.Subcomplex)
    [IsIso (realizationProductComparison X Y)] (z : SSet.toTop.obj (X ⊗ A.toSSet)) :
    (realizationProductSubcomplexHomeomorph X Y A z).1 =
      (SSet.toTop.map (fst X A.toSSet)).hom z := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.realizationProductSubcomplexHomeomorph
theorem OAI.Thomason.Construction.realizationProductSubcomplexHomeomorph_snd line 527
Source documentation
Its second coordinate retains the entire subcomplex point.
```
theorem realizationProductSubcomplexHomeomorph_snd (X Y : SSet.{0}) (A : Y.Subcomplex)
    [IsIso (realizationProductComparison X Y)] (z : SSet.toTop.obj (X ⊗ A.toSSet)) :
    (realizationProductSubcomplexHomeomorph X Y A z).2 =
      (SSet.toTop.map (snd X A.toSSet)).hom z := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.realizationProductSubcomplexHomeomorph
theorem OAI.Thomason.Construction.realizationProductComparison_subcomplex_isIso line 545
Source documentation
The homeomorphism just constructed is the canonical product comparison.
```
theorem realizationProductComparison_subcomplex_isIso (X Y : SSet.{0}) (A : Y.Subcomplex)
    [IsIso (realizationProductComparison X Y)] :
    IsIso (realizationProductComparison X A.toSSet) := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison
theorem OAI.Thomason.Construction.realizationProductComparison_boundary_isIso line 559
Source documentation
In particular the complete simplex boundary satisfies product realization.
```
theorem realizationProductComparison_boundary_isIso (X : SSet.{0}) (n : ℕ) :
    IsIso (realizationProductComparison X (SSet.boundary n).toSSet) := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison
theorem OAI.Thomason.Construction.realizationProductComparison_cubeBoundary_isIso line 565
Source documentation
The complete finite cube boundary satisfies the same exact comparison.
```
theorem realizationProductComparison_cubeBoundary_isIso (X : SSet.{0}) (n : ℕ) :
    IsIso (realizationProductComparison X (RealizedCube.boundary n).toSSet) := by
…
```
Mentions: OAI.Thomason.Construction.realizationProductComparison, OAI.Thomason.Construction.RealizedCube.boundary
structure OAI.Thomason.Construction.TopologicalDeformation.ScheduledData line 592
Source documentation
A deformation toward a retract which waits until time a.
```
structure ScheduledData {A B : TopCat.{0}} (i : A ⟶ B) (a : ℝ) where
…
```
def OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.toData line 601
Source documentation
Forgetting the schedule gives ordinary stationary deformation data.
```
def ScheduledData.toData (d : ScheduledData i a) : Data i where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.ScheduledData, OAI.Thomason.Construction.TopologicalDeformation.Data
def OAI.Thomason.Construction.TopologicalDeformation.scheduledIdentity line 607
Source documentation
The identity can wait for the entire interval.
```
def scheduledIdentity (A : TopCat.{0}) : ScheduledData (𝟙 A) 1 where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.ScheduledData
def OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.early line 614
Source documentation
The attaching deformation is completed during [a/2,a].
```
def ScheduledData.early (_d : ScheduledData i a) (e : Data j) : C(unitInterval × C, C) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.ScheduledData, OAI.Thomason.Construction.TopologicalDeformation.Data
def OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.late line 619
Source documentation
The later part is the old deformation, with its original time parameter.
```
def ScheduledData.late (d : ScheduledData i a) (e : Data j) : C(unitInterval × C, C) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.ScheduledData, OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.early_at_cut line 623
theorem OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.early_idle line 631
def OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.stepTrack line 637
Source documentation
Join the new deformation to the old one at their common stationary value.
```
def ScheduledData.stepTrack (d : ScheduledData i a) (e : Data j) (ha : 0 < a) :
    C(unitInterval × C, C) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.ScheduledData, OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.stepTrack_low line 649
theorem OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.stepTrack_high line 653
theorem OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.early_stationary line 681
Source documentation
Even outside the original time interval, the extended track fixes the retract.
```
theorem ScheduledData.early_stationary (d : ScheduledData i a) (e : Data j)
    (t : unitInterval) (x : B) : d.early e (t, j.hom x) = j.hom x := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.ScheduledData, OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.stepTrack_compatible line 687
Source documentation
The new track restricts to the previous track with exactly the same time.
```
theorem ScheduledData.stepTrack_compatible (d : ScheduledData i a) (e : Data j)
    (ha : 0 < a) (t : unitInterval) (x : B) :
    d.stepTrack e ha (t, j.hom x) = j.hom (d.homotopy (t, x)) := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.ScheduledData, OAI.Thomason.Construction.TopologicalDeformation.Data
def OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.step line 698
Source documentation
Extend a scheduled deformation across one additional stationary retract.
```
def ScheduledData.step (d : ScheduledData i a) (e : Data j)
    (ha : 0 < a) (ha' : a ≤ 1) : ScheduledData (i ≫ j) (a/2) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.ScheduledData, OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.TopologicalDeformation.ScheduledData.step_retraction line 728
Source documentation
Retractions also agree on the earlier stage.
```
theorem ScheduledData.step_retraction (d : ScheduledData i a) (e : Data j)
    (ha : 0 < a) (ha' : a ≤ 1) :
    j ≫ (d.step e ha ha').retraction = d.retraction := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.ScheduledData, OAI.Thomason.Construction.TopologicalDeformation.Data
def OAI.Thomason.Construction.TopologicalDeformation.Sequential.delay line 753
Source documentation
The time reserved for subsequent attaching deformations.
```
def delay : ℕ → ℝ
  | 0 => 1
  | n+1 => delay n / 2
```
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.delay_pos line 757
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.delay_le_one line 762
abbrev OAI.Thomason.Construction.TopologicalDeformation.Sequential.next line 770
Source documentation
The actual successor map of the diagram.
```
abbrev next (n : ℕ) := X.map (homOfLE (Nat.le_succ n))
```
def OAI.Thomason.Construction.TopologicalDeformation.Sequential.initial line 773
Source documentation
The inclusion of stage zero, written recursively for the deformation construction.
```
def initial : (n : ℕ) → (X.obj 0 ⟶ X.obj n)
  | 0 => 𝟙 _
  | n+1 => initial n ≫ next X n

variable (d : ∀ n, Data (next X n))

/-- A compatible deformation at every finite stage. -/
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Sequential.next, OAI.Thomason.Construction.TopologicalDeformation.Data
def OAI.Thomason.Construction.TopologicalDeformation.Sequential.stage line 780
Source documentation
A compatible deformation at every finite stage.
```
def stage : (n : ℕ) → ScheduledData (initial X n) (delay n)
  | 0 => scheduledIdentity (X.obj 0)
  | n+1 => (stage n).step (d n) (delay_pos n) (delay_le_one n)

@[reassoc]
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.ScheduledData, OAI.Thomason.Construction.TopologicalDeformation.Sequential.initial, OAI.Thomason.Construction.TopologicalDeformation.Sequential.delay, OAI.Thomason.Construction.TopologicalDeformation.scheduledIdentity, OAI.Thomason.Construction.TopologicalDeformation.Sequential.delay_pos, OAI.Thomason.Construction.TopologicalDeformation.Sequential.delay_le_one
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.stage_retraction line 785
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.stage_compatible line 789
def OAI.Thomason.Construction.TopologicalDeformation.Sequential.retractCocone line 795
Source documentation
Retractions form a cocone to the initial stage.
```
def retractCocone : Cocone X where
…
```
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.initial_leg line 806
def OAI.Thomason.Construction.TopologicalDeformation.Sequential.trackLeg line 817
Source documentation
Finite tracks mapped into the actual colimit cocone.
```
def trackLeg (n : ℕ) : TopologicalInterval.cylinder.obj (X.obj n) ⟶ c.pt :=
…
```
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.trackLeg_next line 822
def OAI.Thomason.Construction.TopologicalDeformation.Sequential.trackCocone line 833
Source documentation
Tracks form a cocone after product with the interval.
```
def trackCocone : Cocone (X ⋙ TopologicalInterval.cylinder) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalInterval.cylinder
def OAI.Thomason.Construction.TopologicalDeformation.Sequential.retraction line 869
Source documentation
The compatible stage retractions descend to the colimit.
```
def retraction : c.pt ⟶ X.obj 0 := hc.desc (retractCocone X d)
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Sequential.retractCocone
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.retraction_fac line 872
def OAI.Thomason.Construction.TopologicalDeformation.Sequential.track line 877
Source documentation
Product with the interval preserves the colimit used to assemble the tracks.
```
def track : TopologicalInterval.cylinder.obj c.pt ⟶ c.pt :=
…
```
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.track_fac line 881
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.retraction_left line 885
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.track_zero line 889
Source documentation
The assembled track starts at the identity.
```
theorem track_zero : TopologicalInterval.sectionAt c.pt 0 ≫ track hc d = 𝟙 c.pt := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.TopologicalDeformation.Sequential.track
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.track_one line 900
Source documentation
At the end, every stage has been retracted to stage zero.
```
theorem track_one :
    TopologicalInterval.sectionAt c.pt 1 ≫ track hc d = retraction hc d ≫ c.ι.app 0 := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.TopologicalDeformation.Sequential.track, OAI.Thomason.Construction.TopologicalDeformation.Sequential.retraction
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.track_stationary line 917
Source documentation
The initial stage is fixed throughout the assembled deformation.
```
theorem track_stationary (t : unitInterval) (x : X.obj 0) :
    (track hc d).hom ((c.ι.app 0).hom x, t) = (c.ι.app 0).hom x := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Sequential.track
def OAI.Thomason.Construction.TopologicalDeformation.Sequential.colimitData line 923
Source documentation
A countable composite of stationary deformation inclusions is again one.
```
def colimitData : Data (c.ι.app 0) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.TopologicalDeformation.Sequential.colimit_weak line 939
Source documentation
The actual homotopy-group test for the countable colimit inclusion.
```
theorem colimit_weak : topologicalWeakEquivalences (c.ι.app 0) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences

def OAI.Thomason.Construction.singularHornFiller line 967

Source documentation

An explicit filler of any horn in the singular simplicial set.

def singularHornFiller (X : TopCat.{0}) {n : ℕ} (i : Fin (n+2))
    (f : (Λ[n+1, i] : SSet.{0}) ⟶ TopCat.toSSet.obj X) :
    (Δ[n+1] : SSet.{0}) ⟶ TopCat.toSSet.obj X :=
…

theorem OAI.Thomason.Construction.singularHornFiller_fac line 974
theorem OAI.Thomason.Construction.singular_kan line 982
Source documentation
Singular simplicial sets satisfy the genuine horn-filling condition.
```
theorem singular_kan (X : TopCat.{0}) : SSet.KanComplex (TopCat.toSSet.obj X) := by
…
```