OAI/CategoryTheory/Thomason/Transfer/PastingGlobeCylinderPushout.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thomason.Construction.RightGrayInput.finite_stationary_zigzag_pushout_weakEquivalence line 25

   Source documentation

   The finite-dimensional gluing theorem uses the finite pushout itself, without assuming the ambient inclusion preserves it.

   theorem finite_stationary_zigzag_pushout_weakEquivalence
       {A B X Y : StrictOmegaCategory.Truncated.{0} (n + 1)}
       {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
       (hp : IsPushout i a b j) (r : B ⟶ A) (hir : i ≫ r = 𝟙 A)
       (P Q : G.cylinder.obj B.val ⟶ B.val)
       (hP : G.cylinder.map i ≫ P = G.projection.app A.val ≫ i)
       (hQ : G.cylinder.map i ≫ Q = G.projection.app A.val ≫ i)
       (hP₀ : (G.endpoint false).app B.val ≫ P = 𝟙 B.val)
       (hPQ : (G.endpoint true).app B.val ≫ P = (G.endpoint true).app B.val ≫ Q)
       (hQ₀ : (G.endpoint false).app B.val ≫ Q =
         (StrictOmegaCategory.inclusion (n + 1)).map r ≫ (StrictOmegaCategory.inclusion (n + 1)).map i) :
       h.streetWeakEquivalences ((StrictOmegaCategory.inclusion (n + 1)).map j) := by
   …

   Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion

2. theorem OAI.Thomason.Construction.SieveRetraction.finite_greatest_new_pushout_weakEquivalence line 120

   Source documentation

   Every finite-dimensional attaching pushout in the greatest-new-element case is a Street weak equivalence.

   theorem finite_greatest_new_pushout_weakEquivalence
       {X Y : StrictOmegaCategory.Truncated.{0} (n + 1)}
       {a : r.reflect.obj (h.categorification.obj (nerve A)) ⟶ X}
       {b : r.reflect.obj (h.categorification.obj (nerve E)) ⟶ Y} {j : X ⟶ Y}
       (hp : IsPushout (r.reflect.map (h.posetMap (subposetInclusion A))) a b j) :
       h.streetWeakEquivalences ((StrictOmegaCategory.inclusion (n + 1)).map j) := by
   …

   Mentions: OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.StrictOmegaCategory.inclusion

3. theorem OAI.Thomason.Construction.RightGrayInput.stationary_zigzag_pushout_weakEquivalence line 186

   Source documentation

   A stationary two-cylinder contraction makes every pushout of its retract inclusion a Street-nerve weak equivalence.

   theorem stationary_zigzag_pushout_weakEquivalence
       {A B X Y : StrictOmegaCategory.{0}}
       {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
       (hp : IsPushout i a b j) (r : B ⟶ A) (hir : i ≫ r = 𝟙 A)
       (P Q : G.cylinder.obj B ⟶ B)
       (hP : G.cylinder.map i ≫ P = G.projection.app A ≫ i)
       (hQ : G.cylinder.map i ≫ Q = G.projection.app A ≫ i)
       (hP₀ : (G.endpoint false).app B ≫ P = 𝟙 B)
       (hPQ : (G.endpoint true).app B ≫ P = (G.endpoint true).app B ≫ Q)
       (hQ₀ : (G.endpoint false).app B ≫ Q = r ≫ i) :
       h.streetWeakEquivalences j := by
   …

4. theorem OAI.Thomason.Construction.SieveRetraction.greatest_new_pushout_weakEquivalence line 270

   Source documentation

   Every pushout of this categorified sieve inclusion is an actual Street-nerve weak equivalence.

   theorem greatest_new_pushout_weakEquivalence {X Y : StrictOmegaCategory.{0}}
       {a : h.categorification.obj (nerve A) ⟶ X}
       {b : h.categorification.obj (nerve E) ⟶ Y} {j : X ⟶ Y}
       (hp : IsPushout (h.posetMap (subposetInclusion A)) a b j) :
       h.streetWeakEquivalences j := by
   …

   Mentions: OAI.Thomason.Construction.subposetInclusion

5. structure OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing line 305

   Source documentation

   Atomic data for gluing two pieces. The overlap condition is an actual common-source representative, rather than an equality assumed in the unknown target pushout.

   structure PushoutGluing {A C D : StrictOmegaCategory.{0}} (f : A ⟶ C) (g : A ⟶ D) where
   …

6. abbrev OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.Source line 330
7. abbrev OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.Index line 332
8. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.label line 334
9. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.sourceLift line 338
10. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.comparison line 342
11. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.sourceLift_image line 345
12. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.sourceLift_dimension line 357
13. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.sourceLift_eq line 364

    Source documentation

    Duplicate labels are identified by the given common-source cells.

    theorem sourceLift_eq {a b : d.Index} (h : d.label a = d.label b) :
        d.sourceLift a = d.sourceLift b := by
    …

14. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.representative line 396
15. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.label_representative line 401
16. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.atomLift line 406
17. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.atomLift_image line 408
18. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.atomLift_dimension line 413
19. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.sourceLift_eq_atomLift line 419
20. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.generated_left_image line 423
21. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.generated_right_image line 432
22. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.generated line 442

    Source documentation

    Covering piece atoms generate the actual strict pushout.

    theorem generated (x : d.Source) :
        Nonempty (CompositionExpression d.Source d.atomLift x) := by
    …

23. def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.iso line 452

    Source documentation

    Atomic coverage and actual common-source overlaps imply the full strict pushout comparison is an isomorphism.

    def iso : d.Source ≅ K.realization :=
    …

24. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.iso_hom line 455
25. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.comparison_isIso line 457
26. theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.PushoutGluing.isPushout line 461
27. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.basisIso line 492
28. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.basisIso_hom line 497
29. def OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.modelIso line 500
30. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.modelIso_hom line 504
31. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.comparison_isIso line 509
32. theorem OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.CylinderSource.isPushout line 515

    Source documentation

    The actual chain-model cylinder preserves this pasted-globe pushout. No preservation of colimits by positive-table realization is assumed.

    theorem isPushout {n k : ℕ} (hkn : k < n) :
        IsPushout (model.map (Globe.faceMap true k n)) (model.map (Globe.faceMap false k n))
          (model.map (PastingGlobe.left n n k)) (model.map (PastingGlobe.right n n k)) := by
    …

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Globe.faceMap, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.left, OAI.Thomason.Construction.StrictOmegaCategory.PastingGlobe.right