KanQuillenLiftingReduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The Kan–Quillen boundary-lifting implication

Goerss–Jardine (1999), Theorems I.11.3–I.11.4 and Corollary II.8.6 imply that a Kan fibration which is a weak equivalence of actual realizations lifts against each boundary. The implication identifies acyclic Kan fibrations with the boundary right-lifting class.

abbrev OAI.Thomason.Construction.PublishedAcyclicKanLifting line 23
Source documentation
The boundary-lifting consequence of Goerss–Jardine, Theorems I.11.3–I.11.4; Corollary II.8.6 records properness.
```
abbrev PublishedAcyclicKanLifting : Prop :=
…
```
theorem OAI.Thomason.Construction.anodyne_class_of_acyclic_kan_lifting line 27
Source documentation
The reverse anodyne implication follows by horn factorization and a concrete retract.
```
theorem anodyne_class_of_acyclic_kan_lifting (h : PublishedAcyclicKanLifting) :
    SSet.anodyneExtensions.{0} = monomorphisms SSet.{0} ⊓ realizationWeakEquivalences := by
…
```
Mentions: OAI.Thomason.Construction.PublishedAcyclicKanLifting, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.boundary_class_of_acyclic_kan_lifting line 51
Source documentation
The trivial-fibration class equality follows from acyclic Kan lifting.
```
theorem boundary_class_of_acyclic_kan_lifting (h : PublishedAcyclicKanLifting) :
    I.rlp = J.rlp ⊓ realizationWeakEquivalences.{0} := by
…
```
Mentions: OAI.Thomason.Construction.PublishedAcyclicKanLifting
theorem OAI.Thomason.Construction.kanQuillenInput_of_acyclic_kan_lifting line 60
Source documentation
Acyclic Kan lifting supplies the Kan–Quillen model axioms.
```
theorem kanQuillenInput_of_acyclic_kan_lifting (h : PublishedAcyclicKanLifting) :
    KanQuillenPublishedInput.{0} :=
…
```
Mentions: OAI.Thomason.Construction.PublishedAcyclicKanLifting