NonsingularFaceGluing.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Subdivision and extension preserve the Kan lifting classes

The explicit subdivided horn collapse proves preservation of Kan lifting classes by subdivision and extension.

theorem OAI.Thomason.Construction.extension_kan_rlp line 28
Source documentation
Extension preserves the right lifting property against all actual horns.
```
theorem extension_kan_rlp {X Y : SSet.{0}} (p : X ⟶ Y) (hp : J.rlp p) :
    J.rlp (SSet.ex.map p) := by
…
```
instance OAI.Thomason.Construction.extension_fibration line 36
instance OAI.Thomason.Construction.extension_kan line 42
Source documentation
In particular, extension of an actual Kan complex is again Kan.
```
instance extension_kan (K : SSet.{0}) [SSet.KanComplex K] :
    SSet.KanComplex (SSet.ex.obj K) := by
…
```

theorem OAI.Thomason.Construction.subdivision_anodyne line 50

Source documentation

Subdivision preserves the full horn-generated left lifting class.

theorem subdivision_anodyne {X Y : SSet.{0}} (f : X ⟶ Y)
    (hf : SSet.anodyneExtensions f) : SSet.anodyneExtensions (SSet.sd.map f) := by
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonLeft_preserves_weakEquivalences line 81
Source documentation
The constructed omega-dimensional left adjoint preserves every actual Kan–Quillen weak equivalence, without using the localization conclusion.
```
theorem thomasonLeft_preserves_weakEquivalences
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0}) (transfer : PublishedThomasonReduction h)
    {X Y : SSet.{0}} (f : X ⟶ Y) (hf : realizationWeakEquivalences f) :
    h.streetWeakEquivalences (h.thomasonLeft.map f) :=
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.FiniteReflectionInput.thomasonLeft_preserves_weakEquivalences line 100
Source documentation
The same weak-equivalence bridge for each positive finite dimension.
```
theorem thomasonLeft_preserves_weakEquivalences
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0}) (transfer : PublishedThomasonReduction h)
    {X Y : SSet.{0}} (f : X ⟶ Y) (hf : realizationWeakEquivalences f) :
    realizationWeakEquivalences ((h.finiteStreetNerve (n+1)).map
      ((r.thomasonLeft h).map f)) :=
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.SimplicialSpan.boundary_right_pair line 131
def OAI.Thomason.Construction.SimplicialSpan.factorPrefixUnconditional line 137
def OAI.Thomason.Construction.SimplicialSpan.factorizationUnconditional line 170
theorem OAI.Thomason.Construction.SimplicialSpan.Cofibration.compUnconditional line 204
theorem OAI.Thomason.Construction.SimplicialSpan.inl_cofibrationUnconditional line 233
theorem OAI.Thomason.Construction.SimplicialSpan.inr_cofibrationUnconditional line 240
theorem OAI.Thomason.Construction.SimplicialSpan.relativeB_weakUnconditional line 248
theorem OAI.Thomason.Construction.SimplicialSpan.pushoutMap_weak_of_cofibrationUnconditional line 259
Source documentation
A span cofibration which is weak at each object induces a weak equivalence of the actual simplicial pushouts. This derives the comparison from geometric deformation.
```
theorem pushoutMap_weak_of_cofibrationUnconditional {X Y : Diagram} (f : X ⟶ Y)
    (hi : Cofibration f)
    (ha : realizationWeakEquivalences f.a) (hb : realizationWeakEquivalences f.b)
    (hc : realizationWeakEquivalences f.c) : realizationWeakEquivalences (pushoutMap f) := by
…
```
Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram, OAI.Thomason.Construction.SimplicialSpan.Cofibration, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.SimplicialSpan.pushoutMap
theorem OAI.Thomason.Construction.SimplicialSpan.ObjectwiseWeak.of_comp_unconditional line 271
theorem OAI.Thomason.Construction.SimplicialSpan.pushoutMap_weakUnconditional line 277
theorem OAI.Thomason.Construction.constructedSimplicialGluingUnconditional line 320
instance OAI.Thomason.Construction.NonsingularLastVertex.faceSubset_nerve_mono line 356
theorem OAI.Thomason.Construction.NonsingularLastVertex.faceSubset_range line 367
theorem OAI.Thomason.Construction.NonsingularLastVertex.source_union_isPushout line 380

theorem OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap_weak_union line 418

Source documentation

Three weak face comparisons glue to the union comparison.

theorem restrictedMap_weak_union (S T : Set X.N)
    (hS : IsLowerSet S) (hT : IsLowerSet T)
    (wS : realizationWeakEquivalences (restrictedMap S))
    (wT : realizationWeakEquivalences (restrictedMap T))
    (wI : realizationWeakEquivalences (restrictedMap (S ∩ T))) :
    realizationWeakEquivalences (restrictedMap (S ∪ T)) := by
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.NonsingularLastVertex.restrictedMap