ThomasonSmallObject.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

All dimensions with the actual Kan–Quillen input constructed

Acyclic Kan lifting for realization weak equivalences supplies the Kan–Quillen axioms in the conditional strict-category theorem.

theorem OAI.Thomason.Construction.constructedKanQuillenInput line 26

theorem OAI.Thomason.Construction.main_with_four_published_inputs line 30

Source documentation

The complete main theorem family after discharging acyclic Kan lifting.

theorem main_with_four_published_inputs
    (G : RightGrayInput normalizedSimplexIdentities) (t : GrayTruncationInput G)
    (transfer : PublishedThomasonReduction normalizedSimplexIdentities)
    (loc : PublishedStreetLocalizationInput normalizedSimplexIdentities) :
    Nonempty (ThomasonModelResult normalizedSimplexIdentities.thomasonLeft
      normalizedSimplexIdentities.streetNerve constructedKanQuillenInput canonicalExtension_weak) ∧
      ∀ n, Nonempty (ThomasonModelResult
        ((constructedFiniteReflection n).thomasonLeft normalizedSimplexIdentities)
        (normalizedSimplexIdentities.finiteStreetNerve (n+1))
        constructedKanQuillenInput canonicalExtension_weak) :=
…

theorem OAI.Thomason.Construction.boundary_rlp_kanBaseChangeWeak line 64
Source documentation
A boundary-lifting map remains weak under arbitrary base change.
```
theorem boundary_rlp_kanBaseChangeWeak {A B : SSet.{0}} (f : A ⟶ B)
    (hf : I.rlp f) : kanBaseChangeWeak f := by
…
```
Mentions: OAI.Thomason.Construction.kanBaseChangeWeak
theorem OAI.Thomason.Construction.realization_weak_kanBaseChangeWeak line 71
Source documentation
Every actual realization weak equivalence is weak after arbitrary base change along a Kan fibration.
```
theorem realization_weak_kanBaseChangeWeak {A B : SSet.{0}} (f : A ⟶ B)
    (hf : realizationWeakEquivalences f) : kanBaseChangeWeak f := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.kanBaseChangeWeak

theorem OAI.Thomason.Construction.realization_weak_of_kan_pullback line 85

Source documentation

Right properness, retaining any specified cartesian square.

theorem realization_weak_of_kan_pullback {A B A' B' : SSet.{0}}
    {f : A ⟶ B} {f' : A' ⟶ B'} {a : A' ⟶ A} {p : B' ⟶ B}
    [HomotopicalAlgebra.Fibration p]
    (sq : IsPullback f' a p f) (hf : realizationWeakEquivalences f) :
    realizationWeakEquivalences f' :=
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.kan_pullback_weak line 93

Source documentation

The canonical pullback projection satisfies the same unrestricted test.

theorem kan_pullback_weak {A B E : SSet.{0}} (f : A ⟶ B)
    (hf : realizationWeakEquivalences f) (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] :
    realizationWeakEquivalences (pullback.fst p f) :=
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

instance OAI.Thomason.Construction.realizationWeakEquivalences_rightProper line 101
Source documentation
Actual realization weak equivalences are stable under all base changes along the horn-lifting class.
```
instance realizationWeakEquivalences_rightProper :
    realizationWeakEquivalences.{0}.IsStableUnderBaseChangeAgainst J.rlp where
…
```

theorem OAI.Thomason.Construction.realization_weak_pushout_mono line 108

Source documentation

Left properness, retaining any specified cocartesian square.

theorem realization_weak_pushout_mono {A B C P : SSet.{0}}
    {i : A ⟶ B} {f : A ⟶ C} {b : B ⟶ P} {j : C ⟶ P}
    [Mono i] (sq : IsPushout i f b j) (hf : realizationWeakEquivalences f) :
    realizationWeakEquivalences b := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.mono_pushout_weak line 118
Source documentation
The canonical pushout of a weak equivalence along any monomorphism is weak.
```
theorem mono_pushout_weak {A B C : SSet.{0}} (i : A ⟶ B) [Mono i]
    (f : A ⟶ C) (hf : realizationWeakEquivalences f) :
    realizationWeakEquivalences (pushout.inl i f) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
instance OAI.Thomason.Construction.realizationWeakEquivalences_leftProper line 125
Source documentation
Actual realization weak equivalences are stable under all cobase changes along monomorphisms.
```
instance realizationWeakEquivalences_leftProper :
    realizationWeakEquivalences.{0}.IsStableUnderCobaseChangeAgainst
      (monomorphisms SSet.{0}) where
…
```
theorem OAI.Thomason.Construction.kanQuillenCofibrations_eq_monomorphisms line 154
Source documentation
The lifting definition of cofibration agrees with monomorphisms for the actual realization weak equivalences and horn fibrations.
```
theorem kanQuillenCofibrations_eq_monomorphisms :
    (J.rlp ⊓ realizationWeakEquivalences.{0}).llp = monomorphisms SSet.{0} := by
…
```
theorem OAI.Thomason.Construction.kanQuillenProperCombinatorialAxioms line 161
Source documentation
All the prescribed proper combinatorial model axioms on simplicial sets, constructed without an assumed model structure or properness theorem.
```
theorem kanQuillenProperCombinatorialAxioms :
    ProperCombinatorialAxioms SSet.{0} realizationWeakEquivalences J.rlp where
…
```
Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.realization_inverseImage_rightProper line 202

Source documentation

Pullback preservation transfers the proved simplicial right-properness statement to the exact inverse-image classes.

theorem realization_inverseImage_rightProper {C : Type u} [Category.{v} C]
    (R : C ⥤ SSet.{0}) [PreservesLimitsOfShape WalkingCospan R] :
    (realizationWeakEquivalences.inverseImage R).IsStableUnderBaseChangeAgainst
      (J.rlp.inverseImage R) where
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetWeakEquivalences_eq_thomasonRight line 216
Source documentation
Twice extension does not change the Street weak-equivalence class.
```
theorem streetWeakEquivalences_eq_thomasonRight :
    h.streetWeakEquivalences = realizationWeakEquivalences.inverseImage h.thomasonRight := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomason_rightProper line 226
Source documentation
All pullbacks of Street weak equivalences along the prescribed Thomason fibrations are Street weak equivalences, in omega dimension.
```
theorem thomason_rightProper :
    h.streetWeakEquivalences.IsStableUnderBaseChangeAgainst h.thomasonFibrations := by
…
```
theorem OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences_eq_thomasonRight line 238
theorem OAI.Thomason.Construction.FiniteReflectionInput.thomason_rightProper line 252
Source documentation
The same actual right-properness statement holds in every positive finite dimension, using the specified reflection adjunction.
```
theorem thomason_rightProper :
    (thomasonWeakEquivalences (n := n) h).IsStableUnderBaseChangeAgainst
…
```
Mentions: OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences
theorem OAI.Thomason.Construction.finite_thomason_rightProper line 264
Source documentation
In finite dimension the reflection used above is the constructed intelligent truncation, so there is no reflection hypothesis.
```
theorem finite_thomason_rightProper (h : NormalizedSimplexIdentities) (n : ℕ) :
    (FiniteReflectionInput.thomasonWeakEquivalences (n := n) h).IsStableUnderBaseChangeAgainst
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences
def OAI.Thomason.Construction.imageBoundaries line 297
Source documentation
The small family consists of the literal images of simplex boundaries.
```
noncomputable def imageBoundaries (L : SSet.{0} ⥤ C) : MorphismProperty C :=
…
```
def OAI.Thomason.Construction.imageHorns line 301
Source documentation
A single countable index type packages the literal images of all horns.
```
noncomputable def imageHorns (L : SSet.{0} ⥤ C) : MorphismProperty C :=
…
```
theorem OAI.Thomason.Construction.imageBoundaries_rlp line 307
theorem OAI.Thomason.Construction.imageHorns_rlp line 319
theorem OAI.Thomason.Construction.boundaryInverseImage_weakFactorizationSystem line 336
theorem OAI.Thomason.Construction.hornInverseImage_weakFactorizationSystem line 342
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomason_cofibrationFactorization line 357
Source documentation
The prescribed trivial fibrations and their left lifting class form the first Thomason weak factorization system unconditionally.
```
theorem thomason_cofibrationFactorization :
    MorphismProperty.IsWeakFactorizationSystem
      (h.thomasonFibrations ⊓ h.streetWeakEquivalences).llp
      (h.thomasonFibrations ⊓ h.streetWeakEquivalences) := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomason_hornFactorization line 368
Source documentation
The higher horn-generated left lifting class and prescribed fibrations form a weak factorization system, before identifying that left class as weak.
```
theorem thomason_hornFactorization :
    MorphismProperty.IsWeakFactorizationSystem
      h.thomasonFibrations.llp h.thomasonFibrations :=
…
```
theorem OAI.Thomason.Construction.FiniteReflectionInput.thomason_cofibrationFactorization line 381
theorem OAI.Thomason.Construction.FiniteReflectionInput.thomason_hornFactorization line 391