StrictPosetWeakEquivalences.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Joint labels agree with intersections of poset sieves

theorem OAI.Thomason.Construction.sieveCharacteristic_inter line 20

Source documentation

The characteristic label of an intersection is the maximum of the two labels.

theorem sieveCharacteristic_inter {E : Type} [PartialOrder E]
    (A B : Set E) (hA : IsLowerSet A) (hB : IsLowerSet B) (x : E) :
    sieveCharacteristic (A ∩ B) (hA.inter hB) x =
      max (sieveCharacteristic A hA x) (sieveCharacteristic B hB x) := by
…

Mentions: OAI.Thomason.Construction.sieveCharacteristic

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.membershipLabel_inter line 46

Source documentation

On the actual categorification, the joint label is exactly the canonical membership label for the intersected sieve.

theorem membershipLabel_inter {E : Type} [PartialOrder E]
    (A B : Set E) (hA : IsLowerSet A) (hB : IsLowerSet B) :
    maxLabel (h.membershipLabel A hA) (h.membershipLabel B hB) =
      h.membershipLabel (A ∩ B) (hA.inter hB) := by
…

theorem OAI.Thomason.Construction.FiniteReflectionInput.membershipLabel_inter line 64

Source documentation

Reflection preserves the same joint-label compatibility on all cells.

theorem membershipLabel_inter {E : Type} [PartialOrder E]
    (A B : Set E) (hA : IsLowerSet A) (hB : IsLowerSet B) :
    maxLabel (r.membershipLabel h A hA) (r.membershipLabel h B hB) =
      r.membershipLabel h (A ∩ B) (hA.inter hB) := by
…

def OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetCarrierHomeomorph line 93

Source documentation

The actual full Street nerve realizes to its intrinsic carrier subspace.

def fullStreetCarrierHomeomorph (S : Set C) :
    SSet.toTop.obj (h.streetNerve.obj (C.fullOn S)) ≃ₜ
      Set.ofPred (fun x : SSet.toTop.obj (h.streetNerve.obj C) =>
        RealizationPrism.carrier (h.streetNerve.obj C) x ≤ h.fullStreetSubcomplex C S) :=
…

Mentions: OAI.Thomason.Construction.RealizationPrism.carrier

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetCarrierHomeomorph_inclusion line 101

Source documentation

This homeomorphism preserves the original strict full-inclusion map.

theorem fullStreetCarrierHomeomorph_inclusion (S : Set C) :
    (RealizationPrism.carrierInclusion (h.streetNerve.obj C) (h.fullStreetSubcomplex C S)).comp
      (h.fullStreetCarrierHomeomorph C S : C(_, _)) =
        (SSet.toTop.map (h.streetNerve.map (C.fullInclusion S))).hom := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.carrierInclusion

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullInclusion_realization_isClosedEmbedding line 110
Source documentation
Full strict higher subcategories give closed embeddings on actual Street realizations.
```
theorem fullInclusion_realization_isClosedEmbedding (S : Set C) :
    IsClosedEmbedding (SSet.toTop.map (h.streetNerve.map (C.fullInclusion S))).hom := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullInclusion_streetWeak_iff line 118
Source documentation
The actual Street weak test for a full inclusion is the weak test of its closed carrier subspace.
```
theorem fullInclusion_streetWeak_iff (S : Set C) :
    h.streetWeakEquivalences (C.fullInclusion S) ↔
      IsWeakHomotopyEquivalence
        (RealizationPrism.carrierInclusion (h.streetNerve.obj C) (h.fullStreetSubcomplex C S)) := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.RealizationPrism.carrierInclusion

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetSubcomplex_preimage line 129

Source documentation

Full Street subcomplexes commute with inverse image along strict higher functors.

theorem fullStreetSubcomplex_preimage {D : StrictOmegaCategory.{0}} (f : D ⟶ C) (S : Set C) :
    (h.fullStreetSubcomplex C S).preimage (h.streetNerve.map f) =
      h.fullStreetSubcomplex D (f.toFun ⁻¹' S) := by
…

def OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetPreimageHomeomorph line 139

Source documentation

Realizing a strict full inverse image gives the actual inverse image of the corresponding closed Street carrier subspace.

def fullStreetPreimageHomeomorph {D : StrictOmegaCategory.{0}} (f : D ⟶ C) (S : Set C) :
    SSet.toTop.obj (h.streetNerve.obj (D.fullOn (f.toFun ⁻¹' S))) ≃ₜ
      ((SSet.toTop.map (h.streetNerve.map f)).hom ⁻¹'
        Set.ofPred (fun x : SSet.toTop.obj (h.streetNerve.obj C) =>
          RealizationPrism.carrier (h.streetNerve.obj C) x ≤ h.fullStreetSubcomplex C S)) :=
…

Mentions: OAI.Thomason.Construction.RealizationPrism.carrier

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.labelFiberInclusion_realization_isClosedEmbedding line 155
Source documentation
In particular, full fibres of ordered labels realize as closed subspaces.
```
theorem labelFiberInclusion_realization_isClosedEmbedding
    (p : C ⟶ StrictPoset.category (Fin 2)) (e : Fin 2) :
    IsClosedEmbedding (SSet.toTop.map (h.streetNerve.map (labelFiberInclusion p e))).hom :=
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.strictPosetNerveMap_naturality line 179
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.strictPoset_map_weak_iff line 187
Source documentation
On actual strict posets, the Street weak equivalences are exactly the ordinary-nerve realization weak equivalences.
```
theorem strictPoset_map_weak_iff (f : P →o Q) :
    h.streetWeakEquivalences (StrictPoset.map f) ↔
      realizationWeakEquivalences (nerveMap f.monotone.functor) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.map, OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.strictPoset_orderHomotopy_weak_iff line 205
Source documentation
Comparable monotone maps have the same actual Street weak test, through the explicitly realized ordinary-nerve homotopy.
```
theorem strictPoset_orderHomotopy_weak_iff (f g : P →o Q) (hfg : ∀ x, f x ≤ g x) :
    h.streetWeakEquivalences (StrictPoset.map f) ↔
      h.streetWeakEquivalences (StrictPoset.map g) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.map