OAI/CategoryTheory/Thomason/Simplicial/SubcomplexFaceLifting.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Detecting finite simplicial homotopies in a Kan realization

A continuous extension over a parameter that embeds in a simplex gives an exact simplicial extension. Applying this to the two ends of the actual simplicial cylinder detects homotopies in the original Kan target.

  1. theorem OAI.Thomason.Construction.kan_extension_of_realization_extension_of_simplex_mono line 34

    Source documentation

    Transport the simplex-subcomplex extension theorem along the actual range isomorphisms of a pair of monomorphisms.

    theorem kan_extension_of_realization_extension_of_simplex_mono
    {A B X : SSet.{0}} [SSet.KanComplex X] {n : ℕ}
    (e : B ⟶ (Δ[n] : SSet.{0})) [Mono e] (i : A ⟶ B) [Mono i]
    (a : A ⟶ X) (b : SSet.toTop.obj B ⟶ SSet.toTop.obj X)
    (h : SSet.toTop.map i ≫ b = SSet.toTop.map a) :
    ∃ d : B ⟶ X, i ≫ d = a := by
…
  2. theorem OAI.Thomason.Construction.kan_extension_of_finitePoset_realization_extension line 73

    Source documentation

    A finite-poset parameter is an actual simplex subcomplex after a finite linear extension, so the same exact extension theorem applies.

    theorem kan_extension_of_finitePoset_realization_extension
    (P : Type) [PartialOrder P] [Finite P] [Nonempty P]
    {A X : SSet.{0}} [SSet.KanComplex X]
    (i : A ⟶ nerve P) [Mono i] (a : A ⟶ X)
    (b : SSet.toTop.obj (nerve P) ⟶ SSet.toTop.obj X)
    (h : SSet.toTop.map i ≫ b = SSet.toTop.map a) :
    ∃ d : nerve P ⟶ X, i ≫ d = a := by
…
  3. theorem OAI.Thomason.Construction.simplicialCylinder_inclusion_comp line 83
  4. theorem OAI.Thomason.Construction.simplicialCylinder_desc_comp line 92
  5. def OAI.Thomason.Construction.realizedHomotopyCylinder line 101
  6. theorem OAI.Thomason.Construction.realizedHomotopyCylinder_ends line 109

    Source documentation

    The singular homotopy can be evaluated on the actual simplicial cylinder, with the two original realized endpoint maps exact.

    theorem realizedHomotopyCylinder_ends {K X : SSet.{0}} {f g : K ⟶ X}
    (H : (SSet.toTop.map f).hom.Homotopy (SSet.toTop.map g).hom) :
    SSet.toTop.map (SimplicialCylinder.inclusion K) ≫ realizedHomotopyCylinder H =
      SSet.toTop.map (SimplicialCylinder.desc f g) := by
…

    Mentions: OAI.Thomason.Construction.SimplicialCylinder.inclusion, OAI.Thomason.Construction.realizedHomotopyCylinder, OAI.Thomason.Construction.SimplicialCylinder.desc

  7. theorem OAI.Thomason.Construction.realizedHomotopy_cylinder_extension line 122
  8. theorem OAI.Thomason.Construction.realizedHomotopyCylinder_stationary line 131

    Source documentation

    The same evaluated cylinder retains stationarity on the whole realized image of a prescribed simplicial subobject.

    theorem realizedHomotopyCylinder_stationary {A K X : SSet.{0}} {f g : K ⟶ X}
    (i : A ⟶ K)
    (H : (SSet.toTop.map f).hom.Homotopy (SSet.toTop.map g).hom)
    (hH : ∀ (t : unitInterval) (x : SSet.toTop.obj A),
      H (t, (SSet.toTop.map i).hom x) =
        (SSet.toTop.map f).hom ((SSet.toTop.map i).hom x)) :
    SSet.toTop.map (i ▷ Δ[1]) ≫ realizedHomotopyCylinder H =
      SSet.toTop.map (fst A Δ[1] ≫ i ≫ f) := by
…

    Mentions: OAI.Thomason.Construction.realizedHomotopyCylinder

  9. theorem OAI.Thomason.Construction.cylinder_simplex_embedding line 151
  10. theorem OAI.Thomason.Construction.kan_homotopy_of_realization_homotopy_of_simplex_mono line 175

    Source documentation

    A continuous homotopy between two simplicial maps into a Kan complex is detected by a genuine simplicial homotopy for every simplex subcomplex parameter, including every finite-poset nerve.

    theorem kan_homotopy_of_realization_homotopy_of_simplex_mono
    {K X : SSet.{0}} [SSet.KanComplex X] {n : ℕ}
    (e : K ⟶ (Δ[n] : SSet.{0})) [Mono e] {f g : K ⟶ X}
    (H : (SSet.toTop.map f).hom.Homotopy (SSet.toTop.map g).hom) :
    Nonempty (SSet.Homotopy f g) := by
…
  11. theorem OAI.Thomason.Construction.kan_finitePoset_homotopy_iff line 199
  12. theorem OAI.Thomason.Construction.intervalBoundaryFamily_comp line 232
  13. theorem OAI.Thomason.Construction.intervalBoundaryFamily_self line 245
  14. theorem OAI.Thomason.Construction.realizedHomotopyCylinder_intervalBoundary line 255
  15. theorem OAI.Thomason.Construction.kan_homotopy_of_realization_homotopy_rel line 270

    Source documentation

    Relative continuous homotopy gives a simplicial homotopy which fixes the prescribed subcomplex exactly.

    theorem kan_homotopy_of_realization_homotopy_rel
    {K X : SSet.{0}} [SSet.KanComplex X] {n : ℕ}
    (e : K ⟶ (Δ[n] : SSet.{0})) [Mono e] (A : K.Subcomplex)
    {f g : K ⟶ X} (hfg : A.ι ≫ f = A.ι ≫ g)
    (H : (SSet.toTop.map f).hom.HomotopyRel (SSet.toTop.map g).hom
      (Set.range (SSet.toTop.map A.ι).hom)) :
    ∃ h : SSet.Homotopy f g,
      A.ι ▷ Δ[1] ≫ h.h = fst A.toSSet Δ[1] ≫ A.ι ≫ f := by
…
  16. theorem OAI.Thomason.Construction.SubdivisionBarycentric.iteratedChainRealization_homotopy line 350
  17. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_iteratedSubdivision_descent_homotopy line 373
  18. theorem OAI.Thomason.Construction.realization_homotopy_of_precomp line 404

    Source documentation

    A weak equivalence of actual realizations reflects continuous homotopies after precomposition.

    theorem realization_homotopy_of_precomp {A B : SSet.{0}} (u : A ⟶ B)
    (hu : realizationWeakEquivalences u) {T : TopCat.{0}}
    (f g : SSet.toTop.obj B ⟶ T)
    (H : (f.hom.comp (SSet.toTop.map u).hom).Homotopy
      (g.hom.comp (SSet.toTop.map u).hom)) :
    Nonempty (f.hom.Homotopy g.hom) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  19. theorem OAI.Thomason.Construction.exists_kan_realization_approximation line 420

    Source documentation

    No subdivision remains in the source, and the comparison is a homotopy to the given continuous map in the original Kan realization.

    theorem exists_kan_realization_approximation (P : PartOrd.{0}) [Fintype P]
    (X : SSet.{0}) [SSet.KanComplex X]
    (F : C(SSet.toTop.obj (nerve P), SSet.toTop.obj X)) :
    ∃ g : nerve P ⟶ X, Nonempty (F.Homotopy (SSet.toTop.map g).hom) := by
…
  20. theorem OAI.Thomason.Construction.exactify_realization_relative_lift line 478

    Source documentation

    Exactify a relative lift when the projection comparison is an actual continuous homotopy fixing the prescribed subcomplex.

    theorem exactify_realization_relative_lift
    {K E B : SSet.{0}} [SSet.KanComplex B] {n : ℕ}
    (e : K ⟶ (Δ[n] : SSet.{0})) [Mono e] (A : K.Subcomplex)
    (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (d : K ⟶ E) (b : K ⟶ B)
    (hdb : A.ι ≫ (d ≫ p) = A.ι ≫ b)
    (H : (SSet.toTop.map (d ≫ p)).hom.HomotopyRel (SSet.toTop.map b).hom
      (Set.range (SSet.toTop.map A.ι).hom)) :
    ∃ l : K ⟶ E, A.ι ≫ l = A.ι ≫ d ∧ l ≫ p = b := by
…
  21. theorem OAI.Thomason.Construction.exists_kan_stationary_lift_of_realization_homotopy line 494

    Source documentation

    The exactification can itself be chosen with a stationary simplicial homotopy from the initial map. In particular it preserves the actual realization weak-equivalence test.

    theorem exists_kan_stationary_lift_of_realization_homotopy
    {K E B : SSet.{0}} [SSet.KanComplex B] {n : ℕ}
    (e : K ⟶ (Δ[n] : SSet.{0})) [Mono e] (A : K.Subcomplex)
    (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (d : K ⟶ E) (b : K ⟶ B)
    (hdb : A.ι ≫ (d ≫ p) = A.ι ≫ b)
    (H : (SSet.toTop.map (d ≫ p)).hom.HomotopyRel (SSet.toTop.map b).hom
      (Set.range (SSet.toTop.map A.ι).hom)) :
    ∃ (l : K ⟶ E) (s : SSet.Homotopy d l),
      A.ι ≫ l = A.ι ≫ d ∧ l ≫ p = b ∧
      A.ι ▷ Δ[1] ≫ s.h = fst A.toSSet Δ[1] ≫ A.ι ≫ d ∧
      Nonempty ((SSet.toTop.map d).hom.HomotopyRel (SSet.toTop.map l).hom
…
  22. theorem OAI.Thomason.Construction.exactify_realization_relative_lift_mono line 543

    Source documentation

    The relative realization exactification theorem applies to any monomorphism into a simplex subcomplex, using its actual range.

    theorem exactify_realization_relative_lift_mono
    {A K E B : SSet.{0}} [SSet.KanComplex B] {n : ℕ}
    (e : K ⟶ (Δ[n] : SSet.{0})) [Mono e] (i : A ⟶ K) [Mono i]
    (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (d : K ⟶ E) (b : K ⟶ B)
    (hdb : i ≫ (d ≫ p) = i ≫ b)
    (H : (SSet.toTop.map (d ≫ p)).hom.HomotopyRel (SSet.toTop.map b).hom
      (Set.range (SSet.toTop.map i).hom)) :
    ∃ l : K ⟶ E, i ≫ l = i ≫ d ∧ l ≫ p = b := by
…
  23. theorem OAI.Thomason.Construction.kan_weak_map_surjective_homotopy line 603
  24. theorem OAI.Thomason.Construction.kan_weak_map_reflects_homotopy line 619
  25. theorem OAI.Thomason.Construction.kan_weak_fibration_lift_finitePoset line 645

    Source documentation

    This lifts the base map exactly; no boundary condition is asserted by this intermediate theorem.

    theorem kan_weak_fibration_lift_finitePoset
    (P : PartOrd.{0}) [Fintype P] [Nonempty P]
    {E B : SSet.{0}} [SSet.KanComplex E] [SSet.KanComplex B]
    (p : E ⟶ B) [HomotopicalAlgebra.Fibration p]
    (hp : realizationWeakEquivalences p) (b : nerve P ⟶ B) :
    ∃ a : nerve P ⟶ E, a ≫ p = b := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  26. theorem OAI.Thomason.Construction.weaklyContractible_kan_boundary_extension line 681
  27. theorem OAI.Thomason.Construction.kan_boundary_lifting_of_weak_fibers line 689
  28. theorem OAI.Thomason.Construction.kan_boundary_rlp_of_weak_fibers line 720
  29. theorem OAI.Thomason.Construction.weak_fibers_of_boundary_rlp line 732

    Source documentation

    Boundary lifting also forces actual weak contractibility of every original vertex fibre. Thus the preceding sufficient condition captures the precise fibre obstruction, independently of any model structure.

    theorem weak_fibers_of_boundary_rlp {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (hp : I.rlp p) (v : B _⦋0⦌) :
    IsWeakHomotopyEquivalence
      (ContinuousMap.const (SSet.toTop.obj (simplicialPointFiber p v).toSSet) ()) := by
…

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

  30. theorem OAI.Thomason.Construction.kan_boundary_rlp_iff_weak_fibers line 763
  31. theorem OAI.Thomason.Construction.InfiniteExtension.weak_fiber_of_point_pullback_weak line 795

    Source documentation

    Weakness of the actual pullback over a vertex makes the original simplicial vertex fibre weakly contractible.

    theorem weak_fiber_of_point_pullback_weak {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (v : B _⦋0⦌)
    (h : realizationWeakEquivalences
      (pullback.snd p (SSet.const (X := (Δ[0] : SSet.{0})) v))) :
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences

  32. theorem OAI.Thomason.Construction.InfiniteExtension.boundary_rlp_of_map_arbitrary_base line 829

    Source documentation

    The infinite extension reflects boundary lifting without any Kan assumption on the original base.

    theorem boundary_rlp_of_map_arbitrary_base {E B : SSet.{0}} (p : E ⟶ B)
    [HomotopicalAlgebra.Fibration p] (hp : I.rlp (map p)) : I.rlp p := by
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.map

  33. theorem OAI.Thomason.Construction.InfiniteExtension.map_boundary_rlp_iff_arbitrary_base line 840
  34. theorem OAI.Thomason.Construction.InfiniteExtension.acyclicKanLifting_of_fibrant_case line 847

    Source documentation

    Only weak Kan fibrations between Kan complexes remain in the general acyclic lifting problem. This is a reduction, not an assumption in the main theorem or a proof of that restricted case.

    theorem acyclicKanLifting_of_fibrant_case
    (h : ∀ {E B : SSet.{0}} [SSet.KanComplex E] [SSet.KanComplex B]
      (p : E ⟶ B) [HomotopicalAlgebra.Fibration p],
        realizationWeakEquivalences p → I.rlp p) : PublishedAcyclicKanLifting := by
…

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

  35. theorem OAI.Thomason.Construction.simplexSubcomplex_lift_of_facePoset_lift line 880