HornAttachmentWeakEquivalences.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

The simplicial gluing input, derived from Kan–Quillen

A Brown factorization in the one span shape reduces arbitrary objectwise weak equivalences to the acyclic relative cofibrations proved above. The only published hypothesis is the explicitly stated Kan–Quillen input.

def OAI.Thomason.Construction.SimplicialSpan.ObjectwiseWeak line 22
Source documentation
Weak equivalence at the three objects of this span.
```
def ObjectwiseWeak {X Y : Diagram} (f : X ⟶ Y) : Prop :=
…
```
Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram
theorem OAI.Thomason.Construction.SimplicialSpan.ObjectwiseWeak.of_comp line 26
theorem OAI.Thomason.Construction.SimplicialSpan.pushoutMap_weak line 36
Source documentation
Actual realization weak equivalences are preserved by the pushout functor on spans whose specified left legs are monomorphisms.
```
theorem pushoutMap_weak {X Y : Diagram} (f : X ⟶ Y)
    [Mono X.left] [Mono Y.left] (kq : KanQuillenPublishedInput.{0})
    (hf : ObjectwiseWeak f) : realizationWeakEquivalences (pushoutMap f) := by
…
```
Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram, OAI.Thomason.Construction.SimplicialSpan.ObjectwiseWeak, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.SimplicialSpan.pushoutMap
theorem OAI.Thomason.Construction.constructedSimplicialGluing line 81
Source documentation
The classical gluing specialization used by the strict-category proof follows from the Kan–Quillen model axioms.
```
theorem constructedSimplicialGluing (kq : KanQuillenPublishedInput.{0}) :
    PublishedSimplicialGluingInput where
…
```
Mentions: OAI.Thomason.Construction.PublishedSimplicialGluingInput
structure OAI.Thomason.Construction.TopologicalDeformation.Data line 116
Source documentation
The precise deformation data needed for a horn attachment.
```
structure Data {A B : TopCat.{0}} (i : A ⟶ B) where
…
```
def OAI.Thomason.Construction.TopologicalDeformation.Data.track line 122
Source documentation
A homotopy with its time coordinate in the cylinder's second factor.
```
def Data.track {A B : TopCat.{0}} {i : A ⟶ B} (d : Data i) :
    TopologicalInterval.cylinder.obj B ⟶ B :=
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.TopologicalDeformation.Data.track_zero line 128
theorem OAI.Thomason.Construction.TopologicalDeformation.Data.track_one line 136
theorem OAI.Thomason.Construction.TopologicalDeformation.Data.track_stationary line 144
Source documentation
The full track is stationary on the attaching subspace.
```
theorem Data.track_stationary {A B : TopCat.{0}} {i : A ⟶ B} (d : Data i) :
    TopologicalInterval.cylinder.map i ≫ d.track = TopologicalInterval.projection A ≫ i := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data, OAI.Thomason.Construction.TopologicalInterval.projection
def OAI.Thomason.Construction.TopologicalDeformation.pushoutRetraction line 159
Source documentation
Retraction on the actual pushout.
```
def pushoutRetraction (h : IsPushout i f b j) (d : Data i) : P ⟶ X :=
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.TopologicalDeformation.pushoutRetraction_left line 162
theorem OAI.Thomason.Construction.TopologicalDeformation.track_compatible line 165
def OAI.Thomason.Construction.TopologicalDeformation.pushoutTrack line 172
Source documentation
Gluing the relative track uses preservation of pushouts by product with I.
```
def pushoutTrack (h : IsPushout i f b j) (d : Data i) :
    TopologicalInterval.cylinder.obj P ⟶ P :=
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.TopologicalDeformation.pushoutTrack_inl line 178
theorem OAI.Thomason.Construction.TopologicalDeformation.pushoutTrack_inr line 183
theorem OAI.Thomason.Construction.TopologicalDeformation.pushoutRetraction_inl line 189
theorem OAI.Thomason.Construction.TopologicalDeformation.section_naturality line 192
theorem OAI.Thomason.Construction.TopologicalDeformation.pushoutTrack_zero line 197
Source documentation
The glued track starts at the retraction followed by the inclusion.
```
theorem pushoutTrack_zero (h : IsPushout i f b j) (d : Data i) :
    TopologicalInterval.sectionAt P 0 ≫ pushoutTrack h d = pushoutRetraction h d ≫ j := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data, OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.TopologicalDeformation.pushoutTrack, OAI.Thomason.Construction.TopologicalDeformation.pushoutRetraction
theorem OAI.Thomason.Construction.TopologicalDeformation.pushoutTrack_one line 220
Source documentation
The glued track ends at the identity of the pushout.
```
theorem pushoutTrack_one (h : IsPushout i f b j) (d : Data i) :
    TopologicalInterval.sectionAt P 1 ≫ pushoutTrack h d = 𝟙 P := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data, OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.TopologicalDeformation.pushoutTrack
def OAI.Thomason.Construction.TopologicalDeformation.pushoutData line 240
Source documentation
The pushout of a stationary deformation is itself a stationary deformation.
```
def pushoutData (h : IsPushout i f b j) (d : Data i) : Data j where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data
theorem OAI.Thomason.Construction.TopologicalDeformation.pushout_weak line 256
Source documentation
The weak test for the pushout follows directly from the glued deformation.
```
theorem pushout_weak (h : IsPushout i f b j) (d : Data i) :
    topologicalWeakEquivalences j := by
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data, OAI.Thomason.Construction.topologicalWeakEquivalences
def OAI.Thomason.Construction.realizedHornData line 285
Source documentation
The constructed strong deformation data for a realized horn inclusion.
```
def realizedHornData {n : ℕ} (i : Fin (n+2)) :
    TopologicalDeformation.Data (SSet.toTop.map (Λ[n+1, i].ι : _ ⟶ (Δ[n+1] : SSet.{0}))) where
…
```
Mentions: OAI.Thomason.Construction.TopologicalDeformation.Data

theorem OAI.Thomason.Construction.horn_attachment_weak line 295

Source documentation

Attaching any simplex along any horn gives an actual realization weak equivalence.

theorem horn_attachment_weak {n : ℕ} (i : Fin (n+2))
    {X P : SSet.{0}} {f : (Λ[n+1, i] : SSet.{0}) ⟶ X}
    {b : (Δ[n+1] : SSet.{0}) ⟶ P} {j : X ⟶ P}
    (h : IsPushout Λ[n+1, i].ι f b j) : realizationWeakEquivalences j :=
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.horn_pushouts_weak line 302
Source documentation
The entire cobase-change closure of the generating horn family is weak.
```
theorem horn_pushouts_weak :
    SSet.modelCategoryQuillen.J.{0}.pushouts ≤ realizationWeakEquivalences := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences