OAI/CategoryTheory/Thomason/Simplicial/BarycentricSupportInclusion.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thomason.Construction.SubdivisionBarycentric.iteratedChainRealization line 26
2. theorem OAI.Thomason.Construction.SubdivisionBarycentric.affineRealization_iteratedChainRealization line 33
3. theorem OAI.Thomason.Construction.SubdivisionBarycentric.iteratedChainRealization_simplex_dist line 64

   Source documentation

   Complete closed simplices of every stage have the asserted shrinking diameter after mapping into the original realization.

   theorem iteratedChainRealization_simplex_dist (P : PartOrd.{0}) [Fintype P]
       {N d : ℕ} (hP : ChainCardBound P N) (x : P → Fin d → ℝ)
       (D : ℝ) (hD : 0 ≤ D) (hx : ChainMesh x D) (r m : ℕ)
       (s : Fin (m+1) ⥤ iteratedChainPoset P r)
       (p q : Convexity.StdSimplex ℝ (Fin (m+1))) :
       dist (affineRealization x (iteratedChainRealization P r
           (RealizationPrism.simplexPoint (nerve (iteratedChainPoset P r)) s p)))
         (affineRealization x (iteratedChainRealization P r
           (RealizationPrism.simplexPoint (nerve (iteratedChainPoset P r)) s q))) ≤
         (meshRatio N)^r*D := by
   …

   Mentions: OAI.Thomason.Construction.ChainCardBound, OAI.Thomason.Construction.SubdivisionBarycentric.ChainMesh, OAI.Thomason.Construction.iteratedChainPoset, OAI.Thomason.Construction.SubdivisionBarycentric.affineRealization, OAI.Thomason.Construction.SubdivisionBarycentric.iteratedChainRealization, OAI.Thomason.Construction.RealizationPrism.simplexPoint, OAI.Thomason.Construction.SubdivisionBarycentric.meshRatio

4. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_iteratedChainRealization_cover line 98
5. def OAI.Thomason.Construction.SubdivisionBarycentric.standardVertexPositions line 144
6. theorem OAI.Thomason.Construction.SubdivisionBarycentric.finiteAffineValue_standardVertexPositions line 147
7. theorem OAI.Thomason.Construction.SubdivisionBarycentric.standardVertexPositions_mesh line 155
8. theorem OAI.Thomason.Construction.SubdivisionBarycentric.standardVertexPositions_isClosedEmbedding line 164
9. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_iteratedChainRealization_intrinsic_cover line 184

   Source documentation

   One stage refines the open cover on every whole closed simplex, in the actual original realization topology.

   theorem exists_iteratedChainRealization_intrinsic_cover (P : PartOrd.{0}) [Fintype P]
       {ι : Type*} (U : ι → Set (SSet.toTop.obj (nerve P)))
       (hU : ∀ i, IsOpen (U i)) (hcover : ⋃ i, U i = Set.univ) :
       ∃ r : ℕ, ∀ (m : ℕ) (s : Fin (m+1) ⥤ iteratedChainPoset P r),
         ∃ i : ι, ∀ p : StdSimplex ℝ (Fin (m+1)),
           iteratedChainRealization P r
             (RealizationPrism.simplexPoint (nerve (iteratedChainPoset P r)) s p) ∈ U i := by
   …

   Mentions: OAI.Thomason.Construction.iteratedChainPoset, OAI.Thomason.Construction.SubdivisionBarycentric.iteratedChainRealization, OAI.Thomason.Construction.RealizationPrism.simplexPoint

10. def OAI.Thomason.Construction.SubdivisionBarycentric.posetVertexPoint line 237
11. theorem OAI.Thomason.Construction.SubdivisionBarycentric.simplexPoint_single line 240
12. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_iteratedChainRealization_star_cover line 254
13. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_iteratedChainRealization_intrinsic_star_cover line 286
14. theorem OAI.Thomason.Construction.SubdivisionBarycentric.iteratedChainRealization_weak line 339
15. def OAI.Thomason.Construction.SubdivisionBarycentric.edgeOrderHom line 372
16. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_poset_approximation_labels line 378
17. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_poset_approximation_map line 419

    Source documentation

    The chosen labels already give an actual map from a finite subdivision into the original simplicial target.

    theorem exists_poset_approximation_map (Q : PartOrd.{0}) [Fintype Q]
        (P : Type) [PartialOrder P]
        (f : C(SSet.toTop.obj (nerve Q), SSet.toTop.obj (nerve P))) :
        ∃ (r : ℕ) (label : iteratedChainPoset Q r → P)
          (hlabel : ChainLabelApproximation.MapsChains label),
          ∃ g : SSet.sd.obj (nerve (iteratedChainPoset Q r)) ⟶ nerve P,
            g = ChainLabelApproximation.subdivisionMapOfLabels label hlabel ∧
            ∀ (m : ℕ) (s : Fin (m+1) ⥤ iteratedChainPoset Q r)
              (p : StdSimplex ℝ (Fin (m+1))) (k : Fin (m+1)),
              0 < (PosetGeometry.coordinates P (f (iteratedChainRealization Q r
                (RealizationPrism.simplexPoint (nerve (iteratedChainPoset Q r)) s p)))).weights
                  (label (s.obj k)) := by
    …

    Mentions: OAI.Thomason.Construction.iteratedChainPoset, OAI.Thomason.Construction.ChainLabelApproximation.MapsChains, OAI.Thomason.Construction.ChainLabelApproximation.subdivisionMapOfLabels, OAI.Thomason.Construction.PosetGeometry.coordinates, OAI.Thomason.Construction.SubdivisionBarycentric.iteratedChainRealization, OAI.Thomason.Construction.RealizationPrism.simplexPoint

18. theorem OAI.Thomason.Construction.SubdivisionBarycentric.labelApproximation_support line 455
19. def OAI.Thomason.Construction.SubdivisionBarycentric.labelApproximationHomotopy line 500
20. theorem OAI.Thomason.Construction.SubdivisionBarycentric.labelApproximation_weak_iff line 514
21. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_poset_simplicial_approximation line 531
22. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_poset_weak_simplicial_approximation line 545

    Source documentation

    The approximation retains the original actual weak-equivalence test, with no Kan--Quillen or simplicial-approximation assumption.

    theorem exists_poset_weak_simplicial_approximation (Q : PartOrd.{0}) [Fintype Q]
        (P : Type) [PartialOrder P] [Finite P]
        (f : C(SSet.toTop.obj (nerve Q), SSet.toTop.obj (nerve P))) :
        ∃ (r : ℕ) (g : nerve (NonemptyFiniteChains (iteratedChainPoset Q r)) ⟶ nerve P),
          (IsWeakHomotopyEquivalence f ↔ realizationWeakEquivalences g) ∧
          letI := Fintype.ofFinite (iteratedChainPoset Q r)
    …

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

23. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_nonsingular_weak_simplicial_approximation line 588

    Source documentation

    Approximation into the original finite nonsingular target, together with its actual continuous comparison homotopy and weak-equivalence test.

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

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

24. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_nonsingular_iterated_weak_approximation line 629

    Source documentation

    The same existence statement on the actual iterated subdivision, with the original target and the original continuous weak-equivalence test.

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

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

25. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_subcomplex_approximation_map line 665

    Source documentation

    Approximate labels for a map into a subcomplex already have carriers in that exact subcomplex.

    theorem exists_subcomplex_approximation_map (Q : PartOrd.{0}) [Fintype Q]
        (P : Type) [PartialOrder P] (A : (nerve P).Subcomplex)
        (f : C(SSet.toTop.obj (nerve Q), SSet.toTop.obj A.toSSet)) :
        ∃ (r : ℕ) (label : iteratedChainPoset Q r → P)
          (hlabel : ChainLabelApproximation.MapsChains label),
          ∃ g : SSet.sd.obj (nerve (iteratedChainPoset Q r)) ⟶ A.toSSet,
            g ≫ A.ι = ChainLabelApproximation.subdivisionMapOfLabels label hlabel := by
    …

    Mentions: OAI.Thomason.Construction.iteratedChainPoset, OAI.Thomason.Construction.ChainLabelApproximation.MapsChains, OAI.Thomason.Construction.ChainLabelApproximation.subdivisionMapOfLabels

26. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_label_subcomplex_homotopy line 718
27. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_subcomplex_simplicial_approximation line 758
28. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_subcomplex_weak_simplicial_approximation line 774

    Source documentation

    The actual realization-W test of the simplicial approximation agrees with the original continuous map, inside the prescribed target.

    theorem exists_subcomplex_weak_simplicial_approximation (Q : PartOrd.{0}) [Fintype Q]
        (P : Type) [PartialOrder P] [Finite P] (A : (nerve P).Subcomplex)
        (f : C(SSet.toTop.obj (nerve Q), SSet.toTop.obj A.toSSet)) :
        ∃ (r : ℕ) (g : nerve (NonemptyFiniteChains (iteratedChainPoset Q r)) ⟶ A.toSSet),
          IsWeakHomotopyEquivalence f ↔ realizationWeakEquivalences g := by
    …

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

29. theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_subcomplex_iterated_weak_approximation line 795

    Source documentation

    The same approximation on the actual iterated-subdivision functor, using the proved canonical chain-nerve isomorphism.

    theorem exists_subcomplex_iterated_weak_approximation (Q : PartOrd.{0}) [Fintype Q]
        (P : Type) [PartialOrder P] [Finite P] (A : (nerve P).Subcomplex)
        (f : C(SSet.toTop.obj (nerve Q), SSet.toTop.obj A.toSSet)) :
        ∃ (r : ℕ) (g : (iteratedSubdivision r).obj (nerve Q) ⟶ A.toSSet),
          IsWeakHomotopyEquivalence f ↔ realizationWeakEquivalences g := by
    …

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

30. def OAI.Thomason.Construction.RelativeLabelCarrier.greatestVertex line 832

    Source documentation

    The recursively greatest original vertex of a subdivided vertex.

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

    Mentions: OAI.Thomason.Construction.iteratedChainPoset

31. theorem OAI.Thomason.Construction.RelativeLabelCarrier.coordinate_map_support line 839

    Source documentation

    Positive coordinates of a realized order map come from positive coordinates in its source.

    theorem coordinate_map_support {Q P : Type} [PartialOrder Q] [PartialOrder P]
        (g : Q →o P) (z : SSet.toTop.obj (nerve Q)) (p : P)
        (hp : (PosetGeometry.coordinates P ((SSet.toTop.map (nerveMap g.monotone.functor)).hom z)).weights p ≠ 0) :
        ∃ q : Q, (PosetGeometry.coordinates Q z).weights q ≠ 0 ∧ g q = p := by
    …

    Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates

32. theorem OAI.Thomason.Construction.RelativeLabelCarrier.iterated_coordinate_support line 853

    Source documentation

    Every original positive coordinate comes from a stage face containing it below that face's recursively greatest vertex.

    theorem iterated_coordinate_support (Q : PartOrd.{0}) [Finite Q] (r : ℕ)
        (z : SSet.toTop.obj (nerve (iteratedChainPoset Q r))) (q : Q)
        (hq : (PosetGeometry.coordinates Q (iteratedChainRealization Q r z)).weights q ≠ 0) :
        ∃ v : iteratedChainPoset Q r,
          (PosetGeometry.coordinates (iteratedChainPoset Q r) z).weights v ≠ 0 ∧
            q ≤ greatestVertex Q r v := by
    …

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

33. theorem OAI.Thomason.Construction.RelativeLabelCarrier.coordinates_vertexPoint line 873
34. theorem OAI.Thomason.Construction.RelativeLabelCarrier.iterated_vertex_coordinate_le line 881

    Source documentation

    In particular, the barycentric image of a stage vertex lies below its recursively greatest original vertex.

    theorem iterated_vertex_coordinate_le (Q : PartOrd.{0}) [Finite Q] (r : ℕ)
        (v : iteratedChainPoset Q r) (q : Q)
        (hq : (PosetGeometry.coordinates Q
          (iteratedChainRealization Q r (posetVertexPoint v))).weights q ≠ 0) :
        q ≤ greatestVertex Q r v := by
    …

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

35. theorem OAI.Thomason.Construction.RelativeLabelCarrier.label_le_prescribed line 896

    Source documentation

    This is the boundary-label bound: positivity after the prescribed realized order map gives an order comparison to the exact last vertex.

    theorem label_le_prescribed (Q : PartOrd.{0}) [Finite Q]
        {P : Type} [PartialOrder P] (g : Q →o P) (r : ℕ)
        (v : iteratedChainPoset Q r) (p : P)
        (hp : 0 < (PosetGeometry.coordinates P
          ((SSet.toTop.map (nerveMap g.monotone.functor)).hom
            (iteratedChainRealization Q r (posetVertexPoint v)))).weights p) :
        p ≤ g (greatestVertex Q r v) := by
    …

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

36. theorem OAI.Thomason.Construction.RelativeLabelCarrier.greatestVertex_lastVertex line 909

    Source documentation

    The recursively greatest map is the actual iterated last-vertex map.

    theorem greatestVertex_lastVertex (Q : PartOrd.{0}) [Finite Q] (r : ℕ) :
        (iteratedSubdivisionNerveIso Q r).hom ≫ nerveMap (greatestVertex Q r).monotone.functor =
          iteratedLastVertex (nerve Q) r := by
    …

    Mentions: OAI.Thomason.Construction.iteratedSubdivisionNerveIso, OAI.Thomason.Construction.RelativeLabelCarrier.greatestVertex, OAI.Thomason.Construction.iteratedLastVertex

37. theorem OAI.Thomason.Construction.SubdivisionBarycentric.chainPoint_positive_of_mem line 958
38. theorem OAI.Thomason.Construction.SubdivisionBarycentric.iterated_greatest_coordinate_positive line 975
39. theorem OAI.Thomason.Construction.SubdivisionBarycentric.iterated_lastVertex_support_subset line 993
40. def OAI.Thomason.Construction.SubdivisionBarycentric.iteratedCarrierHomotopy line 1007

    Source documentation

    The comparison with exact last vertex can be made wholly inside the original barycentric carrier at each point.

    def iteratedCarrierHomotopy (P : PartOrd.{0}) [Finite P] (r : ℕ) :
        (iteratedChainRealization P r).Homotopy
          (SSet.toTop.map (nerveMap (greatestVertex P r).monotone.functor)).hom :=
    …

    Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.iteratedChainRealization