OAI/CategoryTheory/Thomason/Simplicial/InfiniteExtensionKan.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

A common flag for points with sorted barycentric coordinates

The positive faces of a point are prefixes of any ordering which sorts its affine coordinates. Grouping their masses gives an exact flag representative in the actual geometric realization.

  1. theorem OAI.Thomason.Construction.SubdivisionBarycentric.mem_permuted_prefix line 32
  2. theorem OAI.Thomason.Construction.SubdivisionBarycentric.positive_face_mem_permuted_prefix line 50
  3. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_permuted_prefix_representation line 65

    Source documentation

    Sorting the affine image determines one common flag which contains the original realization point, even on all intersections of chambers.

    theorem exists_permuted_prefix_representation (n : ℕ)
    (z : SSet.toTop.obj (nerve (Faces n)))
    (σ : Equiv.Perm (Fin (n+1)))
    (hσ : Antitone (fun i => (point n z).weights (σ i))) :
    ∃ p : StdSimplex ℝ (Fin (n+1)), z =
      simplexPoint (nerve (Faces n))
        (prefixSimplex n ⋙ (permutationFaceMap n σ).monotone.functor) p := by
…

    Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.SubdivisionBarycentric.prefixSimplex, OAI.Thomason.Construction.SubdivisionBarycentric.permutationFaceMap

  4. theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_injective line 99

    Source documentation

    The barycentric affine map distinguishes points of the actual face-nerve realization.

    theorem point_injective (n : ℕ) : Function.Injective (point n) := by
…

    Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.point

  5. def OAI.Thomason.Construction.SubdivisionBarycentric.homeomorph line 130

    Source documentation

    The affine barycentric map, as a homeomorphism of actual spaces.

    def homeomorph (n : ℕ) :
    SSet.toTop.obj (nerve (Faces n)) ≃ₜ StdSimplex ℝ (Fin (n+1)) := by
…

    Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces

  6. theorem OAI.Thomason.Construction.SubdivisionBarycentric.homeomorph_apply line 140
  7. theorem OAI.Thomason.Construction.SubdivisionBarycentric.homeomorph_face_naturality line 143
  8. theorem OAI.Thomason.Construction.SubdivisionBarycentric.homeomorph_symm_face_naturality line 149

    Source documentation

    The inverse also commutes with every injective ordinal face map.

    theorem homeomorph_symm_face_naturality {m n : ℕ} (f : Fin (m+1) ↪o Fin (n+1))
    (p : StdSimplex ℝ (Fin (m+1))) :
    (homeomorph n).symm (StdSimplex.map f p) =
      (SSet.toTop.map (nerveMap (faceMap f).monotone.functor)).hom
        ((homeomorph m).symm p) := by
…

    Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.homeomorph, OAI.Thomason.Construction.SubdivisionBarycentric.faceMap

  9. theorem OAI.Thomason.Construction.SubdivisionBarycentric.homeomorph_symm_face_carrier line 160

    Source documentation

    A complete coordinate face has precisely its expected subdivided face as inverse image, including every intersection of faces.

    theorem homeomorph_symm_face_carrier (n : ℕ) (V : Set (Fin (n+1)))
    (p : StdSimplex ℝ (Fin (n+1))) :
    carrier (nerve (Faces n)) ((homeomorph n).symm p) ≤
      fullSubposetComplex (permittedFaces n V) ↔ ∀ i ∉ V, p.weights i = 0 := by
…

    Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.homeomorph, OAI.Thomason.Construction.fullSubposetComplex, OAI.Thomason.Construction.SubdivisionBarycentric.permittedFaces

  10. def OAI.Thomason.Construction.SubdivisionBarycentric.faceHomeomorph line 170

    Source documentation

    The restriction identifies the actual subdivided face realization with its full coordinate face, not merely their interiors.

    def faceHomeomorph (n : ℕ) (V : Set (Fin (n+1))) :
    SSet.toTop.obj (fullSubposetComplex (permittedFaces n V)).toSSet ≃ₜ
      {p : StdSimplex ℝ (Fin (n+1)) // ∀ i ∉ V, p.weights i = 0} :=
…

    Mentions: OAI.Thomason.Construction.fullSubposetComplex, OAI.Thomason.Construction.SubdivisionBarycentric.permittedFaces

  11. theorem OAI.Thomason.Construction.SubdivisionBarycentric.faceHomeomorph_inclusion line 176
  12. theorem OAI.Thomason.Construction.SubdivisionBarycentric.subdividedFace_eq_permitted line 202
  13. theorem OAI.Thomason.Construction.SubdivisionBarycentric.carrier_subdividedFaceUnion_iff line 211
  14. theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_faceUnion_preimage line 244
  15. def OAI.Thomason.Construction.SubdivisionBarycentric.faceUnionHomeomorph line 257

    Source documentation

    Restriction to an arbitrary finite union of coordinate faces.

    def faceUnionHomeomorph {n : ℕ} (F : Finset (Finset (Fin (n+1)))) :
    SSet.toTop.obj (subdividedFaceUnion F).toSSet ≃ₜ
      {p : StdSimplex ℝ (Fin (n+1)) // ∃ S ∈ F, ∀ i ∉ S, p.weights i = 0} :=
…

    Mentions: OAI.Thomason.Construction.subdividedFaceUnion

  16. theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_boundary_preimage line 263
  17. def OAI.Thomason.Construction.SubdivisionBarycentric.boundaryHomeomorph line 279

    Source documentation

    The full subdivided boundary realizes to the entire geometric boundary.

    def boundaryHomeomorph (n : ℕ) :
    SSet.toTop.obj (subdividedFaceUnion (boundaryFaces n)).toSSet ≃ₜ
      {p : StdSimplex ℝ (Fin (n+1)) // ∃ i, p.weights i = 0} :=
…

    Mentions: OAI.Thomason.Construction.subdividedFaceUnion, OAI.Thomason.Construction.boundaryFaces

  18. def OAI.Thomason.Construction.SubdivisionBarycentric.standardSubdivisionHomeomorph line 306
  19. def OAI.Thomason.Construction.SubdivisionBarycentric.boundarySubdivisionIso line 312
  20. def OAI.Thomason.Construction.SubdivisionBarycentric.boundarySubdivisionHomeomorph line 322
  21. theorem OAI.Thomason.Construction.SubdivisionBarycentric.boundarySubdivisionIso_inclusion line 328
  22. theorem OAI.Thomason.Construction.SubdivisionBarycentric.standardSubdivisionHomeomorph_boundary line 334

    Source documentation

    Both homeomorphisms are compatible with the actual boundary arrow.

    theorem standardSubdivisionHomeomorph_boundary (n : ℕ)
    (z : SSet.toTop.obj (SSet.sd.obj (SSet.boundary.{0} n).toSSet)) :
    standardSubdivisionHomeomorph n
      ((SSet.toTop.map (SSet.sd.map (SSet.boundary.{0} n).ι)).hom z) =
      (SSet.toTop.map (SSet.boundary.{0} n).ι).hom
        (boundarySubdivisionHomeomorph n z) := by
…

    Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.standardSubdivisionHomeomorph, OAI.Thomason.Construction.SubdivisionBarycentric.boundarySubdivisionHomeomorph

  23. abbrev OAI.Thomason.Construction.InfiniteExtension.stage line 387

    Source documentation

    The actual n-fold extension of the original simplicial set.

    abbrev stage (X : SSet.{0}) (n : ℕ) : SSet.{0} :=
…
  24. abbrev OAI.Thomason.Construction.InfiniteExtension.step line 390
  25. abbrev OAI.Thomason.Construction.InfiniteExtension.diagram line 393
  26. theorem OAI.Thomason.Construction.InfiniteExtension.diagram_map_succ line 399
  27. abbrev OAI.Thomason.Construction.InfiniteExtension.obj line 404

    Source documentation

    The chosen colimit of the canonical-extension tower.

    abbrev obj (X : SSet.{0}) : SSet.{0} := colimit (diagram X)

    Mentions: OAI.Thomason.Construction.InfiniteExtension.diagram

  28. abbrev OAI.Thomason.Construction.InfiniteExtension.inclusion line 406
  29. abbrev OAI.Thomason.Construction.InfiniteExtension.unit line 409
  30. theorem OAI.Thomason.Construction.InfiniteExtension.step_inclusion line 412
  31. theorem OAI.Thomason.Construction.InfiniteExtension.map_mono_weak line 417
  32. instance OAI.Thomason.Construction.InfiniteExtension.inclusion_mono line 439
  33. abbrev OAI.Thomason.Construction.InfiniteExtension.range line 445

    Source documentation

    Stage images in the actual colimit, used only to control finite families and to apply the proved realization exhaustion theorem.

    abbrev range (X : SSet.{0}) (n : ℕ) : (obj X).Subcomplex :=
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.obj

  34. theorem OAI.Thomason.Construction.InfiniteExtension.range_monotone line 448
  35. theorem OAI.Thomason.Construction.InfiniteExtension.range_iSup line 457
  36. def OAI.Thomason.Construction.InfiniteExtension.rangeIso line 465
  37. theorem OAI.Thomason.Construction.InfiniteExtension.rangeIso_hom_inclusion line 472
  38. theorem OAI.Thomason.Construction.InfiniteExtension.range_initial_map_weak line 475
  39. theorem OAI.Thomason.Construction.InfiniteExtension.unit_weak line 495

    Source documentation

    The original simplicial set maps weakly into the actual sequential colimit. Compact cubes and based homotopies give the finite-stage witnesses.

    theorem unit_weak (X : SSet.{0}) : realizationWeakEquivalences (unit X) := by
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.InfiniteExtension.unit

  40. theorem OAI.Thomason.Construction.InfiniteExtension.finite_map_factors line 505

    Source documentation

    Every finite simplicial family in the infinite extension is already an exact family in a single finite iterate.

    theorem finite_map_factors {A : SSet.{0}} [A.Finite] (X : SSet.{0})
    (f : A ⟶ obj X) :
    ∃ (n : ℕ) (g : A ⟶ stage X n), g ≫ inclusion X n = f := by
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.obj, OAI.Thomason.Construction.InfiniteExtension.stage, OAI.Thomason.Construction.InfiniteExtension.inclusion

  41. theorem OAI.Thomason.Construction.InfiniteExtension.finite_relative_map_factors line 524

    Source documentation

    Factoring a finite family through a stage preserves its complete prescribed boundary from the original simplicial set.

    theorem finite_relative_map_factors {A K : SSet.{0}} [K.Finite]
    (X : SSet.{0}) (i : A ⟶ K) (a : A ⟶ X) (f : K ⟶ obj X)
    (hf : i ≫ f = a ≫ unit X) :
    ∃ (n : ℕ) (g : K ⟶ stage X n),
      g ≫ inclusion X n = f ∧
      i ≫ g = a ≫ (diagram X).map (homOfLE (Nat.zero_le n)) := by
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.obj, OAI.Thomason.Construction.InfiniteExtension.unit, OAI.Thomason.Construction.InfiniteExtension.stage, OAI.Thomason.Construction.InfiniteExtension.inclusion, OAI.Thomason.Construction.InfiniteExtension.diagram, OAI.Thomason.Construction.InfiniteExtension.map

  42. theorem OAI.Thomason.Construction.InfiniteExtension.compact_map_factors line 538

    Source documentation

    Compact continuous families also occur at one finite extension stage. The factorization is exact on every point of the parameter space.

    theorem compact_map_factors {Z : Type} [TopologicalSpace Z] [CompactSpace Z]
    (X : SSet.{0}) (f : C(Z, SSet.toTop.obj (obj X))) :
    ∃ (n : ℕ) (g : C(Z, SSet.toTop.obj (stage X n))),
      (SSet.toTop.map (inclusion X n)).hom.comp g = f := by
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.obj, OAI.Thomason.Construction.InfiniteExtension.stage, OAI.Thomason.Construction.InfiniteExtension.inclusion

  43. def OAI.Thomason.Construction.InfiniteExtension.stageMap line 568
  44. theorem OAI.Thomason.Construction.InfiniteExtension.stageMap_id line 572
  45. theorem OAI.Thomason.Construction.InfiniteExtension.stageMap_comp line 581
  46. def OAI.Thomason.Construction.InfiniteExtension.diagramMap line 590
  47. def OAI.Thomason.Construction.InfiniteExtension.map line 596
  48. theorem OAI.Thomason.Construction.InfiniteExtension.inclusion_map line 598
  49. theorem OAI.Thomason.Construction.InfiniteExtension.map_id line 602
  50. theorem OAI.Thomason.Construction.InfiniteExtension.map_comp line 608
  51. def OAI.Thomason.Construction.InfiniteExtension.functor line 618

    Source documentation

    The actual colimit construction, as an endofunctor on simplicial sets.

    def functor : SSet.{0} ⥤ SSet.{0} where
…
  52. def OAI.Thomason.Construction.InfiniteExtension.coaugmentation line 625

    Source documentation

    Its canonical coaugmentation is the inclusion of the original stage.

    def coaugmentation : 𝟭 SSet.{0} ⟶ functor where
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.functor

  53. theorem OAI.Thomason.Construction.InfiniteExtension.map_weak_iff line 631

    Source documentation

    The sequential extension construction preserves and reflects actual realization weak equivalences, without any fibrancy assertion.

    theorem map_weak_iff {X Y : SSet.{0}} (f : X ⟶ Y) :
    realizationWeakEquivalences (map f) ↔ realizationWeakEquivalences f :=
…

    Mentions: OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.InfiniteExtension.map

  54. abbrev OAI.Thomason.Construction.InfiniteExtension.stageUnit line 651
  55. theorem OAI.Thomason.Construction.InfiniteExtension.stageUnit_zero line 654
  56. theorem OAI.Thomason.Construction.InfiniteExtension.stageUnit_succ line 657
  57. theorem OAI.Thomason.Construction.InfiniteExtension.stageMap_isMono line 664
  58. theorem OAI.Thomason.Construction.InfiniteExtension.stageUnit_simplex_lift line 674

    Source documentation

    The cartesian property persists through every finite extension stage.

    theorem stageUnit_simplex_lift {A B : SSet.{0}} (i : A ⟶ B) [Mono i]
    (n : ℕ) (d : SimplexCategory) (x : SSet.stdSimplex.obj d ⟶ B)
    (a : SSet.stdSimplex.obj d ⟶ stage A n)
    (h : x ≫ stageUnit B n = a ≫ stageMap i n) :
    ∃ b : SSet.stdSimplex.obj d ⟶ A, b ≫ i = x ∧ b ≫ stageUnit A n = a := by
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.stage, OAI.Thomason.Construction.InfiniteExtension.stageUnit, OAI.Thomason.Construction.InfiniteExtension.stageMap

  59. theorem OAI.Thomason.Construction.InfiniteExtension.unit_simplex_lift line 699

    Source documentation

    Every simplex in the infinite extension over an original simplex of B already comes from the corresponding original subobject.

    theorem unit_simplex_lift {A B : SSet.{0}} (i : A ⟶ B) [Mono i]
    (d : SimplexCategory) (x : SSet.stdSimplex.obj d ⟶ B)
    (a : SSet.stdSimplex.obj d ⟶ obj A)
    (h : x ≫ unit B = a ≫ map i) :
    ∃ b : SSet.stdSimplex.obj d ⟶ A, b ≫ i = x ∧ b ≫ unit A = a := by
…

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

  60. theorem OAI.Thomason.Construction.InfiniteExtension.unit_isPullback line 722

    Source documentation

    The coaugmentation into the constructed Kan replacement is cartesian along every monomorphism.

    theorem unit_isPullback {A B : SSet.{0}} (i : A ⟶ B) [Mono i] :
    IsPullback i (unit A) (unit B) (map i) := by
…

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

  61. theorem OAI.Thomason.Construction.InfiniteExtension.unit_preimage_range line 743

    Source documentation

    No new preimages of an original subobject appear in the Kan replacement, even at the sequential colimit.

    theorem unit_preimage_range {A B : SSet.{0}} (i : A ⟶ B) [Mono i] :
    (SSet.Subcomplex.range (map i)).preimage (unit B) = SSet.Subcomplex.range i :=
…

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

  62. def OAI.Thomason.Construction.InfiniteExtension.stageFunctor line 769

    Source documentation

    Iterated extension, with precisely the maps used in the colimit tower.

    def stageFunctor (n : ℕ) : SSet.{0} ⥤ SSet.{0} where
…
  63. instance OAI.Thomason.Construction.InfiniteExtension.stageFunctor_preservesLimits line 775
  64. def OAI.Thomason.Construction.InfiniteExtension.towerFunctor line 784

    Source documentation

    The whole sequence, before taking its colimit.

    def towerFunctor : SSet.{0} ⥤ ℕ ⥤ SSet.{0} where
…
  65. def OAI.Thomason.Construction.InfiniteExtension.towerEvaluationIso line 796
  66. instance OAI.Thomason.Construction.InfiniteExtension.towerFunctor_preservesLimits line 800
  67. instance OAI.Thomason.Construction.InfiniteExtension.simplicialSequenceColimit_preservesFiniteLimits line 805
  68. def OAI.Thomason.Construction.InfiniteExtension.colimitFunctorIso line 812
  69. instance OAI.Thomason.Construction.InfiniteExtension.functor_preservesFiniteLimits line 817

    Source documentation

    Extension to infinity commutes with finite limits, including the pullbacks used for Kan fibres and base change.

    instance functor_preservesFiniteLimits : PreservesFiniteLimits functor :=
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.functor

  70. instance OAI.Thomason.Construction.InfiniteExtension.stageFunctor_preservesFilteredColimitsOfShape line 841
  71. instance OAI.Thomason.Construction.InfiniteExtension.towerFunctor_preservesFilteredColimitsOfShape line 850
  72. instance OAI.Thomason.Construction.InfiniteExtension.functor_preservesFilteredColimitsOfShape line 856
  73. instance OAI.Thomason.Construction.InfiniteExtension.functor_preservesFilteredColimits line 860
  74. theorem OAI.Thomason.Construction.InfiniteExtension.stageMap_fibration line 880
  75. theorem OAI.Thomason.Construction.InfiniteExtension.map_horn_lifting line 892

    Source documentation

    A Kan lifting square in the colimit lies in a common finite stage. Its exact commutativity there follows from the monic stage inclusion.

    theorem map_horn_lifting {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] (n : ℕ) (k : Fin (n+2)) :
    HasLiftingProperty (SSet.horn (n+1) k).ι (map p) := by
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.map

  76. theorem OAI.Thomason.Construction.InfiniteExtension.map_fibration line 930

    Source documentation

    The extension colimit preserves Kan fibrations.

    theorem map_fibration {X Y : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] : HomotopicalAlgebra.Fibration (map p) := by
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.map

  77. theorem OAI.Thomason.Construction.InfiniteExtension.stage_kan line 938
  78. theorem OAI.Thomason.Construction.InfiniteExtension.horn_filling_of_kan line 949

    Source documentation

    For an already Kan complex, the extension colimit remains Kan. The arbitrary-source fibrancy theorem requires a further explicit horn filler.

    theorem horn_filling_of_kan (X : SSet.{0}) [SSet.KanComplex X]
    (n : ℕ) (k : Fin (n+2)) :
    HasLiftingProperty (SSet.horn (n+1) k).ι (terminal.from (obj X)) := by
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.obj

  79. theorem OAI.Thomason.Construction.InfiniteExtension.kan_of_kan line 961

    Source documentation

    A Kan source remains Kan after the sequential extension construction.

    theorem kan_of_kan (X : SSet.{0}) [SSet.KanComplex X] : SSet.KanComplex (obj X) := by
…

    Mentions: OAI.Thomason.Construction.InfiniteExtension.obj