PosetSubcomplexHomotopy.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Uniform shrinking on the actual iterated chain posets

The same dimension bound controls every stage, although the number of vertices increases. Vertex locations are recursively their actual face barycenters, so the estimate applies to geometric subdivision.

def OAI.Thomason.Construction.SubdivisionBarycentric.meshRatio line 25
theorem OAI.Thomason.Construction.SubdivisionBarycentric.meshRatio_nonneg line 27
theorem OAI.Thomason.Construction.SubdivisionBarycentric.meshRatio_lt_one line 33
def OAI.Thomason.Construction.SubdivisionBarycentric.iteratedAffineVertices line 38
theorem OAI.Thomason.Construction.SubdivisionBarycentric.iteratedAffineVertices_mesh line 45
theorem OAI.Thomason.Construction.SubdivisionBarycentric.iteratedAffineVertices_mesh_tendsto_zero line 63
theorem OAI.Thomason.Construction.SubdivisionBarycentric.exists_iteratedAffineVertices_small line 71
Source documentation
Every positive geometric scale is reached uniformly on all chains of one subdivision stage.
```
theorem exists_iteratedAffineVertices_small (P : PartOrd.{0}) [Finite P]
    {N d : ℕ} (hP : ChainCardBound P N) (x : P → Fin d → ℝ)
    (D : ℝ) (hD : 0 ≤ D) (hx : ChainMesh x D)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ r : ℕ, ∀ i j : iteratedChainPoset P r, (i ≤ j ∨ j ≤ i) →
      dist (iteratedAffineVertices P x r i) (iteratedAffineVertices P x r j) < ε := by
…
```
Mentions: OAI.Thomason.Construction.ChainCardBound, OAI.Thomason.Construction.SubdivisionBarycentric.ChainMesh, OAI.Thomason.Construction.iteratedChainPoset, OAI.Thomason.Construction.SubdivisionBarycentric.iteratedAffineVertices
theorem OAI.Thomason.Construction.SubdivisionBarycentric.finiteAffineValue_map line 102
def OAI.Thomason.Construction.SubdivisionBarycentric.affineRealization line 116
theorem OAI.Thomason.Construction.SubdivisionBarycentric.affineRealization_simplexPoint line 128
theorem OAI.Thomason.Construction.SubdivisionBarycentric.affineCoordinates_dist line 142
theorem OAI.Thomason.Construction.SubdivisionBarycentric.affineRealization_simplex_dist line 169
theorem OAI.Thomason.Construction.SubdivisionBarycentric.iteratedAffineRealization_simplex_dist line 181
theorem OAI.Thomason.Construction.PosetGeometry.carrier_le_iff_coordinates_support_subset line 224
Source documentation
The actual carrier order is exactly inclusion of positive coordinate supports, even when the ambient poset is infinite.
```
theorem carrier_le_iff_coordinates_support_subset
    (y z : SSet.toTop.obj (nerve P)) :
    carrier (nerve P) y ≤ carrier (nerve P) z ↔
      (coordinates P y).weights.support ⊆ (coordinates P z).weights.support := by
…
```
Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates

theorem OAI.Thomason.Construction.PosetGeometry.mem_subcomplex_of_coordinates_support_subset line 260

Source documentation

Decreasing positive support cannot leave a specified subcomplex.

theorem mem_subcomplex_of_coordinates_support_subset
    (A : (nerve P).Subcomplex) (y z : SSet.toTop.obj (nerve P))
    (hz : z ∈ Set.range (SSet.toTop.map A.ι).hom)
    (hyz : (coordinates P y).weights.support ⊆ (coordinates P z).weights.support) :
    y ∈ Set.range (SSet.toTop.map A.ι).hom := by
…

Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates

theorem OAI.Thomason.Construction.PosetGeometry.simplex_mem_of_vertices_positive line 271
Source documentation
A simplex whose vertices belong to the positive support of a point of a subcomplex belongs to that subcomplex. No fullness is required.
```
theorem simplex_mem_of_vertices_positive (A : (nerve P).Subcomplex)
    (z : SSet.toTop.obj (nerve P))
    (hz : z ∈ Set.range (SSet.toTop.map A.ι).hom)
    {n : ℕ} (s : (nerve P).obj (.op (.mk n)))
    (hs : ∀ i, 0 < (coordinates P z).weights (s.obj i)) : s ∈ A.obj _ := by
…
```
Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates

theorem OAI.Thomason.Construction.PosetGeometry.simplex_mem_of_vertices_positive' line 293

Source documentation

The same carrier test for all degrees of the nerve.

theorem simplex_mem_of_vertices_positive' (A : (nerve P).Subcomplex)
    (z : SSet.toTop.obj (nerve P))
    (hz : z ∈ Set.range (SSet.toTop.map A.ι).hom)
    (d : SimplexCategoryᵒᵖ) (s : (nerve P).obj d)
    (hs : ∀ i, 0 < (coordinates P z).weights (s.obj i)) : s ∈ A.obj d := by
…

Mentions: OAI.Thomason.Construction.PosetGeometry.coordinates

theorem OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabels_range_le line 314
Source documentation
A point in the target subcomplex carrying the labels of each source face suffices to factor the whole nerve map through the subcomplex.
```
theorem nerveMapOfLabels_range_le (A : (nerve P).Subcomplex)
    (label : Q → P) (hlabel : MapsChains label)
    (hcarrier : ∀ C : NonemptyFiniteChains Q,
      ∃ z : SSet.toTop.obj (nerve P),
        z ∈ Set.range (SSet.toTop.map A.ι).hom ∧
          ∀ q ∈ C.finset, 0 < (PosetGeometry.coordinates P z).weights (label q)) :
    SSet.Subcomplex.range (nerveMapOfLabels label hlabel) ≤ A := by
…
```
Mentions: OAI.Thomason.Construction.ChainLabelApproximation.MapsChains, OAI.Thomason.Construction.PosetGeometry.coordinates, OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabels

def OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabelsToSubcomplex line 331

Source documentation

The label map with its actual prescribed subcomplex as codomain.

def nerveMapOfLabelsToSubcomplex (A : (nerve P).Subcomplex)
    (label : Q → P) (hlabel : MapsChains label)
    (hcarrier : ∀ C : NonemptyFiniteChains Q,
      ∃ z : SSet.toTop.obj (nerve P),
        z ∈ Set.range (SSet.toTop.map A.ι).hom ∧
          ∀ q ∈ C.finset, 0 < (PosetGeometry.coordinates P z).weights (label q)) :
    nerve (NonemptyFiniteChains Q) ⟶ A :=
…

Mentions: OAI.Thomason.Construction.ChainLabelApproximation.MapsChains, OAI.Thomason.Construction.PosetGeometry.coordinates

theorem OAI.Thomason.Construction.ChainLabelApproximation.nerveMapOfLabelsToSubcomplex_ι line 342
theorem OAI.Thomason.Construction.PosetGeometry.blend_support_subset line 372
theorem OAI.Thomason.Construction.PosetGeometry.interpolate_mem_subcomplex line 385
def OAI.Thomason.Construction.PosetGeometry.liftSubcomplexHomotopy line 396
def OAI.Thomason.Construction.PosetGeometry.subcomplexHomotopyOfSupportSubset line 414