OAI/CategoryTheory/Thomason/Gray/GrayFinitePosetUnits.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite-poset unit comparisons from the strict Gray input alone

Geometric gluing and direct realization of the Gray prisms remove every Kan–Quillen hypothesis from these unit comparisons. The exact right Gray and finite internal-hom truncation inputs remain explicit.

  1. theorem OAI.Thomason.Construction.RelativePrismData.weakEquivalence_iff_direct line 24
  2. theorem OAI.Thomason.Construction.nerve_greatest_point_weakEquivalences_direct line 39
  3. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.unit_of_point_iso_direct line 54
  4. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.categorified_greatest_point_weakEquivalences_direct line 64

    Source documentation

    The same contraction is weak after actual strict categorification.

    theorem categorified_greatest_point_weakEquivalences_direct
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)

    {P : Type} [PartialOrder P] (x : P) (hx : ∀ y, y ≤ x) :
    h.streetWeakEquivalences (h.posetMap (posetFromPoint x)) ∧
      h.streetWeakEquivalences (h.posetMap (posetToPoint P)) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.posetFromPoint, OAI.Thomason.Construction.posetToPoint

  5. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.unit_greatestElement_direct line 86

    Source documentation

    The finite-poset unit input is proved here for every greatest-element poset; finiteness is not needed in this case.

    theorem unit_greatestElement_direct (G : RightGrayInput h)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    {P : Type} [PartialOrder P] (x : P) (hx : ∀ y, y ≤ x) :
    realizationWeakEquivalences (h.categorificationAdjunction.unit.app (nerve P)) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.realizationWeakEquivalences

  6. theorem OAI.Thomason.Construction.FiniteReflectionInput.unit_of_point_iso_direct line 103
  7. theorem OAI.Thomason.Construction.FiniteReflectionInput.categorified_greatest_point_weakEquivalences_direct line 114

    Source documentation

    Reflection of the strict contraction gives actual finite Street weak equivalences on both the point inclusion and the collapse.

    theorem categorified_greatest_point_weakEquivalences_direct
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    {P : Type} [PartialOrder P] (x : P) (hx : ∀ y, y ≤ x) :
    realizationWeakEquivalences ((h.finiteStreetNerve (n + 1)).map
      (r.reflect.map (h.posetMap (posetFromPoint x)))) ∧
    realizationWeakEquivalences ((h.finiteStreetNerve (n + 1)).map
      (r.reflect.map (h.posetMap (posetToPoint P)))) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.posetFromPoint, OAI.Thomason.Construction.posetToPoint

  8. theorem OAI.Thomason.Construction.FiniteReflectionInput.unit_greatestElement_direct line 138

    Source documentation

    The actual unit comparison is weak on all greatest-element posets in dimension n+1. No finite-poset unit theorem is used.

    theorem unit_greatestElement_direct
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    {P : Type} [PartialOrder P] (x : P) (hx : ∀ y, y ≤ x) :
    realizationWeakEquivalences ((r.categorificationAdjunction h).unit.app (nerve P)) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.realizationWeakEquivalences

  9. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.unit_finite_poset_fromGray line 157

    Source documentation

    Finite-poset units in omega dimension require the strict Gray input, with no Kan–Quillen, extension, transfer, or localization assumption.

    theorem unit_finite_poset_fromGray (G : RightGrayInput h)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (P : Type) [PartialOrder P] [Finite P] :
    realizationWeakEquivalences (h.categorificationAdjunction.unit.app (nerve P)) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.realizationWeakEquivalences

  10. theorem OAI.Thomason.Construction.FiniteReflectionInput.unit_finite_poset_fromGray line 183

    Source documentation

    The finite-dimensional unit comparison only adds the specified interval internal-hom truncation input.

    theorem unit_finite_poset_fromGray (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h)
    (P : Type) [PartialOrder P] [Finite P] :
    realizationWeakEquivalences ((r.categorificationAdjunction h).unit.app (nerve P)) := by
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.realizationWeakEquivalences

  11. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finitePosetUnitInput_fromGray line 208

    Source documentation

    Strict Gray cylinder comparisons and finite internal-hom truncation give the finite-poset unit comparisons.

    theorem finitePosetUnitInput_fromGray (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h) : PublishedFinitePosetUnitInput h where
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.PublishedFinitePosetUnitInput

  12. theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finite_poset_map_weakEquivalence_fromGray line 215

    Source documentation

    On finite-poset nerves the actual Street and ordinary realization weak criteria agree using only the right Gray data.

    theorem finite_poset_map_weakEquivalence_fromGray
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    {P Q : Type} [PartialOrder P] [PartialOrder Q] [Finite P] [Finite Q]
    (f : nerve P ⟶ nerve Q) :
    h.streetWeakEquivalences (h.categorification.map f) ↔ realizationWeakEquivalences f :=
…

    Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.SimplexComplex.AlexanderWhitneyInput, OAI.Thomason.Construction.realizationWeakEquivalences