OAI/CategoryTheory/Thomason/Simplicial/FiniteRelativeRealizationLifting.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thomason.Construction.hornFacets line 27
2. theorem OAI.Thomason.Construction.faceUnion_hornFacets line 30
3. def OAI.Thomason.Construction.hornFaceSet line 37
4. theorem OAI.Thomason.Construction.hornFaceSet_iff line 40
5. theorem OAI.Thomason.Construction.subdivided_hornFacets line 59
6. theorem OAI.Thomason.Construction.subdivision_horn_range line 87
7. theorem OAI.Thomason.Construction.hornFaceNerve_range line 93
8. theorem OAI.Thomason.Construction.subdivision_horn_anodyne line 110

   Source documentation

   The actual left-Kan-extension subdivision sends every generating horn inclusion to an anodyne map, by the explicit finite face-poset collapse.

   theorem subdivision_horn_anodyne (n : ℕ) (k : Fin (n + 2)) :
       SSet.anodyneExtensions (SSet.sd.map (SSet.horn.{0} (n+1) k).ι) := by
   …

9. theorem OAI.Thomason.Construction.singular_to_point_fibration line 167

   Source documentation

   The map to a point is a singular Kan fibration for every topological space.

   theorem singular_to_point_fibration (T : TopCat.{0}) :
       HomotopicalAlgebra.Fibration
         (TopCat.toSSet.map (TopCat.ofHom (ContinuousMap.const T ()) : T ⟶ TopCat.of Unit)) := by
   …

10. theorem OAI.Thomason.Construction.singular_counit_weak_of_weaklyContractible line 189

    Source documentation

    Weak contractibility suffices for the actual singular-realization comparison; no contraction or global counit-W theorem is assumed.

    theorem singular_counit_weak_of_weaklyContractible (X : TopCat.{0})
        (hX : IsWeakHomotopyEquivalence (ContinuousMap.const X ())) :
        topologicalWeakEquivalences (sSetTopAdj.counit.app X) := by
    …

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

11. theorem OAI.Thomason.Construction.singular_point_hom_ext line 224
12. theorem OAI.Thomason.Construction.singular_anodyne_endpoint_extension line 237

    Source documentation

    A homotopy over an anodyne parameter inclusion extends while preserving both arbitrary endpoint maps on the entire target parameter object.

    theorem singular_anodyne_endpoint_extension {A K : SSet.{0}} (i : A ⟶ K)
        (hi : SSet.anodyneExtensions i) (Y : TopCat.{0})
        (f₀ f₁ : K ⟶ TopCat.toSSet.obj Y)
        (a : A ⊗ Δ[1] ⟶ TopCat.toSSet.obj Y)
        (ha₀ : SSet.ι₀ ≫ a = i ≫ f₀) (ha₁ : SSet.ι₁ ≫ a = i ≫ f₁) :
        ∃ e : K ⊗ Δ[1] ⟶ TopCat.toSSet.obj Y,
          i ▷ Δ[1] ≫ e = a ∧ SSet.ι₀ ≫ e = f₀ ∧ SSet.ι₁ ≫ e = f₁ := by
    …

13. theorem OAI.Thomason.Construction.realization_anodyne_endpoint_extension line 257

    Source documentation

    The endpoint-preserving extension evaluated on actual realizations.

    theorem realization_anodyne_endpoint_extension {A K : SSet.{0}} (i : A ⟶ K)
        (hi : SSet.anodyneExtensions i) {Y : TopCat.{0}}
        (f₀ f₁ : SSet.toTop.obj K ⟶ Y)
        (a : C(unitInterval × SSet.toTop.obj A, Y))
        (ha₀ : ∀ z, a (0, z) = f₀.hom ((SSet.toTop.map i).hom z))
        (ha₁ : ∀ z, a (1, z) = f₁.hom ((SSet.toTop.map i).hom z)) :
        ∃ e : C(unitInterval × SSet.toTop.obj K, Y),
          (∀ t z, e (t, (SSet.toTop.map i).hom z) = a (t, z)) ∧
          (∀ z, e (0, z) = f₀.hom z) ∧ ∀ z, e (1, z) = f₁.hom z := by
    …

14. theorem OAI.Thomason.Construction.boundary_rlp_lifts_homotopic line 310

    Source documentation

    Two simplicial lifts through a boundary-trivial fibration are connected by one simplicial cylinder, still over the same base map.

    theorem boundary_rlp_lifts_homotopic {X Y K : SSet.{0}} (p : X ⟶ Y)
        (hp : I.rlp p) (f₀ f₁ : K ⟶ X) (he : f₀ ≫ p = f₁ ≫ p) :
        ∃ H : K ⊗ Δ[1] ⟶ X,
          SSet.ι₀ ≫ H = f₀ ∧ SSet.ι₁ ≫ H = f₁ ∧
          H ≫ p = fst K Δ[1] ≫ f₀ ≫ p := by
    …

15. theorem OAI.Thomason.Construction.singular_acyclic_lifts_homotopic line 345

    Source documentation

    Two continuous lifts from any actual realization through a singular Kan fibration which is weak are homotopic.

    theorem singular_acyclic_lifts_homotopic {X Y : TopCat.{0}} (p : X ⟶ Y)
        [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
        (hp : IsWeakHomotopyEquivalence p.hom) (K : SSet.{0})
        (f₀ f₁ : SSet.toTop.obj K ⟶ X) (he : f₀ ≫ p = f₁ ≫ p) :
        Nonempty (f₀.hom.Homotopy f₁.hom) := by
    …

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

16. theorem OAI.Thomason.Construction.singular_acyclic_realized_lift line 371

    Source documentation

    Maps from realizations lift through acyclic singular fibrations, even when the target map is not itself a realized simplicial map.

    theorem singular_acyclic_realized_lift {X Y : TopCat.{0}} (p : X ⟶ Y)
        [HomotopicalAlgebra.Fibration (TopCat.toSSet.map p)]
        (hp : IsWeakHomotopyEquivalence p.hom) (K : SSet.{0})
        (b : SSet.toTop.obj K ⟶ Y) :
        ∃ a : SSet.toTop.obj K ⟶ X, a ≫ p = b := by
    …

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

17. theorem OAI.Thomason.Construction.mappingPath_singular_lifting line 410

    Source documentation

    Mapping-path projections lift every anodyne simplicial parameter extension.

    theorem mappingPath_singular_lifting {X Y : TopCat.{0}} (p : X ⟶ Y)
        {A K : SSet.{0}} (i : A ⟶ K) (hi : SSet.anodyneExtensions i) :
        HasLiftingProperty i (TopCat.toSSet.map (mappingPathProjection p)) := by
    …

    Mentions: OAI.Thomason.Construction.mappingPathProjection

18. theorem OAI.Thomason.Construction.mappingPath_singular_fibration line 474

    Source documentation

    The endpoint projection is a genuine singular Kan fibration for every continuous map, without any weak-equivalence hypothesis.

    theorem mappingPath_singular_fibration {X Y : TopCat.{0}} (p : X ⟶ Y) :
        HomotopicalAlgebra.Fibration (TopCat.toSSet.map (mappingPathProjection p)) := by
    …

    Mentions: OAI.Thomason.Construction.mappingPathProjection

19. def OAI.Thomason.Construction.realizationWhiteheadEquiv line 502

    Source documentation

    A weak map between geometric realizations has a constructed continuous homotopy inverse. The proof uses the actual mapping-path fibration and the proved singular boundary lifts, without a Kan–Quillen model structure.

    def realizationWhiteheadEquiv {K L : SSet.{0}}
        (f : SSet.toTop.obj K ⟶ SSet.toTop.obj L)
        (hf : IsWeakHomotopyEquivalence f.hom) :
        ContinuousMap.HomotopyEquiv (SSet.toTop.obj K) (SSet.toTop.obj L) := by
    …

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

20. theorem OAI.Thomason.Construction.realization_weak_iff_homotopyEquiv line 531

    Source documentation

    The actual weak test on a realized simplicial map is precisely the existence of a homotopy equivalence with that same continuous forward map.

    theorem realization_weak_iff_homotopyEquiv {K L : SSet.{0}} (f : K ⟶ L) :
        realizationWeakEquivalences f ↔
          ∃ e : ContinuousMap.HomotopyEquiv (SSet.toTop.obj K) (SSet.toTop.obj L),
            e.toFun = (SSet.toTop.map f).hom := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

21. theorem OAI.Thomason.Construction.singular_map_weak_iff line 563

    Source documentation

    The actual singular realization detects exactly the original topological weak-equivalence test for every continuous map. The preservation direction uses the constructed mapping-path factorization and full boundary lifting.

    theorem singular_map_weak_iff {X Y : TopCat.{0}} (p : X ⟶ Y) :
        realizationWeakEquivalences (TopCat.toSSet.map p) ↔
          IsWeakHomotopyEquivalence p.hom := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.IsWeakHomotopyEquivalence

22. theorem OAI.Thomason.Construction.singular_counit_weak_iff_of_weak line 580

    Source documentation

    The counit weak test transports along every actual weak homotopy equivalence, without requiring a chosen homotopy inverse.

    theorem singular_counit_weak_iff_of_weak {X Y : TopCat.{0}} (p : X ⟶ Y)
        (hp : IsWeakHomotopyEquivalence p.hom) :
        topologicalWeakEquivalences (sSetTopAdj.counit.app X) ↔
          topologicalWeakEquivalences (sSetTopAdj.counit.app Y) := by
    …

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

23. theorem OAI.Thomason.Construction.fixedPathToInternal_postcomp line 615
24. theorem OAI.Thomason.Construction.fixedPathInternalIso_naturality line 639

    Source documentation

    Naturality retains the specified endpoints under the actual singular vertex identification, rather than choosing them up to paths.

    theorem fixedPathInternalIso_naturality {X Y : TopCat.{0}} (p : X ⟶ Y) (x y : X) :
        TopCat.toSSet.map (TopCat.ofHom (PathSpace.map p.hom (x := x) (y := y))) ≫
    …

    Mentions: OAI.Thomason.Construction.PathSpace.map

25. def OAI.Thomason.Construction.fixedPathInternalMapArrowIso line 654
26. theorem OAI.Thomason.Construction.fixedInternalPathMap_singular_weak line 664

    Source documentation

    The fixed-endpoint internal-path map of an actual singular weak map is a realization weak equivalence. This uses the proved dimension shift for continuous fixed-path spaces and exact singular preservation of W.

    theorem fixedInternalPathMap_singular_weak {X Y : TopCat.{0}} (p : X ⟶ Y)
        (hp : realizationWeakEquivalences (TopCat.toSSet.map p)) (x y : X) :
        realizationWeakEquivalences (fixedInternalPathMap (TopCat.toSSet.map p)
          (TopCat.toSSetObj₀Equiv.symm x) (TopCat.toSSetObj₀Equiv.symm y)) := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.fixedInternalPathMap

27. theorem OAI.Thomason.Construction.continuousHomotopyFiber_weak line 690

    Source documentation

    All actual homotopy fibres of a weak continuous map are weakly contractible. This uses the constructed singular Kan mapping-path fibration.

    theorem continuousHomotopyFiber_weak {X Y : TopCat.{0}} (p : X ⟶ Y)
        (hp : IsWeakHomotopyEquivalence p.hom) (b : Y) :
        IsWeakHomotopyEquivalence
          (ContinuousMap.const (continuousHomotopyFiber p b) ()) := by
    …

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.continuousHomotopyFiber

28. theorem OAI.Thomason.Construction.continuousHomotopyFiber_extension line 700

    Source documentation

    In every dimension, a continuous boundary family in the genuine homotopy fibre of a weak map extends exactly over the original realization.

    theorem continuousHomotopyFiber_extension {X Y : TopCat.{0}} (p : X ⟶ Y)
        (hp : IsWeakHomotopyEquivalence p.hom) (b : Y)
        {K L : SSet.{0}} (i : K ⟶ L) [Mono i]
        (a : SSet.toTop.obj K ⟶ continuousHomotopyFiber p b) :
        ∃ g : SSet.toTop.obj L ⟶ continuousHomotopyFiber p b,
          SSet.toTop.map i ≫ g = a := by
    …

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.continuousHomotopyFiber

29. theorem OAI.Thomason.Construction.weaklyContractible_realized_extension line 730

    Source documentation

    A weakly contractible space fills any realized monomorphism exactly. The proof uses the already proved singular acyclic lifting theorem.

    theorem weaklyContractible_realized_extension (T : TopCat.{0})
        (hT : IsWeakHomotopyEquivalence (ContinuousMap.const T ()))
        {A K : SSet.{0}} (i : A ⟶ K) [Mono i] (a : SSet.toTop.obj A ⟶ T) :
        ∃ c : SSet.toTop.obj K ⟶ T, SSet.toTop.map i ≫ c = a := by
    …

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

30. theorem OAI.Thomason.Construction.kan_acyclic_simplex_continuousFiber_weak line 747

    Source documentation

    Every literal point fibre of an acyclic Kan map over a simplex is weakly contractible, including fibres over nonvertex points.

    theorem kan_acyclic_simplex_continuousFiber_weak {E : SSet.{0}} (n : ℕ)
        (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
        (hp : realizationWeakEquivalences p) (b : SSet.toTop.obj (Δ[n] : SSet.{0})) :
        IsWeakHomotopyEquivalence (ContinuousMap.const (continuousFiber (SSet.toTop.map p) b) ()) :=
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.continuousFiber

31. theorem OAI.Thomason.Construction.kan_acyclic_simplex_continuousFiber_extension line 757

    Source documentation

    Higher continuous boundary families extend EXACTLY inside a literal fibre of an acyclic Kan simplex map. This is a geometric extension and does not claim a simplicial filler.

    theorem kan_acyclic_simplex_continuousFiber_extension {E A K : SSet.{0}} (n : ℕ)
        (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
        (hp : realizationWeakEquivalences p) (b : SSet.toTop.obj (Δ[n] : SSet.{0}))
        (i : A ⟶ K) [Mono i]
        (a : SSet.toTop.obj A ⟶ continuousFiber (SSet.toTop.map p) b) :
        ∃ c : SSet.toTop.obj K ⟶ continuousFiber (SSet.toTop.map p) b,
          SSet.toTop.map i ≫ c = a :=
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.continuousFiber

32. theorem OAI.Thomason.Construction.finite_acyclic_simplex_continuousFiber_extension line 769

    Source documentation

    For a finite parameter complex, the exact fibre extension takes place in one finite subcomplex of the ORIGINAL total space, with constant base coordinate at every point and the whole continuous boundary retained.

    theorem finite_acyclic_simplex_continuousFiber_extension {E A K : SSet.{0}} [K.Finite]
        (n : ℕ) (p : E ⟶ (Δ[n] : SSet.{0})) [HomotopicalAlgebra.Fibration p]
        (hp : realizationWeakEquivalences p) (b : SSet.toTop.obj (Δ[n] : SSet.{0}))
        (i : A ⟶ K) [Mono i]
        (a : SSet.toTop.obj A ⟶ continuousFiber (SSet.toTop.map p) b) :
        ∃ (S : E.Subcomplex) (_ : SSet.Finite S.toSSet)
          (c : SSet.toTop.obj K ⟶ SSet.toTop.obj S.toSSet),
          SSet.toTop.map i ≫ c ≫ SSet.toTop.map S.ι =
            a ≫ continuousFiberInclusion (SSet.toTop.map p) b ∧
          ∀ z, (SSet.toTop.map p).hom ((SSet.toTop.map S.ι).hom (c.hom z)) = b := by
    …

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.continuousFiber, OAI.Thomason.Construction.continuousFiberInclusion

33. theorem OAI.Thomason.Construction.RealizedCube.kan_acyclic_cube_continuousFiber_weak line 816

    Source documentation

    Every literal point fibre of an acyclic Kan map over a cube is weakly contractible, including fibres over nonvertex points.

    theorem kan_acyclic_cube_continuousFiber_weak {E : SSet.{0}} (n : ℕ)
        (p : E ⟶ (obj n)) [HomotopicalAlgebra.Fibration p]
        (hp : realizationWeakEquivalences p) (b : SSet.toTop.obj (obj n)) :
        IsWeakHomotopyEquivalence (ContinuousMap.const (continuousFiber (SSet.toTop.map p) b) ()) :=
    …

    Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.IsWeakHomotopyEquivalence, OAI.Thomason.Construction.continuousFiber

34. theorem OAI.Thomason.Construction.RealizedCube.kan_acyclic_cube_continuousFiber_extension line 826

    Source documentation

    Higher continuous boundary families extend EXACTLY inside a literal fibre of an acyclic Kan cube map. This is a geometric extension and does not claim a simplicial filler.

    theorem kan_acyclic_cube_continuousFiber_extension {E A K : SSet.{0}} (n : ℕ)
        (p : E ⟶ (obj n)) [HomotopicalAlgebra.Fibration p]
        (hp : realizationWeakEquivalences p) (b : SSet.toTop.obj (obj n))
        (i : A ⟶ K) [Mono i]
        (a : SSet.toTop.obj A ⟶ continuousFiber (SSet.toTop.map p) b) :
        ∃ c : SSet.toTop.obj K ⟶ continuousFiber (SSet.toTop.map p) b,
          SSet.toTop.map i ≫ c = a :=
    …

    Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.continuousFiber

35. theorem OAI.Thomason.Construction.RealizedCube.finite_acyclic_cube_continuousFiber_extension line 838

    Source documentation

    For a finite parameter complex, the exact fibre extension takes place in one finite subcomplex of the ORIGINAL total space, with constant base coordinate at every point and the whole continuous boundary retained.

    theorem finite_acyclic_cube_continuousFiber_extension {E A K : SSet.{0}} [K.Finite]
        (n : ℕ) (p : E ⟶ (obj n)) [HomotopicalAlgebra.Fibration p]
        (hp : realizationWeakEquivalences p) (b : SSet.toTop.obj (obj n))
        (i : A ⟶ K) [Mono i]
        (a : SSet.toTop.obj A ⟶ continuousFiber (SSet.toTop.map p) b) :
        ∃ (S : E.Subcomplex) (_ : SSet.Finite S.toSSet)
          (c : SSet.toTop.obj K ⟶ SSet.toTop.obj S.toSSet),
          SSet.toTop.map i ≫ c ≫ SSet.toTop.map S.ι =
            a ≫ continuousFiberInclusion (SSet.toTop.map p) b ∧
          ∀ z, (SSet.toTop.map p).hom ((SSet.toTop.map S.ι).hom (c.hom z)) = b := by
    …

    Mentions: OAI.Thomason.Construction.RealizedCube.obj, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.continuousFiber, OAI.Thomason.Construction.continuousFiberInclusion

36. theorem OAI.Thomason.Construction.weak_relative_realization_lift line 885

    Source documentation

    Every actual weak equivalence lifts a square on a realized simplicial mono up to a target homotopy. The source boundary extension is exact and the target homotopy fixes the entire realized subcomplex pointwise.

    theorem weak_relative_realization_lift {X Y : TopCat.{0}} (f : X ⟶ Y)
        (hf : IsWeakHomotopyEquivalence f.hom) {K L : SSet.{0}} (i : K ⟶ L) [Mono i]
        (a : SSet.toTop.obj K ⟶ X) (b : SSet.toTop.obj L ⟶ Y)
        (h : a ≫ f = SSet.toTop.map i ≫ b) :
        ∃ c : SSet.toTop.obj L ⟶ X,
          SSet.toTop.map i ≫ c = a ∧
          Nonempty ((c ≫ f).hom.HomotopyRel b.hom (Set.range (SSet.toTop.map i).hom)) := by
    …

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

37. theorem OAI.Thomason.Construction.finite_relative_realization_lift line 942

    Source documentation

    Relative lifting along an actual weak map with realization source can be performed in one finite simplicial subcomplex. The prescribed simplicial boundary map factors through that same subcomplex exactly.

    theorem finite_relative_realization_lift {A B L : SSet.{0}} [B.Finite]
        (i : A ⟶ B) [Mono i] {Y : TopCat.{0}} (f : SSet.toTop.obj L ⟶ Y)
        (hf : IsWeakHomotopyEquivalence f.hom) (a : A ⟶ L)
        (b : SSet.toTop.obj B ⟶ Y) (h : SSet.toTop.map a ≫ f = SSet.toTop.map i ≫ b) :
        ∃ S : L.Subcomplex, SSet.Finite (S : SSet) ∧
          ∃ (a' : A ⟶ (S : SSet)) (c : SSet.toTop.obj B ⟶ SSet.toTop.obj (S : SSet)),
            a' ≫ S.ι = a ∧ SSet.toTop.map i ≫ c = SSet.toTop.map a' ∧
            Nonempty ((c ≫ SSet.toTop.map S.ι ≫ f).hom.HomotopyRel b.hom
              (Set.range (SSet.toTop.map i).hom)) := by
    …

    Mentions: OAI.Thomason.Construction.IsWeakHomotopyEquivalence

38. theorem OAI.Thomason.Construction.finite_relative_internalPath_approximation line 1000

    Source documentation

    A continuous family of paths in a Kan realization admits a relative finite approximation by realized internal paths. The homotopy is fixed on the prescribed simplicial parameter subcomplex. No claim about fixed endpoint fibres is hidden in this statement.

    theorem finite_relative_internalPath_approximation {A B X : SSet.{0}} [B.Finite]
        [SSet.KanComplex X] (i : A ⟶ B) [Mono i]
        (a : A ⟶ internalPathObject X)
        (b : SSet.toTop.obj B ⟶ continuousPathSpace (SSet.toTop.obj X))
        (h : SSet.toTop.map a ≫ realizedInternalPathComparison X = SSet.toTop.map i ≫ b) :
        ∃ S : (internalPathObject X).Subcomplex, SSet.Finite (S : SSet) ∧
          ∃ (a' : A ⟶ (S : SSet)) (c : SSet.toTop.obj B ⟶ SSet.toTop.obj (S : SSet)),
            a' ≫ S.ι = a ∧ SSet.toTop.map i ≫ c = SSet.toTop.map a' ∧
            Nonempty ((c ≫ SSet.toTop.map S.ι ≫ realizedInternalPathComparison X).hom.HomotopyRel
              b.hom (Set.range (SSet.toTop.map i).hom)) :=
    …

    Mentions: OAI.Thomason.Construction.internalPathObject, OAI.Thomason.Construction.continuousPathSpace, OAI.Thomason.Construction.realizedInternalPathComparison