OAI/CategoryTheory/Thomason/Chains/NerveFaceChains.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Barycentric subdivision maps for finite poset realizations

The affine combination of a chain of nonempty faces is supported in its greatest face. It therefore gives a continuous map to the original nerve realization, with the expected affine-coordinate compatibility.

  1. def OAI.Thomason.Construction.SubdivisionBarycentric.chainPoint line 29
  2. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainPoint_weight line 33
  3. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainPoint_support line 48
  4. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainPoint_chainSupported line 64
  5. def OAI.Thomason.Construction.SubdivisionBarycentric.chainPointMap line 76
  6. def OAI.Thomason.Construction.SubdivisionBarycentric.chainRealizationMap line 90
  7. theorem OAI.Thomason.Construction.SubdivisionBarycentric.coordinates_chainRealizationMap line 98
  8. theorem OAI.Thomason.Construction.SubdivisionBarycentric.affineRealization_chainRealizationMap line 103
  9. def OAI.Thomason.Construction.SubdivisionBarycentric.greatestRealizationMap line 149
  10. theorem OAI.Thomason.Construction.SubdivisionBarycentric.greatestRealizationMap_support line 154
  11. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainRealizationMap_compatible line 172
  12. def OAI.Thomason.Construction.SubdivisionBarycentric.chainRealizationMapHomotopy line 194
  13. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainRealizationMap_weak line 198
  14. def OAI.Thomason.Construction.SubdivisionBarycentric.finiteChainSimplex line 224
  15. theorem OAI.Thomason.Construction.SubdivisionBarycentric.finiteChainSimplex_range line 230
  16. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_coordinates_on_chain line 240
  17. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_point_on_chain line 265
  18. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainPoint_simplex_support line 274
  19. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainRealizationMap_simplex_representation line 290
  20. def OAI.Thomason.Construction.NerveFaceChains.chainOfFace line 326
  21. theorem OAI.Thomason.Construction.NerveFaceChains.mem_chainOfFace line 338
  22. theorem OAI.Thomason.Construction.NerveFaceChains.chainOfFace_le_iff line 343
  23. def OAI.Thomason.Construction.NerveFaceChains.faceOfChain line 378
  24. theorem OAI.Thomason.Construction.NerveFaceChains.chainOfFace_faceOfChain line 384
  25. def OAI.Thomason.Construction.NerveFaceChains.orderIso line 392
  26. theorem OAI.Thomason.Construction.NerveFaceChains.greatest_chainOfFace line 398
  27. theorem OAI.Thomason.Construction.NerveFaceChains.lastVertex_eq line 407

    Source documentation

    The face-poset comparison reads exactly the greatest original vertex.

    theorem lastVertex_eq :
    NonsingularLastVertex.map (nerve P) =
      nerveMap (orderIso P).toOrderEmbedding.toOrderHom.monotone.functor ≫
        nerveMap (greatestHom (P := P)).monotone.functor := by
…

    Mentions: OAI.Thomason.Construction.NonsingularLastVertex.map, OAI.Thomason.Construction.NerveFaceChains.orderIso

  28. def OAI.Thomason.Construction.NerveFaceChains.nerveIso line 424

    Source documentation

    The subdivision has this face-poset as its nerve.

    def nerveIso (P : Type) [PartialOrder P] :
    nerve (nerve P).N ≅ nerve (NonemptyFiniteChains P) where
…
  29. def OAI.Thomason.Construction.NerveFaceChains.subdivisionIso line 445
  30. theorem OAI.Thomason.Construction.NerveFaceChains.subdivisionIso_lastVertex line 449
  31. theorem OAI.Thomason.Construction.NerveFaceChains.chainOfFace_naturality line 459
  32. theorem OAI.Thomason.Construction.NerveFaceChains.nerveIso_naturality line 476
  33. theorem OAI.Thomason.Construction.NerveFaceChains.subdivisionIso_naturality line 491