SimplicialHomotopyWhiskering.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The carrier of a realized ordered homotopy

An ordered simplicial prism chooses an endpoint image at every vertex. Its realized support is therefore contained in the union of the two endpoint supports at the original parameter point.

theorem OAI.Thomason.Construction.PosetGeometry.homotopy_support_of_vertex_choices line 25
theorem OAI.Thomason.Construction.PosetGeometry.orderedVertexHomotopy_support line 73
theorem OAI.Thomason.Construction.PosetGeometry.orderNerveHomotopy_support line 89
theorem OAI.Thomason.Construction.PosetGeometry.orderedVertexHomotopy_naturality line 121

def OAI.Thomason.Construction.whiskerSimplicialHomotopy line 164

Source documentation

Pre- and postcompose an actual simplicial homotopy.

def whiskerSimplicialHomotopy {A X Y B : SSet.{0}} (a : A ⟶ X) {f g : X ⟶ Y}
    (H : SSet.Homotopy f g) (b : Y ⟶ B) :
    SSet.Homotopy (a ≫ f ≫ b) (a ≫ g ≫ b) where
…

theorem OAI.Thomason.Construction.kan_extension_of_boundary_homotopy_reverse line 195
Source documentation
Kan cylinder lifting works also when the prescribed total-space map is the final endpoint. It makes a boundary homotopy exact at its start.
```
theorem kan_extension_of_boundary_homotopy_reverse {A K X : SSet.{0}}
    [SSet.KanComplex X] (i : A ⟶ K) [Mono i] (a : A ⟶ X) (d : K ⟶ X)
    (H : SSet.Homotopy a (i ≫ d)) :
    ∃ l : K ⟶ X, i ≫ l = a := by
…
```

theorem OAI.Thomason.Construction.kan_extension_iff_of_boundary_homotopy line 212

Source documentation

Solvability of an exact extension problem in a Kan target is unchanged by an actual simplicial homotopy of its prescribed boundary map.

theorem kan_extension_iff_of_boundary_homotopy {A K X : SSet.{0}}
    [SSet.KanComplex X] (i : A ⟶ K) [Mono i] {a b : A ⟶ X}
    (H : SSet.Homotopy a b) :
    (∃ d : K ⟶ X, i ≫ d = a) ↔ (∃ d : K ⟶ X, i ≫ d = b) := by
…

theorem OAI.Thomason.Construction.kan_extension_iff_of_homotopy_left_inverse line 228

Source documentation

A map with a simplicial homotopy left inverse preserves and reflects all exact monomorphic extension problems in a Kan source.

theorem kan_extension_iff_of_homotopy_left_inverse {A K X Y : SSet.{0}}
    [SSet.KanComplex X] (i : A ⟶ K) [Mono i] (a : A ⟶ X)
    (f : X ⟶ Y) (g : Y ⟶ X) (H : SSet.Homotopy (𝟙 X) (f ≫ g)) :
    (∃ d : K ⟶ X, i ≫ d = a) ↔ (∃ d : K ⟶ Y, i ≫ d = a ≫ f) := by
…