FiniteSieveWeakEquivalenceBridge.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual finite-dimensional full-fibre maps detect weak equivalences

theorem OAI.Thomason.Construction.SieveMap.finiteFiberMap_weak_iff line 22
Source documentation
The original finite full-fibre restriction has the same Street weak property as the reflected categorification of the restricted poset map.
```
theorem finiteFiberMap_weak_iff :
    realizationWeakEquivalences ((h.finiteStreetNerve (n+1)).map
      (finiteFiberMap r A B f hf h hA hB)) ↔
    realizationWeakEquivalences ((h.finiteStreetNerve (n+1)).map
      (r.reflect.map (h.posetMap (restriction A B f hf)))) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.SieveMap.finiteFiberMap, OAI.Thomason.Construction.SieveMap.restriction
theorem OAI.Thomason.Construction.SieveMap.finiteFiberMap_weak_iff_nerve line 49
Source documentation
In every positive finite dimension, the full-fibre map is weak exactly when the ordinary restricted nerve is weak.
```
theorem finiteFiberMap_weak_iff_nerve [Finite P] [Finite Q]
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h) (kq : KanQuillenPublishedInput.{0}) :
    realizationWeakEquivalences ((h.finiteStreetNerve (n+1)).map
      (finiteFiberMap r A B f hf h hA hB)) ↔
      realizationWeakEquivalences (nerveMap (restriction A B f hf).monotone.functor) :=
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.SieveMap.finiteFiberMap, OAI.Thomason.Construction.SieveMap.restriction

theorem OAI.Thomason.Construction.SieveMap.finiteFiberMap_extended_weak_iff_nerve line 61

Source documentation

The same concrete full-fibre maps are detected by the Thomason right adjoint Ex²N.

theorem finiteFiberMap_extended_weak_iff_nerve [Finite P] [Finite Q]
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h) (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X : SSet.{0}, realizationWeakEquivalences (canonicalExtension.app X)) :
    realizationWeakEquivalences ((h.finiteStreetNerve (n+1) ⋙ SSet.ex ⋙ SSet.ex).map
      (finiteFiberMap r A B f hf h hA hB)) ↔
      realizationWeakEquivalences (nerveMap (restriction A B f hf).monotone.functor) := by
…

Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.SieveMap.finiteFiberMap, OAI.Thomason.Construction.SieveMap.restriction