OAI/CategoryTheory/Thomason/Simplicial/SimplicialApproximation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Support control for the barycentric comparison homotopy

Order maps preserve inclusions of positive supports. In particular the comparison from a barycentric parameter to its exact last vertex stays in the original carrier even after the prescribed boundary order map.

  1. theorem OAI.Thomason.Construction.coordinates_map_support_mono line 24
  2. theorem OAI.Thomason.Construction.SubdivisionBarycentric.iteratedCarrierHomotopy_support line 40
  3. theorem OAI.Thomason.Construction.SubdivisionBarycentric.iteratedCarrierHomotopy_map_support line 48
  4. def OAI.Thomason.Construction.PosetGeometry.carrierTriangle line 65

    Source documentation

    Three paths in one carrier satisfy the endpoint-fixed triangle coherence needed by a relative simplicial approximation.

    def carrierTriangle {P : Type} [PartialOrder P] [Finite P]
    {X : Type} [TopologicalSpace X]
    {f g h : C(X, SSet.toTop.obj (nerve P))}
    (H : f.Homotopy g) (G : g.Homotopy h) (D : f.Homotopy h)
    (c : C(X, SSet.toTop.obj (nerve P)))
    (hH : ∀ t x, (coordinates P (H (t, x))).weights.support ⊆ (coordinates P (c x)).weights.support)
    (hG : ∀ t x, (coordinates P (G (t, x))).weights.support ⊆ (coordinates P (c x)).weights.support)
    (hD : ∀ t x, (coordinates P (D (t, x))).weights.support ⊆ (coordinates P (c x)).weights.support) :
    (H.trans G).toContinuousMap.HomotopyRel D.toContinuousMap
      {z | z.1 = 0 ∨ z.1 = 1 ∨ z.2 ∈ (∅ : Set X)} :=
…

    Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates

  5. theorem OAI.Thomason.Construction.RelativeLabelCarrier.chainDistribution_map line 104
  6. theorem OAI.Thomason.Construction.RelativeLabelCarrier.chainMap_injective line 116
  7. theorem OAI.Thomason.Construction.RelativeLabelCarrier.chainRealizationMap_naturality line 124
  8. def OAI.Thomason.Construction.RelativeLabelCarrier.iteratedMap line 142

    Source documentation

    The induced order map on every iterated chain stage.

    def iteratedMap {P Q : PartOrd.{0}} (f : P →o Q) (r : ℕ) :
    iteratedChainPoset P r →o iteratedChainPoset Q r :=
…

    Mentions: OAI.Thomason.Construction.iteratedChainPoset

  9. theorem OAI.Thomason.Construction.RelativeLabelCarrier.iteratedMap_injective line 148
  10. theorem OAI.Thomason.Construction.RelativeLabelCarrier.iteratedSubdivisionNerveIso_naturality line 156

    Source documentation

    The chain-nerve identification is natural for arbitrary monotone maps. No injectivity is needed for this simplicial identity.

    theorem iteratedSubdivisionNerveIso_naturality {P Q : PartOrd.{0}} [Finite P] [Finite Q]
    (f : P →o Q) (r : ℕ) :
    (iteratedSubdivision r).map (nerveMap f.monotone.functor) ≫
        (iteratedSubdivisionNerveIso Q r).hom =
      (iteratedSubdivisionNerveIso P r).hom ≫ nerveMap (iteratedMap f r).monotone.functor := by
…

    Mentions: OAI.Thomason.Construction.iteratedSubdivision, OAI.Thomason.Construction.iteratedSubdivisionNerveIso, OAI.Thomason.Construction.RelativeLabelCarrier.iteratedMap

  11. theorem OAI.Thomason.Construction.RelativeLabelCarrier.iteratedChainRealization_naturality line 177

    Source documentation

    Boundary inclusions commute with the actual iterated barycentric maps, not only with their homotopy classes.

    theorem iteratedChainRealization_naturality {P Q : PartOrd.{0}} [Finite P] [Finite Q]
    (f : P →o Q) (hf : Function.Injective f) (r : ℕ)
    (z : SSet.toTop.obj (nerve (iteratedChainPoset P r))) :
    (SSet.toTop.map (nerveMap f.monotone.functor)).hom (iteratedChainRealization P r z) =
      iteratedChainRealization Q r ((SSet.toTop.map
        (nerveMap (iteratedMap f r).monotone.functor)).hom z) := by
…

    Mentions: OAI.Thomason.Construction.iteratedChainPoset, OAI.Thomason.Construction.RelativeLabelCarrier.iteratedMap

  12. theorem OAI.Thomason.Construction.RelativeLabelCarrier.posetVertexPoint_map line 198
  13. theorem OAI.Thomason.Construction.RelativeLabelCarrier.boundary_label_le line 208

    Source documentation

    Labels selected on the full parameter space compare to the prescribed order map on its injected boundary parameter space.

    theorem boundary_label_le {A B : PartOrd.{0}} [Finite A] [Finite 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)
    (r : ℕ) (label : iteratedChainPoset B r → P)
    (hl : ∀ v, 0 < (PosetGeometry.coordinates P
      (F (iteratedChainRealization B r (posetVertexPoint v)))).weights (label v))
    (v : iteratedChainPoset A r) :
    label (iteratedMap i r v) ≤ g (greatestVertex A r v) := by
…

    Mentions: OAI.Thomason.Construction.iteratedChainPoset, OAI.Thomason.Construction.PosetGeometry.coordinates, OAI.Thomason.Construction.RelativeLabelCarrier.iteratedMap, OAI.Thomason.Construction.RelativeLabelCarrier.greatestVertex

  14. theorem OAI.Thomason.Construction.PosetGeometry.map_blend line 248
  15. theorem OAI.Thomason.Construction.PosetGeometry.interpolate_map_of_eq line 252
  16. theorem OAI.Thomason.Construction.SubdivisionBarycentric.greatestVertex_map line 271
  17. theorem OAI.Thomason.Construction.SubdivisionBarycentric.greatestVertex_realization_naturality line 283
  18. theorem OAI.Thomason.Construction.SubdivisionBarycentric.iteratedCarrierHomotopy_naturality line 304
  19. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_simplicial_approximation line 343

    Source documentation

    The target is the original arbitrary simplicial set. No Kan or nonsingularity hypothesis is imposed on it.

    theorem exists_simplicial_approximation (Q : PartOrd.{0}) [Fintype Q]
    (K : SSet.{0}) (f : C(SSet.toTop.obj (nerve Q), SSet.toTop.obj K)) :
    ∃ (r : ℕ) (g : nerve (NonemptyFiniteChains (iteratedChainPoset Q r)) ⟶ K),
      letI := Fintype.ofFinite (iteratedChainPoset Q r)
…

    Mentions: OAI.Thomason.Construction.iteratedChainPoset

  20. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_weak_simplicial_approximation line 382

    Source documentation

    The approximation keeps the actual weak-homotopy-equivalence test.

    theorem exists_weak_simplicial_approximation (Q : PartOrd.{0}) [Fintype Q]
    (K : SSet.{0}) (f : C(SSet.toTop.obj (nerve Q), SSet.toTop.obj K)) :
    ∃ (r : ℕ) (g : nerve (NonemptyFiniteChains (iteratedChainPoset Q r)) ⟶ K),
      IsWeakHomotopyEquivalence f ↔ realizationWeakEquivalences g := by
…

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

  21. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_iterated_weak_approximation line 400