OAI/CategoryTheory/Thomason/Simplicial/CobaseChangeCellularClosure.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

The universal weak-preserving attachment class

For left properness the relevant attaching maps preserve weak maps after any cobase change. We keep this universal condition explicit; it is stronger than testing only weak maps from the original source.

  1. def OAI.Thomason.Construction.CobaseChangeCellularClosure.weakPreserving line 26

    Source documentation

    A single attaching map preserves weak maps under pushout.

    def weakPreserving (W : MorphismProperty C) : MorphismProperty C :=
…
  2. abbrev OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving line 30

    Source documentation

    Every cobase change of the attaching map preserves weak maps.

    abbrev universalWeakPreserving (W : MorphismProperty C) : MorphismProperty C :=
…
  3. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_iff line 34
  4. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_along line 41
  5. instance OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_respectsIso line 45
  6. instance OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_cobaseChange line 50
  7. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.weakPreserving_of_isIso line 56
  8. instance OAI.Thomason.Construction.CobaseChangeCellularClosure.weakPreserving_composition line 64
  9. instance OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_multiplicative line 72
  10. abbrev OAI.Thomason.Construction.CobaseChangeCellularClosure.comparison line 86

    Source documentation

    The map between the two pushouts induced by a map of attaching targets.

    abbrev comparison : pushout i a ⟶ pushout i (a ≫ w) :=
…
  11. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.inl_comparison line 90
  12. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.inr_comparison line 94
  13. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.comparison_isPushout line 98
  14. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.comparison_weak line 106
  15. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.of_comparison_weak line 114

    Source documentation

    Canonical pushouts suffice to test all the universal squares.

    theorem of_comparison_weak (W : MorphismProperty C) [W.RespectsIso]
    {A B : C} (i : A ⟶ B)
    (h : ∀ {X Y : C} (a : A ⟶ X) (w : X ⟶ Y),
      W w → W (comparison i a w)) : universalWeakPreserving W i := by
…

    Mentions: OAI.Thomason.Construction.CobaseChangeCellularClosure.comparison, OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving

  16. def OAI.Thomason.Construction.CobaseChangeCellularClosure.constColimitIso line 144
  17. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.constColimitIso_ι line 148
  18. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.constColimitIso_map line 152
  19. def OAI.Thomason.Construction.CobaseChangeCellularClosure.toConstant line 163

    Source documentation

    A map from a diagram to a constant target, induced by its colimit.

    def toConstant {D : J ⥤ C} {X : C} (a : colimit D ⟶ X) :
    D ⟶ (Functor.const J).obj X :=
…
  20. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.toConstant_colimMap line 167
  21. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.constColimitIso_inv_map line 176
  22. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.colimit_constant_pushout line 184

    Source documentation

    Commuting colimits with a pushout having a constant right leg.

    theorem colimit_constant_pushout {D E : J ⥤ C} (η : D ⟶ E) {X : C}
    (β : D ⟶ (Functor.const J).obj X) (b : colimit D ⟶ X)
    (hb : colim.map β ≫ (constColimitIso (J := J) X).hom = b) :
…

    Mentions: OAI.Thomason.Construction.CobaseChangeCellularClosure.constColimitIso

  23. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_colimMap line 198

    Source documentation

    Universal weak preservation is stable under a filtered colimit of attaching maps, with no monomorphism assumption on the diagram.

    theorem universalWeakPreserving_colimMap (W : MorphismProperty C) [W.RespectsIso]
    [W.IsStableUnderFilteredColimits.{0,0}] {D E : J ⥤ C} (η : D ⟶ E)
    (hη : ∀ j, universalWeakPreserving W (η.app j)) :
    universalWeakPreserving W (colim.map η) := by
…

    Mentions: OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving

  24. instance OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_filtered line 248
  25. instance OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_filteredColimits line 268
  26. instance OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_transfinite line 273
  27. abbrev OAI.Thomason.Construction.CobaseChangeCellularClosure.pushoutEmbedding line 284
  28. abbrev OAI.Thomason.Construction.CobaseChangeCellularClosure.pushoutProjection line 288
  29. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.pushoutEmbedding_projection line 292
  30. abbrev OAI.Thomason.Construction.CobaseChangeCellularClosure.liftedComparison line 301

    Source documentation

    The larger comparison written with a fixed association of its target.

    abbrev liftedComparison : pushout g (r.r.left ≫ a) ⟶ pushout g (r.r.left ≫ (a ≫ w)) :=
…
  31. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.liftedComparison_isPushout line 305
  32. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.pushoutEmbedding_comparison line 317
  33. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.pushoutProjection_comparison line 324
  34. def OAI.Thomason.Construction.CobaseChangeCellularClosure.comparisonRetract line 331
  35. instance OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_retracts line 341
  36. instance OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving_coproducts line 354
  37. theorem OAI.Thomason.Construction.CobaseChangeCellularClosure.generated_left_preserves_weak line 368

    Source documentation

    Universal weak preservation by the generators propagates to every map in their generated left lifting class.

    theorem generated_left_preserves_weak (I W : MorphismProperty C)
    [I.HasSmallObjectArgument.{0}] [W.RespectsIso] [W.IsStableUnderRetracts]
    [W.IsStableUnderFilteredColimits.{0,0}]
    (hI : I ≤ universalWeakPreserving W) :
    W.IsStableUnderCobaseChangeAgainst I.rlp.llp := by
…

    Mentions: OAI.Thomason.Construction.CobaseChangeCellularClosure.universalWeakPreserving