OAI/CategoryTheory/Thomason/Transfer/FiniteStreetSievePushouts.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Monic pushout comparisons from exact image intersections

  1. theorem OAI.Thomason.Construction.simplicial_pushout_comparison_mono line 22

    Source documentation

    A map out of a simplicial pushout is monic when the two monic image pieces intersect in precisely the image of the common source.

    theorem simplicial_pushout_comparison_mono
    {A B C D X : SSet.{0}} {i : A ⟶ B} {j : A ⟶ C}
    {u : B ⟶ D} {v : C ⟶ D} (hp : IsPushout i j u v)
    (k : D ⟶ X) (b : B ⟶ X) (c : C ⟶ X)
    [Mono b] [Mono c] [Mono (i ≫ b)]
    (hb : u ≫ k = b) (hc : v ≫ k = c)
    (hinter : SSet.Subcomplex.range (i ≫ b) =
      SSet.Subcomplex.range b ⊓ SSet.Subcomplex.range c) : Mono k := by
…
  2. theorem OAI.Thomason.Construction.simplicial_pushout_comparison_range line 61

    Source documentation

    The actual image of any pushout comparison is the union of its two pieces, with no injectivity assumption.

    theorem simplicial_pushout_comparison_range
    {A B C D X : SSet.{0}} {i : A ⟶ B} {j : A ⟶ C}
    {u : B ⟶ D} {v : C ⟶ D} (hp : IsPushout i j u v)
    (k : D ⟶ X) (b : B ⟶ X) (c : C ⟶ X)
    (hb : u ≫ k = b) (hc : v ≫ k = c) :
    SSet.Subcomplex.range k = SSet.Subcomplex.range b ⊔ SSet.Subcomplex.range c := by
…
  3. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.street_endpoint_factor_mono line 98
  4. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.street_endpoint_factor_range line 104
  5. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fiberStreetSubcomplex_min line 112
  6. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetCosieveStreet_range line 130

    Source documentation

    The image of the original Street map is exactly its full labelled fibre.

    theorem posetCosieveStreet_range {P : Type} [PartialOrder P] (A : Set P) (hA : IsUpperSet A) :
    SSet.Subcomplex.range (h.streetNerve.map (h.posetMap (subposetInclusion A))) =
      h.fiberStreetSubcomplex (h.membershipLabel Aᶜ hA.compl) 1 := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion

  7. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetCosieve_nerve_mono line 139

    Source documentation

    Full cosieve inclusions have monomorphic actual Street nerves.

    theorem posetCosieve_nerve_mono
    {P : Type} [PartialOrder P] (A : Set P) (hA : IsUpperSet A) :
    Mono (h.streetNerve.map (h.posetMap (subposetInclusion A))) := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion

  8. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.street_cosieve_maps_isPushout line 147

    Source documentation

    The actual composite N c takes this two-cosieve square to a pushout.

    theorem street_cosieve_maps_isPushout
    {P : Type} [PartialOrder P]
    (A B : Set P) (hA : IsUpperSet A) (hB : IsUpperSet B)
    (hcover : ∀ x, x ∈ A ∨ x ∈ B) :
    IsPushout ((h.categorification ⋙ h.streetNerve).map
        (nerveMap (interLeft A B).monotone.functor))
      ((h.categorification ⋙ h.streetNerve).map
        (nerveMap (interRight A B).monotone.functor))
      (h.streetNerve.map (h.posetMap (subposetInclusion A)))
      (h.streetNerve.map (h.posetMap (subposetInclusion B))) := by
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities.map, OAI.Thomason.Construction.interLeft, OAI.Thomason.Construction.interRight, OAI.Thomason.Construction.subposetInclusion

  9. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.cosieve_piece_pushout line 207

    Source documentation

    A containing sieve gives the corresponding smaller attachment as the actual full fibre in the original pushout.

    theorem cosieve_piece_pushout {P : Type} [PartialOrder P]
    (A U : Set P) (hU : IsUpperSet U) (hAU : A ⊆ U)
    {X Y : StrictOmegaCategory.{0}}
    {a : h.categorification.obj (nerve A) ⟶ X}
    {b : h.categorification.obj (nerve P) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (h.posetMap (subposetInclusion A)) a b j)
    (pY : Y ⟶ StrictPoset.category (Fin 2))
    (hb : b ≫ pY = h.membershipLabel Uᶜ hU.compl) (hj : j ≫ pY = constantLabel X 1) :
    IsPushout (h.posetMap (subposetInclusionWithin A U hAU)) a
      ((h.cosievePosetFiberMap U hU) ≫ labelFiberMap (h.membershipLabel Uᶜ hU.compl) pY 1 b hb)
      ((constantFiberIso X 1).inv ≫ labelFiberMap (constantLabel X 1) pY 1 j hj) := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.subposetInclusionWithin

  10. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.cosieve_piece_label line 228

    Source documentation

    The required compatible label exists for every containing sieve.

    theorem cosieve_piece_label {P : Type} [PartialOrder P]
    (A U : Set P) (hU : IsUpperSet U) (hAU : A ⊆ U)
    {X Y : StrictOmegaCategory.{0}}
    {a : h.categorification.obj (nerve A) ⟶ X}
    {b : h.categorification.obj (nerve P) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (h.posetMap (subposetInclusion A)) a b j) :
    ∃ pY : Y ⟶ StrictPoset.category (Fin 2),
      b ≫ pY = h.membershipLabel Uᶜ hU.compl ∧ j ≫ pY = constantLabel X 1 := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.StrictPoset.category

  11. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.disjoint_cosieve_piece_label line 247

    Source documentation

    A cosieve disjoint from the old part extends by the constant zero label.

    theorem disjoint_cosieve_piece_label {P : Type} [PartialOrder P]
    (A U : Set P) (hU : IsUpperSet U) (hAU : ∀ x ∈ A, x ∉ U)
    {X Y : StrictOmegaCategory.{0}}
    {a : h.categorification.obj (nerve A) ⟶ X}
    {b : h.categorification.obj (nerve P) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (h.posetMap (subposetInclusion A)) a b j) :
    ∃ pY : Y ⟶ StrictPoset.category (Fin 2),
      b ≫ pY = h.membershipLabel Uᶜ hU.compl ∧ j ≫ pY = constantLabel X 0 := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.StrictPoset.category

  12. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.disjoint_cosieve_piece_iso line 267

    Source documentation

    The original categorified disjoint cosieve is exactly the post-attachment full one fibre; this retains the original map into the pushout.

    theorem disjoint_cosieve_piece_iso {P : Type} [PartialOrder P]
    (A U : Set P) (hU : IsUpperSet U) (hAU : ∀ x ∈ A, x ∉ U)
    {X Y : StrictOmegaCategory.{0}}
    {a : h.categorification.obj (nerve A) ⟶ X}
    {b : h.categorification.obj (nerve P) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (h.posetMap (subposetInclusion A)) a b j)
    (pY : Y ⟶ StrictPoset.category (Fin 2))
    (hb : b ≫ pY = h.membershipLabel Uᶜ hU.compl) (hj : j ≫ pY = constantLabel X 0) :
    IsIso (h.cosievePosetFiberMap U hU ≫
      labelFiberMap (h.membershipLabel Uᶜ hU.compl) pY 1 b hb) := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.StrictPoset.category

  13. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.street_cosieve_fiber_pushout line 304

    Source documentation

    Identify a square with a cover by two full cosieves and their full intersection. No preservation of arbitrary pushouts by Street is assumed.

    theorem street_cosieve_fiber_pushout
    {I B C D : StrictOmegaCategory.{0}}
    {i : I ⟶ B} {j : I ⟶ C} {b : B ⟶ D} {c : C ⟶ D}
    (p q : D ⟶ StrictPoset.category (Fin 2))
    (cover : ∀ x : Objects D, p.toFun x.val = StrictPoset.identity 1 ∨
      q.toFun x.val = StrictPoset.identity 1)
    (eB : B ≅ labelFiber p 1) (eC : C ≅ labelFiber q 1)
    (eI : I ≅ labelFiber (minLabel p q) 1)
    (hb : eB.hom ≫ labelFiberInclusion p 1 = b)
    (hc : eC.hom ≫ labelFiberInclusion q 1 = c)
    (hi : i ≫ b = eI.hom ≫ labelFiberInclusion (minLabel p q) 1)
    (hw : i ≫ b = j ≫ c) :
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictPoset.identity

  14. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.cosieve_attachment_street_pushout line 358

    Source documentation

    The actual post-attachment cover is a simplicial pushout. In particular, the attaching functor is allowed to identify arbitrary old cells.

    theorem cosieve_attachment_street_pushout
    {P : Type} [PartialOrder P] (A Z C : Set P)
    (hZ : IsUpperSet Z) (hC : IsUpperSet C)
    (hAC : ∀ x ∈ A, x ∉ C) (cover : ∀ x, x ∈ Z ∨ x ∈ C)
    {X Y : StrictOmegaCategory.{0}}
    {a : h.categorification.obj (nerve A) ⟶ X}
    {b : h.categorification.obj (nerve P) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (h.posetMap (subposetInclusion A)) a b j)
    (p q : Y ⟶ StrictPoset.category (Fin 2))
    (hbp : b ≫ p = h.membershipLabel Zᶜ hZ.compl)
    (hjp : j ≫ p = constantLabel X 1)
    (hbq : b ≫ q = h.membershipLabel Cᶜ hC.compl)
…

    Mentions: OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.StrictPoset.category

  15. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.containing_cosieve_attachment_comparison line 446

    Source documentation

    Extend couniversality on a containing cosieve to the nerve-pushout comparison on the original ambient poset.

    theorem containing_cosieve_attachment_comparison
    (g : PublishedSimplicialGluingInput) (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] (A Z C : Set P)
    (hZ : IsUpperSet Z) (hC : IsUpperSet C) (hAZ : A ⊆ Z)
    (hAC : ∀ x ∈ A, x ∉ C) (cover : ∀ x, x ∈ Z ∨ x ∈ C)
    (wZ : h.CouniversalStreetWeakEquivalence (h.posetMap (subposetInclusionWithin A Z hAZ)))
    [Mono (h.streetNerve.map (h.posetMap (subposetInclusionWithin A Z hAZ)))]
    {X Y : StrictOmegaCategory.{0}}
    {a : h.categorification.obj (nerve A) ⟶ X}
    {b : h.categorification.obj (nerve P) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (h.posetMap (subposetInclusion A)) a b j) :
    realizationWeakEquivalences (nervePushoutComparison h.streetNerve hp) := by
…

    Mentions: OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.subposetInclusionWithin, OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.nervePushoutComparison

  16. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_dwyer_attachment_comparison line 497

    Source documentation

    The right adjoint is required only on the containing cosieve, rather than on the ambient poset. This covers the actual subdivided horn pairs.

    theorem finite_dwyer_attachment_comparison
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h) (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P] (A Z : Set P)
    (hA : IsLowerSet A) (hZ : IsUpperSet Z) (hAZ : A ⊆ Z)
    (R : SieveRetraction {z : Z | z.val ∈ A})
    {X Y : StrictOmegaCategory.{0}}
    {a : h.categorification.obj (nerve A) ⟶ X}
    {b : h.categorification.obj (nerve P) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (h.posetMap (subposetInclusion A)) a b j) :
    realizationWeakEquivalences (nervePushoutComparison h.streetNerve hp) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.SieveRetraction, OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.nervePushoutComparison

  17. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.street_factor_mono line 545
  18. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.street_factor_range line 551
  19. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fiberStreetSubcomplex_max line 559
  20. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetStreet_range line 577

    Source documentation

    The image of the original Street map is exactly its full labelled fibre.

    theorem posetStreet_range (s : PublishedPosetSieveInput h)
    {P : Type} [PartialOrder P] [Finite P] (A : Set P) (hA : IsLowerSet A) :
    SSet.Subcomplex.range (h.streetNerve.map (h.posetMap (subposetInclusion A))) =
      h.fiberStreetSubcomplex (h.membershipLabel A hA) 0 := by
…

    Mentions: OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.subposetInclusion

  21. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.street_sieve_maps_isPushout line 587

    Source documentation

    The actual composite N c takes this two-sieve square to a pushout.

    theorem street_sieve_maps_isPushout
    (s : PublishedPosetSieveInput h)
    {P : Type} [PartialOrder P] [Finite P]
    (A B : Set P) (hA : IsLowerSet A) (hB : IsLowerSet B)
    (hcover : ∀ x, x ∈ A ∨ x ∈ B) :
    IsPushout ((h.categorification ⋙ h.streetNerve).map
        (nerveMap (interLeft A B).monotone.functor))
      ((h.categorification ⋙ h.streetNerve).map
        (nerveMap (interRight A B).monotone.functor))
      (h.streetNerve.map (h.posetMap (subposetInclusion A)))
      (h.streetNerve.map (h.posetMap (subposetInclusion B))) := by
…

    Mentions: OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.NormalizedSimplexIdentities.map, OAI.Thomason.Construction.interLeft, OAI.Thomason.Construction.interRight, OAI.Thomason.Construction.subposetInclusion

  22. theorem OAI.Thomason.Construction.FiniteReflectionInput.posetFiberMap_inclusion line 650
  23. theorem OAI.Thomason.Construction.FiniteReflectionInput.posetStreet_mono line 658
  24. theorem OAI.Thomason.Construction.FiniteReflectionInput.posetStreet_range line 674
  25. theorem OAI.Thomason.Construction.FiniteReflectionInput.street_sieve_maps_isPushout line 691