KanSimplexContinuousFibers.lean`

47 declarations, 0 contain sorry, 0 declared as axioms

Exact finite cubical families in the original Kan total space

theorem OAI.Thomason.Construction.RealizedCube.finite_kan_cube_family_lift line 30

Source documentation

With finite source, the entire exact higher family and its two given faces live in a single finite subcomplex of the original total space.

theorem finite_kan_cube_family_lift {A K E B : SSet.{0}} [K.Finite]
    (i : A ⟶ K) [Mono i] (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (n : ℕ) (f : K ⟶ E) (h : A ⊗ (obj n) ⟶ E)
    (b : K ⊗ (obj n) ⟶ B)
    (h₀ : productChosenVertex A (initialVertex n) ≫ h = i ≫ f)
    (hb : h ≫ p = i ▷ (obj n) ≫ b)
    (hf : f ≫ p = productChosenVertex K (initialVertex n) ≫ b) :
    ∃ (S : E.Subcomplex) (_ : SSet.Finite S.toSSet)
      (eS : K ⊗ (obj n) ⟶ S.toSSet)
      (fS : K ⟶ S.toSSet) (hS : A ⊗ (obj n) ⟶ S.toSSet),
      fS ≫ S.ι = f ∧ hS ≫ S.ι = h ∧
      productChosenVertex K (initialVertex n) ≫ eS = fS ∧
…

Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.productChosenVertex, OAI.Thomason.Construction.RealizedCube.initialVertex

theorem OAI.Thomason.Construction.realizedHomotopy_over line 76

Source documentation

An exact simplicial homotopy over a base stays over that same base point at every real cylinder parameter.

theorem realizedHomotopy_over {E F B : SSet.{0}} (p : E ⟶ B) (q : F ⟶ B)
    {f g : E ⟶ F} (H : SSet.Homotopy f g)
    (hH : H.h ≫ q = fst E Δ[1] ≫ p)
    (t : unitInterval) (x : SSet.toTop.obj E) :
    (SSet.toTop.map q).hom (RealizedCylinder.homotopy H (t,x)) =
      (SSet.toTop.map p).hom x := by
…

Mentions: OAI.Thomason.Construction.RealizedCylinder.homotopy

theorem OAI.Thomason.Construction.realizedFiberMap_weak line 92

Source documentation

Literal point fibres of a realized fibrewise simplicial homotopy equivalence are weakly equivalent at EVERY real base point.

theorem realizedFiberMap_weak {E F B : SSet.{0}} (p : E ⟶ B) (q : F ⟶ B)
    (f : E ⟶ F) (g : F ⟶ E) (hf : f ≫ q = p) (hg : g ≫ p = q)
    (H : SSet.Homotopy (𝟙 E) (f ≫ g)) (K : SSet.Homotopy (𝟙 F) (g ≫ f))
    (hH : H.h ≫ p = fst E Δ[1] ≫ p)
    (hK : K.h ≫ q = fst F Δ[1] ≫ q) (b : SSet.toTop.obj B) :
    topologicalWeakEquivalences (continuousFiberMap (SSet.toTop.map p) (SSet.toTop.map q)
      b (SSet.toTop.map f) (by rw [← SSet.toTop.map_comp, hf])) := by
…

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

def OAI.Thomason.Construction.intervalEdge line 129
Source documentation
The nondegenerate edge of the simplicial interval, with its actual initial and final vertices.
```
def intervalEdge : SSet.Edge (initialSimplexVertex 1) (finalSimplexVertex 1) :=
…
```
Mentions: OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.finalSimplexVertex
theorem OAI.Thomason.Construction.intervalEdge_time line 148
Source documentation
The canonical interval edge uses precisely the affine time coordinate of the realized cylinder.
```
theorem intervalEdge_time (t : unitInterval) :
    PrismBarycentric.realizationTime.hom (RealizationPrism.edgePath intervalEdge t) = t := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.edgePath, OAI.Thomason.Construction.intervalEdge
theorem OAI.Thomason.Construction.realizationTime_injective line 162
Source documentation
Affine time distinguishes all points in the realized interval.
```
theorem realizationTime_injective : Function.Injective PrismBarycentric.realizationTime.hom := by
…
```
theorem OAI.Thomason.Construction.realizedCylinder_second line 170
Source documentation
Every point of the cylinder has the same interval coordinate as the canonical edge at that time.
```
theorem realizedCylinder_second {K : SSet.{0}} (x : SSet.toTop.obj K) (t : unitInterval) :
    (SSet.toTop.map (snd K (Δ[1] : SSet.{0}))).hom ((RealizedCylinder.comparison K).hom (x,t)) =
      RealizationPrism.edgePath intervalEdge t := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCylinder.comparison, OAI.Thomason.Construction.RealizationPrism.edgePath, OAI.Thomason.Construction.intervalEdge
def OAI.Thomason.Construction.realizedIntervalPath line 177
Source documentation
The path realized by a base interval, with the exact image vertices.
```
def realizedIntervalPath {B : SSet.{0}} (g : (Δ[1] : SSet.{0}) ⟶ B) :
    Path (RealizationPrism.vertexPoint B (g.app _ (initialSimplexVertex 1)))
      (RealizationPrism.vertexPoint B (g.app _ (finalSimplexVertex 1))) :=
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.finalSimplexVertex

theorem OAI.Thomason.Construction.realized_interval_homotopy_projection line 185

Source documentation

A simplicial cylinder lying exactly over the base interval realizes to a continuous lift of that same parametrized path.

theorem realized_interval_homotopy_projection {K E B : SSet.{0}}
    (p : E ⟶ B) (g : (Δ[1] : SSet.{0}) ⟶ B) {f h : K ⟶ E}
    (H : SSet.Homotopy f h) (hH : H.h ≫ p = snd K Δ[1] ≫ g)
    (t : unitInterval) (x : SSet.toTop.obj K) :
    (SSet.toTop.map p).hom (RealizedCylinder.homotopy H (t,x)) = realizedIntervalPath g t := by
…

Mentions: OAI.Thomason.Construction.RealizedCylinder.homotopy, OAI.Thomason.Construction.realizedIntervalPath

theorem OAI.Thomason.Construction.realizedPointFiber_projection line 218

Source documentation

The realized point-fibre inclusion has exactly the specified constant image.

theorem realizedPointFiber_projection {E B : SSet.{0}} (p : E ⟶ B) (b : B _⦋0⦌)
    (z : SSet.toTop.obj (simplicialPointFiber p b).toSSet) :
    (SSet.toTop.map p).hom ((SSet.toTop.map (simplicialPointFiber p b).ι).hom z) =
      RealizationPrism.vertexPoint B b := by
…

Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.RealizationPrism.vertexPoint

def OAI.Thomason.Construction.realizedPointFiberComparison line 228
Source documentation
The canonical comparison attaches the constant path at the specified vertex. No preservation of pullbacks by realization is assumed.
```
def realizedPointFiberComparison {E B : SSet.{0}} (p : E ⟶ B) (b : B _⦋0⦌) :
    SSet.toTop.obj (simplicialPointFiber p b).toSSet ⟶
      continuousHomotopyFiber (SSet.toTop.map p) (RealizationPrism.vertexPoint B b) :=
…
```
Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.continuousHomotopyFiber, OAI.Thomason.Construction.RealizationPrism.vertexPoint
theorem OAI.Thomason.Construction.realizedPointFiberComparison_retraction line 241
theorem OAI.Thomason.Construction.kan_simplex_realizedPointFiberComparison_weak line 250
Source documentation
For any Kan fibration over a standard simplex, the actual point-fibre comparison is a weak equivalence. This is the local geometric homotopy-fibre statement, proved independently of general acyclic Kan lifting.
```
theorem kan_simplex_realizedPointFiberComparison_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (b : (Δ[n] : SSet.{0}) _⦋0⦌) :
    topologicalWeakEquivalences (realizedPointFiberComparison p b) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedPointFiberComparison
def OAI.Thomason.Construction.realizedFiberAlongInterval line 282
Source documentation
Attach the actual realized base edge to the initial point fibre.
```
def realizedFiberAlongInterval {E B : SSet.{0}} (p : E ⟶ B)
    (g : (Δ[1] : SSet.{0}) ⟶ B) :
    SSet.toTop.obj (simplicialPointFiber p (g.app _ (initialSimplexVertex 1))).toSSet ⟶
      continuousHomotopyFiber (SSet.toTop.map p)
        (RealizationPrism.vertexPoint B (g.app _ (finalSimplexVertex 1))) :=
…
```
Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.continuousHomotopyFiber, OAI.Thomason.Construction.RealizationPrism.vertexPoint, OAI.Thomason.Construction.finalSimplexVertex
theorem OAI.Thomason.Construction.kan_transport_homotopy_fiber line 295
Source documentation
The weak simplicial transport furnished by the Kan lifting property commutes, by a constructed continuous homotopy, with the actual comparison to the terminal homotopy fibre. The homotopy retains the prescribed base edge and the remaining-path coordinate.
```
theorem kan_transport_homotopy_fiber {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (g : (Δ[1] : SSet.{0}) ⟶ B) :
    ∃ t : (simplicialPointFiber p (g.app _ (initialSimplexVertex 1))).toSSet ⟶
        (simplicialPointFiber p (g.app _ (finalSimplexVertex 1))).toSSet,
      realizationWeakEquivalences t ∧
      Nonempty ((realizedFiberAlongInterval p g).hom.Homotopy
        (SSet.toTop.map t ≫ realizedPointFiberComparison p (g.app _ (finalSimplexVertex 1))).hom) := by
…
```
Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.finalSimplexVertex, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.realizedFiberAlongInterval, OAI.Thomason.Construction.realizedPointFiberComparison
theorem OAI.Thomason.Construction.kan_transport_homotopy_fiber_weak_iff line 331
Source documentation
Weakness of the canonical comparison is detected after transporting any neighbouring fibre along its actual base edge. This uses all homotopy groups, with no global fibration-realization theorem assumed.
```
theorem kan_transport_homotopy_fiber_weak_iff {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (g : (Δ[1] : SSet.{0}) ⟶ B) :
    topologicalWeakEquivalences (realizedFiberAlongInterval p g) ↔
      topologicalWeakEquivalences
        (realizedPointFiberComparison p (g.app _ (finalSimplexVertex 1))) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedFiberAlongInterval, OAI.Thomason.Construction.realizedPointFiberComparison, OAI.Thomason.Construction.finalSimplexVertex

def OAI.Thomason.Construction.homotopyFiberFromPathHomotopy line 360

Source documentation

Homotopic chosen paths produce homotopic maps from a fixed point fibre into the actual terminal homotopy fibre.

def homotopyFiberFromPathHomotopy {A E B : TopCat.{0}} (p : E ⟶ B) (f : A ⟶ E)
    {x y : B} {γ δ : Path x y} (H : γ.Homotopy δ) (hf : ∀ a, p.hom (f.hom a) = x) :
    (homotopyFiberFromPath p f γ hf).hom.Homotopy
      (homotopyFiberFromPath p f δ hf).hom where
…

Mentions: OAI.Thomason.Construction.homotopyFiberFromPath

theorem OAI.Thomason.Construction.realizedFiberAlongInterval_append line 386
Source documentation
The exact comparison with a transported point fibre agrees with appending the base path, up to the canonical left-unit homotopy.
```
theorem realizedFiberAlongInterval_append {E B : SSet.{0}} (p : E ⟶ B)
    (g : (Δ[1] : SSet.{0}) ⟶ B) :
    Nonempty ((realizedPointFiberComparison p (g.app _ (initialSimplexVertex 1)) ≫
      homotopyFiberPathTransport (SSet.toTop.map p) (realizedIntervalPath g)).hom.Homotopy
      (realizedFiberAlongInterval p g).hom) := by
…
```
Mentions: OAI.Thomason.Construction.realizedPointFiberComparison, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.homotopyFiberPathTransport, OAI.Thomason.Construction.realizedIntervalPath, OAI.Thomason.Construction.realizedFiberAlongInterval
theorem OAI.Thomason.Construction.kan_fiber_comparison_weak_iff_of_interval line 407
Source documentation
For an arbitrary Kan fibration, the full actual weak-equivalence test for its point-fibre comparison is unchanged along a base interval.
```
theorem kan_fiber_comparison_weak_iff_of_interval {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (g : (Δ[1] : SSet.{0}) ⟶ B) :
    topologicalWeakEquivalences
      (realizedPointFiberComparison p (g.app _ (initialSimplexVertex 1))) ↔
    topologicalWeakEquivalences
      (realizedPointFiberComparison p (g.app _ (finalSimplexVertex 1))) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedPointFiberComparison, OAI.Thomason.Construction.initialSimplexVertex, OAI.Thomason.Construction.finalSimplexVertex
theorem OAI.Thomason.Construction.kan_fiber_comparison_weak_iff_of_edge line 421
Source documentation
The same genuine comparison test is invariant along every simplicial edge, with its given endpoints.
```
theorem kan_fiber_comparison_weak_iff_of_edge {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] {x y : B _⦋0⦌} (e : SSet.Edge x y) :
    topologicalWeakEquivalences (realizedPointFiberComparison p x) ↔
      topologicalWeakEquivalences (realizedPointFiberComparison p y) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedPointFiberComparison
theorem OAI.Thomason.Construction.kan_fiber_comparison_weak_iff_of_realization_path line 454
Source documentation
The actual point-fibre/homotopy-fibre comparison is weak at one vertex if and only if it is weak at any vertex joined to it by a continuous path.
```
theorem kan_fiber_comparison_weak_iff_of_realization_path {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] {x y : B _⦋0⦌}
    (h : Path (RealizationPrism.vertexPoint B x) (RealizationPrism.vertexPoint B y)) :
    topologicalWeakEquivalences (realizedPointFiberComparison p x) ↔
      topologicalWeakEquivalences (realizedPointFiberComparison p y) := by
…
```
Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint, OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedPointFiberComparison
theorem OAI.Thomason.Construction.realizedVertexSubcomplex_range line 485
def OAI.Thomason.Construction.realizedPointFiberHomeomorph line 503
Source documentation
Realization commutes homeomorphically with a fibre over a simplicial vertex, using the closed subcomplex embedding.
```
def realizedPointFiberHomeomorph {E B : SSet.{0}} (p : E ⟶ B) (b : B _⦋0⦌) :
    SSet.toTop.obj (simplicialPointFiber p b).toSSet ≃ₜ
      {x : SSet.toTop.obj E // (SSet.toTop.map p).hom x = RealizationPrism.vertexPoint B b} :=
…
```
Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.RealizationPrism.vertexPoint
theorem OAI.Thomason.Construction.realizedPointFiberHomeomorph_val line 513
Source documentation
The homeomorphism retains the original total-space point exactly.
```
theorem realizedPointFiberHomeomorph_val {E B : SSet.{0}} (p : E ⟶ B) (b : B _⦋0⦌)
    (x : SSet.toTop.obj (simplicialPointFiber p b).toSSet) :
    (realizedPointFiberHomeomorph p b x).val =
      (SSet.toTop.map (simplicialPointFiber p b).ι).hom x := rfl
```
Mentions: OAI.Thomason.Construction.simplicialPointFiber, OAI.Thomason.Construction.realizedPointFiberHomeomorph
def OAI.Thomason.Construction.continuousPointFiberComparison line 520
Source documentation
The canonical map from the literal continuous point fibre into the homotopy fibre appends its constant path.
```
def continuousPointFiberComparison {X Y : TopCat.{0}} (p : X ⟶ Y) (b : Y) :
    TopCat.of {x : X // p.hom x = b} ⟶ continuousHomotopyFiber p b :=
…
```
Mentions: OAI.Thomason.Construction.continuousHomotopyFiber
theorem OAI.Thomason.Construction.realizedPointFiberComparison_homeomorph line 530
Source documentation
The two fibre comparisons commute exactly under the homeomorphism.
```
theorem realizedPointFiberComparison_homeomorph {E B : SSet.{0}} (p : E ⟶ B)
    (b : B _⦋0⦌) :
    (TopCat.isoOfHomeo (realizedPointFiberHomeomorph p b)).hom ≫
      continuousPointFiberComparison (SSet.toTop.map p) (RealizationPrism.vertexPoint B b) =
        realizedPointFiberComparison p b := by
…
```
Mentions: OAI.Thomason.Construction.realizedPointFiberHomeomorph, OAI.Thomason.Construction.continuousPointFiberComparison, OAI.Thomason.Construction.RealizationPrism.vertexPoint, OAI.Thomason.Construction.realizedPointFiberComparison
theorem OAI.Thomason.Construction.kan_simplex_continuousPointFiberComparison_weak line 544
Source documentation
At every vertex of a standard simplex, the realized Kan fibration is quasifibrant: its literal continuous fibre maps weakly to its homotopy fibre.
```
theorem kan_simplex_continuousPointFiberComparison_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (b : (Δ[n] : SSet.{0}) _⦋0⦌) :
    topologicalWeakEquivalences
      (continuousPointFiberComparison (SSet.toTop.map p) (RealizationPrism.vertexPoint _ b)) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousPointFiberComparison, OAI.Thomason.Construction.RealizationPrism.vertexPoint
theorem OAI.Thomason.Construction.continuousPointFiberComparison_naturality line 572
Source documentation
The constant-path comparison commutes exactly with every commutative square of continuous maps, including the full path coordinate.
```
@[reassoc] theorem continuousPointFiberComparison_naturality {X Y A B : TopCat.{0}}
    (p : X ⟶ A) (q : Y ⟶ B) (f : X ⟶ Y) (g : A ⟶ B)
    (h : f ≫ q = p ≫ g) (b : A) :
    continuousFiberBaseChangeMap p q f g h b ≫
        continuousPointFiberComparison q (g.hom b) =
      continuousPointFiberComparison p b ≫ continuousHomotopyFiberMap p q f g h b := by
…
```
Mentions: OAI.Thomason.Construction.continuousFiberBaseChangeMap, OAI.Thomason.Construction.continuousPointFiberComparison, OAI.Thomason.Construction.continuousHomotopyFiberMap
theorem OAI.Thomason.Construction.continuousFiberBaseChange_weak_iff_homotopyFiberMap line 592
Source documentation
If the two canonical comparisons are weak equivalences, a square induces a weak equivalence on literal fibres precisely when it does on homotopy fibres. This transports the actual weak-equivalence tests.
```
theorem continuousFiberBaseChange_weak_iff_homotopyFiberMap {X Y A B : TopCat.{0}}
    (p : X ⟶ A) (q : Y ⟶ B) (f : X ⟶ Y) (g : A ⟶ B)
    (h : f ≫ q = p ≫ g) (b : A)
    (hp : topologicalWeakEquivalences (continuousPointFiberComparison p b))
    (hq : topologicalWeakEquivalences (continuousPointFiberComparison q (g.hom b))) :
    topologicalWeakEquivalences (continuousFiberBaseChangeMap p q f g h b) ↔
      topologicalWeakEquivalences (continuousHomotopyFiberMap p q f g h b) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousPointFiberComparison, OAI.Thomason.Construction.continuousFiberBaseChangeMap, OAI.Thomason.Construction.continuousHomotopyFiberMap
theorem OAI.Thomason.Construction.RealizedCube.kan_realizedPointFiberComparison_weak line 631
Source documentation
The literal realized vertex fibre of a Kan fibration over a finite cube maps weakly to its genuine continuous homotopy fibre.
```
theorem kan_realizedPointFiberComparison_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p] (b : (obj n) _⦋0⦌) :
    topologicalWeakEquivalences (realizedPointFiberComparison p b) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.realizedPointFiberComparison
theorem OAI.Thomason.Construction.RealizedCube.kan_continuousPointFiberComparison_weak line 644
Source documentation
Under the constructed fibre homeomorphism, the comparison is exactly the ordinary continuous point-fibre map which appends a constant path.
```
theorem kan_continuousPointFiberComparison_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p] (b : (obj n) _⦋0⦌) :
    topologicalWeakEquivalences
      (continuousPointFiberComparison (SSet.toTop.map p) (RealizationPrism.vertexPoint _ b)) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousPointFiberComparison, OAI.Thomason.Construction.RealizationPrism.vertexPoint
theorem OAI.Thomason.Construction.RealizedCube.kan_baseChange_weak line 655
Source documentation
Every simplicial map between finite cubes preserves the total space of a Kan fibration up to the actual realization weak-equivalence test.
```
theorem kan_baseChange_weak {E : SSet.{0}} (n m : ℕ)
    (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p] (g : obj m ⟶ obj n) :
    realizationWeakEquivalences (pullback.fst p g) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.RealizedCube.homotopyFiberMap line 669
Source documentation
The actual map on continuous homotopy fibres induced by a cubical base change retains both point and path coordinates.
```
def homotopyFiberMap {E : SSet.{0}} (n m : ℕ)
    (p : E ⟶ obj n) (g : obj m ⟶ obj n) (b : SSet.toTop.obj (obj m)) :
    continuousHomotopyFiber (SSet.toTop.map (pullback.snd p g)) b ⟶
      continuousHomotopyFiber (SSet.toTop.map p) ((SSet.toTop.map g).hom b) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.continuousHomotopyFiber
theorem OAI.Thomason.Construction.RealizedCube.homotopyFiberMap_weak line 678
Source documentation
Cubical base change commutes with the genuine continuous homotopy fibre by an actual weak equivalence.
```
theorem homotopyFiberMap_weak {E : SSet.{0}} (n m : ℕ)
    (p : E ⟶ obj n) [HomotopicalAlgebra.Fibration p] (g : obj m ⟶ obj n)
    (b : SSet.toTop.obj (obj m)) :
    topologicalWeakEquivalences (homotopyFiberMap n m p g b) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.RealizedCube.homotopyFiberMap
theorem OAI.Thomason.Construction.RealizedCube.realizedProductCubeFiberInclusion_weak line 707
Source documentation
The literal fibre inclusion of a realized product projection over any point of the cube is a weak equivalence.
```
theorem realizedProductCubeFiberInclusion_weak (F : SSet.{0}) (n : ℕ)
    (b : SSet.toTop.obj (obj n)) :
    topologicalWeakEquivalences (continuousFiberInclusion
      (SSet.toTop.map (snd F (obj n))) b) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousFiberInclusion
theorem OAI.Thomason.Construction.RealizedCube.kan_cube_continuousFiberInclusion_weak line 721
Source documentation
For a Kan fibration over a standard cube, EVERY literal continuous fibre includes by a weak equivalence. The point need not be a vertex.
```
theorem kan_cube_continuousFiberInclusion_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (obj n)) [HomotopicalAlgebra.Fibration p]
    (b : SSet.toTop.obj (obj n)) :
    topologicalWeakEquivalences (continuousFiberInclusion (SSet.toTop.map p) b) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousFiberInclusion
theorem OAI.Thomason.Construction.RealizedCube.kan_cube_allPointFiberComparison_weak line 739
Source documentation
The canonical constant-path comparison from the literal continuous fibre to the actual homotopy fibre is weak at every point of a cube.
```
theorem kan_cube_allPointFiberComparison_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (obj n)) [HomotopicalAlgebra.Fibration p]
    (b : SSet.toTop.obj (obj n)) :
    topologicalWeakEquivalences (continuousPointFiberComparison (SSet.toTop.map p) b) := by
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousPointFiberComparison

theorem OAI.Thomason.Construction.RealizedCube.kan_cube_continuousFiberBaseChange_weak line 770

Source documentation

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

theorem kan_cube_continuousFiberBaseChange_weak {E : SSet.{0}} (n m : ℕ)
    (p : E ⟶ (obj n)) [HomotopicalAlgebra.Fibration p]
    (g : (obj m) ⟶ obj n) (b : SSet.toTop.obj (obj m)) :
    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.RealizedCube.obj, OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousFiberBaseChangeMap

def OAI.Thomason.Construction.continuousProductFiberHomeomorph line 803
Source documentation
The fibre of the ordinary second projection is canonically its first factor. This identification retains the literal subspace topology.
```
def continuousProductFiberHomeomorph (X B : TopCat.{0}) (b : B) :
    continuousFiber (continuousProductProjection X B) b ≃ₜ X where
…
```
Mentions: OAI.Thomason.Construction.continuousFiber, OAI.Thomason.Construction.continuousProductProjection
theorem OAI.Thomason.Construction.realizedFiniteContractedProductFiberInclusion_weak line 817
Source documentation
A stationary contraction of a finite simplicial base makes the inclusion of every literal fibre of the realized product weak, even at a point which is not a simplicial vertex.
```
theorem realizedFiniteContractedProductFiberInclusion_weak
    (F B : SSet.{0}) [B.Finite] (v : B _⦋0⦌)
    (C : SSet.Homotopy (SSet.const v) (𝟙 B))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…
```
theorem OAI.Thomason.Construction.kan_finite_contracted_continuousFiberInclusion_weak line 849
Source documentation
The exact fibrewise Kan trivialization transports the preceding product theorem to any Kan fibration over the finite contracted base.
```
theorem kan_finite_contracted_continuousFiberInclusion_weak
    {E B : SSet.{0}} [B.Finite] (v : B _⦋0⦌)
    (C : SSet.Homotopy (SSet.const v) (𝟙 B))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…
```
theorem OAI.Thomason.Construction.kan_finite_contracted_simplicialFiberInclusion_weak line 870
Source documentation
At a vertex this is the inclusion of the original simplicial fibre, via the proved realization homeomorphism of literal point fibres.
```
theorem kan_finite_contracted_simplicialFiberInclusion_weak
    {E B : SSet.{0}} [B.Finite] (v : B _⦋0⦌)
    (C : SSet.Homotopy (SSet.const v) (𝟙 B))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…
```

theorem OAI.Thomason.Construction.kan_finite_contracted_baseChange_weak line 905

Source documentation

The pullback projection of a Kan fibration along a map between finite contracted parameter complexes is weak. The proof identifies a common literal vertex fibre; it does not assume right properness.

theorem kan_finite_contracted_baseChange_weak
    {E B D : SSet.{0}} [B.Finite] [D.Finite]
    (v : B _⦋0⦌) (w : D _⦋0⦌)
    (C : SSet.Homotopy (SSet.const v) (𝟙 B))
    (T : SSet.Homotopy (SSet.const w) (𝟙 D))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…

theorem OAI.Thomason.Construction.kan_finite_contracted_continuousFiberBaseChange_weak line 933

Source documentation

Under the same finite-parameter hypotheses, every real-point fibre map induced by base change is weak. This retains the exact specified point, rather than replacing it by a chosen vertex.

theorem kan_finite_contracted_continuousFiberBaseChange_weak
    {E B D : SSet.{0}} [B.Finite] [D.Finite]
    (v : B _⦋0⦌) (w : D _⦋0⦌)
    (C : SSet.Homotopy (SSet.const v) (𝟙 B))
    (T : SSet.Homotopy (SSet.const w) (𝟙 D))
    (hC : ∀ L : SSet.{0}, (SSet.const (X := L) v) ▷ Δ[1] ≫ C.h =
…

theorem OAI.Thomason.Construction.realizedProductSimplexFiberInclusion_weak line 975
Source documentation
The literal fibre inclusion of a realized product projection over any point of the simplex is a weak equivalence.
```
theorem realizedProductSimplexFiberInclusion_weak (F : SSet.{0}) (n : ℕ)
    (b : SSet.toTop.obj (Δ[n] : SSet.{0})) :
    topologicalWeakEquivalences (continuousFiberInclusion
      (SSet.toTop.map (snd F (Δ[n] : SSet.{0}))) b) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousFiberInclusion
theorem OAI.Thomason.Construction.kan_simplex_continuousFiberInclusion_weak line 987
Source documentation
For a Kan fibration over a standard simplex, EVERY literal continuous fibre includes by a weak equivalence. The point need not be a vertex.
```
theorem kan_simplex_continuousFiberInclusion_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (b : SSet.toTop.obj (Δ[n] : SSet.{0})) :
    topologicalWeakEquivalences (continuousFiberInclusion (SSet.toTop.map p) b) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousFiberInclusion
theorem OAI.Thomason.Construction.kan_simplex_allPointFiberComparison_weak line 1004
Source documentation
The canonical constant-path comparison from the literal continuous fibre to the actual homotopy fibre is weak at every point of a simplex.
```
theorem kan_simplex_allPointFiberComparison_weak {E : SSet.{0}} (n : ℕ)
    (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
    (b : SSet.toTop.obj (Δ[n] : SSet.{0})) :
    topologicalWeakEquivalences (continuousPointFiberComparison (SSet.toTop.map p) b) := by
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousPointFiberComparison