TopologicalConePrism.lean`

66 declarations, 0 contain sorry, 0 declared as axioms

Gray deformation retractions induce actual Thomason weak equivalences

This connects the constructed strict cylinders, their Street-nerve homotopies, and the actual realization weak equivalences. Its classical inputs are only the specified normalized chains, right Gray comparison, Alexander--Whitney identities and Kan--Quillen WFS. No strict-category model structure is assumed.

theorem OAI.Thomason.Construction.KanQuillenPublishedInput.weakEquivalences_retracts line 41
Source documentation
Retract stability is derived from the two classical WFS, through the model-category constructor, rather than added as a new input.
```
theorem weakEquivalences_retracts : realizationWeakEquivalences.{0}.IsStableUnderRetracts := by
…
```
theorem OAI.Thomason.Construction.RightGrayInput.cylinder_weakEquivalence_iff line 55
Source documentation
Strict right-cylinder homotopies preserve the prescribed Thomason weak-equivalence class, defined by actual realizations of Street nerves.
```
theorem cylinder_weakEquivalence_iff {X Y : StrictOmegaCategory.{0}}
    (P : G.cylinder.obj X ⟶ Y) :
    h.streetWeakEquivalences ((G.endpoint false).app X ≫ P) ↔
      h.streetWeakEquivalences ((G.endpoint true).app X ≫ P) :=
…
```

theorem OAI.Thomason.Construction.RightGrayInput.deformation_retract_weakEquivalences line 63

Source documentation

A strict retraction with a Gray homotopy from its other composite to identity is a weak equivalence on both maps.

theorem deformation_retract_weakEquivalences {A X : StrictOmegaCategory.{0}}
    (i : A ⟶ X) (r : X ⟶ A) (hi : i ≫ r = 𝟙 A)
    (P : G.cylinder.obj X ⟶ X)
    (h₀ : (G.endpoint false).app X ≫ P = r ≫ i)
    (h₁ : (G.endpoint true).app X ≫ P = 𝟙 X) :
    h.streetWeakEquivalences i ∧ h.streetWeakEquivalences r := by
…

theorem OAI.Thomason.Construction.RelativePrismData.finite_weakEquivalence_iff line 115
Source documentation
In every positive finite dimension, either categorified endpoint is a Street-nerve weak equivalence exactly when the other endpoint is.
```
theorem finite_weakEquivalence_iff :
    h.streetWeakEquivalences ((StrictOmegaCategory.inclusion (n + 1)).map
      (r.reflect.map (h.posetMap D.first))) ↔
    h.streetWeakEquivalences ((StrictOmegaCategory.inclusion (n + 1)).map
      (r.reflect.map (h.posetMap D.last))) := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.inclusion
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.aboveAtomOrZero_comp_factors line 148
Source documentation
At a strictly lower composition degree, the upper atom belongs to one factor and the other factor has zero upper tables.
```
theorem aboveAtomOrZero_comp_factors (n s : ℕ) (hs : s < n)
    (Y Z : Cell K) (hyz : Y.face true s = Z.face false s)
    (hX : B.AboveAtomOrZero n (Cell.comp Y Z s hyz)) :
    B.AboveAtomOrZero n Y ∧ B.AboveAtomOrZero n Z := by
…
```
Mentions: OAI.Thomason.Construction.DirectedComplex.Cell, OAI.Thomason.Construction.DirectedComplex.Cell.comp

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.essential_levelsLE line 173

Source documentation

No essential composition lies above the preceding decomposition level of the image. This controls the whole expression, not just its root.

theorem essential_levelsLE {C : StrictOmegaCategory.{0}}
    (g : B.AtomIndex → C) (F : C ⟶ K.realization)
    (hg : ∀ a, F.toFun (g a) = B.atomCell a)
    (hd : ∀ a, C.DimensionLE a.1 (g a))
    {x : C} (t : EssentialExpression C g x) (n : ℕ)
    (hX : B.AboveAtomOrZero (n+1) (F.toFun x)) : t.levelsLE n := by
…

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.preimage_atom_string line 203

Source documentation

Every preimage of a level-(n+1) cell is either n-dimensional or an actual n-string whose factors have specified upper atoms above n.

theorem preimage_atom_string {C : StrictOmegaCategory.{0}}
    (g : B.AtomIndex → C) (F : C ⟶ K.realization)
    (hg : ∀ a, F.toFun (g a) = B.atomCell a)
    (hd : ∀ a, C.DimensionLE a.1 (g a))
    (hgen : ∀ x : C, Nonempty (CompositionExpression C g x))
    (n : ℕ) (x : C) (hX : B.AboveAtomOrZero (n+1) (F.toFun x)) :
    C.DimensionLE n x ∨ ∃ xs : List C, xs ≠ [] ∧ CompositeList C n xs x ∧
      ∀ y ∈ xs, ∃ a : B.AtomIndex, n < a.1 ∧
        ∀ q, n < q → ∀ side, (F.toFun y).table side q = (B.atomCell a).table side q := by
…

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.preimages_eq_of_dimensionLE line 247
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.preimages_eq_successor line 260

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.unique_preimage_level line 292

Source documentation

Every atom-decomposition level has unique preimages. The induction hypotheses are discharged internally by actual sorting and interchange.

theorem unique_preimage_level {C : StrictOmegaCategory.{0}}
    (g : B.AtomIndex → C) (F : C ⟶ K.realization)
    (hg : ∀ a, F.toFun (g a) = B.atomCell a)
    (hd : ∀ a, C.DimensionLE a.1 (g a))
    (hgen : ∀ x : C, Nonempty (CompositionExpression C g x)) :
    ∀ n X, B.AboveAtomOrZero n X → ∃! x : C, F.toFun x = X := by
…

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.comparison_bijective line 309

Source documentation

The ordered-atom comparison is bijective on the actual cell carriers.

theorem comparison_bijective {C : StrictOmegaCategory.{0}}
    (g : B.AtomIndex → C) (F : C ⟶ K.realization)
    (hg : ∀ a, F.toFun (g a) = B.atomCell a)
    (hd : ∀ a, C.DimensionLE a.1 (g a))
    (hgen : ∀ x : C, Nonempty (CompositionExpression C g x)) :
    Function.Bijective F.toFun := by
…

def OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.comparisonIso line 329

Source documentation

The actual strict isomorphism, with the specified comparison as its forward functor.

noncomputable def comparisonIso {C : StrictOmegaCategory.{0}}
    (g : B.AtomIndex → C) (F : C ⟶ K.realization)
    (hg : ∀ a, F.toFun (g a) = B.atomCell a)
    (hd : ∀ a, C.DimensionLE a.1 (g a))
    (hgen : ∀ x : C, Nonempty (CompositionExpression C g x)) : C ≅ K.realization :=
…

theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.comparisonIso_hom line 336
theorem OAI.Thomason.Construction.DirectedComplex.OrderedAtomBasis.comparison_isIso line 343
theorem OAI.Thomason.Construction.PastingGlobeBasis.mixed_coefficient line 371
theorem OAI.Thomason.Construction.PastingGlobeBasis.ordered_disjoint line 381
def OAI.Thomason.Construction.PastingGlobeBasis.orderedAtomBasis line 395
Source documentation
The base ordered atoms are inherited from the explicit signed cylinder.
```
def orderedAtomBasis {n k : ℕ} (hkn : k < n) : OrderedAtomBasis (complex n k hkn) where
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.complex
def OAI.Thomason.Construction.PastingGlobeBasis.piece line 411
def OAI.Thomason.Construction.PastingGlobeBasis.pieceAtom line 414
def OAI.Thomason.Construction.PastingGlobeBasis.atomLift line 419
Source documentation
Lift the canonical representative to the appropriate actual globe face.
```
def atomLift {n k : ℕ} (hkn : k < n) (a : (orderedAtomBasis hkn).AtomIndex) :
    PastingGlobe.category n n k :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.orderedAtomBasis
theorem OAI.Thomason.Construction.PastingGlobeBasis.atomLift_dimension line 423
theorem OAI.Thomason.Construction.PastingGlobeBasis.pieceAtom_image line 429
theorem OAI.Thomason.Construction.PastingGlobeBasis.atomLift_image line 445
theorem OAI.Thomason.Construction.PastingGlobeBasis.shared_lower line 450
theorem OAI.Thomason.Construction.PastingGlobeBasis.pieceAtom_normalize line 458
theorem OAI.Thomason.Construction.PastingGlobeBasis.piece_generated line 483
theorem OAI.Thomason.Construction.PastingGlobeBasis.generated line 499
def OAI.Thomason.Construction.PastingGlobeBasis.pastingIso line 509
Source documentation
The canonical comparison of the actual pasted globes is a strict isomorphism.
```
def pastingIso {n k : ℕ} (hkn : k < n) :
    PastingGlobe.category n n k ≅ (complex n k hkn).realization :=
…
```
Mentions: OAI.Thomason.Construction.PastingGlobeBasis.complex
theorem OAI.Thomason.Construction.PastingGlobeBasis.pastingIso_hom line 514

def OAI.Thomason.Construction.PastingGlobeBasis.pastingUnitIso line 518

Source documentation

Strict abelianization also recovers the actual binary pasting parameter.

def pastingUnitIso {n k : ℕ} (hkn : k < n) :
    PastingGlobe.category n n k ≅
      (Abelianization.complex (PastingGlobe.category n n k)).realization :=
…

theorem OAI.Thomason.Construction.PastingGlobeBasis.pastingUnitIso_hom line 523
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelCollapse line 560
Source documentation
Collapse the interval in the global chain model.
```
def modelCollapse : model ⟶ Abelianization.functor ⋙ realizationFunctor where
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.model, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.functor
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelEndpoint_collapse line 567
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameterUnitComponent line 577
Source documentation
The unit comparison at one actual globe or binary pasting.
```
def parameterUnitComponent (i : GlobePasting.Shape) :
    GlobePasting.object i ≅ (Abelianization.complex (GlobePasting.object i)).realization :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.Shape, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.object, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.complex
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameterUnitComponent_hom line 583
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameterUnitIso line 590
Source documentation
The actual unit is an isomorphism on every chosen finite parameter.
```
def parameterUnitIso : GlobePasting.inclusion ≅
    GlobePasting.inclusion ⋙ Abelianization.functor ⋙ realizationFunctor :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion, OAI.Thomason.Construction.StrictOmegaCategory.Abelianization.functor
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameterUnitIso_hom_app line 600
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameterProjection line 605
Source documentation
Collapse on each actual finite parameter, with the unit inverted.
```
def parameterProjection : parameters ⟶ GlobePasting.inclusion :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameters, OAI.Thomason.Construction.StrictOmegaCategory.GlobePasting.inclusion
def OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.projection line 609
Source documentation
The global strict cylinder collapse is the unique extension of these maps.
```
def projection : cylinder ⟶ 𝟭 StrictOmegaCategory.{0} :=
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.cylinder
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.projection_parameters line 612
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.parameterEndpoint_projection line 617
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpoint_projection line 632
Source documentation
Both actual global endpoint maps are sections of the constructed collapse.
```
theorem endpoint_projection (a : Bool) (C : StrictOmegaCategory.{0}) :
    (endpoint a).app C ≫ projection.app C = 𝟙 C := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.endpoint
theorem OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.projection_unit line 657
Source documentation
The strict collapse agrees with the literal chain collapse after the abelianization unit, on every strict category.
```
theorem projection_unit :
    projection ≫ Abelianization.adjunction.unit = comparison ≫ modelCollapse := by
…
```
Mentions: OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.projection, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.comparison, OAI.Thomason.Construction.StrictOmegaCategory.GrayChainExtension.modelCollapse

theorem OAI.Thomason.Construction.RelativePrismData.weakEquivalence_iff line 710

Source documentation

Relative poset-prism endpoints simultaneously induce Street weak equivalences.

theorem weakEquivalence_iff :
    h.streetWeakEquivalences (h.categorification.map (nerveMap D.first.monotone.functor)) ↔
      h.streetWeakEquivalences (h.categorification.map (nerveMap D.last.monotone.functor)) := by
…

abbrev OAI.Thomason.Construction.RealizationPrism.diagram line 740
Source documentation
The actual topological simplices indexing a realization.
```
noncomputable abbrev diagram (K : SSet.{0}) :=
…
```
abbrev OAI.Thomason.Construction.RealizationPrism.cocone line 744
Source documentation
The canonical cocone, using Mathlib's realization comparison on simplices.
```
noncomputable abbrev cocone (K : SSet.{0}) : Cocone (diagram K) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.diagram
def OAI.Thomason.Construction.RealizationPrism.isColimit line 748
Source documentation
Its actual colimit universal property.
```
noncomputable def isColimit (K : SSet.{0}) : IsColimit (cocone K) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.cocone
abbrev OAI.Thomason.Construction.RealizationPrism.leg line 753
Source documentation
The continuous map from an original topological simplex to realization.
```
noncomputable abbrev leg (K : SSet.{0}) (j : CostructuredArrow SSet.stdSimplex K) :=
…
```
theorem OAI.Thomason.Construction.RealizationPrism.leg_naturality line 757
Source documentation
Realization legs commute with every actual simplicial map.
```
theorem leg_naturality {K L : SSet.{0}} (f : K ⟶ L)
    (j : CostructuredArrow SSet.stdSimplex K) :
    leg K j ≫ SSet.toTop.map f = leg L ((CostructuredArrow.map f).obj j) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.leg

def OAI.Thomason.Construction.RealizationPrism.prismCocone line 765

Source documentation

Compatible topological prisms indexed by every simplex, including degenerate ones.

noncomputable def prismCocone (K : SSet.{0}) (Z : TopCat.{0})
    (P : ∀ j, TopologicalInterval.cylinder.obj ((diagram K).obj j) ⟶ Z)
    (hp : ∀ {i j} (f : i ⟶ j),
      TopologicalInterval.cylinder.map ((diagram K).map f) ≫ P j = P i) :
    Cocone (diagram K ⋙ TopologicalInterval.cylinder) where
…

Mentions: OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.TopologicalInterval.cylinder

def OAI.Thomason.Construction.RealizationPrism.assemble line 777

Source documentation

The assembled prism is defined on the actual geometric realization times I.

noncomputable def assemble (K : SSet.{0}) (Z : TopCat.{0})
    (P : ∀ j, TopologicalInterval.cylinder.obj ((diagram K).obj j) ⟶ Z)
    (hp : ∀ {i j} (f : i ⟶ j),
      TopologicalInterval.cylinder.map ((diagram K).map f) ≫ P j = P i) :
    TopologicalInterval.cylinder.obj (SSet.toTop.obj K) ⟶ Z :=
…

Mentions: OAI.Thomason.Construction.RealizationPrism.diagram

theorem OAI.Thomason.Construction.RealizationPrism.assemble_fac line 785

theorem OAI.Thomason.Construction.RealizationPrism.assemble_endpoint line 794

Source documentation

The global endpoint equation follows from its equations on original simplex legs.

theorem assemble_endpoint (K : SSet.{0}) (Z : TopCat.{0})
    (P : ∀ j, TopologicalInterval.cylinder.obj ((diagram K).obj j) ⟶ Z)
    (hp : ∀ {i j} (f : i ⟶ j),
      TopologicalInterval.cylinder.map ((diagram K).map f) ≫ P j = P i)
    (t : unitInterval) (f : SSet.toTop.obj K ⟶ Z)
    (he : ∀ j, TopologicalInterval.sectionAt ((diagram K).obj j) t ≫ P j = leg K j ≫ f) :
    TopologicalInterval.sectionAt (SSet.toTop.obj K) t ≫ assemble K Z P hp = f := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.RealizationPrism.assemble

def OAI.Thomason.Construction.RealizationPrism.homotopy line 813

Source documentation

A pair of compatible endpoint equations gives an actual continuous homotopy.

noncomputable def homotopy (K : SSet.{0}) (Z : TopCat.{0})
    (P : ∀ j, TopologicalInterval.cylinder.obj ((diagram K).obj j) ⟶ Z)
    (hp : ∀ {i j} (f : i ⟶ j),
      TopologicalInterval.cylinder.map ((diagram K).map f) ≫ P j = P i)
    (f g : SSet.toTop.obj K ⟶ Z)
    (h₀ : ∀ j, TopologicalInterval.sectionAt ((diagram K).obj j) 0 ≫ P j = leg K j ≫ f)
    (h₁ : ∀ j, TopologicalInterval.sectionAt ((diagram K).obj j) 1 ≫ P j = leg K j ≫ g) :
    f.hom.Homotopy g.hom where
…

Mentions: OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.RealizationPrism.leg

theorem OAI.Thomason.Construction.RealizationPrism.assemble_stationary line 850

Source documentation

Local stationarity descends along the source realization colimit.

theorem assemble_stationary
    (hs : ∀ j : CostructuredArrow SSet.stdSimplex K,
      P ((CostructuredArrow.map i).obj j) =
        TopologicalInterval.projection ((diagram K).obj j) ≫ leg K j ≫ SSet.toTop.map i) :
    TopologicalInterval.cylinder.map (SSet.toTop.map i) ≫ assemble L _ P hp =
      TopologicalInterval.projection (SSet.toTop.obj K) ≫ SSet.toTop.map i := by
…

Mentions: OAI.Thomason.Construction.TopologicalInterval.projection, OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.RealizationPrism.assemble

theorem OAI.Thomason.Construction.RealizationPrism.weak_of_stationary_prisms line 880

Source documentation

An actual simplicial retraction whose realization has compatible stationary simplex prisms is a realization weak equivalence.

theorem weak_of_stationary_prisms
    (h₀ : ∀ j, TopologicalInterval.sectionAt ((diagram L).obj j) 0 ≫ P j =
      leg L j ≫ (SSet.toTop.map r ≫ SSet.toTop.map i))
    (h₁ : ∀ j, TopologicalInterval.sectionAt ((diagram L).obj j) 1 ≫ P j =
      leg L j ≫ 𝟙 (SSet.toTop.obj L))
    (hs : ∀ j : CostructuredArrow SSet.stdSimplex K,
      P ((CostructuredArrow.map i).obj j) =
        TopologicalInterval.projection ((diagram K).obj j) ≫ leg K j ≫ SSet.toTop.map i) :
    realizationWeakEquivalences i := by
…

Mentions: OAI.Thomason.Construction.TopologicalInterval.sectionAt, OAI.Thomason.Construction.RealizationPrism.diagram, OAI.Thomason.Construction.RealizationPrism.leg, OAI.Thomason.Construction.TopologicalInterval.projection, OAI.Thomason.Construction.realizationWeakEquivalences

def OAI.Thomason.Construction.ConePrism.append line 924

Source documentation

Append a vertex above the final vertex of an ordered simplex.

def append {P : Type*} [Preorder P] {n : ℕ} (s : Fin (n+1) →o P)
    (v : P) (hv : s (Fin.last n) ≤ v) : Fin (n+2) →o P where
…

theorem OAI.Thomason.Construction.ConePrism.append_castSucc line 931
theorem OAI.Thomason.Construction.ConePrism.append_last line 938
def OAI.Thomason.Construction.ConePrism.ordinalMap line 945
Source documentation
Extend an ordinal map by the new final vertex.
```
def ordinalMap {m n : ℕ} (f : Fin (m+1) →o Fin (n+1)) : Fin (m+2) →o Fin (n+2) :=
…
```
theorem OAI.Thomason.Construction.ConePrism.ordinalMap_castSucc line 949
theorem OAI.Thomason.Construction.ConePrism.ordinalMap_last line 953
def OAI.Thomason.Construction.ConePrism.barycentric line 957
Source documentation
The barycentric straight-line cone to the newly appended final vertex.
```
noncomputable def barycentric (n : ℕ) :
    C(StdSimplex ℝ (Fin (n+1)) × unitInterval, StdSimplex ℝ (Fin (n+2))) where
…
```
theorem OAI.Thomason.Construction.ConePrism.barycentric_zero line 976
theorem OAI.Thomason.Construction.ConePrism.barycentric_one line 982
theorem OAI.Thomason.Construction.ConePrism.barycentric_naturality line 988
Source documentation
Naturality of the topological cone under every ordinal map.
```
theorem barycentric_naturality {m n : ℕ} (f : Fin (m+1) →o Fin (n+1))
    (x : StdSimplex ℝ (Fin (m+1))) (t : unitInterval) :
    StdSimplex.map (ordinalMap f) (barycentric m (x, t)) =
      barycentric n (StdSimplex.map f x, t) := by
…
```
Mentions: OAI.Thomason.Construction.ConePrism.ordinalMap, OAI.Thomason.Construction.ConePrism.barycentric