CanonicalExtensionAnodyneHorn.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

Actual homotopy-fibre compatibility of standard-simplex restrictions

def OAI.Thomason.Construction.realizedSimplexHomotopyFiberMap line 38

Source documentation

Restriction to a base simplex induces the literal continuous map of homotopy fibres, by projecting the point and applying the simplex map to its path.

def realizedSimplexHomotopyFiberMap {E : SSet.{0}} (n m : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) (g : (Δ[m] : SSet.{0}) ⟶ Δ[n])
    (b : SSet.toTop.obj (Δ[m] : SSet.{0})) :
    continuousHomotopyFiber (SSet.toTop.map (pullback.snd p g)) b ⟶
      continuousHomotopyFiber (SSet.toTop.map p) ((SSet.toTop.map g).hom b) :=
…

Mentions: OAI.Thomason.Construction.continuousHomotopyFiber

theorem OAI.Thomason.Construction.realizedSimplexHomotopyFiberMap_weak line 49
Source documentation
Every standard-simplex restriction is compatible with the genuine continuous homotopy fibre by an actual weak equivalence. No general realization/pullback theorem or acyclic Kan lifting input is used.
```
theorem realizedSimplexHomotopyFiberMap_weak {E : SSet.{0}} (n m : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (g : (Δ[m] : SSet.{0}) ⟶ Δ[n]) (b : SSet.toTop.obj (Δ[m] : SSet.{0})) :
    topologicalWeakEquivalences (realizedSimplexHomotopyFiberMap n m p g b) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedSimplexHomotopyFiberMap

theorem OAI.Thomason.Construction.kan_simplex_continuousFiberBaseChange_weak line 79

Source documentation

Restriction along any map of standard simplices induces a weak equivalence of the literal continuous fibres at every real point. This includes all faces, degeneracies, and their composites.

theorem kan_simplex_continuousFiberBaseChange_weak {E : SSet.{0}} (n m : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (g : (Δ[m] : SSet.{0}) ⟶ Δ[n]) (b : SSet.toTop.obj (Δ[m] : SSet.{0})) :
    topologicalWeakEquivalences (continuousFiberBaseChangeMap
      (SSet.toTop.map (pullback.snd p g)) (SSet.toTop.map p)
      (SSet.toTop.map (pullback.fst p g)) (SSet.toTop.map g)
      (by rw [← SSet.toTop.map_comp, pullback.condition, SSet.toTop.map_comp]) b) := by
…

Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousFiberBaseChangeMap

abbrev OAI.Thomason.Construction.simplexDensityCocone line 110
Source documentation
The standard-simplex density presentation, with the harmless universe lift already included in SSet.stdSimplex.
```
abbrev simplexDensityCocone (E : SSet.{0}) :
    Cocone (CostructuredArrow.proj SSet.stdSimplex E ⋙ SSet.stdSimplex) :=
…
```
def OAI.Thomason.Construction.simplexDensityIsColimit line 114

def OAI.Thomason.Construction.simplexPullbackSection line 118

Source documentation

A simplex in the total space lifts its own base simplex canonically.

def simplexPullbackSection {E B : SSet.{0}} (p : E ⟶ B) {n : SimplexCategory}
    (e : SSet.stdSimplex.obj n ⟶ E) :
    SSet.stdSimplex.obj n ⟶ pullback p (e ≫ p) :=
…

theorem OAI.Thomason.Construction.simplexPullbackSection_fst line 124
theorem OAI.Thomason.Construction.simplexPullbackSection_snd line 130

theorem OAI.Thomason.Construction.simplexPullbackSection_naturality line 137

Source documentation

Restricting a total-space simplex commutes with its canonical lift to its base-simplex pullback.

theorem simplexPullbackSection_naturality {E B : SSet.{0}} (p : E ⟶ B)
    {s t : CostructuredArrow SSet.stdSimplex E} (f : s ⟶ t) :
    SSet.stdSimplex.map f.left ≫ simplexPullbackSection p t.hom =
      simplexPullbackSection p s.hom ≫ (simplexPullbackDiagram p).map
        ((CostructuredArrow.map p).map f) := by
…

Mentions: OAI.Thomason.Construction.simplexPullbackSection, OAI.Thomason.Construction.simplexPullbackDiagram

def OAI.Thomason.Construction.simplexPullbackDescCocone line 155
Source documentation
Every cocone on base-simplex pullbacks induces a compatible cocone on the standard simplices of the original total space.
```
def simplexPullbackDescCocone {E B : SSet.{0}} (p : E ⟶ B)
    (s : Cocone (simplexPullbackDiagram p)) :
    Cocone (CostructuredArrow.proj SSet.stdSimplex E ⋙ SSet.stdSimplex) where
…
```
Mentions: OAI.Thomason.Construction.simplexPullbackDiagram
def OAI.Thomason.Construction.simplexPullbackDesc line 171
Source documentation
The induced map is defined through the actual density colimit.
```
def simplexPullbackDesc {E B : SSet.{0}} (p : E ⟶ B)
    (s : Cocone (simplexPullbackDiagram p)) : E ⟶ s.pt :=
…
```
Mentions: OAI.Thomason.Construction.simplexPullbackDiagram
theorem OAI.Thomason.Construction.simplexPullbackDesc_simplex line 176
theorem OAI.Thomason.Construction.simplexPullbackDesc_fac line 184
Source documentation
The induced map agrees with the given cocone on every full simplex pullback, not just on individual chosen lifts.
```
theorem simplexPullbackDesc_fac {E B : SSet.{0}} (p : E ⟶ B)
    (s : Cocone (simplexPullbackDiagram p))
    (b : CostructuredArrow SSet.stdSimplex B) :
    pullback.fst p b.hom ≫ simplexPullbackDesc p s = s.ι.app b := by
…
```
Mentions: OAI.Thomason.Construction.simplexPullbackDiagram, OAI.Thomason.Construction.simplexPullbackDesc
def OAI.Thomason.Construction.simplexPullbackIsColimit line 224
Source documentation
The canonical pullback cocone really reconstructs the original total simplicial set. No Kan or weak-equivalence assumption is needed here.
```
def simplexPullbackIsColimit {E B : SSet.{0}} (p : E ⟶ B) :
    IsColimit (simplexPullbackCocone p) where
…
```
Mentions: OAI.Thomason.Construction.simplexPullbackCocone
theorem OAI.Thomason.Construction.RealizationPrism.cylinder_vertex_cases line 257
Source documentation
The only vertices of a simplicial cylinder over a fixed vertex are its two endpoints.
```
theorem cylinder_vertex_cases {K : SSet.{0}}
    (z : (K ⊗ Δ[1]).obj (.op (.mk 0))) :
    z = SSet.ι₀.app _ z.1 ∨ z = SSet.ι₁.app _ z.1 := by
…
```

theorem OAI.Thomason.Construction.RealizationPrism.homotopy_mem_vertexStar line 277

Source documentation

If the endpoints send a vertex to the same target vertex, the whole realized homotopy sends its open star into the target open star.

theorem homotopy_mem_vertexStar {K L : SSet.{0}} {f g : K ⟶ L}
    (H : SSet.Homotopy f g) (v : K.obj (.op (.mk 0)))
    (w : L.obj (.op (.mk 0)))
    (hf : f.app (.op (.mk 0)) v = w) (hg : g.app (.op (.mk 0)) v = w)
    (t : unitInterval) (x : SSet.toTop.obj K) (hx : x ∈ vertexStar K v) :
    RealizedCylinder.homotopy H (t, x) ∈ vertexStar L w := by
…

Mentions: OAI.Thomason.Construction.RealizationPrism.vertexStar, OAI.Thomason.Construction.RealizedCylinder.homotopy

def OAI.Thomason.Construction.RealizationPrism.vertexStarMap line 297
Source documentation
Restriction of an actual realized simplicial map to an open vertex star.
```
def vertexStarMap {K L : SSet.{0}} (f : K ⟶ L)
    (v : K.obj (.op (.mk 0))) (w : L.obj (.op (.mk 0)))
    (h : f.app (.op (.mk 0)) v = w) : C(vertexStar K v, vertexStar L w) where
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexStar
def OAI.Thomason.Construction.RealizationPrism.vertexStarHomotopy line 307
Source documentation
Restrict a simplicial homotopy fixing a vertex to its actual open star. This does not assert that the star is contractible for a general simplicial set.
```
def vertexStarHomotopy {K : SSet.{0}} {f g : K ⟶ K}
    (H : SSet.Homotopy f g) (v : K.obj (.op (.mk 0)))
    (hf : f.app (.op (.mk 0)) v = v) (hg : g.app (.op (.mk 0)) v = v) :
    (vertexStarMap f v v hf).Homotopy (vertexStarMap g v v hg) where
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexStarMap
theorem OAI.Thomason.Construction.PosetGeometry.simplex_vertex_le line 343
def OAI.Thomason.Construction.PosetGeometry.orderedVertexHomotopy line 351
Source documentation
A pointwise inequality on vertices gives a simplicial homotopy into a poset nerve, even when the source is not itself an ordinary nerve.
```
def orderedVertexHomotopy : SSet.Homotopy f g where
…
```
theorem OAI.Thomason.Construction.PosetGeometry.orderedVertex_weak_iff line 394
Source documentation
This ordered-vertex criterion preserves the actual realization weak test.
```
theorem orderedVertex_weak_iff : realizationWeakEquivalences f ↔ realizationWeakEquivalences g :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.PosetGeometry.orderedVertexHomotopy_stationary line 421
Source documentation
The constructed homotopy is stationary along any map on which its endpoints agree, with equality of actual cylinder maps.
```
theorem orderedVertexHomotopy_stationary (i : A ⟶ K) (hi : i ≫ f = i ≫ g) :
    i ▷ Δ[1] ≫ (orderedVertexHomotopy f g hfg).h =
      fst A Δ[1] ≫ i ≫ f := by
…
```
Mentions: OAI.Thomason.Construction.PosetGeometry.orderedVertexHomotopy
theorem OAI.Thomason.Construction.PosetGeometry.nerve_const line 457
theorem OAI.Thomason.Construction.PosetGeometry.vertexStar_contractible_of_clamp line 464
Source documentation
A monotone clamp gives a contraction on the open star: both order homotopies stay inside the star because they fix its chosen vertex.
```
theorem vertexStar_contractible_of_clamp (v : P) (a : P →o P)
    (ha : ∀ x, x ≤ a x) (hv : ∀ x, v ≤ a x) (hav : a v = v) :
    ContractibleSpace (vertexStar (nerve P) (vertex v)) := by
…
```
Mentions: OAI.Thomason.Construction.PosetGeometry.vertex
theorem OAI.Thomason.Construction.PosetGeometry.vertexStar_contractible line 500
Source documentation
Open vertex stars of arbitrary small poset nerves are contractible. The statement concerns the actual realization subspace topology.
```
theorem vertexStar_contractible (v : P) :
    ContractibleSpace (vertexStar (nerve P) (vertex v)) := by
…
```
Mentions: OAI.Thomason.Construction.PosetGeometry.vertex
theorem OAI.Thomason.Construction.PosetGeometry.vertexStar_singular_counit_weak line 529
Source documentation
Evaluation on an actual open vertex star of a poset realization is a weak equivalence on components and every positive homotopy group.
```
theorem vertexStar_singular_counit_weak (v : P) :
    topologicalWeakEquivalences
      (sSetTopAdj.counit.app (TopCat.of (vertexStar (nerve P) (vertex v)))) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.PosetGeometry.vertex
theorem OAI.Thomason.Construction.PosetGeometry.cube_grid_singular_comparison line 538
Source documentation
Cubes in poset realizations have a uniform finite grid subordinate to actual contractible stars, on which the singular comparison is proved. This is local control, not an assumed global approximation theorem.
```
theorem cube_grid_singular_comparison (n : ℕ)
    (f : C((Fin n → unitInterval), SSet.toTop.obj (nerve P))) :
    ∃ m : ℕ, ∀ k : Fin n → Fin (m+1), ∃ v : P,
      (∀ x ∈ CubeGrid.cell n m k, f x ∈ vertexStar (nerve P) (vertex v)) ∧
      ContractibleSpace (vertexStar (nerve P) (vertex v)) ∧
      topologicalWeakEquivalences
        (sSetTopAdj.counit.app (TopCat.of (vertexStar (nerve P) (vertex v)))) := by
…
```
Mentions: OAI.Thomason.Construction.CubeGrid.cell, OAI.Thomason.Construction.PosetGeometry.vertex, OAI.Thomason.Construction.topologicalWeakEquivalences
theorem OAI.Thomason.Construction.RealizationPrism.iso_mem_vertexStar_iff line 569
def OAI.Thomason.Construction.RealizationPrism.isoVertexStarHomeomorph line 585
Source documentation
The star correspondence uses the actual geometric-realization homeomorphism.
```
def isoVertexStarHomeomorph {K L : SSet.{0}} (e : K ≅ L)
    (v : K.obj (.op (.mk 0))) :
    vertexStar K v ≃ₜ vertexStar L (e.hom.app _ v) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexStar
theorem OAI.Thomason.Construction.extension_map_const line 620
Source documentation
Naturality on constant maps also holds with an extended source, since extension preserves the terminal simplex.
```
theorem extension_map_const (X Y : SSet.{u}) (y : Y _⦋0⦌) :
    SSet.ex.map (SSet.const (X := X) y) =
…
```
def OAI.Thomason.Construction.extensionCylinder line 640
Source documentation
The natural comparison from the cylinder on Ex X into Ex of the cylinder on X.
```
def extensionCylinder (X : SSet.{u}) :
    SSet.ex.obj X ⊗ Δ[1] ⟶ SSet.ex.obj (X ⊗ Δ[1]) :=
…
```
theorem OAI.Thomason.Construction.extensionCylinder_zero line 645
theorem OAI.Thomason.Construction.extensionCylinder_one line 652
def OAI.Thomason.Construction.extensionHomotopy line 661
Source documentation
Applying actual extension to both endpoints of a simplicial homotopy produces a simplicial homotopy.
```
def extensionHomotopy {X Y : SSet.{u}} {f g : X ⟶ Y} (H : SSet.Homotopy f g) :
    SSet.Homotopy (SSet.ex.map f) (SSet.ex.map g) where
…
```
theorem OAI.Thomason.Construction.extension_homotopy_inverse_weak line 679
Source documentation
Extension preserves simplicial homotopy equivalences with explicit chosen inverses; this needs no Kan--Quillen model structure.
```
theorem extension_homotopy_inverse_weak {X Y : SSet.{0}} (f : X ⟶ Y) (g : Y ⟶ X)
    (hX : SSet.Homotopy (𝟙 X) (f ≫ g)) (hY : SSet.Homotopy (𝟙 Y) (g ≫ f)) :
    realizationWeakEquivalences (SSet.ex.map f) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.canonicalExtension_isIso_of_terminal line 687
Source documentation
The canonical extension of a terminal simplicial set is an isomorphism.
```
theorem canonicalExtension_isIso_of_terminal {X : SSet.{u}} (hX : IsTerminal X) :
    IsIso (canonicalExtension.app X) := by
…
```
theorem OAI.Thomason.Construction.canonicalExtension_weak_of_contractible line 694
Source documentation
The canonical extension map is weak on every simplicial set with a specified simplicial homotopy equivalence to the point.
```
theorem canonicalExtension_weak_of_contractible (X : SSet.{0})
    (f : X ⟶ Δ[0]) (g : Δ[0] ⟶ X)
    (hX : SSet.Homotopy (𝟙 X) (f ≫ g))
    (hT : SSet.Homotopy (𝟙 (Δ[0] : SSet.{0})) (g ≫ f)) :
    realizationWeakEquivalences (canonicalExtension.app X) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.extensionCylinder_canonical line 733
Source documentation
The extension cylinder restricts to the original cylinder along the canonical map, with equality of maps rather than a further homotopy.
```
theorem extensionCylinder_canonical (X : SSet.{0}) :
    (canonicalExtension.app X) ▷ (Δ[1] : SSet.{0}) ≫ extensionCylinder X =
      canonicalExtension.app (X ⊗ (Δ[1] : SSet.{0})) := by
…
```
Mentions: OAI.Thomason.Construction.extensionCylinder

theorem OAI.Thomason.Construction.extensionHomotopy_canonical line 742

Source documentation

A homotopy and its extension form an exact homotopy of arrows.

theorem extensionHomotopy_canonical {X Y : SSet.{0}} {f g : X ⟶ Y}
    (H : SSet.Homotopy f g) :
    (canonicalExtension.app X) ▷ (Δ[1] : SSet.{0}) ≫ (extensionHomotopy H).h =
      H.h ≫ canonicalExtension.app Y := by
…

Mentions: OAI.Thomason.Construction.extensionHomotopy

theorem OAI.Thomason.Construction.canonicalExtension_anodyne_of_contraction line 754
Source documentation
A specified simplicial contraction makes the actual canonical extension inclusion anodyne. This supplies exact relative Kan lifts over that parameter, with no weak-equivalence recognition theorem.
```
theorem canonicalExtension_anodyne_of_contraction (X : SSet.{0})
    (f : X ⟶ (Δ[0] : SSet.{0})) (g : (Δ[0] : SSet.{0}) ⟶ X)
    (H : SSet.Homotopy (𝟙 X) (f ≫ g)) :
    SSet.anodyneExtensions (canonicalExtension.app X) := by
…
```
theorem OAI.Thomason.Construction.canonicalExtension_standard_anodyne line 777
Source documentation
In particular every standard simplex has the exact Kan lifting property against its canonical inclusion into its extension.
```
theorem canonicalExtension_standard_anodyne (n : ℕ) :
    SSet.anodyneExtensions (canonicalExtension.app (Δ[n] : SSet.{0})) := by
…
```
theorem OAI.Thomason.Construction.canonicalExtension_weak_nerve_greatest line 809
Source documentation
A greatest element contracts the actual nerve, and this contraction persists through the actual extension functor.
```
theorem canonicalExtension_weak_nerve_greatest {P : Type} [PartialOrder P]
    (v : P) (hv : ∀ x, x ≤ v) :
    realizationWeakEquivalences (canonicalExtension.app (nerve P)) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.canonicalExtension_weak_standard_simplex line 835
Source documentation
Every standard simplex satisfies the actual canonical-extension weak equivalence theorem.
```
theorem canonicalExtension_weak_standard_simplex (n : ℕ) :
    realizationWeakEquivalences (canonicalExtension.app (Δ[n] : SSet.{0})) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.relativeCanonicalExtension line 870
theorem OAI.Thomason.Construction.relativeCanonicalExtension_inl line 876
theorem OAI.Thomason.Construction.relativeCanonicalExtension_inr line 881
instance OAI.Thomason.Construction.relativeCanonicalExtension_mono line 885

theorem OAI.Thomason.Construction.relativeCanonicalExtension_anodyne line 899

Source documentation

Absolute anodyne canonical extensions on a pair imply the relative anodyne extension, using the actual union map.

theorem relativeCanonicalExtension_anodyne {A B : SSet.{0}} (i : A ⟶ B) [Mono i]
    (hA : SSet.anodyneExtensions (canonicalExtension.app A))
    (hB : SSet.anodyneExtensions (canonicalExtension.app B)) :
    SSet.anodyneExtensions (relativeCanonicalExtension i) := by
…

Mentions: OAI.Thomason.Construction.relativeCanonicalExtension

theorem OAI.Thomason.Construction.relativeCanonicalExtension_standard_anodyne line 912
Source documentation
In particular any monomorphic map of standard simplices has exact relative lifting after canonical extension. Both the original target and the entire extended face are prescribed.
```
theorem relativeCanonicalExtension_standard_anodyne {m n : ℕ}
    (i : (Δ[m] : SSet.{0}) ⟶ (Δ[n] : SSet.{0})) [Mono i] :
    SSet.anodyneExtensions (relativeCanonicalExtension i) :=
…
```
Mentions: OAI.Thomason.Construction.relativeCanonicalExtension

theorem OAI.Thomason.Construction.canonicalExtension_anodyne_of_homotopy_cospan line 941

Source documentation

Two compatible homotopies from a common map to the identity and a constant also suffice for an anodyne canonical extension.

theorem canonicalExtension_anodyne_of_homotopy_cospan (X : SSet.{0})
    (f : X ⟶ (Δ[0] : SSet.{0})) (g : (Δ[0] : SSet.{0}) ⟶ X) (u : X ⟶ X)
    (H : SSet.Homotopy u (f ≫ g)) (G : SSet.Homotopy u (𝟙 X)) :
    SSet.anodyneExtensions (canonicalExtension.app X) := by
…

theorem OAI.Thomason.Construction.canonicalExtension_horn_anodyne line 970
Source documentation
Every positive-dimensional horn has an anodyne canonical extension, by its explicit simplicial contraction through lowerMap.
```
theorem canonicalExtension_horn_anodyne (n : ℕ) (k : Fin (n+2)) :
    SSet.anodyneExtensions (canonicalExtension.app (Λ[n+1, k] : SSet.{0})) := by
…
```
theorem OAI.Thomason.Construction.relativeCanonicalExtension_horn_anodyne line 982
Source documentation
The whole extended horn and the original simplex can both be fixed when lifting through a Kan fibration into the extended simplex.
```
theorem relativeCanonicalExtension_horn_anodyne (n : ℕ) (k : Fin (n+2)) :
    SSet.anodyneExtensions (relativeCanonicalExtension (Λ[n+1, k].ι :
      (Λ[n+1, k] : SSet.{0}) ⟶ (Δ[n+1] : SSet.{0}))) :=
…
```
Mentions: OAI.Thomason.Construction.relativeCanonicalExtension
theorem OAI.Thomason.Construction.extension_horn_anodyne line 990
Source documentation
Applying Ex to a generating horn inclusion is anodyne, by the original horn attachment followed by the exact relative comparison.
```
theorem extension_horn_anodyne (n : ℕ) (k : Fin (n+2)) :
    SSet.anodyneExtensions (SSet.ex.map (Λ[n+1, k].ι :
      (Λ[n+1, k] : SSet.{0}) ⟶ (Δ[n+1] : SSet.{0}))) := by
…
```