StreetSingularWeakReflection.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Intelligent finite reflection

The quotient of bounded cells gives the reflection adjunction of Ara–Maltsiniotis (2014), §5.8.

def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.functor line 23
theorem OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unit_naturality line 42
Source documentation
The projection is natural on all original strict cells.
```
theorem unit_naturality (n : ℕ) {C D : StrictOmegaCategory.{0}} (f : C ⟶ D) :
    unit C n ≫ (functor n).map f = f ≫ unit D n := unit_descend _ _
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unit, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.functor, OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.unit_descend
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.homEquiv line 45
def OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.adjunction line 53
Source documentation
The explicit intelligent-truncation / inclusion adjunction.
```
noncomputable def adjunction (n : ℕ) : functor n ⊣ inclusion n :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.IntelligentTruncation.functor, OAI.Thomason.Construction.StrictOmegaCategory.inclusion
def OAI.Thomason.Construction.constructedFiniteReflection line 72
Source documentation
Positive finite reflection, obtained from the quotient universal property.
```
noncomputable def constructedFiniteReflection (n : ℕ) : FiniteReflectionInput n where
…
```
Mentions: OAI.Thomason.Construction.FiniteReflectionInput
def OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreetCellComplex line 96
Source documentation
A strict full inclusion has an actual relative barycentric cell presentation on Street realizations.
```
def fullStreetCellComplex (S : Set C) :
    RelativeCellComplex.{0} barycentricBoundaryCell
      (SSet.toTop.map (h.streetNerve.map (C.fullInclusion S))) :=
…
```
theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreet_realized_range line 101

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreet_interior_iff line 117

Source documentation

A point in a Street simplex interior lies in a full strict realization exactly when all cells of that strict simplex lie in the full subcategory.

theorem fullStreet_interior_iff (S : Set C) {n : ℕ}
    (s : (h.streetNerve.obj C).obj (.op (.mk n)))
    (x : StdSimplex ℝ (Fin (n+1))) (hx : x ∈ fullSupport n) :
    simplexPoint (h.streetNerve.obj C) s x ∈
        Set.range (SSet.toTop.map (h.streetNerve.map (C.fullInclusion S))).hom ↔
      ∀ a, C.FullCell S (s.toFun a) := by
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreet_topological_lifting line 128
Source documentation
The concrete barycentric boundary lifting property suffices to extend continuous maps across every full strict Street inclusion.
```
theorem fullStreet_topological_lifting (S : Set C) {X Y : TopCat.{0}} (p : X ⟶ Y)
    (hp : ∀ n, HasLiftingProperty (boundaryInclusion n) p) :
    HasLiftingProperty (SSet.toTop.map (h.streetNerve.map (C.fullInclusion S))) p :=
…
```

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreet_homotopy_extension line 154

Source documentation

A homotopy on a full strict higher subcategory extends over the entire actual Street realization, with its restriction retained pointwise.

theorem fullStreet_homotopy_extension (S : Set C) {X : TopCat.{0}}
    (f : SSet.toTop.obj (h.streetNerve.obj C) ⟶ X)
    {g : SSet.toTop.obj (h.streetNerve.obj (C.fullOn S)) ⟶ X}
    (H : (SSet.toTop.map (h.streetNerve.map (C.fullInclusion S)) ≫ f).hom.Homotopy g.hom) :
    ∃ (g' : SSet.toTop.obj (h.streetNerve.obj C) ⟶ X)
      (H' : f.hom.Homotopy g'.hom),
      ∀ t x, H' (t, (SSet.toTop.map (h.streetNerve.map (C.fullInclusion S))).hom x) =
        H (t, x) :=
…

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.fullStreet_gray_homotopy_extension line 167

Source documentation

A prescribed full-subcategory Gray homotopy extends continuously over the ambient Street realization. The endpoint keeps the actual weak test of the initial strict functor. No strict ambient Gray extension is asserted.

theorem fullStreet_gray_homotopy_extension (S : Set C)
    (G : RightGrayInput h) (aw : SimplexComplex.AlexanderWhitneyInput h)
    {D : StrictOmegaCategory.{0}} (f : C ⟶ D)
    (P : G.cylinder.obj (C.fullOn S) ⟶ D)
    (h₀ : (G.endpoint false).app (C.fullOn S) ≫ P = C.fullInclusion S ≫ f) :
    ∃ (g' : SSet.toTop.obj (h.streetNerve.obj C) ⟶
        SSet.toTop.obj (h.streetNerve.obj D))
      (H' : (SSet.toTop.map (h.streetNerve.map f)).hom.Homotopy g'.hom),
      (∀ t x,
        H' (t, (SSet.toTop.map (h.streetNerve.map (C.fullInclusion S))).hom x) =
          G.realizedHomotopy aw P (t, x)) ∧
      (h.streetWeakEquivalences f ↔ IsWeakHomotopyEquivalence g'.hom) := by
…

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

theorem OAI.Thomason.Construction.NormalizedSimplexIdentities.streetWeak_of_singular_realization line 205
Source documentation
Weak equivalence of the singular map of an actual Street realization implies the original Thomason weak-equivalence test, without Gray or KQ inputs.
```
theorem streetWeak_of_singular_realization (h : NormalizedSimplexIdentities)
    {C D : StrictOmegaCategory.{0}} (f : C ⟶ D)
    (hf : realizationWeakEquivalences
      (TopCat.toSSet.map (SSet.toTop.map (h.streetNerve.map f)))) :
    h.streetWeakEquivalences f :=
…
```
Mentions: OAI.Thomason.Construction.NormalizedSimplexIdentities, OAI.Thomason.Construction.realizationWeakEquivalences