TruncatedLocalPresentability.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

Finite limits and colimits in the actual positive finite categories

The constructed intelligent reflection makes the full inclusion reflective. Finite limits and small colimits therefore follow from the explicitly constructed omega-category limits and colimits.

def OAI.Thomason.Construction.FiniteReflectionInput.reflectiveInclusion line 32
Source documentation
The actual truncation inclusion, with the given reflection adjunction.
```
noncomputable def reflectiveInclusion : Reflective (StrictOmegaCategory.inclusion (n+1)) where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion
theorem OAI.Thomason.Construction.FiniteReflectionInput.hasSmallColimits line 41
Source documentation
Small colimits exist in the finite category itself.
```
theorem hasSmallColimits : HasColimitsOfSize.{0,0} (Truncated.{0} (n+1)) := by
…
```
theorem OAI.Thomason.Construction.FiniteReflectionInput.hasFiniteLimits line 46
Source documentation
Finite limits exist in the finite category itself.
```
theorem hasFiniteLimits : HasFiniteLimits (Truncated.{0} (n+1)) := by
…
```
instance OAI.Thomason.Construction.constructedFiniteHasSmallColimits line 58
instance OAI.Thomason.Construction.constructedFiniteHasFiniteLimits line 62

theorem OAI.Thomason.Construction.retraction_weakEquivalences line 86

Source documentation

A retraction whose other composite is weak has both maps weak.

theorem retraction_weakEquivalences {C : Type*} [Category* C]
    (W : MorphismProperty C) [W.HasTwoOutOfThreeProperty]
    [W.ContainsIdentities] [W.IsStableUnderRetracts]
    {A X : C} (i : A ⟶ X) (r : X ⟶ A) (hi : i ≫ r = 𝟙 A)
    (hri : W (r ≫ i)) : W i ∧ W r := by
…

theorem OAI.Thomason.Construction.weak_component_iff line 102

Source documentation

A natural transformation is weak at either end of a map which is weak both before and after applying the endofunctor.

theorem weak_component_iff {C : Type*} [Category* C]
    (W : MorphismProperty C) [W.HasTwoOutOfThreeProperty]
    {F : C ⥤ C} (η : 𝟭 C ⟶ F) {X Y : C} (f : X ⟶ Y)
    (hf : W f) (hFf : W (F.map f)) : W (η.app X) ↔ W (η.app Y) := by
…

abbrev OAI.Thomason.Construction.PosetPoint line 118
Source documentation
The ordinary point used in the contraction, with its canonical simplex iso.
```
abbrev PosetPoint : Type := ULift.{0} (Fin 1)
```
def OAI.Thomason.Construction.posetToPoint line 120
def OAI.Thomason.Construction.posetFromPoint line 123
theorem OAI.Thomason.Construction.poset_point_retraction line 126
def OAI.Thomason.Construction.greatestElementPrism line 134
Source documentation
The greatest-element contraction satisfies precisely the hypotheses of the constructed relative chain prism, with empty stationary locus.
```
def greatestElementPrism {P : Type} [PartialOrder P] (x : P) (hx : ∀ y, y ≤ x) :
    RelativePrismData P where
…
```
Mentions: OAI.Thomason.Construction.RelativePrismData
theorem OAI.Thomason.Construction.nerve_greatest_point_weakEquivalences line 146
Source documentation
The point inclusion and collapse of a greatest-element poset are weak equivalences of ordinary nerves, with the actual realization definition.
```
theorem nerve_greatest_point_weakEquivalences (kq : KanQuillenPublishedInput.{0})
    {P : Type} [PartialOrder P] (x : P) (hx : ∀ y, y ≤ x) :
    realizationWeakEquivalences (nerveMap (posetFromPoint x).monotone.functor) ∧
      realizationWeakEquivalences (nerveMap (posetToPoint P).monotone.functor) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.posetFromPoint, OAI.Thomason.Construction.posetToPoint
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.object_zero_subsingleton line 165
Source documentation
The constructed zero-dimensional oriental has exactly one cell.
```
theorem object_zero_subsingleton : Subsingleton (h.object 0) := by
…
```
def OAI.Thomason.Construction.NormalizedSimplexIdentities.object_zero_isTerminal line 173
Source documentation
Its terminality uses the full strict functor laws, not just its objects.
```
noncomputable def object_zero_isTerminal : IsTerminal (h.object 0) := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.unit_point_isIso line 188
Source documentation
The unit on the standard point is an actual isomorphism.
```
theorem unit_point_isIso : IsIso (h.categorificationAdjunction.unit.app (Δ[0])) := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.unit_of_point_iso line 197
Source documentation
The comparison on any simplicial point is weak, by naturality along an actual isomorphism from the standard point.
```
theorem unit_of_point_iso (kq : KanQuillenPublishedInput.{0})
    {X : SSet.{0}} (e : (Δ[0] : SSet.{0}) ≅ X) :
    realizationWeakEquivalences (h.categorificationAdjunction.unit.app X) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.categorified_greatest_point_weakEquivalences line 209
Source documentation
The same contraction is weak after actual strict categorification.
```
theorem categorified_greatest_point_weakEquivalences
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    (kq : KanQuillenPublishedInput.{0})
    {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
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.unit_greatestElement line 233
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 (G : RightGrayInput h)
    (aw : SimplexComplex.AlexanderWhitneyInput h) (kq : KanQuillenPublishedInput.{0})
    {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
def OAI.Thomason.Construction.FiniteReflectionInput.finitePoint line 268
Source documentation
The zero-dimensional oriental is terminal also in the full finite category.
```
noncomputable def finitePoint : Truncated (n + 1) :=
…
```
def OAI.Thomason.Construction.FiniteReflectionInput.finitePoint_isTerminal line 271
theorem OAI.Thomason.Construction.FiniteReflectionInput.unit_point_isIso line 278
Source documentation
The actual composite adjunction has an isomorphic unit on the point.
```
theorem unit_point_isIso : IsIso ((r.categorificationAdjunction h).unit.app (Δ[0])) := by
…
```
theorem OAI.Thomason.Construction.FiniteReflectionInput.unit_of_point_iso line 291
theorem OAI.Thomason.Construction.FiniteReflectionInput.categorified_greatest_point_weakEquivalences line 304
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
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h) (kq : KanQuillenPublishedInput.{0})
    {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
theorem OAI.Thomason.Construction.FiniteReflectionInput.unit_greatestElement line 330
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
    (G : RightGrayInput h) (t : GrayTruncationInput G)
    (aw : SimplexComplex.AlexanderWhitneyInput h) (kq : KanQuillenPublishedInput.{0})
    {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
theorem OAI.Thomason.Construction.isIso_of_empty_levels line 359
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.unit_empty_isIso line 375
Source documentation
The omega-dimensional unit on an empty poset is an isomorphism.
```
theorem unit_empty_isIso (P : Type) [PartialOrder P] [IsEmpty P] :
    IsIso (h.categorificationAdjunction.unit.app (nerve P)) := by
…
```
theorem OAI.Thomason.Construction.FiniteReflectionInput.unit_empty_isIso line 394
Source documentation
Empty posets remain empty under the actual finite categorification.
```
theorem unit_empty_isIso (P : Type) [PartialOrder P] [IsEmpty P] :
    IsIso ((r.categorificationAdjunction h).unit.app (nerve P)) := by
…
```
theorem OAI.Thomason.Construction.StrictOmegaCategory.TruncatedFilteredColimit.isTruncated line 428
def OAI.Thomason.Construction.StrictOmegaCategory.TruncatedFilteredColimit.cocone line 442
def OAI.Thomason.Construction.StrictOmegaCategory.TruncatedFilteredColimit.underlyingIsColimit line 448
def OAI.Thomason.Construction.StrictOmegaCategory.TruncatedFilteredColimit.isColimit line 452
instance OAI.Thomason.Construction.StrictOmegaCategory.inclusion_preservesFilteredColimitsOfShape line 457
instance OAI.Thomason.Construction.StrictOmegaCategory.inclusion_preservesFilteredColimits line 483
instance OAI.Thomason.Construction.StrictOmegaCategory.inclusion_finitelyAccessible line 487
instance OAI.Thomason.Construction.StrictOmegaCategory.truncated_locallyFinitelyPresentable line 491
instance OAI.Thomason.Construction.StrictOmegaCategory.truncated_locallyPresentable line 495
instance OAI.Thomason.Construction.StrictOmegaCategory.truncated_globe_finitelyPresentable line 500
Source documentation
The reflected finite globes are finitely presentable in finite dimension.
```
instance truncated_globe_finitelyPresentable (n k : ℕ) :
    IsFinitelyPresentable.{0} ((IntelligentTruncation.functor n).obj (Globe.category k)) :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.functor, OAI.Thomason.Construction.StrictOmegaCategory.Globe.category