OAI/CategoryTheory/Thomason/Transfer/SimplicialRangeGluing.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Couniversality for finite posets in omega dimension

The induction is over the ambient finite poset. The greatest-new case uses the constructed stationary Gray prisms; otherwise two maximal deletions and their intersection give three smaller arbitrary attachments. Their actual full-fibre cover and the simplicial gluing bridge complete the step.

  1. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_poset_couniversal line 32

    Source documentation

    Every categorified finite-poset sieve with a right-adjoint retraction is an actual couniversal Street weak equivalence. No assumption on the target or attaching functor is made.

    theorem finite_poset_couniversal
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P] (A : Set P) (R : SieveRetraction A) :
    h.CouniversalStreetWeakEquivalence (h.posetMap (subposetInclusion A)) := 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

  2. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_poset_pushout_weakEquivalence line 76

    Source documentation

    The finite-poset theorem applied to a specified actual attaching pushout.

    theorem finite_poset_pushout_weakEquivalence
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P] (A : Set P) (R : SieveRetraction 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) : h.streetWeakEquivalences j :=
…

    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

  3. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_couniversal_precompose_iso line 108

    Source documentation

    Renaming the finite attaching source preserves couniversality.

    theorem finite_couniversal_precompose_iso {A A' B : Truncated.{0} (n + 1)}
    (e : A' ≅ A) (i : A ⟶ B) (hi : h.FiniteCouniversalStreetWeakEquivalence n i) :
    h.FiniteCouniversalStreetWeakEquivalence n (e.hom ≫ i) := by
…
  4. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_couniversal_of_isIso line 117

    Source documentation

    A finite-category isomorphism remains a Street equivalence under attachment.

    theorem finite_couniversal_of_isIso (kq : KanQuillenPublishedInput.{0})
    {A B : Truncated.{0} (n + 1)} (i : A ⟶ B) [IsIso (C := Truncated (n + 1)) i] :
…
  5. theorem OAI.Thomason.Construction.FiniteReflectionInput.finite_poset_couniversal line 134

    Source documentation

    Every finite-poset sieve retraction is couniversally a Street weak equivalence in dimension n + 1, with arbitrary attaching maps and targets.

    theorem finite_poset_couniversal
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P] (A : Set P) (R : SieveRetraction A) :
    h.FiniteCouniversalStreetWeakEquivalence n
      (r.reflect.map (h.posetMap (subposetInclusion A))) := by
…

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

  6. theorem OAI.Thomason.Construction.FiniteReflectionInput.finite_poset_pushout_weakEquivalence line 188

    Source documentation

    The resulting bridge for a specified finite-dimensional pushout.

    theorem finite_poset_pushout_weakEquivalence
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P] (A : Set P) (R : SieveRetraction A)
    {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) :
    h.streetWeakEquivalences ((StrictOmegaCategory.inclusion (n + 1)).map j) :=
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.SieveRetraction, OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.StrictOmegaCategory.inclusion

  7. theorem OAI.Thomason.Construction.KanQuillenPublishedInput.pushout_weakEquivalence line 223

    Source documentation

    Pushouts of monomorphic realization weak equivalences remain weak equivalences.

    theorem pushout_weakEquivalence (kq : KanQuillenPublishedInput.{0})
    {A B X Y : SSet.{0}} {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) [Mono i] (wi : realizationWeakEquivalences i) :
    realizationWeakEquivalences j := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  8. def OAI.Thomason.Construction.nervePushoutComparison line 243

    Source documentation

    The canonical comparison retains the two original structure maps.

    noncomputable def nervePushoutComparison (hp : IsPushout i a b j) :
    pushout (N.map i) (N.map a) ⟶ N.obj Y :=
…
  9. theorem OAI.Thomason.Construction.nervePushoutComparison_weakEquivalence line 250

    Source documentation

    Once both attaching legs are weak, the canonical comparison is weak. This applies to actual nerves and to arbitrary attaching maps.

    theorem nervePushoutComparison_weakEquivalence (kq : KanQuillenPublishedInput.{0})
    (hp : IsPushout i a b j) [Mono (N.map i)]
    (wi : realizationWeakEquivalences (N.map i))
    (wj : realizationWeakEquivalences (N.map j)) :
    realizationWeakEquivalences (nervePushoutComparison N hp) := by
…

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

  10. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_poset_attachment_comparison line 268

    Source documentation

    The comparison for every finite-poset sieve retraction in omega dimension.

    theorem finite_poset_attachment_comparison
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P] (A : Set P) (R : SieveRetraction 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

  11. theorem OAI.Thomason.Construction.FiniteReflectionInput.posetSieve_nerve_mono line 292

    Source documentation

    The original reflected sieve has monomorphic Street nerve.

    theorem posetSieve_nerve_mono (s : PublishedPosetSieveInput h)
    {P : Type} [PartialOrder P] [Finite P] (A : Set P) (hA : IsLowerSet A) :
    Mono ((h.finiteStreetNerve (n + 1)).map (r.reflect.map (h.posetMap (subposetInclusion A)))) := by
…

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

  12. theorem OAI.Thomason.Construction.FiniteReflectionInput.finite_poset_attachment_comparison line 312

    Source documentation

    The same canonical comparison is weak for finite-dimensional retracting attachments.

    theorem finite_poset_attachment_comparison
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] [Finite P] (A : Set P) (R : SieveRetraction A)
    {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) :
    realizationWeakEquivalences (nervePushoutComparison (h.finiteStreetNerve (n + 1)) hp) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, 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

  13. theorem OAI.Thomason.Construction.nervePushoutComparison_weak_iff line 350
  14. theorem OAI.Thomason.Construction.nervePushoutComparison_inl line 358
  15. theorem OAI.Thomason.Construction.nervePushoutComparison_inr line 364
  16. theorem OAI.Thomason.Construction.nervePushoutComparison_weak_of_cosieve_cover line 372

    Source documentation

    A weak comparison for the containing piece extends over a two-piece cover when the other piece and the intersection stay unchanged.

    theorem nervePushoutComparison_weak_of_cosieve_cover
    (g : PublishedSimplicialGluingInput)
    {A Z B T U X V Y : C}
    {i : A ⟶ Z} {u : Z ⟶ B} {t : T ⟶ Z} {v : T ⟶ U} {c : U ⟶ B}
    {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    {d : Z ⟶ V} {e : X ⟶ V} {k : V ⟶ Y}
    (hp : IsPushout (i ≫ u) a b j) (hz : IsPushout i a d e)
    (hk : d ≫ k = u ≫ b) (he : e ≫ k = j)
    (hs : IsPushout (N.map t) (N.map v) (N.map u) (N.map c))
    (ht : IsPushout (N.map (t ≫ d)) (N.map v) (N.map k) (N.map (c ≫ b)))
    [Mono (N.map v)]
    (wz : realizationWeakEquivalences (nervePushoutComparison N hz)) :
…

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

  17. theorem OAI.Thomason.Construction.extendedNervePushoutComparison_weakEquivalence line 463

    Source documentation

    The canonical comparison for Ex²N is weak under the same acyclic-attachment criterion as the original nerve.

    theorem extendedNervePushoutComparison_weakEquivalence (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X : SSet.{0}, realizationWeakEquivalences (canonicalExtension.app X))
    (hp : IsPushout i a b j) [Mono (N.map i)]
    (wi : realizationWeakEquivalences (N.map i))
    (wj : realizationWeakEquivalences (N.map j)) :
    realizationWeakEquivalences (nervePushoutComparison (N ⋙ SSet.ex ⋙ SSet.ex) hp) := by
…

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

  18. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_poset_extended_attachment_comparison line 485

    Source documentation

    Finite-poset attachments have weak comparison under the actual omega Thomason right adjoint, with the interval identity supplied by its proof.

    theorem finite_poset_extended_attachment_comparison
    (G : RightGrayInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X : SSet.{0}, realizationWeakEquivalences (canonicalExtension.app X))
    {P : Type} [PartialOrder P] [Finite P] (A : Set P) (R : SieveRetraction 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 ⋙ SSet.ex ⋙ SSet.ex) hp) := by
…

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

  19. theorem OAI.Thomason.Construction.FiniteReflectionInput.finite_poset_extended_attachment_comparison line 512

    Source documentation

    The same actual-right-adjoint comparison is weak in every positive finite dimension.

    theorem finite_poset_extended_attachment_comparison
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X : SSet.{0}, realizationWeakEquivalences (canonicalExtension.app X))
    {P : Type} [PartialOrder P] [Finite P] (A : Set P) (R : SieveRetraction A)
    {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) :
    realizationWeakEquivalences
      (nervePushoutComparison (h.finiteStreetNerve (n + 1) ⋙ SSet.ex ⋙ SSet.ex) hp) := by
…

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

  20. structure OAI.Thomason.Construction.PublishedFinitePosetUnitInput line 560

    Source documentation

    Only the published unit comparison on finite posets, in the actual adjunctions.

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

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

  21. structure OAI.Thomason.Construction.PublishedThomasonReduction line 569

    Source documentation

    The precise published reduction, leaving both (d') and (e) as premises. No model conclusion is assumed without those premises.

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

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

  22. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.conditional_model_axioms line 593

    Source documentation

    Conditional proper combinatorial model axioms in omega dimension. The new couniversality condition is discharged by the constructed prisms and finite-poset induction; only precisely cited published inputs remain.

    theorem conditional_model_axioms
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    (units : PublishedFinitePosetUnitInput h) (transfer : PublishedThomasonReduction h) :
    ProperCombinatorialAxioms StrictOmegaCategory.{0} h.streetWeakEquivalences h.thomasonFibrations := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.PublishedFinitePosetUnitInput, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.ProperCombinatorialAxioms

  23. theorem OAI.Thomason.Construction.FiniteReflectionInput.conditional_model_axioms line 615

    Source documentation

    The same conditional proper combinatorial model axioms in dimension n+1.

    theorem conditional_model_axioms
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    (units : PublishedFinitePosetUnitInput h) (transfer : PublishedThomasonReduction h) :
    ProperCombinatorialAxioms (StrictOmegaCategory.Truncated.{0} (n + 1))
      (thomasonWeakEquivalences (n := n) h) (thomasonFibrations (n := n) h) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.PublishedFinitePosetUnitInput, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.ProperCombinatorialAxioms, OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences, OAI.Thomason.Construction.FiniteReflectionInput.thomasonFibrations

  24. def OAI.Thomason.Construction.nerveLocalizer line 649

    Source documentation

    Any nerve with its inverse-image weak equivalences is a morphism of localizers.

    noncomputable def nerveLocalizer {C : Type*} [Category* C] (N : C ⥤ SSet.{0}) :
    LocalizerMorphism (realizationWeakEquivalences.inverseImage N) realizationWeakEquivalences :=
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  25. def OAI.Thomason.Construction.extensionLocalizer line 654

    Source documentation

    The actual extension functor preserves realization weak equivalences.

    noncomputable def extensionLocalizer (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences (canonicalExtension.app X)) :
    LocalizerMorphism realizationWeakEquivalences realizationWeakEquivalences where
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  26. theorem OAI.Thomason.Construction.extensionLocalizer_isLocalizedEquivalence line 664

    Source documentation

    Extension induces an equivalence on the actual localization at realization W.

    theorem extensionLocalizer_isLocalizedEquivalence (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences (canonicalExtension.app X)) :
    (extensionLocalizer kq hj).IsLocalizedEquivalence := by
…

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

  27. def OAI.Thomason.Construction.thomasonRightLocalizer line 680

    Source documentation

    The morphism of localizers underlying the actual Thomason right adjoint.

    noncomputable def thomasonRightLocalizer {C : Type*} [Category* C] (N : C ⥤ SSet.{0})
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences (canonicalExtension.app X)) :
    LocalizerMorphism (realizationWeakEquivalences.inverseImage N) realizationWeakEquivalences :=
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  28. theorem OAI.Thomason.Construction.thomasonRightLocalizer_isLocalizedEquivalence line 687

    Source documentation

    A Street-nerve equivalence of homotopy categories passes to Ex² N.

    theorem thomasonRightLocalizer_isLocalizedEquivalence {C : Type*} [Category* C]
    (N : C ⥤ SSet.{0}) (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences (canonicalExtension.app X))
    (hN : (nerveLocalizer N).IsLocalizedEquivalence) :
    (thomasonRightLocalizer N kq hj).IsLocalizedEquivalence := by
…

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

  29. structure OAI.Thomason.Construction.PublishedStreetLocalizationInput line 699

    Source documentation

    Gagna (2018), Theorem 5.6: the Street nerve induces an equivalence of homotopy categories for every positive finite dimension and omega. Original source: https://arxiv.org/pdf/1612.04450v2, p.12.

    structure PublishedStreetLocalizationInput (h : NormalizedSimplexIdentities) : Prop where
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities

  30. theorem OAI.Thomason.Construction.localizer_equivalence_of_weak_unit_counit line 730

    Source documentation

    An adjunction whose unit and counit are weak gives an equivalence between the actual localized categories.

    theorem localizer_equivalence_of_weak_unit_counit
    (hu : ∀ X, W₂ (adj.unit.app X)) (hc : ∀ X, W₁ (adj.counit.app X)) :
    Φ.IsLocalizedEquivalence where
…
  31. theorem OAI.Thomason.Construction.right_counit_weak_of_unit line 756

    Source documentation

    The triangle identity forces the right-adjoint image of the counit weak as soon as the actual unit is weak.

    theorem right_counit_weak_of_unit
    {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D]
    {L : C ⥤ D} {R : D ⥤ C} (adj : L ⊣ R)
    (W : MorphismProperty C) [W.HasTwoOutOfThreeProperty] [W.ContainsIdentities]
    (hu : ∀ X, W (adj.unit.app X)) (Y : D) :
    W (R.map (adj.counit.app Y)) := by
…
  32. structure OAI.Thomason.Construction.ThomasonModelResult line 791

    Source documentation

    The main conclusion in the usual derived formulation of Quillen equivalence. Weak equivalences, fibrations, and both generators are fixed by the actual Street nerve and twice-subdivided left adjoint.

    structure ThomasonModelResult {C : Type 1} [Category.{0} C]
    (L : SSet.{0} ⥤ C) (N : C ⥤ SSet.{0})
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences (canonicalExtension.app X)) where
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  33. def OAI.Thomason.Construction.ThomasonModelResult.model line 813

    Source documentation

    The conditional result supplies a genuine Mathlib model category.

    noncomputable def model : ModelCategory C := by
…
  34. theorem OAI.Thomason.Construction.ThomasonModelResult.cofibrations_eq_generated line 818

    Source documentation

    Its cofibrations are generated by the actual twice-subdivided boundaries.

    theorem cofibrations_eq_generated :
    @cofibrations C _ m.model.categoryWithCofibrations = (I.map L).rlp.llp := by
…
  35. theorem OAI.Thomason.Construction.ThomasonModelResult.right_preserves_trivialFibrations line 826

    Source documentation

    The right adjoint preserves trivial fibrations for the actual KQ classes.

    theorem right_preserves_trivialFibrations :
    (J.rlp.inverseImage (N ⋙ SSet.ex ⋙ SSet.ex) ⊓ realizationWeakEquivalences.inverseImage N) ≤
      (J.rlp ⊓ realizationWeakEquivalences).inverseImage (N ⋙ SSet.ex ⋙ SSet.ex) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  36. theorem OAI.Thomason.Construction.ThomasonModelResult.right_preserves_fibrations line 835

    Source documentation

    Right fibrations are preserved by their prescribed definition.

    theorem right_preserves_fibrations :
    J.rlp.inverseImage (N ⋙ SSet.ex ⋙ SSet.ex) ≤
      J.rlp.inverseImage (N ⋙ SSet.ex ⋙ SSet.ex) := le_rfl
…
  37. def OAI.Thomason.Construction.NormalizedSimplexIdentities.conditional_main line 858

    Source documentation

    The conditional main model and Quillen-equivalence conclusion in omega dimension.

    noncomputable def conditional_main
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences (canonicalExtension.app X))
    (units : PublishedFinitePosetUnitInput h) (transfer : PublishedThomasonReduction h)
    (loc : PublishedStreetLocalizationInput h) :
    ThomasonModelResult h.thomasonLeft h.streetNerve kq hj where
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.PublishedFinitePosetUnitInput, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.PublishedStreetLocalizationInput, OAI.Thomason.Construction.ThomasonModelResult

  38. def OAI.Thomason.Construction.FiniteReflectionInput.conditional_main line 881

    Source documentation

    The conditional main theorem in each positive finite dimension n+1.

    noncomputable def conditional_main
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences (canonicalExtension.app X))
    (units : PublishedFinitePosetUnitInput h) (transfer : PublishedThomasonReduction h)
    (loc : PublishedStreetLocalizationInput h) :
    ThomasonModelResult (r.thomasonLeft h) (h.finiteStreetNerve (n + 1)) kq hj where
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.PublishedFinitePosetUnitInput, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.PublishedStreetLocalizationInput, OAI.Thomason.Construction.ThomasonModelResult

  39. theorem OAI.Thomason.Construction.conditional_main_all_dimensions line 904

    Source documentation

    The main result, simultaneously for omega and all positive finite dimensions, conditional only on the explicitly stated published inputs.

    theorem conditional_main_all_dimensions
    (h : NormalizedSimplexIdentities) [StrictColimitsInput]
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (r : ∀ n, FiniteReflectionInput n)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (s : PublishedPosetSieveInput h)
    (g : PublishedSimplicialGluingInput)
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences (canonicalExtension.app X))
    (units : PublishedFinitePosetUnitInput h) (transfer : PublishedThomasonReduction h)
    (loc : PublishedStreetLocalizationInput h) :
    Nonempty (ThomasonModelResult h.thomasonLeft h.streetNerve kq hj) ∧
…

    Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictColimitsInput, OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.FiniteReflectionInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedPosetSieveInput, OAI.Thomason.Construction.PublishedSimplicialGluingInput, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.PublishedFinitePosetUnitInput, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.PublishedStreetLocalizationInput, OAI.Thomason.Construction.ThomasonModelResult

  40. theorem OAI.Thomason.Construction.simplicial_isPushout_of_ranges line 940

    Source documentation

    A square of monomorphisms is a pushout when its two images cover the target and their intersection is the image of the common source.

    theorem simplicial_isPushout_of_ranges
    {I S T P : SSet.{0}} (i : I ⟶ S) (j : I ⟶ T) (b : S ⟶ P) (c : T ⟶ P)
    [Mono b] [Mono c] [Mono (i ≫ b)] (hw : i ≫ b = j ≫ c)
    (hcover : SSet.Subcomplex.range b ⊔ SSet.Subcomplex.range c = ⊤)
    (hinter : SSet.Subcomplex.range (i ≫ b) =
      SSet.Subcomplex.range b ⊓ SSet.Subcomplex.range c) : IsPushout i j b c := by
…
  41. instance OAI.Thomason.Construction.nerve_subposetInclusion_mono line 966

    Source documentation

    The original nerve map of a full subposet is monic.

    instance nerve_subposetInclusion_mono {P : Type} [PartialOrder P] (A : Set P) :
    Mono (nerveMap (subposetInclusion A).monotone.functor) := by
…

    Mentions: OAI.Thomason.Construction.subposetInclusion

  42. theorem OAI.Thomason.Construction.nerve_subposetInclusion_range line 976
  43. def OAI.Thomason.Construction.interLeft line 982
  44. def OAI.Thomason.Construction.interRight line 986
  45. theorem OAI.Thomason.Construction.interLeft_comp line 990
  46. theorem OAI.Thomason.Construction.interRight_comp line 993
  47. theorem OAI.Thomason.Construction.sieve_nerve_maps_isPushout line 997

    Source documentation

    The full-sieve cover is a pushout of the actual ordinary nerve maps.

    theorem sieve_nerve_maps_isPushout {P : Type} [PartialOrder P]
    (A B : Set P) (hA : IsLowerSet A) (hB : IsLowerSet B)
    (hcover : ∀ x, x ∈ A ∨ x ∈ B) :
    IsPushout (nerveMap (interLeft A B).monotone.functor)
      (nerveMap (interRight A B).monotone.functor)
      (nerveMap (subposetInclusion A).monotone.functor)
      (nerveMap (subposetInclusion B).monotone.functor) := by
…

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