OAI/CategoryTheory/Thomason/Transfer/StreetLocalizationFromModel.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thomason.Construction.smallObject_leftLifting_weak line 27
2. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetWeak_transfinite line 49
3. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.horn_left_weak_of_simultaneous_attachments line 55
4. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.weakCofibration_factorization_of_simultaneous_attachments line 64
5. theorem OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeak_transfinite line 89
6. theorem OAI.Thomason.Construction.FiniteReflectionInput.horn_left_weak_of_simultaneous_attachments line 97
7. theorem OAI.Thomason.Construction.FiniteReflectionInput.weakCofibration_factorization_of_simultaneous_attachments line 110
8. abbrev OAI.Thomason.Construction.FiniteSubsetAttachments.object line 147
9. abbrev OAI.Thomason.Construction.FiniteSubsetAttachments.head line 149
10. abbrev OAI.Thomason.Construction.FiniteSubsetAttachments.leg line 151
11. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.arrow_leg line 154
12. def OAI.Thomason.Construction.FiniteSubsetAttachments.map line 158
13. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.head_map line 162
14. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.leg_map line 166
15. abbrev OAI.Thomason.Construction.FiniteSubsetAttachments.diagram line 170
16. def OAI.Thomason.Construction.FiniteSubsetAttachments.heads line 188
17. def OAI.Thomason.Construction.FiniteSubsetAttachments.emptyIso line 194
18. def OAI.Thomason.Construction.FiniteSubsetAttachments.insertLeg line 204
19. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.insertLeg_condition line 211
20. def OAI.Thomason.Construction.FiniteSubsetAttachments.insertDesc line 221
21. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.insertDesc_map line 226
22. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.insertDesc_leg line 239
23. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.insert_isPushout line 244
24. def OAI.Thomason.Construction.FiniteSubsetAttachments.fullLeg line 283
25. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.head_fullLeg line 287
26. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.leg_fullLeg line 290
27. abbrev OAI.Thomason.Construction.FiniteSubsetAttachments.fullCocone line 293
28. def OAI.Thomason.Construction.FiniteSubsetAttachments.glueHead line 305
29. def OAI.Thomason.Construction.FiniteSubsetAttachments.glueLeg line 307
30. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.glue_condition line 310
31. def OAI.Thomason.Construction.FiniteSubsetAttachments.fullDesc line 318
32. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.fullDesc_fac line 321
33. def OAI.Thomason.Construction.FiniteSubsetAttachments.fullIsColimit line 344
34. abbrev OAI.Thomason.Construction.FiniteSubsetAttachments.cobaseWeak line 362

    Source documentation

    A map remains weak after every individual cobase change.

    abbrev cobaseWeak (W : MorphismProperty C) : MorphismProperty C :=
    …

35. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.cobaseWeak_iff line 366
36. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.finite_head_weak line 375
37. theorem OAI.Thomason.Construction.FiniteSubsetAttachments.full_head_weak line 387

    Source documentation

    Arbitrary simultaneous cobase-weak maps remain weak. The proof uses the actual filtered colimit of finite subfamilies.

    theorem full_head_weak (W : MorphismProperty C) [W.IsMultiplicative] [W.RespectsIso]
        [W.IsStableUnderFilteredColimits.{0,0}]
        (hq : ∀ a, cobaseWeak W (q a)) : W (WidePushout.head q) := by
    …

    Mentions: OAI.Thomason.Construction.FiniteSubsetAttachments.cobaseWeak

38. abbrev OAI.Thomason.Construction.SimultaneousAttachments.attachingMap line 427
39. abbrev OAI.Thomason.Construction.SimultaneousAttachments.piece line 429
40. abbrev OAI.Thomason.Construction.SimultaneousAttachments.pieceMap line 431
41. abbrev OAI.Thomason.Construction.SimultaneousAttachments.pieceInclusion line 433
42. abbrev OAI.Thomason.Construction.SimultaneousAttachments.total line 436
43. abbrev OAI.Thomason.Construction.SimultaneousAttachments.totalHead line 438
44. abbrev OAI.Thomason.Construction.SimultaneousAttachments.totalLeg line 440
45. theorem OAI.Thomason.Construction.SimultaneousAttachments.pieceMap_totalLeg line 443
46. abbrev OAI.Thomason.Construction.SimultaneousAttachments.totalInclusion line 447
47. theorem OAI.Thomason.Construction.SimultaneousAttachments.sigma_totalInclusion line 450
48. theorem OAI.Thomason.Construction.SimultaneousAttachments.total_condition line 454
49. theorem OAI.Thomason.Construction.SimultaneousAttachments.piece_condition line 464
50. abbrev OAI.Thomason.Construction.SimultaneousAttachments.pieceDesc line 469
51. theorem OAI.Thomason.Construction.SimultaneousAttachments.pieceInclusion_desc line 472
52. theorem OAI.Thomason.Construction.SimultaneousAttachments.pieceMap_desc line 476
53. abbrev OAI.Thomason.Construction.SimultaneousAttachments.totalDesc line 480
54. theorem OAI.Thomason.Construction.SimultaneousAttachments.totalLeg_desc line 483
55. theorem OAI.Thomason.Construction.SimultaneousAttachments.totalHead_desc line 487
56. theorem OAI.Thomason.Construction.SimultaneousAttachments.totalInclusion_desc line 490
57. theorem OAI.Thomason.Construction.SimultaneousAttachments.total_isPushout line 496
58. theorem OAI.Thomason.Construction.SimultaneousAttachments.pushout_sigma_weak line 519
59. theorem OAI.Thomason.Construction.SimultaneousAttachments.cobaseWeak_le line 532
60. theorem OAI.Thomason.Construction.SimultaneousAttachments.cobaseWeak_sigmaMap line 537
61. instance OAI.Thomason.Construction.SimultaneousAttachments.cobaseWeak_stableUnderCoproducts line 546
62. theorem OAI.Thomason.Construction.SimultaneousAttachments.simultaneous_attachments_weak line 555

    Source documentation

    Only individual pushouts need to be checked. Simultaneous pushouts follow from finite composition and filtered-colimit stability.

    theorem simultaneous_attachments_weak (I W : MorphismProperty C)
        [W.IsMultiplicative] [W.RespectsIso] [W.IsStableUnderFilteredColimits.{0,0}]
        (h : I.pushouts ≤ W) : (coproducts.{0} I).pushouts ≤ W := by
    …

63. theorem OAI.Thomason.Construction.SimultaneousAttachments.smallObject_leftLifting_weak_of_individualAttachments line 567
64. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.horn_left_weak_of_individual_attachments line 609
65. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.weakCofibration_factorization_of_individual_attachments line 618
66. theorem OAI.Thomason.Construction.FiniteReflectionInput.horn_left_weak_of_individual_attachments line 644
67. theorem OAI.Thomason.Construction.FiniteReflectionInput.weakCofibration_factorization_of_individual_attachments line 657
68. theorem OAI.Thomason.Construction.twiceSubdivision_unit_finite_poset line 692

    Source documentation

    Finite-poset units for categorification imply finite-poset units for the composite double-subdivision adjunction.

    theorem twiceSubdivision_unit_finite_poset
        {C : Type 1} [Category.{0} C] {L : SSet.{0} ⥤ C} {N : C ⥤ SSet.{0}}
        (adj : L ⊣ N)
        (hu : ∀ (P : Type) [PartialOrder P] [Finite P],
          realizationWeakEquivalences (adj.unit.app (nerve P)))
        (P : Type) [PartialOrder P] [Finite P] :
        realizationWeakEquivalences
          (((SSet.sdExAdjunction.comp SSet.sdExAdjunction).comp adj).unit.app (nerve P)) := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

69. theorem OAI.Thomason.Construction.thomason_unit_weak_of_finite_poset_units line 718

    Source documentation

    Once the actual proper model axioms hold, the Thomason adjunction has weak unit at every simplicial set if the finite categorification units hold.

    theorem thomason_unit_weak_of_finite_poset_units
        {C : Type 1} [Category.{0} C] {L : SSet.{0} ⥤ C} {N : C ⥤ SSet.{0}}
        (adj : L ⊣ (N ⋙ SSet.ex ⋙ SSet.ex))
        (kq : KanQuillenPublishedInput.{0})
        (a : ProperCombinatorialAxioms C (realizationWeakEquivalences.inverseImage N)
          (SSet.modelCategoryQuillen.J.rlp.inverseImage (N ⋙ SSet.ex ⋙ SSet.ex)))
        [PreservesFilteredColimitsOfSize.{0,0} (N ⋙ SSet.ex ⋙ SSet.ex)]
        (hu : ∀ (P : Type) [PartialOrder P] [Finite P],
          realizationWeakEquivalences (adj.unit.app (nerve P)))
        (X : SSet.{0}) : realizationWeakEquivalences (adj.unit.app X) := by
    …

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.realizationWeakEquivalences

70. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomason_unit_weak line 741

    Source documentation

    The omega-dimensional unit test, using only the finite-poset units and the prescribed model axioms.

    theorem thomason_unit_weak
        (kq : KanQuillenPublishedInput.{0})
        (a : ProperCombinatorialAxioms StrictOmegaCategory.{0} h.streetWeakEquivalences
          h.thomasonFibrations)
        (hu : ∀ (P : Type) [PartialOrder P] [Finite P],
          realizationWeakEquivalences (h.categorificationAdjunction.unit.app (nerve P)))
        (X : SSet.{0}) : realizationWeakEquivalences (h.thomasonAdjunction.unit.app X) :=
    …

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.realizationWeakEquivalences

71. theorem OAI.Thomason.Construction.FiniteReflectionInput.thomason_unit_weak line 759

    Source documentation

    The same exact unit test in every positive finite dimension.

    theorem thomason_unit_weak
        (kq : KanQuillenPublishedInput.{0})
        (a : ProperCombinatorialAxioms (StrictOmegaCategory.Truncated.{0} (n+1))
          (thomasonWeakEquivalences (n := n) h) (thomasonFibrations (n := n) h))
    …

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences, OAI.Thomason.Construction.FiniteReflectionInput.thomasonFibrations

72. def OAI.Thomason.Construction.thomasonLeftLocalizer line 801

    Source documentation

    Brown preservation makes the actual left adjoint a morphism of localizers.

    def thomasonLeftLocalizer : LocalizerMorphism realizationWeakEquivalences
        (realizationWeakEquivalences.inverseImage N) where
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

73. theorem OAI.Thomason.Construction.thomason_counit_weak line 808

    Source documentation

    The original counit is a Street weak equivalence, detected using the triangle identity and the exact twice-extension weak criterion.

    theorem thomason_counit_weak
        (hu : ∀ X, realizationWeakEquivalences (adj.unit.app X)) (Y : C) :
        (realizationWeakEquivalences.inverseImage N) (adj.counit.app Y) := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

74. theorem OAI.Thomason.Construction.thomasonRightLocalizer_equivalence_of_weak_unit line 816

    Source documentation

    The actual Ex² N functor induces an equivalence of localized categories.

    theorem thomasonRightLocalizer_equivalence_of_weak_unit
        (hu : ∀ X, realizationWeakEquivalences (adj.unit.app X)) :
        (thomasonRightLocalizer N kq canonicalExtension_weak).IsLocalizedEquivalence :=
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.thomasonRightLocalizer, OAI.Thomason.Construction.canonicalExtension_weak

75. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomason_localized_equivalence line 831

    Source documentation

    Omega-dimensional localization follows from the prescribed model axioms and the finite-poset unit comparison.

    theorem thomason_localized_equivalence
        (kq : KanQuillenPublishedInput.{0})
        (a : ProperCombinatorialAxioms StrictOmegaCategory.{0} h.streetWeakEquivalences
          h.thomasonFibrations)
        (hu : ∀ (P : Type) [PartialOrder P] [Finite P],
          realizationWeakEquivalences (h.categorificationAdjunction.unit.app (nerve P))) :
        (thomasonRightLocalizer h.streetNerve kq canonicalExtension_weak).IsLocalizedEquivalence :=
    …

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.thomasonRightLocalizer, OAI.Thomason.Construction.canonicalExtension_weak

76. theorem OAI.Thomason.Construction.FiniteReflectionInput.thomason_localized_equivalence line 849

    Source documentation

    The same localization equivalence in each positive finite dimension.

    theorem thomason_localized_equivalence
        (kq : KanQuillenPublishedInput.{0})
        (a : ProperCombinatorialAxioms (StrictOmegaCategory.Truncated.{0} (n+1))
          (thomasonWeakEquivalences (n := n) h) (thomasonFibrations (n := n) h))
    …

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences, OAI.Thomason.Construction.FiniteReflectionInput.thomasonFibrations

77. theorem OAI.Thomason.Construction.localizedEquivalence_cancel_right line 890

    Source documentation

    Cancellation on the right holds for equivalences of the actual localized categories.

    theorem localizedEquivalence_cancel_right
        (Φ : LocalizerMorphism W₁ W₂) (Ψ : LocalizerMorphism W₂ W₃)
        [Ψ.IsLocalizedEquivalence] [(Φ.comp Ψ).IsLocalizedEquivalence] :
        Φ.IsLocalizedEquivalence := by
    …

78. theorem OAI.Thomason.Construction.nerveLocalizer_equivalence_of_thomasonRight line 906

    Source documentation

    Twice extension can be cancelled from the localized nerve comparison.

    theorem nerveLocalizer_equivalence_of_thomasonRight
        {C : Type*} [Category* C] (N : C ⥤ SSet.{0})
        (kq : KanQuillenPublishedInput.{0})
        (hR : (thomasonRightLocalizer N kq canonicalExtension_weak).IsLocalizedEquivalence) :
        (nerveLocalizer N).IsLocalizedEquivalence := by
    …

    Mentions: OAI.Thomason.Construction.thomasonRightLocalizer, OAI.Thomason.Construction.canonicalExtension_weak, OAI.Thomason.Construction.nerveLocalizer

79. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.street_localized_equivalence line 924

    Source documentation

    The omega Street nerve is an equivalence after localization.

    theorem street_localized_equivalence
        (kq : KanQuillenPublishedInput.{0})
        (a : ProperCombinatorialAxioms StrictOmegaCategory.{0} h.streetWeakEquivalences
          h.thomasonFibrations)
        (hu : ∀ (P : Type) [PartialOrder P] [Finite P],
          realizationWeakEquivalences (h.categorificationAdjunction.unit.app (nerve P))) :
        (nerveLocalizer h.streetNerve).IsLocalizedEquivalence :=
    …

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.nerveLocalizer

80. theorem OAI.Thomason.Construction.FiniteReflectionInput.street_localized_equivalence line 942

    Source documentation

    The positive finite-dimensional Street nerve is an equivalence after localization.

    theorem street_localized_equivalence
        (kq : KanQuillenPublishedInput.{0})
        (a : ProperCombinatorialAxioms (StrictOmegaCategory.Truncated.{0} (n+1))
          (thomasonWeakEquivalences (n := n) h) (thomasonFibrations (n := n) h))
    …

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences, OAI.Thomason.Construction.FiniteReflectionInput.thomasonFibrations

81. theorem OAI.Thomason.Construction.streetLocalizationInput_of_models line 956

    Source documentation

    The literal former published localization input is supplied by the actual model axioms and finite-poset units.

    theorem streetLocalizationInput_of_models
        (h : NormalizedSimplexIdentities) [StrictColimitsInput]
        (kq : KanQuillenPublishedInput.{0}) (r : ∀ n, FiniteReflectionInput n)
        (aω : ProperCombinatorialAxioms StrictOmegaCategory.{0} h.streetWeakEquivalences
          h.thomasonFibrations)
        (af : ∀ n, ProperCombinatorialAxioms (StrictOmegaCategory.Truncated.{0} (n+1))
          (FiniteReflectionInput.thomasonWeakEquivalences (n := n) h)
    …

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictColimitsInput, OAI.Thomason.Construction.FiniteReflectionInput, OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences