StrictPosetStarSemantics.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Finite reflection of sieve comparisons

The canonical comparison is compatible with the actual reflected inclusion. Consequently finite reflection transports the omega sieve isomorphism to all finite-dimensional instances.

theorem OAI.Thomason.Construction.FiniteReflectionInput.membershipLabel_unit line 30

Source documentation

The characteristic label in finite dimension descends the original label.

theorem membershipLabel_unit {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsLowerSet A) :
    r.adjunction.unit.app (h.categorification.obj (nerve P)) ≫ r.membershipLabel h A hA =
      h.membershipLabel A hA := by
…

theorem OAI.Thomason.Construction.FiniteReflectionInput.posetFiberMap_eq_reflect line 43

Source documentation

The finite canonical sieve map is exactly the reflected omega map followed by the canonical zero-fibre comparison.

theorem posetFiberMap_eq_reflect {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsLowerSet A) :
    r.posetFiberMap h A hA = r.reflect.map (h.posetFiberMap A hA) ≫
      r.zeroFiberComparison (h.membershipLabel A hA) (r.membershipLabel h A hA)
        (r.membershipLabel_unit h A hA) := by
…

theorem OAI.Thomason.Construction.FiniteReflectionInput.posetFiberMap_isIso_of_omega line 79

Source documentation

Finite reflection preserves the sieve comparison isomorphism.

theorem posetFiberMap_isIso_of_omega {P : Type} [PartialOrder P]
    (A : Set P) (hA : IsLowerSet A) [IsIso (h.posetFiberMap A hA)] :
    IsIso (C := Truncated (n + 1)) (r.posetFiberMap h A hA) := by
…

structure OAI.Thomason.Construction.PublishedOmegaPosetSieveInput line 92
Source documentation
The omega-category specialization of AM2014 Proposition 5.5, Lemma 5.12 and Proposition 5.13(c), for finite posets.
```
structure PublishedOmegaPosetSieveInput (h : NormalizedSimplexIdentities)
    [StrictColimitsInput] : Prop where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictColimitsInput
theorem OAI.Thomason.Construction.PublishedOmegaPosetSieveInput.allDimensions line 98
Source documentation
Recover all positive finite cases using the constructed compatibility.
```
theorem PublishedOmegaPosetSieveInput.allDimensions
    {h : NormalizedSimplexIdentities} [StrictColimitsInput]
    (s : PublishedOmegaPosetSieveInput h) : PublishedPosetSieveInput h where
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.StrictColimitsInput, OAI.Thomason.Construction.PublishedOmegaPosetSieveInput, OAI.Thomason.Construction.PublishedPosetSieveInput
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetNerve_preservesFiniteLimits line 127
Source documentation
The original Street nerve preserves the actual finite limits.
```
theorem streetNerve_preservesFiniteLimits : PreservesFiniteLimits h.streetNerve := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetNerve_pullbackComparison_isIso line 132
Source documentation
Its canonical comparison with a simplicial pullback is an isomorphism.
```
theorem streetNerve_pullbackComparison_isIso
    {X Y Z : StrictOmegaCategory.{0}} (f : X ⟶ Z) (g : Y ⟶ Z) :
    IsIso (pullbackComparison h.streetNerve f g) := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.thomasonRight_pullbackComparison_isIso line 139
Source documentation
The same comparison is an isomorphism for the actual Thomason right adjoint.
```
theorem thomasonRight_pullbackComparison_isIso
    {X Y Z : StrictOmegaCategory.{0}} (f : X ⟶ Z) (g : Y ⟶ Z) :
    IsIso (pullbackComparison h.thomasonRight f g) := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finiteStreetNerve_pullbackComparison_isIso line 146
Source documentation
The finite Street nerve preserves the finite-category pullback itself.
```
theorem finiteStreetNerve_pullbackComparison_isIso (n : ℕ)
    {X Y Z : Truncated.{0} (n+1)} (f : X ⟶ Z) (g : Y ⟶ Z) :
    IsIso (pullbackComparison (h.finiteStreetNerve (n+1)) f g) := by
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.finiteThomasonRight_pullbackComparison_isIso line 153

Source documentation

Twice extension preserves that actual finite-category pullback as well.

theorem finiteThomasonRight_pullbackComparison_isIso (n : ℕ)
    {X Y Z : Truncated.{0} (n+1)} (f : X ⟶ Z) (g : Y ⟶ Z) :
    IsIso (pullbackComparison (h.finiteStreetNerve (n+1) ⋙ SSet.ex ⋙ SSet.ex) f g) := by
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.strictLabel_vertex_le line 184
def OAI.Thomason.Construction.NormalizedSimplexIdentities.strictLabelHomotopy line 191
Source documentation
Ordered object labels give a constructed homotopy of the actual Street nerves.
```
def strictLabelHomotopy : SSet.Homotopy (h.streetNerve.map f) (h.streetNerve.map g) := by
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.strictLabel_weak_iff line 209
Source documentation
The actual Street weak-equivalence test is invariant under ordered labels out of any strict higher category.
```
theorem strictLabel_weak_iff : h.streetWeakEquivalences f ↔ h.streetWeakEquivalences g :=
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.strictLabelHomotopy_stationary line 236

Source documentation

Equality of the labels on a strict subdiagram gives exact stationarity on its entire Street cylinder, in every dimension.

theorem strictLabelHomotopy_stationary (i : D ⟶ C) (hi : i ≫ f = i ≫ g) :
    h.streetNerve.map i ▷ Δ[1] ≫ (h.strictLabelHomotopy f g hfg).h =
      fst (h.streetNerve.obj D) Δ[1] ≫ h.streetNerve.map i ≫ h.streetNerve.map f := by
…

def OAI.Thomason.Construction.NormalizedSimplexIdentities.strictLabelRealizedHomotopyRel line 256

Source documentation

The realized ordered-label homotopy fixes the entire realized image of the equal-label subdiagram, with its actual topology.

def strictLabelRealizedHomotopyRel (i : D ⟶ C) (hi : i ≫ f = i ≫ g) :
    (SSet.toTop.map (h.streetNerve.map f)).hom.HomotopyRel
      (SSet.toTop.map (h.streetNerve.map g)).hom
      (Set.range (SSet.toTop.map (h.streetNerve.map i)).hom) :=
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.strictPoset_vertexStar_contractible line 289
Source documentation
Every vertex star of the actual Street nerve of a strict poset is contractible in its actual realization topology.
```
theorem strictPoset_vertexStar_contractible
    (v : (h.streetNerve.obj (StrictPoset.category P)).obj (.op (.mk 0))) :
    ContractibleSpace (vertexStar (h.streetNerve.obj (StrictPoset.category P)) v) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.strictPoset_vertexStar_singular_counit_weak line 302
Source documentation
On these Street charts, evaluation from the realized singular set satisfies the full actual weak-homotopy-equivalence test.
```
theorem strictPoset_vertexStar_singular_counit_weak
    (v : (h.streetNerve.obj (StrictPoset.category P)).obj (.op (.mk 0))) :
    topologicalWeakEquivalences (sSetTopAdj.counit.app
      (TopCat.of (vertexStar (h.streetNerve.obj (StrictPoset.category P)) v))) := by
…
```
Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.topologicalWeakEquivalences

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.strictPoset_cube_grid_singular_comparison line 311

Source documentation

Compact cube maps into strict-poset Street realizations have a finite grid controlled by charts with proved singular weak equivalences.

theorem strictPoset_cube_grid_singular_comparison (n : ℕ)
    (f : C((Fin n → unitInterval), SSet.toTop.obj (h.streetNerve.obj (StrictPoset.category P)))) :
    ∃ m : ℕ, ∀ k : Fin n → Fin (m+1),
      ∃ v : (h.streetNerve.obj (StrictPoset.category P)).obj (.op (.mk 0)),
        (∀ x ∈ CubeGrid.cell n m k,
          f x ∈ vertexStar (h.streetNerve.obj (StrictPoset.category P)) v) ∧
        topologicalWeakEquivalences (sSetTopAdj.counit.app
          (TopCat.of (vertexStar (h.streetNerve.obj (StrictPoset.category P)) v))) := by
…

Mentions: OAI.Thomason.Construction.StrictPoset.category, OAI.Thomason.Construction.CubeGrid.cell, OAI.Thomason.Construction.topologicalWeakEquivalences