OAI/CategoryTheory/Thomason/Simplicial/KanFinitePosetExtension.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Subdivision descent with a homotopy over the prescribed base

The greatest-vertex prism is stationary after projection. Consequently the descended map and its comparison homotopy both respect the given base map exactly.

  1. theorem OAI.Thomason.Construction.exists_subdivision_stationary_descent_over_kan line 30
  2. theorem OAI.Thomason.Construction.exists_finitePoset_subdivision_stationary_descent_over_kan line 77
  3. theorem OAI.Thomason.Construction.exists_subdivision_domain_relative_descent line 112
  4. theorem OAI.Thomason.Construction.exists_finitePoset_subdivision_domain_relative_descent line 174
  5. theorem OAI.Thomason.Construction.canonicalExtension_subdivision_twice_subcomplex_anodyne line 186
  6. theorem OAI.Thomason.Construction.exists_twice_subdivision_domain_relative_descent line 199

    Source documentation

    A second subdivision of finite simplex subcomplexes can be removed while fixing the entire once-subdivided prescribed source.

    theorem exists_twice_subdivision_domain_relative_descent {m n : ℕ}
    (A : (Δ[m] : SSet.{0}).Subcomplex) (B : (Δ[n] : SSet.{0}).Subcomplex)
    {X : SSet.{0}} [SSet.KanComplex X] (i : A.toSSet ⟶ B.toSSet) [Mono i]
    (a : SSet.sd.obj A.toSSet ⟶ X) (f : SSet.sd.obj (SSet.sd.obj B.toSSet) ⟶ X)
    (hi : SSet.sd.map (SSet.sd.map i) ≫ f = lastVertex.app (SSet.sd.obj A.toSSet) ≫ a) :
    ∃ (g : SSet.sd.obj B.toSSet ⟶ X)
      (H : SSet.Homotopy (lastVertex.app (SSet.sd.obj B.toSSet) ≫ g) f),
      SSet.sd.map i ≫ g = a ∧ (SSet.sd.map (SSet.sd.map i) ▷ Δ[1]) ≫ H.h =
        fst (SSet.sd.obj (SSet.sd.obj A.toSSet)) Δ[1] ≫
          lastVertex.app (SSet.sd.obj A.toSSet) ≫ a := by
…
  7. theorem OAI.Thomason.Construction.exists_simplexSubcomplex_subdivision_relative_descent line 234

    Source documentation

    A subdivision of a simplex subcomplex can be removed while preserving any prescribed simplex subcomplex and its entire constant homotopy.

    theorem exists_simplexSubcomplex_subdivision_relative_descent {m n : ℕ}
    (A : (Δ[m] : SSet.{0}).Subcomplex) (B : (Δ[n] : SSet.{0}).Subcomplex)
    {X : SSet.{0}} [SSet.KanComplex X] (i : A.toSSet ⟶ B.toSSet) [Mono i]
    (a : A.toSSet ⟶ X) (f : SSet.sd.obj B.toSSet ⟶ X)
    (hi : SSet.sd.map i ≫ f = lastVertex.app A.toSSet ≫ a) :
    ∃ (g : B.toSSet ⟶ X) (H : SSet.Homotopy (lastVertex.app B.toSSet ≫ g) f),
      i ≫ g = a ∧ (SSet.sd.map i ▷ Δ[1]) ≫ H.h =
        fst (SSet.sd.obj A.toSSet) Δ[1] ≫ lastVertex.app A.toSSet ≫ a :=
…
  8. theorem OAI.Thomason.Construction.exists_boundary_subdivision_relative_descent line 247
  9. theorem OAI.Thomason.Construction.exists_subdivision_relative_base_descent line 287
  10. theorem OAI.Thomason.Construction.exists_simplexSubcomplex_subdivision_relative_base_descent line 396
  11. theorem OAI.Thomason.Construction.InfiniteExtension.stageUnit_naturality line 438
  12. theorem OAI.Thomason.Construction.InfiniteExtension.exists_stage_relative_descent line 442
  13. theorem OAI.Thomason.Construction.InfiniteExtension.exists_stage_simplexSubcomplex_relative_descent line 481
  14. theorem OAI.Thomason.Construction.InfiniteExtension.exists_stage_boundary_descent line 496
  15. theorem OAI.Thomason.Construction.InfiniteExtension.exists_infinite_boundary_descent line 512

    Source documentation

    Finite support lets an exact original-boundary solution in the infinite extension descend all the way into the original Kan fibration.

    theorem exists_infinite_boundary_descent (n : ℕ) {E Z : SSet.{0}} [SSet.KanComplex Z]
    (p : E ⟶ Z) [HomotopicalAlgebra.Fibration p]
    (a : (SSet.boundary.{0} n).toSSet ⟶ E)
    (f : (Δ[n] : SSet.{0}) ⟶ obj E) (b : (Δ[n] : SSet.{0}) ⟶ Z)
    (ha : a ≫ p = (SSet.boundary.{0} n).ι ≫ b)
    (hf : f ≫ map p = b ≫ unit Z)
    (hi : (SSet.boundary.{0} n).ι ≫ f = a ≫ unit E) :
    ∃ g : (Δ[n] : SSet.{0}) ⟶ E,
      (SSet.boundary.{0} n).ι ≫ g = a ∧ g ≫ p = b := by
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.obj, OAI.Thomason.Construction.InfiniteExtension.map, OAI.Thomason.Construction.InfiniteExtension.unit

  16. theorem OAI.Thomason.Construction.InfiniteExtension.boundary_rlp_of_map line 530

    Source documentation

    On Kan fibrations over Kan bases, the actual infinite extension reflects the boundary right lifting property.

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

    Mentions: OAI.Thomason.Construction.InfiniteExtension.map

  17. theorem OAI.Thomason.Construction.InfiniteExtension.map_boundary_rlp_iff line 543
  18. theorem OAI.Thomason.Construction.iteratedSubdivision_succ_obj line 570
  19. theorem OAI.Thomason.Construction.iteratedLastVertex_naturality line 577
  20. def OAI.Thomason.Construction.subcomplexFirstSubdivisionIso line 592
  21. theorem OAI.Thomason.Construction.iteratedSubdivision_subcomplex_canonical_anodyne line 597
  22. theorem OAI.Thomason.Construction.iteratedSubdivision_standard_canonical_anodyne line 610
  23. theorem OAI.Thomason.Construction.exists_iteratedSubdivision_relative_base_descent line 619

    Source documentation

    A relative lift at any finite subdivision descends to a lift over the original parameter. The two equalities in the conclusion are literal.

    theorem exists_iteratedSubdivision_relative_base_descent {A B E Z : SSet.{0}}
    [SSet.KanComplex Z] (i : A ⟶ B) [Mono i]
    (p : E ⟶ Z) [HomotopicalAlgebra.Fibration p]
    (hA : ∀ r, SSet.anodyneExtensions
      (canonicalExtension.app ((iteratedSubdivision r).obj A)))
    (hB : ∀ r, SSet.anodyneExtensions
      (canonicalExtension.app ((iteratedSubdivision r).obj B)))
    (r : ℕ) (a : A ⟶ E) (f : (iteratedSubdivision r).obj B ⟶ E) (b : B ⟶ Z)
    (ha : a ≫ p = i ≫ b)
    (hf : f ≫ p = iteratedLastVertex B r ≫ b)
    (hi : (iteratedSubdivision r).map i ≫ f = iteratedLastVertex A r ≫ a) :
    ∃ g : B ⟶ E, i ≫ g = a ∧ g ≫ p = b := by
…

    Mentions: OAI.Thomason.Construction.iteratedSubdivision, OAI.Thomason.Construction.iteratedLastVertex

  24. theorem OAI.Thomason.Construction.exists_iterated_simplexSubcomplex_relative_base_descent line 658
  25. theorem OAI.Thomason.Construction.exists_iterated_boundary_lift line 672
  26. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_poset_relative_approximation line 711
  27. theorem OAI.Thomason.Construction.SubdivisionBarycentric.kan_extension_of_poset_realization_extension line 763

    Source documentation

    A continuous relative extension in a poset realization gives an exact simplicial extension after any map into a Kan target. All finite subdivisions and the boundary homotopy are removed in that same target.

    theorem kan_extension_of_poset_realization_extension
    (A B : PartOrd.{0}) [Finite A] [Fintype B]
    {P : Type} [PartialOrder P]
    (i : A →o B) (hi : Function.Injective i) (g : A →o P)
    (F : C(SSet.toTop.obj (nerve B), SSet.toTop.obj (nerve P)))
    (hF : ∀ z, F ((SSet.toTop.map (nerveMap i.monotone.functor)).hom z) =
      (SSet.toTop.map (nerveMap g.monotone.functor)).hom z)
    {X : SSet.{0}} [SSet.KanComplex X] (k : nerve P ⟶ X) :
    ∃ d : nerve B ⟶ X, nerveMap i.monotone.functor ≫ d =
      nerveMap g.monotone.functor ≫ k := by
…
  28. theorem OAI.Thomason.Construction.kan_extension_on_resolved_facePoset line 819
  29. theorem OAI.Thomason.Construction.kan_extension_on_facePoset line 845

    Source documentation

    A continuous extension across a finite nonsingular inclusion gives an exact simplicial extension on its face-poset nerve. The boundary is the specified last-vertex comparison followed by the original map.

    theorem kan_extension_on_facePoset {A B X : SSet.{0}}
    [A.Nonsingular] [B.Nonsingular] [B.Finite] [SSet.KanComplex X]
    (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 : nerve B.N ⟶ X,
      nerveMap (faceMap i (preservesNondegenerate_of_mono i)).monotone.functor ≫ d =
        map A ≫ a := by
…