OAI/CategoryTheory/Thomason/Simplicial/FinitePosetUnitReduction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Relative finite approximation of weak Kan lifts

The actual continuous lift is resolved in a finite nonsingular target. Relative approximation retains its comparison class, so Kan lifting makes its projection exact before relative subdivision descent.

  1. theorem OAI.Thomason.Construction.iteratedChainPoset_nonempty line 31
  2. theorem OAI.Thomason.Construction.weak_kan_lift_on_resolved_facePoset line 47
  3. theorem OAI.Thomason.Construction.weak_kan_lift_on_facePoset line 188
  4. theorem OAI.Thomason.Construction.weak_kan_lift_simplexSubcomplex line 257
  5. theorem OAI.Thomason.Construction.weak_kan_boundary_lifting line 270
  6. theorem OAI.Thomason.Construction.weak_kan_boundary_rlp line 291
  7. theorem OAI.Thomason.Construction.acyclicKanLifting_unconditional line 301

    Source documentation

    Every Kan fibration which is an actual realization weak equivalence lifts against every boundary inclusion, in every dimension.

    theorem acyclicKanLifting_unconditional : PublishedAcyclicKanLifting :=
…

    Mentions: OAI.Thomason.Construction.PublishedAcyclicKanLifting

  8. theorem OAI.Thomason.Construction.kan_filtered_colimMap_weak line 332
  9. theorem OAI.Thomason.Construction.realization_filtered_colimMap_weak line 358
  10. theorem OAI.Thomason.Construction.realization_filtered_colimit_weak line 381

    Source documentation

    The result for arbitrary chosen colimit cocones, retaining the given comparison map rather than replacing it by the canonical colimit map.

    theorem realization_filtered_colimit_weak {c : Cocone D} {d : Cocone E}
    (hc : IsColimit c) (hd : IsColimit d) (η : D ⟶ E) (p : c.pt ⟶ d.pt)
    (hp : ∀ j, c.ι.app j ≫ p = η.app j ≫ d.ι.app j)
    (hη : ∀ j, realizationWeakEquivalences (η.app j)) :
    realizationWeakEquivalences p := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  11. instance OAI.Thomason.Construction.realizationWeakEquivalences_stableUnderFilteredColimits line 402
  12. theorem OAI.Thomason.Construction.WeakNaturalTransformationColimits.app_weak_iff_of_weak_images line 436

    Source documentation

    Weakness of a component propagates across any map whose two functorial images are weak equivalences.

    theorem app_weak_iff_of_weak_images [W.HasTwoOutOfThreeProperty]
    {X Y : C} (f : X ⟶ Y) (hF : W (F.map f)) (hG : W (G.map f)) :
    W (η.app X) ↔ W (η.app Y) := by
…
  13. theorem OAI.Thomason.Construction.WeakNaturalTransformationColimits.app_weak_of_isColimit line 451

    Source documentation

    A natural transformation that is weak on a diagram is weak at its chosen colimit when both functors preserve that colimit.

    theorem app_weak_of_isColimit
    {J : Type u₃} [Category.{v₃} J] [W.IsStableUnderColimitsOfShape J]
    {K : J ⥤ C} {c : Cocone K} (hc : IsColimit c)
    [PreservesColimit K F] [PreservesColimit K G]
    (hη : ∀ j, W (η.app (K.obj j))) : W (η.app c.pt) := by
…
  14. theorem OAI.Thomason.Construction.WeakNaturalTransformationColimits.app_weak_colimit line 464

    Source documentation

    The canonical colimit specialization retains exactly the given component.

    theorem app_weak_colimit
    {J : Type u₃} [Category.{v₃} J] [W.IsStableUnderColimitsOfShape J]
    (K : J ⥤ C) [HasColimit K]
    [PreservesColimit K F] [PreservesColimit K G]
    (hη : ∀ j, W (η.app (K.obj j))) : W (η.app (colimit K)) :=
…
  15. theorem OAI.Thomason.Construction.WeakNaturalTransformationColimits.realization_app_weak_of_isColimit line 480

    Source documentation

    The actual realization weak-equivalence test passes from every object of a filtered diagram to its chosen colimit.

    theorem realization_app_weak_of_isColimit
    {J : Type} [Category.{0} J] [IsFiltered J]
    {K : J ⥤ C} {c : Cocone K} (hc : IsColimit c)
    [PreservesColimit K F] [PreservesColimit K G]
    (hη : ∀ j, realizationWeakEquivalences (η.app (K.obj j))) :
    realizationWeakEquivalences (η.app c.pt) :=
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  16. theorem OAI.Thomason.Construction.WeakNaturalTransformationColimits.realization_unit_weak_of_isColimit line 489

    Source documentation

    In particular this applies to each literal component of an adjunction unit.

    theorem realization_unit_weak_of_isColimit
    {L : SSet.{0} ⥤ C} {R : C ⥤ SSet.{0}} (adj : L ⊣ R)
    {J : Type} [Category.{0} J] [IsFiltered J]
    {K : J ⥤ SSet.{0}} {c : Cocone K} (hc : IsColimit c)
    [PreservesColimit K (L ⋙ R)]
    (hη : ∀ j, realizationWeakEquivalences (adj.unit.app (K.obj j))) :
    realizationWeakEquivalences (adj.unit.app c.pt) :=
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  17. theorem OAI.Thomason.Construction.FinitePosetUnitReduction.finite_nonsingular line 529

    Source documentation

    Finite nonsingular simplicial sets reduce to their actual finite nondegenerate face posets.

    theorem finite_nonsingular (X : SSet.{0}) [X.Finite] [X.Nonsingular] :
    realizationWeakEquivalences (η.app X) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  18. theorem OAI.Thomason.Construction.FinitePosetUnitReduction.nonsingular line 537

    Source documentation

    The filtered union of finite subcomplexes removes the finiteness condition.

    theorem nonsingular [PreservesFilteredColimitsOfSize.{0,0} F]
    (X : SSet.{0}) [X.Nonsingular] :
    realizationWeakEquivalences (η.app X) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  19. theorem OAI.Thomason.Construction.FinitePosetUnitReduction.all line 549

    Source documentation

    Weak components on finite poset nerves imply weak components everywhere, using the proved face-simplex augmentation for arbitrary singular targets.

    theorem all [PreservesFilteredColimitsOfSize.{0,0} F] (X : SSet.{0}) :
    realizationWeakEquivalences (η.app X) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences