WeakFactorizationRecognition.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The actual Kan--Quillen input and the Thomason lifting classes

The weak equivalences are those of geometric realizations, cofibrations are monomorphisms, and fibrations lift against Mathlib's explicit horn inclusions. The classical input is exactly the two weak factorization systems and the two-out-of-three property from Goerss--Jardine (1999), Theorems I.11.3–I.11.4 and Corollary II.8.6. There is no assumption of a model structure on strict higher categories.

structure OAI.Thomason.Construction.KanQuillenPublishedInput line 34
Source documentation
The portion of the published Kan--Quillen theorem required by transfer, with all three classes fixed to their actual definitions.
```
structure KanQuillenPublishedInput : Prop where
…
```
def OAI.Thomason.Construction.KanQuillenPublishedInput.model line 49
Source documentation
The classical input constructs Mathlib's full model-category interface. The weak-equivalence class is defined by geometric realization.
```
noncomputable def model : ModelCategory SSet.{u} := by
…
```
theorem OAI.Thomason.Construction.KanQuillenPublishedInput.trivialFibrations_eq_boundary_rlp line 62
Source documentation
Boundary lifting detects precisely the trivial Kan fibrations. This uses Mathlib's proved generation of monomorphisms by boundary inclusions.
```
theorem trivialFibrations_eq_boundary_rlp :
    J.rlp ⊓ realizationWeakEquivalences.{u} = I.rlp := by
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonRight line 75
Source documentation
The right adjoint candidate Ex² N on the actual strict category.
```
noncomputable def thomasonRight : StrictOmegaCategory.{0} ⥤ SSet.{0} :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonFibrations line 79
Source documentation
The prescribed fibrations are detected by actual horn lifting.
```
noncomputable def thomasonFibrations : MorphismProperty StrictOmegaCategory.{0} :=
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonCofibrations line 83
Source documentation
The prescribed cofibrations, using the lifting definition of the paper.
```
noncomputable def thomasonCofibrations : MorphismProperty StrictOmegaCategory.{0} :=
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomason_trivialFibrations_eq_boundary_lifting line 89
Source documentation
The prescribed trivial fibrations are exactly the maps whose twice extended Street nerve lifts against all boundary inclusions. This is the compatibility needed to apply the transfer theorem's generating cofibrations.
```
theorem thomason_trivialFibrations_eq_boundary_lifting
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences.{0} (canonicalExtension.app X)) :
    h.thomasonFibrations ⊓ h.streetWeakEquivalences =
      I.rlp.inverseImage h.thomasonRight := by
…
```
structure OAI.Thomason.Construction.PublishedSimplicialGluingInput line 128
Source documentation
Only the simplicial specialization of the classical gluing lemma.
```
structure PublishedSimplicialGluingInput : Prop where
…
```

theorem OAI.Thomason.Construction.PublishedSimplicialGluingInput.common_source line 148

Source documentation

A common source mapping weakly equivalently into both pieces and their intersection maps weakly equivalently into their pushout.

theorem common_source {A B C P X : SSet.{0}}
    {i : A ⟶ B} {j : A ⟶ C} {b : B ⟶ P} {c : C ⟶ P}
    (hp : IsPushout i j b c) [Mono i]
    (fA : X ⟶ A) (fB : X ⟶ B) (fC : X ⟶ C) (fP : X ⟶ P)
    (hi : fA ≫ i = fB) (hj : fA ≫ j = fC)
    (hb : fB ≫ b = fP) (hc : fC ≫ c = fP)
    (hA : realizationWeakEquivalences fA) (hB : realizationWeakEquivalences fB)
    (hC : realizationWeakEquivalences fC) : realizationWeakEquivalences fP := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

theorem OAI.Thomason.Construction.smallFamily_hasSmallObjectArgument line 185
Source documentation
Any small family of actual maps permits the small object argument.
```
theorem smallFamily_hasSmallObjectArgument (f : ∀ i, A i ⟶ B i) :
    (MorphismProperty.ofHoms f).HasSmallObjectArgument.{0} := by
…
```
theorem OAI.Thomason.Construction.smallFamily_weakFactorizationSystem line 205
Source documentation
The lifting classes of a small family form the actual weak factorization system given by the small object argument.
```
theorem smallFamily_weakFactorizationSystem (f : ∀ i, A i ⟶ B i) :
    MorphismProperty.IsWeakFactorizationSystem
      (MorphismProperty.ofHoms f).rlp.llp (MorphismProperty.ofHoms f).rlp := by
…
```
theorem OAI.Thomason.Construction.leftLifting_eq_cofibration_inter_weak line 233
theorem OAI.Thomason.Construction.weakCofibration_factorization_of_leftLifting_weak line 255