HomotopyFiberPathEquivalence.lean`

47 declarations, 0 contain sorry, 0 declared as axioms

Path-space compatibility with actual weak equivalences

def OAI.Thomason.Construction.continuousPathStart line 19
Source documentation
Evaluation at the initial endpoint of an unrestricted continuous path.
```
def continuousPathStart (X : TopCat.{0}) : continuousPathSpace X ⟶ X :=
…
```
Mentions: OAI.Thomason.Construction.continuousPathSpace
def OAI.Thomason.Construction.continuousPathConstant line 23
Source documentation
The constant-path section of initial evaluation.
```
def continuousPathConstant (X : TopCat.{0}) : X ⟶ continuousPathSpace X :=
…
```
Mentions: OAI.Thomason.Construction.continuousPathSpace
def OAI.Thomason.Construction.continuousPathContraction line 27
Source documentation
Shrinking the time coordinate contracts each path to its initial point.
```
def continuousPathContraction (X : TopCat.{0}) :
    ((continuousPathConstant X).hom.comp (continuousPathStart X).hom).Homotopy
      (ContinuousMap.id (continuousPathSpace X)) where
…
```
Mentions: OAI.Thomason.Construction.continuousPathConstant, OAI.Thomason.Construction.continuousPathStart, OAI.Thomason.Construction.continuousPathSpace
def OAI.Thomason.Construction.continuousPathStartEquiv line 51
Source documentation
Initial evaluation is an actual homotopy equivalence, naturally in the space.
```
def continuousPathStartEquiv (X : TopCat.{0}) :
    ContinuousMap.HomotopyEquiv (continuousPathSpace X) X where
…
```
Mentions: OAI.Thomason.Construction.continuousPathSpace
theorem OAI.Thomason.Construction.continuousPathStart_naturality line 58
theorem OAI.Thomason.Construction.continuousPathMap_weak_iff line 63
Source documentation
Forming the unrestricted path space preserves and reflects the actual topological weak-equivalence test.
```
theorem continuousPathMap_weak_iff {X Y : TopCat.{0}} (p : X ⟶ Y) :
    IsWeakHomotopyEquivalence (continuousPathMap p).hom ↔
      IsWeakHomotopyEquivalence p.hom := by
…
```
Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.continuousPathMap
theorem OAI.Thomason.Construction.singularPathMap_weak_iff line 83
Source documentation
The same equivalence holds for the actual realization weak test on singular maps, without assuming a general singular comparison theorem.
```
theorem singularPathMap_weak_iff {X Y : TopCat.{0}} (p : X ⟶ Y) :
    realizationWeakEquivalences (TopCat.toSSet.map (continuousPathMap p)) ↔
      realizationWeakEquivalences (TopCat.toSSet.map p) := by
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.continuousPathMap
def OAI.Thomason.Construction.mappingPathSpace line 122
def OAI.Thomason.Construction.mappingPathInclusion line 125
def OAI.Thomason.Construction.mappingPathRetraction line 131
def OAI.Thomason.Construction.mappingPathProjection line 134
theorem OAI.Thomason.Construction.mappingPath_factorization line 138
def OAI.Thomason.Construction.mappingPathContraction line 142
Source documentation
Shrinking a path to its initial point leaves its point over p fixed.
```
def mappingPathContraction {X Y : TopCat.{0}} (p : X ⟶ Y) :
    ((mappingPathInclusion p).hom.comp (mappingPathRetraction p).hom).Homotopy
      (ContinuousMap.id (mappingPathSpace p)) where
…
```
Mentions: OAI.Thomason.Construction.mappingPathInclusion, OAI.Thomason.Construction.mappingPathRetraction, OAI.Thomason.Construction.mappingPathSpace
def OAI.Thomason.Construction.mappingPathEquiv line 173
Source documentation
The mapping-path inclusion is an actual homotopy equivalence.
```
def mappingPathEquiv {X Y : TopCat.{0}} (p : X ⟶ Y) :
    ContinuousMap.HomotopyEquiv X (mappingPathSpace p) where
…
```
Mentions: OAI.Thomason.Construction.mappingPathSpace
theorem OAI.Thomason.Construction.mappingPathProjection_weak_iff line 180
def OAI.Thomason.Construction.continuousHomotopyFiber line 211
Source documentation
The homotopy fibre consists of a point and a path from its image to b.
```
def continuousHomotopyFiber {X Y : TopCat.{0}} (p : X ⟶ Y) (b : Y) : TopCat.{0} :=
…
```
def OAI.Thomason.Construction.continuousHomotopyFiberRetraction line 214

def OAI.Thomason.Construction.continuousHomotopyFiberSection line 219

Source documentation

A continuous interpolation provides a canonical path into the fibre.

def continuousHomotopyFiberSection {X Y : TopCat.{0}} (p : X ⟶ Y) (b : Y)
    (c : C(unitInterval × (Y × Y), Y))
    (h₀ : ∀ x y, c (0, x, y) = x) (h₁ : ∀ x y, c (1, x, y) = y) :
    X ⟶ continuousHomotopyFiber p b :=
…

Mentions: OAI.Thomason.Construction.continuousHomotopyFiber

def OAI.Thomason.Construction.continuousHomotopyFiberContraction line 236
Source documentation
Interpolation contracts each path to the canonical one, fixing both endpoints. This uses an explicit diagonal-preserving interpolation, not a homotopy-fibre preservation assumption.
```
def continuousHomotopyFiberContraction {X Y : TopCat.{0}} (p : X ⟶ Y) (b : Y)
    (c : C(unitInterval × (Y × Y), Y))
    (h₀ : ∀ x y, c (0, x, y) = x) (h₁ : ∀ x y, c (1, x, y) = y)
    (hd : ∀ t x, c (t, x, x) = x) :
    (ContinuousMap.id (continuousHomotopyFiber p b)).Homotopy
      ((continuousHomotopyFiberSection p b c h₀ h₁).hom.comp
        (continuousHomotopyFiberRetraction p b).hom) where
…
```
Mentions: OAI.Thomason.Construction.continuousHomotopyFiber, OAI.Thomason.Construction.continuousHomotopyFiberSection, OAI.Thomason.Construction.continuousHomotopyFiberRetraction

def OAI.Thomason.Construction.continuousHomotopyFiberEquiv line 276

Source documentation

Over a continuously interpolated space the homotopy fibre projects by an actual homotopy equivalence to the original source.

def continuousHomotopyFiberEquiv {X Y : TopCat.{0}} (p : X ⟶ Y) (b : Y)
    (c : C(unitInterval × (Y × Y), Y))
    (h₀ : ∀ x y, c (0, x, y) = x) (h₁ : ∀ x y, c (1, x, y) = y)
    (hd : ∀ t x, c (t, x, x) = x) :
    ContinuousMap.HomotopyEquiv (continuousHomotopyFiber p b) X where
…

Mentions: OAI.Thomason.Construction.continuousHomotopyFiber

def OAI.Thomason.Construction.continuousHomotopyFiberMap line 302
theorem OAI.Thomason.Construction.continuousHomotopyFiberMap_retraction line 322

theorem OAI.Thomason.Construction.continuousHomotopyFiberMap_weak line 331

Source documentation

In a map of homotopy fibres, if both retractions and the source map are weak equivalences, so is the original canonical fibre map.

theorem continuousHomotopyFiberMap_weak {X X' Y Y' : TopCat.{0}}
    (p : X ⟶ Y) (p' : X' ⟶ Y') (f : X ⟶ X') (g : Y ⟶ Y')
    (h : f ≫ p' = p ≫ g) (b : Y)
    (hr : topologicalWeakEquivalences (continuousHomotopyFiberRetraction p b))
    (hr' : topologicalWeakEquivalences (continuousHomotopyFiberRetraction p' (g.hom b)))
    (hf : topologicalWeakEquivalences f) :
    topologicalWeakEquivalences (continuousHomotopyFiberMap p p' f g h b) := by
…

Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.continuousHomotopyFiberRetraction, OAI.Thomason.Construction.continuousHomotopyFiberMap

def OAI.Thomason.Construction.RealizedCube.pointInterpolation line 360
Source documentation
Straight interpolation in the actual coordinates of a realized cube.
```
def pointInterpolation (n : ℕ) :
    C(unitInterval × (SSet.toTop.obj (obj n) × SSet.toTop.obj (obj n)),
      SSet.toTop.obj (obj n)) :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj
theorem OAI.Thomason.Construction.RealizedCube.pointInterpolation_zero line 383
theorem OAI.Thomason.Construction.RealizedCube.pointInterpolation_one line 393
theorem OAI.Thomason.Construction.RealizedCube.pointInterpolation_diagonal line 403
def OAI.Thomason.Construction.RealizedCube.homotopyFiberEquiv line 415
Source documentation
For every continuous map into the realized cube, its actual homotopy fibre projects by a homotopy equivalence to its source.
```
def homotopyFiberEquiv {X : TopCat.{0}} (n : ℕ)
    (p : X ⟶ SSet.toTop.obj (obj n)) (b : SSet.toTop.obj (obj n)) :
    ContinuousMap.HomotopyEquiv (continuousHomotopyFiber p b) X :=
…
```
Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.continuousHomotopyFiber
def OAI.Thomason.Construction.remainingPathParameter line 439
Source documentation
The remaining part of an interval after time s, parametrized again by the unit interval.
```
def remainingPathParameter (s t : unitInterval) : unitInterval :=
…
```
theorem OAI.Thomason.Construction.remainingPathParameter_zero_right line 442
theorem OAI.Thomason.Construction.remainingPathParameter_one_right line 445
theorem OAI.Thomason.Construction.remainingPathParameter_zero_left line 448
theorem OAI.Thomason.Construction.remainingPathParameter_one_left line 451
def OAI.Thomason.Construction.homotopyFiberFromPath line 456
Source documentation
A family of points over the start of a path maps to its terminal homotopy fibre by attaching that same path to every point.
```
def homotopyFiberFromPath {A E B : TopCat.{0}} (p : E ⟶ B) (f : A ⟶ E)
    {x y : B} (γ : Path x y) (hf : ∀ a, p.hom (f.hom a) = x) :
    A ⟶ continuousHomotopyFiber p y :=
…
```
Mentions: OAI.Thomason.Construction.continuousHomotopyFiber

def OAI.Thomason.Construction.homotopyFiberLiftedPath line 469

Source documentation

An actual lift of a base path gives an explicit homotopy in its terminal homotopy fibre. The path coordinate is its remaining tail, so the statement retains the whole family, not just its path components or weak status.

def homotopyFiberLiftedPath {A E B : TopCat.{0}} (p : E ⟶ B)
    {f g : A ⟶ E} (H : f.hom.Homotopy g.hom) {x y : B} (γ : Path x y)
    (hH : ∀ s a, p.hom (H (s,a)) = γ s) :
    (homotopyFiberFromPath p f γ
      (fun a => (congrArg p.hom (H.apply_zero a)).symm.trans ((hH 0 a).trans γ.source))).hom.Homotopy
    (homotopyFiberFromPath p g (Path.refl y)
      (fun a => (congrArg p.hom (H.apply_one a)).symm.trans ((hH 1 a).trans γ.target))).hom where
…

Mentions: OAI.Thomason.Construction.homotopyFiberFromPath

theorem OAI.Thomason.Construction.homotopyFiberLiftedPath_weak_iff line 517

Source documentation

Consequently the two canonical maps into the actual homotopy fibre have the same weak-equivalence status in every degree.

theorem homotopyFiberLiftedPath_weak_iff {A E B : TopCat.{0}} (p : E ⟶ B)
    {f g : A ⟶ E} (H : f.hom.Homotopy g.hom) {x y : B} (γ : Path x y)
    (hH : ∀ s a, p.hom (H (s,a)) = γ s) :
    topologicalWeakEquivalences (homotopyFiberFromPath p f γ
      (fun a => (congrArg p.hom (H.apply_zero a)).symm.trans ((hH 0 a).trans γ.source))) ↔
    topologicalWeakEquivalences (homotopyFiberFromPath p g (Path.refl y)
      (fun a => (congrArg p.hom (H.apply_one a)).symm.trans ((hH 1 a).trans γ.target))) :=
…

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

def OAI.Thomason.Construction.homotopyFiberPath line 544
Source documentation
The path coordinate of an actual homotopy-fibre point, with both endpoints recorded in its type.
```
def homotopyFiberPath {E B : TopCat.{0}} {p : E ⟶ B} {b : B}
    (z : continuousHomotopyFiber p b) : Path (p.hom z.val.val.1) b where
…
```
Mentions: OAI.Thomason.Construction.continuousHomotopyFiber
def OAI.Thomason.Construction.homotopyFiberPathTransport line 552
Source documentation
Transport in the base appends the specified path and leaves the point in the total space fixed.
```
def homotopyFiberPathTransport {E B : TopCat.{0}} (p : E ⟶ B) {b c : B}
    (γ : Path b c) : continuousHomotopyFiber p b ⟶ continuousHomotopyFiber p c :=
…
```
Mentions: OAI.Thomason.Construction.continuousHomotopyFiber

def OAI.Thomason.Construction.homotopyFiberReparametrize line 570

Source documentation

Reparametrizing a homotopy-fibre path preserves its point coordinate.

def homotopyFiberReparametrize {E B : TopCat.{0}} (p : E ⟶ B) (b : B)
    (α : unitInterval → unitInterval) (hα : Continuous α) (h₀ : α 0 = 0) (h₁ : α 1 = 1) :
    continuousHomotopyFiber p b ⟶ continuousHomotopyFiber p b :=
…

Mentions: OAI.Thomason.Construction.continuousHomotopyFiber

def OAI.Thomason.Construction.homotopyFiberReparametrizeHomotopy line 588
Source documentation
The reparametrization homotopy is continuous even as the starting point of the path varies over the total space.
```
def homotopyFiberReparametrizeHomotopy {E B : TopCat.{0}} (p : E ⟶ B) (b : B)
    (α : unitInterval → unitInterval) (hα : Continuous α) (h₀ : α 0 = 0) (h₁ : α 1 = 1) :
    (ContinuousMap.id (continuousHomotopyFiber p b)).Homotopy
      (homotopyFiberReparametrize p b α hα h₀ h₁).hom where
…
```
Mentions: OAI.Thomason.Construction.continuousHomotopyFiber, OAI.Thomason.Construction.homotopyFiberReparametrize
def OAI.Thomason.Construction.homotopyFiberPathTransportHomotopy line 617
Source documentation
A homotopy of base paths induces a homotopy of the actual transport maps. All point coordinates remain fixed.
```
def homotopyFiberPathTransportHomotopy {E B : TopCat.{0}} (p : E ⟶ B) {b c : B}
    {γ δ : Path b c} (H : γ.Homotopy δ) :
    (homotopyFiberPathTransport p γ).hom.Homotopy (homotopyFiberPathTransport p δ).hom where
…
```
Mentions: OAI.Thomason.Construction.homotopyFiberPathTransport
def OAI.Thomason.Construction.homotopyFiberPathTransportAssoc line 651
Source documentation
Associating the appended paths is a homotopy on the whole homotopy fibre, including the varying point and starting endpoint.
```
def homotopyFiberPathTransportAssoc {E B : TopCat.{0}} (p : E ⟶ B) {b c d : B}
    (γ : Path b c) (δ : Path c d) :
    (homotopyFiberPathTransport p γ ≫ homotopyFiberPathTransport p δ).hom.Homotopy
      (homotopyFiberPathTransport p (γ.trans δ)).hom := by
…
```
Mentions: OAI.Thomason.Construction.homotopyFiberPathTransport
def OAI.Thomason.Construction.fibreRightUnitParameter line 684
def OAI.Thomason.Construction.homotopyFiberPathTransportUnit line 689
Source documentation
Appending the constant path is homotopic to the identity, continuously in every total-space point and every homotopy-fibre path.
```
def homotopyFiberPathTransportUnit {E B : TopCat.{0}} (p : E ⟶ B) (b : B) :
    (homotopyFiberPathTransport p (Path.refl b)).hom.Homotopy
      (ContinuousMap.id (continuousHomotopyFiber p b)) := by
…
```
Mentions: OAI.Thomason.Construction.homotopyFiberPathTransport, OAI.Thomason.Construction.continuousHomotopyFiber
def OAI.Thomason.Construction.homotopyFiberPathTransportCancel line 706
Source documentation
A path followed by its reverse cancels on the full actual homotopy fibre. This is stronger than equality on components.
```
def homotopyFiberPathTransportCancel {E B : TopCat.{0}} (p : E ⟶ B) {b c : B}
    (γ : Path b c) :
    (homotopyFiberPathTransport p γ ≫ homotopyFiberPathTransport p γ.symm).hom.Homotopy
      (ContinuousMap.id (continuousHomotopyFiber p b)) :=
…
```
Mentions: OAI.Thomason.Construction.homotopyFiberPathTransport, OAI.Thomason.Construction.continuousHomotopyFiber
def OAI.Thomason.Construction.homotopyFiberPathEquiv line 716
Source documentation
The explicit homotopy equivalence between homotopy fibres associated to a base path; its inverse appends the reversed path.
```
def homotopyFiberPathEquiv {E B : TopCat.{0}} (p : E ⟶ B) {b c : B} (γ : Path b c) :
    ContinuousMap.HomotopyEquiv (continuousHomotopyFiber p b) (continuousHomotopyFiber p c) where
…
```
Mentions: OAI.Thomason.Construction.continuousHomotopyFiber
theorem OAI.Thomason.Construction.homotopyFiberPathTransport_weak line 728
Source documentation
Base-path transport on the actual homotopy fibres is an actual weak homotopy equivalence, independently of all simplicial model inputs.
```
theorem homotopyFiberPathTransport_weak {E B : TopCat.{0}} (p : E ⟶ B)
    {b c : B} (γ : Path b c) :
    topologicalWeakEquivalences (homotopyFiberPathTransport p γ) :=
…
```
Mentions: OAI.Thomason.Construction.topologicalWeakEquivalences, OAI.Thomason.Construction.homotopyFiberPathTransport