OAI/CategoryTheory/Thomason/Transfer/FiniteEmptyAttachmentFibers.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Unconditional full endpoint-fibre compatibility for actual attaching pushouts at either endpoint

  1. theorem OAI.Thomason.Construction.EndpointFiber.omega_pushout_fibers line 22

    Source documentation

    The fibre square is a pushout for the original unlabelled attachment, once its four strict labels commute.

    theorem omega_pushout_fibers (e : Fin 2)
    {A B X Y : StrictOmegaCategory.{0}}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j)
    (pA : A ⟶ StrictPoset.category (Fin 2)) (pB : B ⟶ StrictPoset.category (Fin 2))
    (pX : X ⟶ StrictPoset.category (Fin 2)) (pY : Y ⟶ StrictPoset.category (Fin 2))
    (hi : i ≫ pB = pA) (ha : a ≫ pX = pA)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = pX) :
    IsPushout (labelFiberMap pA pB e i hi) (labelFiberMap pA pX e a ha)
      (labelFiberMap pB pY e b hb) (labelFiberMap pX pY e j hj) := by
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category

  2. theorem OAI.Thomason.Construction.EndpointFiber.finite_pushout_fibers line 36

    Source documentation

    The same compatibility theorem uses the finite-category pushout itself.

    theorem finite_pushout_fibers (n : ℕ) (e : Fin 2)
    {A B X Y : Truncated.{0} (n + 1)}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j)
    (pA : A ⟶ finiteInterval n) (pB : B ⟶ finiteInterval n)
    (pX : X ⟶ finiteInterval n) (pY : Y ⟶ finiteInterval n)
    (hi : i ≫ pB = pA) (ha : a ≫ pX = pA)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = pX) :
    IsPushout
      ((finiteLabelFiberFunctor n e).map (Over.homMk i hi : Over.mk pA ⟶ Over.mk pB))
      ((finiteLabelFiberFunctor n e).map (Over.homMk a ha : Over.mk pA ⟶ Over.mk pX))
      ((finiteLabelFiberFunctor n e).map (Over.homMk b hb : Over.mk pB ⟶ Over.mk pY))
…
  3. theorem OAI.Thomason.Construction.EndpointFiber.omega_attachment_complement_iso line 66

    Source documentation

    If both old labels are constant at the other endpoint, the new fibre maps isomorphically onto the fibre of the actual pushout.

    theorem omega_attachment_complement_iso (e d : Fin 2) (hed : d ≠ e)
    {A B X Y : StrictOmegaCategory.{0}}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j)
    (pB : B ⟶ StrictPoset.category (Fin 2)) (pY : Y ⟶ StrictPoset.category (Fin 2))
    (hi : i ≫ pB = constantLabel A d)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = constantLabel X d) :
    IsIso (labelFiberMap pB pY e b hb) := by
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category

  4. theorem OAI.Thomason.Construction.EndpointFiber.omega_attachment_piece line 103

    Source documentation

    The labelled fibre is precisely a pushout with the chosen full piece.

    theorem omega_attachment_piece (e : Fin 2)
    {A B U X Y : StrictOmegaCategory.{0}}
    {i : A ⟶ B} {iU : A ⟶ U} {u : U ⟶ B}
    {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) (hiU : iU ≫ u = i)
    (pB : B ⟶ StrictPoset.category (Fin 2)) (pY : Y ⟶ StrictPoset.category (Fin 2))
    (hi : i ≫ pB = constantLabel A e)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = constantLabel X e)
    (eU : U ≅ labelFiber pB e) (hu : eU.hom ≫ labelFiberInclusion pB e = u) :
    IsPushout iU a
      (eU.hom ≫ labelFiberMap pB pY e b hb)
      ((constantFiberIso X e).inv ≫ labelFiberMap (constantLabel X e) pY e j hj) := by
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category

  5. theorem OAI.Thomason.Construction.EndpointFiber.omega_attachment_piece_inclusion line 132

    Source documentation

    The inclusion of the constructed piece into the original pushout is exactly its original structure map.

    theorem omega_attachment_piece_inclusion (e : Fin 2)
    {B U X Y : StrictOmegaCategory.{0}} {u : U ⟶ B}
    {b : B ⟶ Y} {j : X ⟶ Y}
    (pB : B ⟶ StrictPoset.category (Fin 2)) (pY : Y ⟶ StrictPoset.category (Fin 2))
    (hb : b ≫ pY = pB) (hj : j ≫ pY = constantLabel X e)
    (eU : U ≅ labelFiber pB e) (hu : eU.hom ≫ labelFiberInclusion pB e = u) :
    (eU.hom ≫ labelFiberMap pB pY e b hb) ≫ labelFiberInclusion pY e = u ≫ b ∧
      ((constantFiberIso X e).inv ≫ labelFiberMap (constantLabel X e) pY e j hj) ≫
        labelFiberInclusion pY e = j := by
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category

  6. theorem OAI.Thomason.Construction.ZeroFiber.omega_pushout_fibers line 161

    Source documentation

    The fibre square is a pushout for the original unlabelled attachment, once its four strict labels commute.

    theorem omega_pushout_fibers
    {A B X Y : StrictOmegaCategory.{0}}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j)
    (pA : A ⟶ StrictPoset.category (Fin 2)) (pB : B ⟶ StrictPoset.category (Fin 2))
    (pX : X ⟶ StrictPoset.category (Fin 2)) (pY : Y ⟶ StrictPoset.category (Fin 2))
    (hi : i ≫ pB = pA) (ha : a ≫ pX = pA)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = pX) :
    IsPushout (labelFiberMap pA pB 0 i hi) (labelFiberMap pA pX 0 a ha)
      (labelFiberMap pB pY 0 b hb) (labelFiberMap pX pY 0 j hj) := by
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category

  7. theorem OAI.Thomason.Construction.ZeroFiber.finite_pushout_fibers line 175

    Source documentation

    The same compatibility theorem uses the finite-category pushout itself.

    theorem finite_pushout_fibers (n : ℕ)
    {A B X Y : Truncated.{0} (n + 1)}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j)
    (pA : A ⟶ finiteInterval n) (pB : B ⟶ finiteInterval n)
    (pX : X ⟶ finiteInterval n) (pY : Y ⟶ finiteInterval n)
    (hi : i ≫ pB = pA) (ha : a ≫ pX = pA)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = pX) :
    IsPushout
      ((finiteLabelFiberFunctor n 0).map (Over.homMk i hi : Over.mk pA ⟶ Over.mk pB))
      ((finiteLabelFiberFunctor n 0).map (Over.homMk a ha : Over.mk pA ⟶ Over.mk pX))
      ((finiteLabelFiberFunctor n 0).map (Over.homMk b hb : Over.mk pB ⟶ Over.mk pY))
…
  8. theorem OAI.Thomason.Construction.ZeroFiber.omega_attachment_piece line 210

    Source documentation

    The labelled fibre is precisely a pushout with the chosen full piece.

    theorem omega_attachment_piece
    {A B U X Y : StrictOmegaCategory.{0}}
    {i : A ⟶ B} {iU : A ⟶ U} {u : U ⟶ B}
    {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) (hiU : iU ≫ u = i)
    (pB : B ⟶ StrictPoset.category (Fin 2)) (pY : Y ⟶ StrictPoset.category (Fin 2))
    (hi : i ≫ pB = constantLabel A 0)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = constantLabel X 0)
    (eU : U ≅ labelFiber pB 0) (hu : eU.hom ≫ labelFiberInclusion pB 0 = u) :
    IsPushout iU a
      (eU.hom ≫ labelFiberMap pB pY 0 b hb)
      ((constantFiberIso X 0).inv ≫ labelFiberMap (constantLabel X 0) pY 0 j hj) := by
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category

  9. theorem OAI.Thomason.Construction.ZeroFiber.omega_attachment_piece_inclusion line 239

    Source documentation

    The inclusion of the constructed piece into the original pushout is exactly its original structure map.

    theorem omega_attachment_piece_inclusion
    {B U X Y : StrictOmegaCategory.{0}} {u : U ⟶ B}
    {b : B ⟶ Y} {j : X ⟶ Y}
    (pB : B ⟶ StrictPoset.category (Fin 2)) (pY : Y ⟶ StrictPoset.category (Fin 2))
    (hb : b ≫ pY = pB) (hj : j ≫ pY = constantLabel X 0)
    (eU : U ≅ labelFiber pB 0) (hu : eU.hom ≫ labelFiberInclusion pB 0 = u) :
    (eU.hom ≫ labelFiberMap pB pY 0 b hb) ≫ labelFiberInclusion pY 0 = u ≫ b ∧
      ((constantFiberIso X 0).inv ≫ labelFiberMap (constantLabel X 0) pY 0 j hj) ≫
        labelFiberInclusion pY 0 = j := by
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category

  10. structure OAI.Thomason.Construction.PublishedPosetSieveInput line 277

    Source documentation

    The finite-poset specialization of published sieve preservation.

    structure PublishedPosetSieveInput (h : NormalizedSimplexIdentities) [StrictColimitsInput] : Prop where
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictColimitsInput

  11. theorem OAI.Thomason.Construction.PublishedPosetSieveInput.omega_mono line 292

    Source documentation

    The original categorified sieve map is monic.

    theorem omega_mono {P : Type} [PartialOrder P] [Finite P]
    (A : Set P) (hA : IsLowerSet A) : Mono (h.posetMap (subposetInclusion A)) := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion

  12. theorem OAI.Thomason.Construction.PublishedPosetSieveInput.omega_nerve_mono line 299

    Source documentation

    Its actual Street nerve is a simplicial monomorphism.

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

    Mentions: OAI.Thomason.Construction.subposetInclusion

  13. theorem OAI.Thomason.Construction.PublishedPosetSieveInput.omega_source_fiber_iso line 308

    Source documentation

    Relating the canonical fibre map to the map obtained by taking fibres of the original inclusion with its constant source label.

    theorem omega_source_fiber_iso {P : Type} [PartialOrder P] [Finite P]
    (A : Set P) (hA : IsLowerSet A)
    (hi : h.posetMap (subposetInclusion A) ≫ h.membershipLabel A hA =
      constantLabel (h.categorification.obj (nerve A)) 0) :
    IsIso (labelFiberMap (constantLabel (h.categorification.obj (nerve A)) 0)
      (h.membershipLabel A hA) 0 (h.posetMap (subposetInclusion A)) hi) := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion

  14. theorem OAI.Thomason.Construction.PublishedPosetSieveInput.omega_attachment_full_fiber line 325

    Source documentation

    For every attaching functor, the old target is the actual full zero-fibre of a label on the pushout. The isomorphism commutes with the original map.

    theorem omega_attachment_full_fiber {P : Type} [PartialOrder P] [Finite P] (A : Set P) (hA : IsLowerSet 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) :
    ∃ (pY : Y ⟶ StrictPoset.category (Fin 2)) (e : X ≅ labelFiber pY 0),
      e.hom ≫ labelFiberInclusion pY 0 = j ∧
      b ≫ pY = h.membershipLabel A hA ∧ j ≫ pY = constantLabel X 0 := by
…

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

  15. theorem OAI.Thomason.Construction.PublishedPosetSieveInput.omega_attachment_mono line 355

    Source documentation

    Arbitrary attachments along these finite-poset sieves remain monic.

    theorem omega_attachment_mono {P : Type} [PartialOrder P] [Finite P] (A : Set P) (hA : IsLowerSet 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) : Mono j := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion

  16. def OAI.Thomason.Construction.subposetInclusionWithin line 383

    Source documentation

    The inclusion between two full subposets with nested object sets.

    def subposetInclusionWithin {P : Type} [PartialOrder P]
    (A U : Set P) (hAU : A ⊆ U) : A →o U where
…
  17. def OAI.Thomason.Construction.restrictedOldIso line 389

    Source documentation

    Restricting the ambient poset retains a canonically isomorphic old part.

    def restrictedOldIso {P : Type} [PartialOrder P]
    (A U : Set P) (hAU : A ⊆ U) : A ≃o {x : U | x.val ∈ A} where
…
  18. def OAI.Thomason.Construction.NormalizedSimplexIdentities.posetMapIso line 402

    Source documentation

    Categorification carries an order isomorphism to an actual strict isomorphism.

    noncomputable def posetMapIso {E F : Type} [PartialOrder E] [PartialOrder F]
    (e : E ≃o F) : h.categorification.obj (nerve E) ≅ h.categorification.obj (nerve F) where
…
  19. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.subposetInclusionWithin_fac line 420

    Source documentation

    The original nested inclusions commute after categorification.

    theorem subposetInclusionWithin_fac {P : Type} [PartialOrder P]
    (A U : Set P) (hAU : A ⊆ U) :
    h.posetMap (subposetInclusionWithin A U hAU) ≫ h.posetMap (subposetInclusion U) =
      h.posetMap (subposetInclusion A) := by
…

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

  20. theorem OAI.Thomason.Construction.PublishedPosetSieveInput.omega_piece_pushout line 436

    Source documentation

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

    theorem omega_piece_pushout {P : Type} [PartialOrder P] [Finite P]
    (A U : Set P) (hU : IsLowerSet 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) (hj : j ≫ pY = constantLabel X 0) :
    IsPushout (h.posetMap (subposetInclusionWithin A U hAU)) a
      ((h.posetFiberMap U hU) ≫ labelFiberMap (h.membershipLabel U hU) pY 0 b hb)
      ((constantFiberIso X 0).inv ≫ labelFiberMap (constantLabel X 0) pY 0 j hj) := by
…

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

  21. theorem OAI.Thomason.Construction.PublishedPosetSieveInput.omega_piece_label line 459

    Source documentation

    The required compatible label exists for every containing sieve.

    theorem omega_piece_label {P : Type} [PartialOrder P]
    (A U : Set P) (hU : IsLowerSet 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 ∧ j ≫ pY = constantLabel X 0 := by
…

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

  22. def OAI.Thomason.Construction.NormalizedSimplexIdentities.CouniversalStreetWeakEquivalence line 498

    Source documentation

    Every cobase change of a strict map is a Street weak equivalence.

    def CouniversalStreetWeakEquivalence {A B : StrictOmegaCategory.{0}} (i : A ⟶ B) : Prop :=
…
  23. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.greatestNew_couniversal line 505

    Source documentation

    Stationary Gray prisms supply the greatest-new case.

    theorem greatestNew_couniversal {P : Type} [PartialOrder P] {A : Set P}
    (R : SieveRetraction A) {x : P} (hx : SieveRetraction.GreatestNew (A := A) x)
…

    Mentions: OAI.Thomason.Construction.SieveRetraction, OAI.Thomason.Construction.SieveRetraction.GreatestNew

  24. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.couniversal_of_two_sieve_cover line 513

    Source documentation

    Couniversality glues over two containing sieves and their intersection.

    theorem couniversal_of_two_sieve_cover
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P]
    (A U V : Set P) (hU : IsLowerSet U) (hV : IsLowerSet V)
    (hAU : A ⊆ U) (hAV : A ⊆ V) (cover : ∀ x, x ∈ U ∨ x ∈ V)
    (wU : h.CouniversalStreetWeakEquivalence (h.posetMap (subposetInclusionWithin A U hAU)))
    (wV : h.CouniversalStreetWeakEquivalence (h.posetMap (subposetInclusionWithin A V hAV)))
    (wI : h.CouniversalStreetWeakEquivalence (h.posetMap
      (subposetInclusionWithin A (U ∩ V) (fun _x hx => ⟨hAU hx, hAV hx⟩)))) :
    h.CouniversalStreetWeakEquivalence (h.posetMap (subposetInclusion A)) := by
…

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

  25. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.couniversal_precompose_iso line 595

    Source documentation

    Renaming the attaching source does not change couniversality.

    theorem couniversal_precompose_iso {A A' B : StrictOmegaCategory.{0}}
    (e : A' ≅ A) (i : A ⟶ B) (hi : h.CouniversalStreetWeakEquivalence i) :
    h.CouniversalStreetWeakEquivalence (e.hom ≫ i) := by
…
  26. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.couniversal_of_isIso line 604

    Source documentation

    Isomorphisms remain weak equivalences under arbitrary cobase change.

    theorem couniversal_of_isIso (kq : KanQuillenPublishedInput.{0})
    {A B : StrictOmegaCategory.{0}} (i : A ⟶ B) [IsIso i] :
    h.CouniversalStreetWeakEquivalence i := by
…
  27. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.posetMap_isIso_of_all line 615

    Source documentation

    A sieve containing every object induces an isomorphism.

    theorem posetMap_isIso_of_all {P : Type} [PartialOrder P]
    (A : Set P) (hA : ∀ x, x ∈ A) : IsIso (h.posetMap (subposetInclusion A)) := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion

  28. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.restrictedOldIso_fac line 626

    Source documentation

    Compatibility of the canonical old-source renaming with the actual inclusion.

    theorem restrictedOldIso_fac {P : Type} [PartialOrder P]
    (A U : Set P) (hAU : A ⊆ U) :
    (h.posetMapIso (restrictedOldIso A U hAU)).hom ≫
      h.posetMap (subposetInclusion {x : U | x.val ∈ A}) =
      h.posetMap (subposetInclusionWithin A U hAU) := by
…

    Mentions: OAI.Thomason.Construction.restrictedOldIso, OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.subposetInclusionWithin

  29. instance OAI.Thomason.Construction.StrictOmegaCategory.inclusion_faithful line 657

    Source documentation

    The truncation inclusion does not identify strict functors.

    instance inclusion_faithful (k : ℕ) : (StrictOmegaCategory.inclusion k).Faithful where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion

  30. instance OAI.Thomason.Construction.StrictOmegaCategory.inclusion_full line 661

    Source documentation

    Every ambient strict functor between truncated objects is a finite functor.

    instance inclusion_full (k : ℕ) : (StrictOmegaCategory.inclusion k).Full where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion

  31. def OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiber line 665

    Source documentation

    A full endpoint fibre as an object of the original finite category.

    def finiteLabelFiber {C : Truncated (n + 1)} (p : C ⟶ finiteInterval n) (e : Fin 2) :
    Truncated (n + 1) := (finiteLabelFiberFunctor n e).obj (Over.mk p)

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Truncated, OAI.Thomason.Construction.StrictOmegaCategory.finiteInterval, OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberFunctor

  32. def OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberMap line 669

    Source documentation

    Restriction of a finite-dimensional strict functor to its full fibres.

    def finiteLabelFiberMap {C D : Truncated (n + 1)}
    (p : C ⟶ finiteInterval n) (q : D ⟶ finiteInterval n) (e : Fin 2)
    (f : C ⟶ D) (hf : f ≫ q = p) : finiteLabelFiber p e ⟶ finiteLabelFiber q e :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Truncated, OAI.Thomason.Construction.StrictOmegaCategory.finiteInterval, OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiber

  33. def OAI.Thomason.Construction.StrictOmegaCategory.finiteConstantLabel line 675

    Source documentation

    A constant label in the finite category, on all cells.

    def finiteConstantLabel (C : Truncated (n + 1)) (e : Fin 2) : C ⟶ finiteInterval n :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Truncated, OAI.Thomason.Construction.StrictOmegaCategory.finiteInterval

  34. def OAI.Thomason.Construction.StrictOmegaCategory.finiteConstantFiberIso line 679

    Source documentation

    The constant-label fibre retains the original finite-dimensional object.

    def finiteConstantFiberIso (C : Truncated (n + 1)) (e : Fin 2) :
    finiteLabelFiber (finiteConstantLabel C e) e ≅ C where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Truncated, OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiber, OAI.Thomason.Construction.StrictOmegaCategory.finiteConstantLabel

  35. theorem OAI.Thomason.Construction.ZeroFiber.finite_attachment_piece line 692

    Source documentation

    A full finite-dimensional piece containing the attaching source has exactly the expected pushout, without assuming that inclusion preserves it.

    theorem finite_attachment_piece {n : ℕ}
    {A B U X Y : Truncated.{0} (n + 1)}
    {i : A ⟶ B} {iU : A ⟶ U} {u : U ⟶ B}
    {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) (hiU : iU ≫ u = i)
    (pB : B ⟶ finiteInterval n) (pY : Y ⟶ finiteInterval n)
    (hi : i ≫ pB = finiteConstantLabel A 0)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = finiteConstantLabel X 0)
    (eU : U ≅ finiteLabelFiber pB 0) (hu : eU.hom ≫ labelFiberInclusion pB 0 = u) :
    IsPushout iU a
      (eU.hom ≫ finiteLabelFiberMap pB pY 0 b hb)
      ((finiteConstantFiberIso X 0).inv ≫
…
  36. theorem OAI.Thomason.Construction.PublishedPosetSieveInput.finite_piece_pushout line 739

    Source documentation

    The smaller categorified poset attachment is the actual full finite fibre.

    theorem finite_piece_pushout {P : Type} [PartialOrder P] [Finite P]
    (A U : Set P) (hU : IsLowerSet U) (hAU : A ⊆ U)
    {X Y : Truncated.{0} (n + 1)}
    {a : (r.categorification h).obj (nerve A) ⟶ X}
    {b : (r.categorification h).obj (nerve P) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (r.reflect.map (h.posetMap (subposetInclusion A))) a b j)
    (pY : Y ⟶ finiteInterval n)
    (hb : b ≫ pY = r.membershipLabel h U hU) (hj : j ≫ pY = finiteConstantLabel X 0) :
    IsPushout (r.reflect.map (h.posetMap (subposetInclusionWithin A U hAU))) a
      ((r.posetFiberMap h U hU) ≫ finiteLabelFiberMap (r.membershipLabel h U hU) pY 0 b hb)
      ((finiteConstantFiberIso X 0).inv ≫
        finiteLabelFiberMap (finiteConstantLabel X 0) pY 0 j hj) := by
…

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

  37. theorem OAI.Thomason.Construction.PublishedPosetSieveInput.finite_piece_label line 770

    Source documentation

    Construct the compatible label using the original finite pushout.

    theorem finite_piece_label {P : Type} [PartialOrder P]
    (A U : Set P) (hU : IsLowerSet U) (hAU : A ⊆ U)
    {X Y : Truncated.{0} (n + 1)}
    {a : (r.categorification h).obj (nerve A) ⟶ X}
    {b : (r.categorification h).obj (nerve P) ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout (r.reflect.map (h.posetMap (subposetInclusion A))) a b j) :
    ∃ pY : Y ⟶ finiteInterval n,
      b ≫ pY = r.membershipLabel h U hU ∧ j ≫ pY = finiteConstantLabel X 0 := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion

  38. def OAI.Thomason.Construction.NormalizedSimplexIdentities.FiniteCouniversalStreetWeakEquivalence line 803

    Source documentation

    Cobase changes in the actual finite category are Street weak equivalences.

    def FiniteCouniversalStreetWeakEquivalence (h : NormalizedSimplexIdentities) (n : ℕ)
    {A B : Truncated.{0} (n + 1)} (i : A ⟶ B) : Prop :=
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

  39. theorem OAI.Thomason.Construction.FiniteReflectionInput.greatestNew_couniversal line 816

    Source documentation

    The finite stationary Gray prisms give the greatest-new base case.

    theorem greatestNew_couniversal {P : Type} [PartialOrder P] {A : Set P}
    (R : SieveRetraction A) {x : P} (hx : SieveRetraction.GreatestNew (A := A) x)
…

    Mentions: OAI.Thomason.Construction.SieveRetraction, OAI.Thomason.Construction.SieveRetraction.GreatestNew

  40. theorem OAI.Thomason.Construction.FiniteReflectionInput.couniversal_of_two_sieve_cover line 825

    Source documentation

    The two-sieve induction step uses finite pushouts and ambient Street covers.

    theorem couniversal_of_two_sieve_cover
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P]
    (A U V : Set P) (hU : IsLowerSet U) (hV : IsLowerSet V)
    (hAU : A ⊆ U) (hAV : A ⊆ V) (cover : ∀ x, x ∈ U ∨ x ∈ V)
    (wU : h.FiniteCouniversalStreetWeakEquivalence n
      (r.reflect.map (h.posetMap (subposetInclusionWithin A U hAU))))
    (wV : h.FiniteCouniversalStreetWeakEquivalence n
      (r.reflect.map (h.posetMap (subposetInclusionWithin A V hAV))))
    (wI : h.FiniteCouniversalStreetWeakEquivalence n (r.reflect.map (h.posetMap
…

    Mentions: OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.subposetInclusionWithin

  41. theorem OAI.Thomason.Construction.EndpointFiber.finite_attachment_piece line 922

    Source documentation

    A full finite-dimensional piece containing the attaching source has exactly the expected pushout, without assuming that inclusion preserves it.

    theorem finite_attachment_piece (e : Fin 2) {n : ℕ}
    {A B U X Y : Truncated.{0} (n + 1)}
    {i : A ⟶ B} {iU : A ⟶ U} {u : U ⟶ B}
    {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) (hiU : iU ≫ u = i)
    (pB : B ⟶ finiteInterval n) (pY : Y ⟶ finiteInterval n)
    (hi : i ≫ pB = finiteConstantLabel A e)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = finiteConstantLabel X e)
    (eU : U ≅ finiteLabelFiber pB e) (hu : eU.hom ≫ labelFiberInclusion pB e = u) :
    IsPushout iU a
      (eU.hom ≫ finiteLabelFiberMap pB pY e b hb)
      ((finiteConstantFiberIso X e).inv ≫
…
  42. def OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberInclusion line 972
  43. theorem OAI.Thomason.Construction.StrictOmegaCategory.finiteLabelFiberMap_inclusion line 976
  44. theorem OAI.Thomason.Construction.EndpointFiber.finite_piece_inclusion line 988
  45. theorem OAI.Thomason.Construction.EndpointFiber.finite_attachment_complement_iso line 999

    Source documentation

    The full fibre away from the old constant label is unchanged by the actual finite-dimensional pushout.

    theorem finite_attachment_complement_iso {n : ℕ} (e d : Fin 2) (hed : d ≠ e)
    {A B X Y : Truncated.{0} (n+1)}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) (pB : B ⟶ finiteInterval n) (pY : Y ⟶ finiteInterval n)
    (hi : i ≫ pB = finiteConstantLabel A d)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = finiteConstantLabel X d) :
    IsIso (finiteLabelFiberMap pB pY e b hb) := by
…