OAI/CategoryTheory/Thomason/Simplicial/FixedInternalPathMaps.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

The barycentric image of a poset realization

The image consists exactly of finite probability distributions whose support is a chain. The converse constructs an actual nerve simplex and its coordinates rather than assuming an abstract triangulation theorem.

  1. def OAI.Thomason.Construction.PosetGeometry.ChainSupported line 30
  2. theorem OAI.Thomason.Construction.PosetGeometry.probability_support_nonempty line 34
  3. def OAI.Thomason.Construction.PosetGeometry.chainDimension line 41
  4. theorem OAI.Thomason.Construction.PosetGeometry.chain_card line 44
  5. def OAI.Thomason.Construction.PosetGeometry.chainEnumerationData line 49
  6. def OAI.Thomason.Construction.PosetGeometry.chainEnumeration line 67

    Source documentation

    Increasing enumeration of the support, with the original partial order.

    def chainEnumeration (p : StdSimplex ℝ P) (hp : ChainSupported p) :
    Fin (chainDimension p + 1) ↪o P := (chainEnumerationData p hp).val

    Mentions: OAI.Thomason.Construction.PosetGeometry.ChainSupported, OAI.Thomason.Construction.PosetGeometry.chainDimension, OAI.Thomason.Construction.PosetGeometry.chainEnumerationData

  7. theorem OAI.Thomason.Construction.PosetGeometry.chainEnumeration_range line 70
  8. def OAI.Thomason.Construction.PosetGeometry.chainCoordinates line 74
  9. theorem OAI.Thomason.Construction.PosetGeometry.chainCoordinates_recover line 79

    Source documentation

    Reinserting the enumerated support recovers the original distribution.

    theorem chainCoordinates_recover (p : StdSimplex ℝ P) (hp : ChainSupported p) :
    StdSimplex.map (chainEnumeration p hp) (chainCoordinates p hp) = p := by
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.ChainSupported, OAI.Thomason.Construction.PosetGeometry.chainEnumeration, OAI.Thomason.Construction.PosetGeometry.chainCoordinates

  10. theorem OAI.Thomason.Construction.PosetGeometry.coordinates_chainSupported line 98
  11. theorem OAI.Thomason.Construction.PosetGeometry.mem_range_coordinates_iff line 113

    Source documentation

    Exact image theorem for the actual geometric realization coordinates.

    theorem mem_range_coordinates_iff (p : StdSimplex ℝ P) :
    p ∈ Set.range (coordinates P) ↔ ChainSupported p := by
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates, OAI.Thomason.Construction.PosetGeometry.ChainSupported

  12. def OAI.Thomason.Construction.PosetGeometry.CompatibleSupport line 145

    Source documentation

    The union of two positive supports is a chain.

    def CompatibleSupport (p q : StdSimplex ℝ P) : Prop :=
…
  13. def OAI.Thomason.Construction.PosetGeometry.blend line 149
  14. theorem OAI.Thomason.Construction.PosetGeometry.blend_zero line 154
  15. theorem OAI.Thomason.Construction.PosetGeometry.blend_one line 159
  16. theorem OAI.Thomason.Construction.PosetGeometry.blend_self line 164
  17. theorem OAI.Thomason.Construction.PosetGeometry.blend_chainSupported line 172

    Source documentation

    The whole interpolation stays in the geometric image when the two supports lie in a common chain.

    theorem blend_chainSupported (p q : StdSimplex ℝ P) (h : CompatibleSupport p q)
    (t : unitInterval) : ChainSupported (blend p q t) := by
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.CompatibleSupport, OAI.Thomason.Construction.PosetGeometry.ChainSupported, OAI.Thomason.Construction.PosetGeometry.blend

  18. theorem OAI.Thomason.Construction.PosetGeometry.compatibleSupport_of_subset line 183
  19. def OAI.Thomason.Construction.PosetGeometry.interpolate line 194

    Source documentation

    Continuous interpolation in the barycentric image, with its actual finite-poset realization topology.

    def interpolate (x y : SSet.toTop.obj (nerve P))
    (h : CompatibleSupport (coordinates P x) (coordinates P y)) (t : unitInterval) :
    SSet.toTop.obj (nerve P) :=
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.CompatibleSupport, OAI.Thomason.Construction.PosetGeometry.coordinates

  20. theorem OAI.Thomason.Construction.PosetGeometry.coordinates_interpolate line 201
  21. theorem OAI.Thomason.Construction.PosetGeometry.interpolate_zero line 206
  22. theorem OAI.Thomason.Construction.PosetGeometry.interpolate_one line 211
  23. theorem OAI.Thomason.Construction.PosetGeometry.interpolate_self line 216
  24. def OAI.Thomason.Construction.PosetGeometry.blendMap line 242
  25. def OAI.Thomason.Construction.PosetGeometry.commonChainHomotopy line 263

    Source documentation

    Two maps with pointwise compatible positive supports are homotopic by straight-line interpolation in the proved barycentric image.

    def commonChainHomotopy (f g : C(X, SSet.toTop.obj (nerve P)))
    (h : ∀ x, CompatibleSupport (coordinates P (f x)) (coordinates P (g x))) :
    f.Homotopy g where
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.CompatibleSupport, OAI.Thomason.Construction.PosetGeometry.coordinates

  26. def OAI.Thomason.Construction.PosetGeometry.commonChainHomotopyRel line 274

    Source documentation

    The interpolation fixes the full set where the endpoint maps agree.

    def commonChainHomotopyRel (f g : C(X, SSet.toTop.obj (nerve P)))
    (h : ∀ x, CompatibleSupport (coordinates P (f x)) (coordinates P (g x)))
    (A : Set X) (hA : ∀ x ∈ A, f x = g x) : f.HomotopyRel g A where
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.CompatibleSupport, OAI.Thomason.Construction.PosetGeometry.coordinates

  27. theorem OAI.Thomason.Construction.PosetGeometry.compatible_support_weak_iff line 285

    Source documentation

    In particular compatible-support changes preserve the actual weak homotopy-equivalence test; no model-category input occurs.

    theorem compatible_support_weak_iff (f g : C(X, SSet.toTop.obj (nerve P)))
    (h : ∀ x, CompatibleSupport (coordinates P (f x)) (coordinates P (g x))) :
    IsWeakHomotopyEquivalence f ↔ IsWeakHomotopyEquivalence g :=
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.CompatibleSupport, OAI.Thomason.Construction.PosetGeometry.coordinates, OAI.Thomason.Construction.IsWeakHomotopyEquivalence

  28. theorem OAI.Thomason.Construction.PosetGeometry.blend_support_subset_union line 311
  29. theorem OAI.Thomason.Construction.PosetGeometry.compatibleSupport_of_subsets line 325
  30. theorem OAI.Thomason.Construction.PosetGeometry.commonChainHomotopy_support line 341
  31. theorem OAI.Thomason.Construction.PosetGeometry.homotopy_trans_support line 356
  32. def OAI.Thomason.Construction.PosetGeometry.commonCarrierHomotopyRel line 369

    Source documentation

    A homotopy of paths with exactly fixed ends and stationary side. All interpolation occurs in the given common carrier.

    def commonCarrierHomotopyRel {f g : C(X, SSet.toTop.obj (nerve P))}
    (H G : f.Homotopy g) (A : Set X)
    (hA : ∀ t x, x ∈ A → H (t, x) = G (t, x))
    (c : C(unitInterval × X, SSet.toTop.obj (nerve P)))
    (hH : ∀ z, (coordinates P (H z)).weights.support ⊆ (coordinates P (c z)).weights.support)
    (hG : ∀ z, (coordinates P (G z)).weights.support ⊆ (coordinates P (c z)).weights.support) :
    H.toContinuousMap.HomotopyRel G.toContinuousMap
      {z | z.1 = 0 ∨ z.1 = 1 ∨ z.2 ∈ A} :=
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates

  33. theorem OAI.Thomason.Construction.PosetGeometry.coordinates_nerveMap line 408
  34. def OAI.Thomason.Construction.PosetGeometry.openFace line 443
  35. theorem OAI.Thomason.Construction.PosetGeometry.openFace_isOpen line 446
  36. theorem OAI.Thomason.Construction.PosetGeometry.chain_of_openFace_nonempty line 459

    Source documentation

    A nonempty intersection forces its vertex labels to form a chain.

    theorem chain_of_openFace_nonempty (S : Finset P) (hS : (openFace S).Nonempty) :
    ∀ v ∈ S, ∀ w ∈ S, v ≤ w ∨ w ≤ v := by
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.openFace

  37. theorem OAI.Thomason.Construction.PosetGeometry.subBarycenter_weights line 467
  38. theorem OAI.Thomason.Construction.PosetGeometry.subBarycenter_support line 474
  39. theorem OAI.Thomason.Construction.PosetGeometry.subBarycenter_chainSupported line 486
  40. def OAI.Thomason.Construction.PosetGeometry.openFaceCenter line 495
  41. theorem OAI.Thomason.Construction.PosetGeometry.coordinates_openFaceCenter line 501
  42. theorem OAI.Thomason.Construction.PosetGeometry.openFaceCenter_mem line 506
  43. theorem OAI.Thomason.Construction.PosetGeometry.openFace_nonempty_iff line 514

    Source documentation

    The open-cover nerve has exactly the nonempty chains as simplices.

    theorem openFace_nonempty_iff (S : Finset P) (hS : S.Nonempty) :
    (openFace S).Nonempty ↔ ∀ v ∈ S, ∀ w ∈ S, v ≤ w ∨ w ≤ v :=
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.openFace

  44. theorem OAI.Thomason.Construction.PosetGeometry.blend_positive line 538
  45. theorem OAI.Thomason.Construction.PosetGeometry.compatible_openFace_center line 550
  46. def OAI.Thomason.Construction.PosetGeometry.openFaceContraction line 561

    Source documentation

    The explicit contraction to the barycenter keeps every prescribed star coordinate strictly positive at every time, including endpoints.

    def openFaceContraction (S : Finset P) (hS : S.Nonempty)
    (hchain : ∀ v ∈ S, ∀ w ∈ S, v ≤ w ∨ w ≤ v) :
    (ContinuousMap.id (openFace S)).Homotopy
      (ContinuousMap.const _ ⟨openFaceCenter S hS hchain, openFaceCenter_mem S hS hchain⟩) := by
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.openFace, OAI.Thomason.Construction.PosetGeometry.openFaceCenter, OAI.Thomason.Construction.PosetGeometry.openFaceCenter_mem

  47. theorem OAI.Thomason.Construction.PosetGeometry.openFace_contractible line 581
  48. theorem OAI.Thomason.Construction.PosetGeometry.openFace_singular_counit_weak line 589

    Source documentation

    Every nonempty finite intersection in this open cover has a proved actual singular-counit weak equivalence.

    theorem openFace_singular_counit_weak (S : Finset P) (hS : S.Nonempty)
    (hx : (openFace S).Nonempty) :
    topologicalWeakEquivalences (sSetTopAdj.counit.app (TopCat.of (openFace S))) := by
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.openFace, OAI.Thomason.Construction.topologicalWeakEquivalences

  49. theorem OAI.Thomason.Construction.PosetGeometry.eq_vertex_iff line 614
  50. def OAI.Thomason.Construction.PosetGeometry.comparableVertex line 626
  51. theorem OAI.Thomason.Construction.PosetGeometry.comparable_inclusion_vertex line 628
  52. theorem OAI.Thomason.Construction.PosetGeometry.comparable_preimage_vertexStar line 634
  53. theorem OAI.Thomason.Construction.PosetGeometry.comparable_range_contains_vertexStar line 651

    Source documentation

    The ambient star lies in the actual realization of the comparable subposet.

    theorem comparable_range_contains_vertexStar (v : P) :
    vertexStar (nerve P) (vertex v) ⊆
      Set.range (SSet.toTop.map (nerveMap (fullSubposetInclusion (comparable v)))).hom := by
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.vertex, OAI.Thomason.Construction.fullSubposetInclusion, OAI.Thomason.Construction.PosetGeometry.comparable

  54. def OAI.Thomason.Construction.PosetGeometry.comparableStarHomeomorph line 664

    Source documentation

    Removing vertices incomparable with v does not alter its open star, including the topology inherited from the actual realization.

    def comparableStarHomeomorph (v : P) :
    vertexStar (nerve (comparable v)) (vertex (comparableVertex v)) ≃ₜ
      vertexStar (nerve P) (vertex v) :=
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.comparable, OAI.Thomason.Construction.PosetGeometry.vertex, OAI.Thomason.Construction.PosetGeometry.comparableVertex

  55. def OAI.Thomason.Construction.PosetGeometry.upperClamp line 688

    Source documentation

    On the comparable subposet, raise vertices below v to v.

    def upperClamp (v : P) : comparable v →o comparable v := by
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.comparable

  56. theorem OAI.Thomason.Construction.PosetGeometry.le_upperClamp line 701
  57. theorem OAI.Thomason.Construction.PosetGeometry.comparableVertex_le_upperClamp line 708
  58. theorem OAI.Thomason.Construction.PosetGeometry.upperClamp_vertex line 716
  59. def OAI.Thomason.Construction.RealizationPrism.vertexPoint line 738
  60. theorem OAI.Thomason.Construction.RealizationPrism.vertexPoint_mem_vertexStar line 741
  61. theorem OAI.Thomason.Construction.RealizationPrism.map_vertexPoint line 754
  62. theorem OAI.Thomason.Construction.RealizationPrism.realization_const line 761

    Source documentation

    A constant simplicial map realizes to the constant continuous map at the same actual vertex, even on simplices of arbitrary dimension.

    theorem realization_const {K L : SSet.{0}} (v : L.obj (.op (.mk 0)))
    (x : SSet.toTop.obj K) :
    (SSet.toTop.map (SSet.const (X := K) v)).hom x = vertexPoint L v := by
…

    Mentions: OAI.Thomason.Construction.RealizationPrism.vertexPoint

  63. def OAI.Thomason.Construction.fixedInternalPathSubcomplex line 791

    Source documentation

    The subcomplex of internal paths having the two specified constant endpoint simplices.

    def fixedInternalPathSubcomplex (X : SSet.{0}) (x y : X _⦋0⦌) :
    (internalPathObject X).Subcomplex :=
…

    Mentions: OAI.Thomason.Construction.internalPathObject

  64. abbrev OAI.Thomason.Construction.fixedInternalPaths line 796
  65. theorem OAI.Thomason.Construction.fixedInternalPaths_start line 799
  66. theorem OAI.Thomason.Construction.fixedInternalPaths_end line 808
  67. def OAI.Thomason.Construction.fixedInternalPathsLift line 819

    Source documentation

    A map of internal paths with constant endpoints lands in the actual fixed-endpoint subcomplex.

    def fixedInternalPathsLift {K X : SSet.{0}} (x y : X _⦋0⦌)
    (a : K ⟶ internalPathObject X)
    (h₀ : a ≫ internalPathStart X = SSet.const x)
    (h₁ : a ≫ internalPathEnd X = SSet.const y) : K ⟶ fixedInternalPaths X x y :=
…

    Mentions: OAI.Thomason.Construction.internalPathObject, OAI.Thomason.Construction.internalPathStart, OAI.Thomason.Construction.internalPathEnd, OAI.Thomason.Construction.fixedInternalPaths

  68. theorem OAI.Thomason.Construction.fixedInternalPathsLift_ι line 834
  69. theorem OAI.Thomason.Construction.fixedInternalPaths_kan line 842

    Source documentation

    Fixed-endpoint internal path complexes of Kan complexes are Kan. The proof fixes both ends throughout the actual horn lift.

    theorem fixedInternalPaths_kan (X : SSet.{0}) [SSet.KanComplex X] (x y : X _⦋0⦌) :
    SSet.KanComplex (fixedInternalPaths X x y) := by
…

    Mentions: OAI.Thomason.Construction.fixedInternalPaths

  70. def OAI.Thomason.Construction.fixedInternalPathMap line 893
  71. theorem OAI.Thomason.Construction.fixedInternalPathMap_ι line 903
  72. theorem OAI.Thomason.Construction.fixedInternalPathMap_lifting line 909

    Source documentation

    A fibration gives exact relative lifts in its fixed-endpoint path map. Only the anodyne pushout-product theorem is used.

    theorem fixedInternalPathMap_lifting {X Y A B : SSet.{0}} (p : X ⟶ Y)
    [HomotopicalAlgebra.Fibration p] (x y : X _⦋0⦌)
    (i : A ⟶ B) (hi : SSet.anodyneExtensions i) :
    HasLiftingProperty i (fixedInternalPathMap p x y) := by
…

    Mentions: OAI.Thomason.Construction.fixedInternalPathMap

  73. theorem OAI.Thomason.Construction.fixedInternalPathMap_fibration line 947