OAI/CategoryTheory/Thomason/Chains/FiniteChainMesh.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

From chain-valued vertex labels to a simplicial map

Labels need not be monotone. It suffices that they send comparable vertices to comparable vertices: taking the greatest label on each face then gives a monotone map on the finite-chain poset.

  1. def OAI.Thomason.Construction.ChainLabelApproximation.greatest line 27
  2. theorem OAI.Thomason.Construction.ChainLabelApproximation.greatest_mem line 30
  3. theorem OAI.Thomason.Construction.ChainLabelApproximation.le_greatest line 34
  4. theorem OAI.Thomason.Construction.ChainLabelApproximation.greatest_monotone line 41
  5. def OAI.Thomason.Construction.ChainLabelApproximation.greatestHom line 46
  6. theorem OAI.Thomason.Construction.ChainLabelApproximation.greatest_map line 49
  7. theorem OAI.Thomason.Construction.ChainLabelApproximation.greatest_eq_chainMaximum line 60
  8. def OAI.Thomason.Construction.ChainLabelApproximation.MapsChains line 66
  9. def OAI.Thomason.Construction.ChainLabelApproximation.labelChain line 69
  10. theorem OAI.Thomason.Construction.ChainLabelApproximation.labelChain_monotone line 83
  11. def OAI.Thomason.Construction.ChainLabelApproximation.greatestLabel line 89
  12. theorem OAI.Thomason.Construction.ChainLabelApproximation.greatestLabel_mem line 93
  13. theorem OAI.Thomason.Construction.ChainLabelApproximation.greatestLabel_of_monotone line 99
  14. def OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabels line 108
  15. def OAI.Thomason.Construction.ChainLabelApproximation.subdivisionMapOfLabels line 113
  16. theorem OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabels_carrier line 119

    Source documentation

    All output vertices of a chain simplex are labels of vertices in its greatest source face. This is the finite carrier needed for approximation.

    theorem nerveMapOfLabels_carrier {Q P : Type} [PartialOrder Q] [PartialOrder P]
    (label : Q → P) (hlabel : MapsChains label) (d : SimplexCategoryᵒᵖ)
    (s : (nerve (NonemptyFiniteChains Q)).obj d) (i : Fin (d.unop.len+1)) :
    ∃ q ∈ (s.obj (Fin.last d.unop.len)).finset,
      label q = ((nerveMapOfLabels label hlabel).app d s).obj i := by
…

    Mentions: OAI.Thomason.Construction.ChainLabelApproximation.MapsChains, OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabels

  17. theorem OAI.Thomason.Construction.ChainLabelApproximation.vertices_factor line 128
  18. theorem OAI.Thomason.Construction.ChainLabelApproximation.piece_greatest line 146
  19. theorem OAI.Thomason.Construction.ChainLabelApproximation.subdivision_greatest_eq_lastVertex line 180

    Source documentation

    The greatest-face map agrees with the last-vertex map on subdivision.

    theorem subdivision_greatest_eq_lastVertex (P : Type) [PartialOrder P] :
    NerveSubdivisionMap.map P ≫ nerveMap (greatestHom (P := P)).monotone.functor =
…

    Mentions: OAI.Thomason.Construction.NerveSubdivisionMap.map, OAI.Thomason.Construction.ChainLabelApproximation.greatestHom

  20. theorem OAI.Thomason.Construction.ChainLabelApproximation.greatest_nerveMap_weak line 191
  21. theorem OAI.Thomason.Construction.ChainLabelApproximation.greatestLabel_le line 226

    Source documentation

    Every bound on the labels of a face bounds its greatest label.

    theorem greatestLabel_le (C : NonemptyFiniteChains Q) (b : P)
    (h : ∀ q ∈ C.finset, label q ≤ b) : greatestLabel label hlabel C ≤ b := by
…

    Mentions: OAI.Thomason.Construction.ChainLabelApproximation.greatestLabel

  22. def OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabelsCarrierHomotopy line 234

    Source documentation

    A prescribed monotone carrier upper bound gives the comparison homotopy without requiring the labels themselves to be monotone.

    def nerveMapOfLabelsCarrierHomotopy (g : NonemptyFiniteChains Q →o P)
    (h : ∀ C, ∀ q ∈ C.finset, label q ≤ g C) :
    SSet.Homotopy (nerveMapOfLabels label hlabel) (nerveMap g.monotone.functor) :=
…

    Mentions: OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabels

  23. theorem OAI.Thomason.Construction.ChainLabelApproximation.greatestLabel_le_comp_greatest line 241

    Source documentation

    A pointwise comparison propagates to the chain-valued approximation.

    theorem greatestLabel_le_comp_greatest (g : Q →o P) (h : ∀ q, label q ≤ g q)
    (C : NonemptyFiniteChains Q) : greatestLabel label hlabel C ≤ g (greatest C) := by
…

    Mentions: OAI.Thomason.Construction.ChainLabelApproximation.greatestLabel, OAI.Thomason.Construction.ChainLabelApproximation.greatest

  24. def OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabelsHomotopy line 249

    Source documentation

    Labels with a common prescribed upper map give a homotopy to that map composed with the greatest-face comparison.

    def nerveMapOfLabelsHomotopy (g : Q →o P) (h : ∀ q, label q ≤ g q) :
    SSet.Homotopy (nerveMapOfLabels label hlabel)
      (nerveMap (greatestHom (P := Q)).monotone.functor ≫ nerveMap g.monotone.functor) := by
…

    Mentions: OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabels, OAI.Thomason.Construction.ChainLabelApproximation.greatestHom

  25. def OAI.Thomason.Construction.ChainLabelApproximation.subdivisionMapOfLabelsHomotopy line 257

    Source documentation

    The comparison on subdivision has the last-vertex map as its endpoint.

    def subdivisionMapOfLabelsHomotopy (g : Q →o P) (h : ∀ q, label q ≤ g q) :
    SSet.Homotopy (subdivisionMapOfLabels label hlabel)
      (lastVertex.app (nerve Q) ≫ nerveMap g.monotone.functor) := by
…

    Mentions: OAI.Thomason.Construction.ChainLabelApproximation.subdivisionMapOfLabels

  26. def OAI.Thomason.Construction.ChainSieve.old line 287
  27. def OAI.Thomason.Construction.ChainSieve.upper line 290
  28. theorem OAI.Thomason.Construction.ChainSieve.old_lower line 293
  29. theorem OAI.Thomason.Construction.ChainSieve.upper_upper line 296
  30. theorem OAI.Thomason.Construction.ChainSieve.old_subset_upper line 299
  31. def OAI.Thomason.Construction.ChainSieve.intersection line 304
  32. theorem OAI.Thomason.Construction.ChainSieve.intersection_old line 307
  33. theorem OAI.Thomason.Construction.ChainSieve.intersection_upper line 310
  34. def OAI.Thomason.Construction.ChainSieve.retraction line 315

    Source documentation

    The face-chain inclusion retracts on precisely the chains meeting the old faces, with the order adjunction.

    noncomputable def retraction (S : Set P) :
    SieveRetraction {c : upper S | c.val ∈ old S} where
…

    Mentions: OAI.Thomason.Construction.SieveRetraction, OAI.Thomason.Construction.ChainSieve.upper, OAI.Thomason.Construction.ChainSieve.old

  35. def OAI.Thomason.Construction.ChainSieve.chainInclusion line 354
  36. def OAI.Thomason.Construction.ChainSieve.restrict line 357
  37. def OAI.Thomason.Construction.ChainSieve.subsetIso line 360
  38. theorem OAI.Thomason.Construction.ChainSieve.subsetIso_inclusion line 364

    Source documentation

    The identification commutes with the original chain inclusion.

    theorem subsetIso_inclusion (S : Set P) :
    (subposetInclusion (old S)).comp (subsetIso S).toOrderEmbedding.toOrderHom =
      NonemptyFiniteChains.orderHomMap (subposetInclusion S) := rfl
…

    Mentions: OAI.Thomason.Construction.subposetInclusion, OAI.Thomason.Construction.ChainSieve.old, OAI.Thomason.Construction.ChainSieve.subsetIso

  39. def OAI.Thomason.Construction.SubdivisionBarycentric.chainDistribution line 387
  40. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainDistribution_weight line 390
  41. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainDistribution_lower line 397
  42. def OAI.Thomason.Construction.SubdivisionBarycentric.chainAverage line 406
  43. def OAI.Thomason.Construction.SubdivisionBarycentric.ChainMesh line 410
  44. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainAverage_dist_of_le line 413
  45. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainMesh_average line 452