OAI/CategoryTheory/Thomason/Transfer/ThomasonQuillenBridge.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Semantic class identifications in the Kan–Quillen theorem

Goerss–Jardine, Theorems I.11.3–I.11.4 and Corollary II.8.6 identify the boundary and horn lifting classes with the geometric realization weak equivalences and Kan fibrations. Algebraic factorization, retract stability and two-out-of-three give the other model axioms.

  1. theorem OAI.Thomason.Construction.kanQuillenInput_of_remaining_semantics line 36

    Source documentation

    The semantic class identifications and source cancellation supply the Kan–Quillen model axioms.

    theorem kanQuillenInput_of_remaining_semantics
    (hpre : realizationWeakEquivalences.{0}.HasOfPrecompProperty realizationWeakEquivalences)
    (hb : I.rlp = J.rlp ⊓ realizationWeakEquivalences.{0})
    (hh : SSet.anodyneExtensions.{0} = monomorphisms SSet.{0} ⊓ realizationWeakEquivalences) :
    KanQuillenPublishedInput.{0} := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  2. theorem OAI.Thomason.Construction.kanQuillenInput_of_class_identifications line 49

    Source documentation

    The two semantic class identifications of the Kan–Quillen theorem suffice, using the homotopy-group proof of two-out-of-three.

    theorem kanQuillenInput_of_class_identifications
    (hb : I.rlp = J.rlp ⊓ realizationWeakEquivalences.{0})
    (hh : SSet.anodyneExtensions.{0} = monomorphisms SSet.{0} ⊓ realizationWeakEquivalences) :
    KanQuillenPublishedInput.{0} :=
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  3. theorem OAI.Thomason.Construction.boundary_class_of_anodyne_class line 76

    Source documentation

    The boundary identification follows from the anodyne identification, the explicit cylinder construction, and the two proved algebraic WFS.

    theorem boundary_class_of_anodyne_class
    (hh : SSet.anodyneExtensions.{0} = monomorphisms SSet.{0} ⊓ realizationWeakEquivalences) :
    I.rlp = J.rlp ⊓ realizationWeakEquivalences.{0} := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  4. theorem OAI.Thomason.Construction.kanQuillenInput_of_anodyne_class line 116

    Source documentation

    Only the anodyne/realization identification remains as a KQ input.

    theorem kanQuillenInput_of_anodyne_class
    (hh : SSet.anodyneExtensions.{0} = monomorphisms SSet.{0} ⊓ realizationWeakEquivalences) :
    KanQuillenPublishedInput.{0} :=
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  5. theorem OAI.Thomason.Construction.RightGrayInput.glue_stationary_cylinder line 143

    Source documentation

    A stationary cylinder descends across every pushout. The last two conclusions identify its endpoint maps on both pushout pieces.

    theorem glue_stationary_cylinder {A B X Y : StrictOmegaCategory.{0}}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) (P : G.cylinder.obj B ⟶ B)
    (hP : G.cylinder.map i ≫ P = G.projection.app A ≫ i) :
    ∃ Q : G.cylinder.obj Y ⟶ Y,
      G.cylinder.map b ≫ Q = P ≫ b ∧
      G.cylinder.map j ≫ Q = G.projection.app X ≫ j ∧
      (∀ δ, j ≫ ((G.endpoint δ).app Y ≫ Q) = j) ∧
      (∀ δ, b ≫ ((G.endpoint δ).app Y ≫ Q) = ((G.endpoint δ).app B ≫ P) ≫ b) := by
…
  6. theorem OAI.Thomason.Construction.RightGrayInput.glue_finite_stationary_cylinder line 208

    Source documentation

    Finite pushouts glue the ambient right Gray cylinders because their maps into a finite target are represented by a finite internal hom.

    theorem glue_finite_stationary_cylinder
    {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) (P : G.cylinder.obj B.val ⟶ B.val)
    (hP : G.cylinder.map i ≫ P = G.projection.app A.val ≫ i) :
    ∃ Q : G.cylinder.obj Y.val ⟶ Y.val,
      G.cylinder.map b ≫ Q = P ≫ b ∧
      G.cylinder.map j ≫ Q = G.projection.app X.val ≫ j ∧
      (∀ δ, (StrictOmegaCategory.inclusion (n + 1)).map j ≫
        ((G.endpoint δ).app Y.val ≫ Q) = (StrictOmegaCategory.inclusion (n + 1)).map j) ∧
      (∀ δ, (StrictOmegaCategory.inclusion (n + 1)).map b ≫
        ((G.endpoint δ).app Y.val ≫ Q) = ((G.endpoint δ).app B.val ≫ P) ≫
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion

  7. theorem OAI.Thomason.Construction.isPushout_over line 298

    Source documentation

    Compatible labels lift the given pushout itself to the slice.

    theorem isPushout_over (hp : IsPushout i a b j)
    (pA : A ⟶ L) (pB : B ⟶ L) (pX : X ⟶ L) (pY : Y ⟶ L)
    (hi : i ≫ pB = pA) (ha : a ≫ pX = pA)
    (hb : b ≫ pY = pB) (hj : j ≫ pY = pX) :
    IsPushout (Over.homMk i hi : Over.mk pA ⟶ Over.mk pB)
      (Over.homMk a ha : Over.mk pA ⟶ Over.mk pX)
      (Over.homMk b hb : Over.mk pB ⟶ Over.mk pY)
      (Over.homMk j hj : Over.mk pX ⟶ Over.mk pY) := by
…
  8. def OAI.Thomason.Construction.StrictOmegaCategory.constantLabel line 314

    Source documentation

    The constant strict label, including every positive-dimensional cell.

    def constantLabel (C : StrictOmegaCategory.{0}) (e : Fin 2) :
    C ⟶ StrictPoset.category (Fin 2) := orderedLabel (fun _ => e) (fun _ => le_rfl)

    Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.StrictOmegaCategory.orderedLabel

  9. theorem OAI.Thomason.Construction.StrictOmegaCategory.constantLabel_apply line 317
  10. def OAI.Thomason.Construction.StrictOmegaCategory.constantFiberIso line 321

    Source documentation

    The fibre of a constant label over its value is the entire original category.

    def constantFiberIso (C : StrictOmegaCategory.{0}) (e : Fin 2) :
    labelFiber (constantLabel C e) e ≅ C where
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.labelFiber, OAI.Thomason.Construction.StrictOmegaCategory.constantLabel

  11. theorem OAI.Thomason.Construction.StrictOmegaCategory.constantFiber_empty line 332

    Source documentation

    The other endpoint fibre of a constant label has no cells.

    theorem constantFiber_empty (C : StrictOmegaCategory.{0}) (e d : Fin 2) (hed : e ≠ d) :
    IsEmpty (labelFiber (constantLabel C e) d) := by
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.labelFiber, OAI.Thomason.Construction.StrictOmegaCategory.constantLabel

  12. theorem OAI.Thomason.Construction.PublishedLabelFiberInput.omega_pushout_fibers line 348

    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) :=
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category

  13. theorem OAI.Thomason.Construction.PublishedLabelFiberInput.omega_attaching_map_mono line 363

    Source documentation

    If the original map identifies its source with a whole label fibre, then the attached copy of X is again precisely that full fibre. In particular the arbitrary attaching map creates no new identifications in X.

    theorem omega_attaching_map_mono (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)
    (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)
    [IsIso (labelFiberMap (constantLabel A e) pB e i hi)] : Mono j := by
…

    Mentions: OAI.Thomason.Construction.StrictPoset.category

  14. theorem OAI.Thomason.Construction.PublishedLabelFiberInput.finite_pushout_fibers line 385

    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))
…
  15. theorem OAI.Thomason.Construction.StrictOmegaCategory.pushout_objects_covered line 419

    Source documentation

    Every object of an arbitrary strict pushout comes from one of its two legs.

    theorem pushout_objects_covered {A B X Y : StrictOmegaCategory.{0}}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) (y : Objects Y) :
    (∃ x : Objects B, b.toOneFunctor.obj x = y) ∨
      ∃ x : Objects X, j.toOneFunctor.obj x = y :=
…

    Mentions: OAI.Thomason.Construction.StrictOmegaCategory.Objects

  16. theorem OAI.Thomason.Construction.StrictOmegaCategory.pushout_label_cover line 428

    Source documentation

    Binary object covers survive attachment even when the attaching functor identifies old objects or cells.

    theorem pushout_label_cover {A B X Y : StrictOmegaCategory.{0}}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) (p q : Y ⟶ StrictPoset.category (Fin 2)) (e : Fin 2)
    (hb : ∀ x : Objects B, p.toFun (b.toFun x.val) = StrictPoset.identity e ∨
      q.toFun (b.toFun x.val) = StrictPoset.identity e)
    (hj : ∀ x : Objects X, p.toFun (j.toFun x.val) = StrictPoset.identity e ∨
      q.toFun (j.toFun x.val) = StrictPoset.identity e) :
    ∀ y : Objects Y, p.toFun y.val = StrictPoset.identity e ∨
      q.toFun y.val = StrictPoset.identity e := by
…

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

  17. theorem OAI.Thomason.Construction.StrictOmegaCategory.finite_pushout_label_cover line 443

    Source documentation

    The object-cover argument also uses genuine finite-category pushouts.

    theorem finite_pushout_label_cover {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) (p q : Y.val ⟶ StrictPoset.category (Fin 2)) (e : Fin 2)
    (hb : ∀ x : Objects B.val, p.toFun (b.toFun x.val) = StrictPoset.identity e ∨
      q.toFun (b.toFun x.val) = StrictPoset.identity e)
    (hj : ∀ x : Objects X.val, p.toFun (j.toFun x.val) = StrictPoset.identity e ∨
      q.toFun (j.toFun x.val) = StrictPoset.identity e) :
    ∀ y : Objects Y.val, p.toFun y.val = StrictPoset.identity e ∨
      q.toFun y.val = StrictPoset.identity e := by
…

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

  18. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.pushout_sieve_street_cover line 466

    Source documentation

    The post-attachment sieve cover is a cover of actual Street simplices.

    theorem pushout_sieve_street_cover
    {A B X Y : StrictOmegaCategory.{0}}
    {i : A ⟶ B} {a : A ⟶ X} {b : B ⟶ Y} {j : X ⟶ Y}
    (hp : IsPushout i a b j) (p q : Y ⟶ StrictPoset.category (Fin 2))
    (hb : ∀ x : Objects B, p.toFun (b.toFun x.val) = StrictPoset.identity 0 ∨
      q.toFun (b.toFun x.val) = StrictPoset.identity 0)
    (hj : ∀ x : Objects X, p.toFun (j.toFun x.val) = StrictPoset.identity 0 ∨
      q.toFun (j.toFun x.val) = StrictPoset.identity 0) :
    h.fiberStreetSubcomplex p 0 ⊔ h.fiberStreetSubcomplex q 0 = ⊤ :=
…

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

  19. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_pushout_sieve_street_cover line 479

    Source documentation

    No preservation of pushouts by the inclusion into omega-categories is needed for the positive finite-dimensional Street cover.

    theorem finite_pushout_sieve_street_cover
    {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) (p q : Y.val ⟶ StrictPoset.category (Fin 2))
    (hb : ∀ x : Objects B.val, p.toFun (b.toFun x.val) = StrictPoset.identity 0 ∨
      q.toFun (b.toFun x.val) = StrictPoset.identity 0)
    (hj : ∀ x : Objects X.val, p.toFun (j.toFun x.val) = StrictPoset.identity 0 ∨
      q.toFun (j.toFun x.val) = StrictPoset.identity 0) :
    h.fiberStreetSubcomplex p 0 ⊔ h.fiberStreetSubcomplex q 0 = ⊤ :=
…

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

  20. abbrev OAI.Thomason.Construction.SimplicialSpan.middle line 507
  21. def OAI.Thomason.Construction.SimplicialSpan.toMiddle line 510
  22. def OAI.Thomason.Construction.SimplicialSpan.fromMiddle line 514
  23. def OAI.Thomason.Construction.SimplicialSpan.relativeToMiddle line 519
  24. theorem OAI.Thomason.Construction.SimplicialSpan.inl_toMiddle line 524
  25. theorem OAI.Thomason.Construction.SimplicialSpan.inr_toMiddle line 528
  26. theorem OAI.Thomason.Construction.SimplicialSpan.inl_fromMiddle line 532
  27. theorem OAI.Thomason.Construction.SimplicialSpan.inr_fromMiddle line 536
  28. theorem OAI.Thomason.Construction.SimplicialSpan.inl_relativeToMiddle line 540
  29. theorem OAI.Thomason.Construction.SimplicialSpan.inr_relativeToMiddle line 544
  30. theorem OAI.Thomason.Construction.SimplicialSpan.toMiddle_isPushout line 548
  31. theorem OAI.Thomason.Construction.SimplicialSpan.fromMiddle_isPushout line 561
  32. theorem OAI.Thomason.Construction.SimplicialSpan.toMiddle_fromMiddle line 578
  33. theorem OAI.Thomason.Construction.SimplicialSpan.relativeB_weak line 584

    Source documentation

    The relative B map is acyclic when the A and B maps are weak and the A and relative maps are cofibrations.

    theorem relativeB_weak {X Y : Diagram} (f : X ⟶ Y)
    (kq : KanQuillenPublishedInput.{0}) (hi : Cofibration f)
    (ha : realizationWeakEquivalences f.a) (hb : realizationWeakEquivalences f.b) :
    realizationWeakEquivalences (relativeB f) := by
…

    Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram, OAI.Thomason.Construction.SimplicialSpan.Cofibration, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.SimplicialSpan.relativeB

  34. theorem OAI.Thomason.Construction.SimplicialSpan.pushoutMap_weak_of_cofibration line 599

    Source documentation

    A span cofibration which is weak at each object induces a weak equivalence of the actual simplicial pushouts. This derives the comparison from KQ.

    theorem pushoutMap_weak_of_cofibration {X Y : Diagram} (f : X ⟶ Y)
    (kq : KanQuillenPublishedInput.{0}) (hi : Cofibration f)
    (ha : realizationWeakEquivalences f.a) (hb : realizationWeakEquivalences f.b)
    (hc : realizationWeakEquivalences f.c) : realizationWeakEquivalences (pushoutMap f) := by
…

    Mentions: OAI.Thomason.Construction.SimplicialSpan.Diagram, OAI.Thomason.Construction.SimplicialSpan.Cofibration, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.SimplicialSpan.pushoutMap

  35. theorem OAI.Thomason.Construction.rlp_map_eq_inverseImage line 636

    Source documentation

    The two actual adjoints transport a right lifting class to the image of its generators, including the isomorphisms in MorphismProperty.map.

    theorem rlp_map_eq_inverseImage {C D : Type*} [Category* C] [Category* D]
    {L : C ⥤ D} {R : D ⥤ C} (adj : L ⊣ R) (P : MorphismProperty C) :
    (P.map L).rlp = P.rlp.inverseImage R := by
…
  36. def OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonGeneratingCofibrations line 654

    Source documentation

    Twice-subdivided boundary generators, categorified by the actual left adjoint.

    noncomputable def thomasonGeneratingCofibrations : MorphismProperty StrictOmegaCategory.{0} :=
…
  37. def OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonGeneratingAcyclicCofibrations line 658

    Source documentation

    Twice-subdivided horn generators, categorified by the actual left adjoint.

    noncomputable def thomasonGeneratingAcyclicCofibrations : MorphismProperty StrictOmegaCategory.{0} :=
…
  38. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonFibrations_eq_generating_rlp line 662

    Source documentation

    Horn lifting after Ex² N is exactly lifting against the strict horn generators.

    theorem thomasonFibrations_eq_generating_rlp :
    h.thomasonFibrations = h.thomasonGeneratingAcyclicCofibrations.rlp :=
…
  39. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomason_trivialFibrations_eq_generating_rlp line 668

    Source documentation

    Boundary lifting against actual strict generators detects precisely fibrations that are actual Street-nerve weak equivalences.

    theorem thomason_trivialFibrations_eq_generating_rlp
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences.{0} (canonicalExtension.app X)) :
    h.thomasonFibrations ⊓ h.streetWeakEquivalences =
      h.thomasonGeneratingCofibrations.rlp :=
…
  40. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonCofibrations_eq_generating_llp_rlp line 678

    Source documentation

    The prescribed cofibrations are the left lifting class generated by these boundary maps, before any model structure is asserted.

    theorem thomasonCofibrations_eq_generating_llp_rlp
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences.{0} (canonicalExtension.app X)) :
    h.thomasonCofibrations = h.thomasonGeneratingCofibrations.rlp.llp :=
…
  41. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.generatingCofibrations_le_cofibrations line 685

    Source documentation

    In particular the boundary generators are genuine prescribed cofibrations.

    theorem generatingCofibrations_le_cofibrations
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences.{0} (canonicalExtension.app X)) :
    h.thomasonGeneratingCofibrations ≤ h.thomasonCofibrations := by
…
  42. def OAI.Thomason.Construction.FiniteReflectionInput.thomasonRight line 699
  43. def OAI.Thomason.Construction.FiniteReflectionInput.thomasonFibrations line 702
  44. def OAI.Thomason.Construction.FiniteReflectionInput.thomasonWeakEquivalences line 706
  45. def OAI.Thomason.Construction.FiniteReflectionInput.thomasonGeneratingCofibrations line 710
  46. def OAI.Thomason.Construction.FiniteReflectionInput.thomasonGeneratingAcyclicCofibrations line 714
  47. theorem OAI.Thomason.Construction.FiniteReflectionInput.thomasonFibrations_eq_generating_rlp line 719

    Source documentation

    The actual finite-dimensional horn lifting criterion.

    theorem thomasonFibrations_eq_generating_rlp :
    thomasonFibrations (n := n) h = (r.thomasonGeneratingAcyclicCofibrations h).rlp :=
…

    Mentions: OAI.Thomason.Construction.FiniteReflectionInput.thomasonFibrations

  48. theorem OAI.Thomason.Construction.FiniteReflectionInput.thomason_trivialFibrations_eq_generating_rlp line 725

    Source documentation

    In every positive finite dimension, strict boundary lifting is equivalent to horn lifting together with the actual Street weak-equivalence condition.

    theorem thomason_trivialFibrations_eq_generating_rlp
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X, realizationWeakEquivalences.{0} (canonicalExtension.app X)) :
    thomasonFibrations (n := n) h ⊓ thomasonWeakEquivalences (n := n) h =
…

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

  49. structure OAI.Thomason.Construction.ProperCombinatorialAxioms line 766

    Source documentation

    The model axioms and proper/local-presentability conclusions needed from the published abstract transfer theorem. This is data to be proved or supplied by a precisely stated published implication, not a global axiom.

    structure ProperCombinatorialAxioms (C : Type u) [Category.{v} C]
    (W F : MorphismProperty C) : Prop where
…
  50. def OAI.Thomason.Construction.ProperCombinatorialAxioms.model line 782

    Source documentation

    Assemble the genuine model-category structure with the prescribed classes.

    noncomputable def model (a : ProperCombinatorialAxioms C W F)
    [W.HasTwoOutOfThreeProperty] : ModelCategory C := by
…

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms

  51. theorem OAI.Thomason.Construction.ProperCombinatorialAxioms.model_weakEquivalences line 797

    Source documentation

    The weak class of this model is the original semantic class.

    theorem model_weakEquivalences (a : ProperCombinatorialAxioms C W F)
    [W.HasTwoOutOfThreeProperty] :
    @weakEquivalences C _ (a.model.categoryWithWeakEquivalences) = W := rfl

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms

  52. theorem OAI.Thomason.Construction.ProperCombinatorialAxioms.model_fibrations line 802

    Source documentation

    Its fibrations are the prescribed right-adjoint lifting class.

    theorem model_fibrations (a : ProperCombinatorialAxioms C W F)
    [W.HasTwoOutOfThreeProperty] :
    @fibrations C _ (a.model.categoryWithFibrations) = F := rfl

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms

  53. theorem OAI.Thomason.Construction.ProperCombinatorialAxioms.model_cofibrations line 807

    Source documentation

    Its cofibrations are precisely the left lifting class specified in the paper.

    theorem model_cofibrations (a : ProperCombinatorialAxioms C W F)
    [W.HasTwoOutOfThreeProperty] :
    @cofibrations C _ (a.model.categoryWithCofibrations) = (F ⊓ W).llp := rfl
…

    Mentions: OAI.Thomason.Construction.ProperCombinatorialAxioms

  54. theorem OAI.Thomason.Construction.ThomasonAdjunction.left_preserves_cofibrations line 841

    Source documentation

    The actual left adjoint takes every simplicial monomorphism to a cofibration for the prescribed Thomason lifting classes.

    theorem left_preserves_cofibrations {X Y : SSet.{0}} (f : X ⟶ Y) [Mono f] :
    (J.rlp.inverseImage (N ⋙ SSet.ex ⋙ SSet.ex) ⊓
      realizationWeakEquivalences.inverseImage N).llp (L.map f) := by
…
  55. theorem OAI.Thomason.Construction.ThomasonAdjunction.left_preserves_trivialCofibrations line 858

    Source documentation

    Actual KQ trivial cofibrations become trivial Thomason cofibrations.

    theorem left_preserves_trivialCofibrations {X Y : SSet.{0}} (f : X ⟶ Y) [Mono f]
    (hf : realizationWeakEquivalences f) :
    ((J.rlp.inverseImage (N ⋙ SSet.ex ⋙ SSet.ex) ⊓
      realizationWeakEquivalences.inverseImage N).llp ⊓
        realizationWeakEquivalences.inverseImage N) (L.map f) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  56. theorem OAI.Thomason.Construction.ThomasonAdjunction.left_preserves_weakEquivalences line 881

    Source documentation

    Brown's factorization upgrades trivial-cofibration preservation to preservation of every actual simplicial realization weak equivalence.

    theorem left_preserves_weakEquivalences {X Y : SSet.{0}} (f : X ⟶ Y)
    (hf : realizationWeakEquivalences f) :
    realizationWeakEquivalences (N.map (L.map f)) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences