SingularAcyclicFibers.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Singular fixed-endpoint paths as the actual internal path subcomplex

def OAI.Thomason.Construction.fixedPathToInternal line 21

Source documentation

Transposing a continuous family of fixed paths lands in the exact fixed-endpoint subcomplex of the singular internal hom.

def fixedPathToInternal {K : SSet.{0}} {X : TopCat.{0}} {x y : X}
    (f : K ⟶ TopCat.toSSet.obj (TopCat.of (Path x y))) :
    K ⟶ fixedInternalPaths (TopCat.toSSet.obj X)
      (TopCat.toSSetObj₀Equiv.symm x) (TopCat.toSSetObj₀Equiv.symm y) :=
…

Mentions: OAI.Thomason.Construction.fixedInternalPaths

def OAI.Thomason.Construction.internalToFixedPath line 33

Source documentation

Evaluation reverses this construction on a family in the actual fixed-endpoint internal path complex.

def internalToFixedPath {K : SSet.{0}} {X : TopCat.{0}} {x y : X}
    (a : K ⟶ fixedInternalPaths (TopCat.toSSet.obj X)
      (TopCat.toSSetObj₀Equiv.symm x) (TopCat.toSSetObj₀Equiv.symm y)) :
    K ⟶ TopCat.toSSet.obj (TopCat.of (Path x y)) :=
…

Mentions: OAI.Thomason.Construction.fixedInternalPaths

theorem OAI.Thomason.Construction.internalToFixedPath_left_inverse line 44
theorem OAI.Thomason.Construction.internalToFixedPath_cylinder line 61
theorem OAI.Thomason.Construction.fixedPathToInternal_right_inverse line 74

def OAI.Thomason.Construction.fixedPathInternalEquiv line 84

Source documentation

This is an isomorphism of hom sets, not merely a bijection of components.

def fixedPathInternalEquiv (K : SSet.{0}) (X : TopCat.{0}) (x y : X) :
    (K ⟶ TopCat.toSSet.obj (TopCat.of (Path x y))) ≃
      (K ⟶ fixedInternalPaths (TopCat.toSSet.obj X)
        (TopCat.toSSetObj₀Equiv.symm x) (TopCat.toSSetObj₀Equiv.symm y)) where
…

Mentions: OAI.Thomason.Construction.fixedInternalPaths

theorem OAI.Thomason.Construction.fixedPathToInternal_naturality line 93
def OAI.Thomason.Construction.fixedPathInternalIso line 105
Source documentation
The singular complex of the genuine fixed-endpoint path space is the actual fixed-endpoint subcomplex of the simplicial internal hom.
```
def fixedPathInternalIso (X : TopCat.{0}) (x y : X) :
    TopCat.toSSet.obj (TopCat.of (Path x y)) ≅
      fixedInternalPaths (TopCat.toSSet.obj X)
        (TopCat.toSSetObj₀Equiv.symm x) (TopCat.toSSetObj₀Equiv.symm y) :=
…
```
Mentions: OAI.Thomason.Construction.fixedInternalPaths

theorem OAI.Thomason.Construction.fixedPath_singular_lifting line 134

Source documentation

Passing to paths with prescribed endpoints preserves lifting against every anodyne parameter inclusion.

theorem fixedPath_singular_lifting {A K : SSet.{0}} (i : A ⟶ K)
    (hi : SSet.anodyneExtensions i) {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)] (x y : X) :
    HasLiftingProperty i (TopCat.toSSet.map
      (TopCat.ofHom (PathSpace.map p.hom (x := x) (y := y)))) := by
…

Mentions: OAI.Thomason.Construction.PathSpace.map

theorem OAI.Thomason.Construction.fixedPath_singular_fibration line 184

Source documentation

The actual map on fixed-endpoint path spaces is a singular Kan fibration.

theorem fixedPath_singular_fibration {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)] (x y : X) :
    HomotopicalAlgebra.Fibration (TopCat.toSSet.map
      (TopCat.ofHom (PathSpace.map p.hom (x := x) (y := y)))) := by
…

Mentions: OAI.Thomason.Construction.PathSpace.map

theorem OAI.Thomason.Construction.singular_fibration_lift_based_homotopy line 213

Source documentation

A singular Kan fibration which is an actual weak equivalence lifts based cubical homotopies with both endpoint cubes and the entire boundary fixed.

theorem singular_fibration_lift_based_homotopy (n : ℕ) {X Y : TopCat.{0}}
    (p : X ⟶ Y) [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) {x : X}
    (a b : GenLoop (Fin n) X x)
    (H : (HomotopyMaps.loopMap p.hom a).val.HomotopyRel
      (HomotopyMaps.loopMap p.hom b).val (Cube.boundary (Fin n))) :
    ∃ F : a.val.HomotopyRel b.val (Cube.boundary (Fin n)),
      ∀ z, p.hom (F z) = H z := by
…

Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.HomotopyMaps.loopMap

theorem OAI.Thomason.Construction.singular_acyclic_lift_based_homotopy line 262

Source documentation

The same exact relative homotopy lift under the singular realization test.

theorem singular_acyclic_lift_based_homotopy (n : ℕ) {X Y : TopCat.{0}}
    (p : X ⟶ Y) [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) {x : X}
    (a b : GenLoop (Fin n) X x)
    (H : (HomotopyMaps.loopMap p.hom a).val.HomotopyRel
      (HomotopyMaps.loopMap p.hom b).val (Cube.boundary (Fin n))) :
    ∃ F : a.val.HomotopyRel b.val (Cube.boundary (Fin n)),
      ∀ z, p.hom (F z) = H z :=
…

Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.HomotopyMaps.loopMap

theorem OAI.Thomason.Construction.singular_fibration_fiber_nonempty line 289
theorem OAI.Thomason.Construction.singular_fibration_fiber_joined line 296

theorem OAI.Thomason.Construction.singular_fibration_fiber_nullhomotopy line 314

Source documentation

Every based cubical map into a point fibre has a nullhomotopy inside that same fibre, relative to the complete cubical boundary.

theorem singular_fibration_fiber_nullhomotopy {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) (y : Y)
    (x : {z : X // p.hom z = y}) (n : ℕ)
    (a : GenLoop (Fin n) {z : X // p.hom z = y} x) :
    Nonempty (a.val.HomotopyRel (ContinuousMap.const _ x) (Cube.boundary (Fin n))) := by
…

Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

theorem OAI.Thomason.Construction.singular_fibration_fiber_components_subsingleton line 339

Source documentation

The fibre has a single component.

theorem singular_fibration_fiber_components_subsingleton {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) (y : Y) :
    Subsingleton (ZerothHomotopy {x : X // p.hom x = y}) := by
…

Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

theorem OAI.Thomason.Construction.singular_fibration_fiber_groups_subsingleton line 352

Source documentation

Every based homotopy group of the fibre is trivial, including degree zero in the cubical quotient convention.

theorem singular_fibration_fiber_groups_subsingleton {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) (y : Y)
    (x : {z : X // p.hom z = y}) (n : ℕ) :
    Subsingleton (HomotopyGroup.Pi n {z : X // p.hom z = y} x) := by
…

Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

theorem OAI.Thomason.Construction.singular_fibration_fiber_weak line 372

Source documentation

The map from each actual point fibre to a point is a weak homotopy equivalence, with no assumption about a singular counit.

theorem singular_fibration_fiber_weak {X Y : TopCat.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
    (hp : IsWeakHomotopyEquivalence p.hom) (y : Y) :
    IsWeakHomotopyEquivalence
      (ContinuousMap.const {x : X // p.hom x = y} ()) := by
…

Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

theorem OAI.Thomason.Construction.singular_acyclic_fiber_weak line 394