ConstructedExtensionLocalizer.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Every point is in an actual barycentric flag simplex

Sorting coordinates and their consecutive differences produces an exact preimage under the affine map from the face-poset realization.

def OAI.Thomason.Construction.SubdivisionBarycentric.permutationFaceMap line 27
theorem OAI.Thomason.Construction.SubdivisionBarycentric.face_permutation line 34
theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_permutation_simplex line 51
theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_permutation line 72
Source documentation
The barycentric affine map respects relabelling of the original vertices.
```
theorem point_permutation (n : ℕ) (σ : Equiv.Perm (Fin (n+1)))
    (z : SSet.toTop.obj (nerve (Faces n))) :
    point n ((SSet.toTop.map (nerveMap (permutationFaceMap n σ).monotone.functor)).hom z) =
      StdSimplex.map σ (point n z) := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.SubdivisionBarycentric.permutationFaceMap
theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_surjective line 81
Source documentation
Every geometric point is represented by one actual simplex of the barycentric face nerve. Zero flag weights handle ties and all boundary faces.
```
theorem point_surjective (n : ℕ) : Function.Surjective (point n) := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.point
theorem OAI.Thomason.Construction.SubdivisionBarycentric.prefix_point_injective line 120
theorem OAI.Thomason.Construction.SubdivisionBarycentric.permuted_prefix_point_injective line 164
Source documentation
Relabelling the vertices preserves uniqueness of flag coordinates.
```
theorem permuted_prefix_point_injective (n : ℕ) (σ : Equiv.Perm (Fin (n+1))) :
    Function.Injective (fun p : StdSimplex ℝ (Fin (n+1)) => point n
      (RealizationPrism.simplexPoint (nerve (Faces n))
        (prefixSimplex n ⋙ (permutationFaceMap n σ).monotone.functor) p)) := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.RealizationPrism.simplexPoint, OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.prefixSimplex, OAI.Thomason.Construction.SubdivisionBarycentric.permutationFaceMap
theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_weight_pos_iff line 209
Source documentation
Positive coordinates of the affine barycentric map have an exact combinatorial support description.
```
theorem point_weight_pos_iff (n : ℕ) (z : SSet.toTop.obj (nerve (Faces n)))
    (i : Fin (n+1)) :
    0 < (point n z).weights i ↔ ∃ A : Faces n,
      0 < (PosetGeometry.coordinates (Faces n) z).weights A ∧ ULift.up i ∈ A.finset := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.PosetGeometry.coordinates
theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_face_simplex line 227
theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_face_naturality line 249
Source documentation
The affine map to the original simplex commutes with every injective ordinal face map, at all points of the actual realization.
```
theorem point_face_naturality {m n : ℕ} (f : Fin (m+1) ↪o Fin (n+1))
    (z : SSet.toTop.obj (nerve (Faces m))) :
    point n ((SSet.toTop.map (nerveMap (faceMap f).monotone.functor)).hom z) =
      StdSimplex.map f (point m z) := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.SubdivisionBarycentric.faceMap
theorem OAI.Thomason.Construction.SubdivisionBarycentric.carrier_le_fullSubposet_iff line 276
def OAI.Thomason.Construction.SubdivisionBarycentric.permittedFaces line 302
Source documentation
Faces of the original simplex are exactly the full subposets of subdivision faces using only their permitted original vertices.
```
def permittedFaces (n : ℕ) (V : Set (Fin (n+1))) : Set (Faces n) :=
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces
theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_face_preimage line 307
Source documentation
The affine barycentric map has exactly the expected face preimage. The statement includes points on every lower-dimensional boundary.
```
theorem point_face_preimage (n : ℕ) (V : Set (Fin (n+1)))
    (z : SSet.toTop.obj (nerve (Faces n))) :
    (∀ i ∉ V, (point n z).weights i = 0) ↔
      carrier (nerve (Faces n)) z ≤ fullSubposetComplex (permittedFaces n V) := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.fullSubposetComplex, OAI.Thomason.Construction.SubdivisionBarycentric.permittedFaces
theorem OAI.Thomason.Construction.SubdivisionBarycentric.point_zero_coordinate_iff line 328
Source documentation
In particular a specified codimension-one face is retained exactly, even where several faces meet.
```
theorem point_zero_coordinate_iff (n : ℕ) (i : Fin (n+1))
    (z : SSet.toTop.obj (nerve (Faces n))) :
    (point n z).weights i = 0 ↔
      carrier (nerve (Faces n)) z ≤
        fullSubposetComplex (permittedFaces n {j | j ≠ i}) := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.fullSubposetComplex, OAI.Thomason.Construction.SubdivisionBarycentric.permittedFaces
def OAI.Thomason.Construction.SubdivisionBarycentric.affineValue line 358
Source documentation
Evaluation of an affine real coordinate by its original vertex values.
```
def affineValue {n : ℕ} (x : Fin (n+1) → ℝ) (p : StdSimplex ℝ (Fin (n+1))) : ℝ :=
…
```
theorem OAI.Thomason.Construction.SubdivisionBarycentric.affineValue_sub_constant line 361
theorem OAI.Thomason.Construction.SubdivisionBarycentric.affineValue_const_sub line 367

theorem OAI.Thomason.Construction.SubdivisionBarycentric.common_mass_bounds line 374

Source documentation

Removing a common vertex mass bounds the remaining affine variation.

theorem common_mass_bounds {n : ℕ} (x : Fin (n+1) → ℝ)
    (p : StdSimplex ℝ (Fin (n+1))) (v : Fin (n+1)) (ε lo hi : ℝ)
    (hmass : ε ≤ p.weights v) (hx : ∀ i, lo ≤ x i ∧ x i ≤ hi) :
    ε * x v + (1-ε) * lo ≤ affineValue x p ∧
      affineValue x p ≤ ε * x v + (1-ε) * hi := by
…

Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.affineValue

theorem OAI.Thomason.Construction.SubdivisionBarycentric.simplex_affine_interval line 399
Source documentation
A single interval of contracted width contains the entire image of a subdivided characteristic simplex under any affine real coordinate.
```
theorem simplex_affine_interval (n m : ℕ) (s : Fin (m+1) ⥤ Faces n)
    (x : Fin (n+1) → ℝ) (lo hi : ℝ) (hx : ∀ i, lo ≤ x i ∧ x i ≤ hi) :
    ∃ v : Fin (n+1), ∀ p : StdSimplex ℝ (Fin (m+1)),
      let z := point n (RealizationPrism.simplexPoint (nerve (Faces n)) s p)
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.RealizationPrism.simplexPoint

theorem OAI.Thomason.Construction.SubdivisionBarycentric.simplex_affine_oscillation line 409

Source documentation

The affine mesh contracts uniformly, including all boundary points.

theorem simplex_affine_oscillation (n m : ℕ) (s : Fin (m+1) ⥤ Faces n)
    (x : Fin (n+1) → ℝ) (lo hi : ℝ) (hx : ∀ i, lo ≤ x i ∧ x i ≤ hi)
    (p q : StdSimplex ℝ (Fin (m+1))) :
    |affineValue x (point n (RealizationPrism.simplexPoint (nerve (Faces n)) s p)) -
      affineValue x (point n (RealizationPrism.simplexPoint (nerve (Faces n)) s q))| ≤
        (1-1/((n : ℝ)+1)) * (hi-lo) := by
…

Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.affineValue, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.RealizationPrism.simplexPoint

theorem OAI.Thomason.Construction.SubdivisionBarycentric.face_chain_dimension_le line 443
Source documentation
A strict chain of faces cannot have greater dimension than its original simplex. Degenerate repetitions are excluded explicitly.
```
theorem face_chain_dimension_le (n m : ℕ) (s : Fin (m+1) ⥤ Faces n)
    (hs : StrictMono s.obj) : m ≤ n := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces
def OAI.Thomason.Construction.SubdivisionBarycentric.affineCoordinates line 463
Source documentation
Affine coordinates with arbitrary Euclidean vertex locations.
```
def affineCoordinates {n d : ℕ} (x : Fin (n+1) → Fin d → ℝ)
    (p : StdSimplex ℝ (Fin (n+1))) : Fin d → ℝ :=
…
```
theorem OAI.Thomason.Construction.SubdivisionBarycentric.simplex_affine_dist line 469
Source documentation
For any Euclidean realization of an n-simplex, every barycentrically subdivided simplex has at most 1-1/(n+1) times the original mesh.
```
theorem simplex_affine_dist (n m d : ℕ) (s : Fin (m+1) ⥤ Faces n)
    (x : Fin (n+1) → Fin d → ℝ) (D : ℝ) (hD : 0 ≤ D)
    (hx : ∀ i j, dist (x i) (x j) ≤ D)
    (p q : StdSimplex ℝ (Fin (m+1))) :
    dist (affineCoordinates x (point n (RealizationPrism.simplexPoint (nerve (Faces n)) s p)))
      (affineCoordinates x (point n (RealizationPrism.simplexPoint (nerve (Faces n)) s q))) ≤
        (1-1/((n : ℝ)+1)) * D := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.affineCoordinates, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.RealizationPrism.simplexPoint
theorem OAI.Thomason.Construction.SubdivisionBarycentric.simplex_affine_diam line 503
Source documentation
The corresponding setwise diameter estimate includes the complete closed characteristic simplex, hence every face and vertex.
```
theorem simplex_affine_diam (n m d : ℕ) (s : Fin (m+1) ⥤ Faces n)
    (x : Fin (n+1) → Fin d → ℝ) (D : ℝ) (hD : 0 ≤ D)
    (hx : ∀ i j, dist (x i) (x j) ≤ D) :
    Metric.diam (Set.range (fun p : StdSimplex ℝ (Fin (m+1)) =>
      affineCoordinates x (point n (RealizationPrism.simplexPoint (nerve (Faces n)) s p)))) ≤
        (1-1/((n : ℝ)+1)) * D := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.affineCoordinates, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.RealizationPrism.simplexPoint
theorem OAI.Thomason.Construction.SubdivisionBarycentric.simplex_affine_dist_of_dim_le line 519
Source documentation
A single ambient dimension gives a uniform contraction factor for all lower-dimensional faces that occur in subsequent subdivisions.
```
theorem simplex_affine_dist_of_dim_le (n k m d : ℕ) (hkn : k ≤ n)
    (s : Fin (m+1) ⥤ Faces k) (x : Fin (k+1) → Fin d → ℝ)
    (D : ℝ) (hD : 0 ≤ D) (hx : ∀ i j, dist (x i) (x j) ≤ D)
    (p q : StdSimplex ℝ (Fin (m+1))) :
    dist (affineCoordinates x (point k (RealizationPrism.simplexPoint (nerve (Faces k)) s p)))
      (affineCoordinates x (point k (RealizationPrism.simplexPoint (nerve (Faces k)) s q))) ≤
        (1-1/((n : ℝ)+1)) * D := by
…
```
Mentions: OAI.Thomason.Construction.SubdivisionBarycentric.Faces, OAI.Thomason.Construction.SubdivisionBarycentric.affineCoordinates, OAI.Thomason.Construction.SubdivisionBarycentric.point, OAI.Thomason.Construction.RealizationPrism.simplexPoint
def OAI.Thomason.Construction.SubdivisionBarycentric.finiteAffineValue line 555
theorem OAI.Thomason.Construction.SubdivisionBarycentric.finiteAffineValue_sub line 558
theorem OAI.Thomason.Construction.SubdivisionBarycentric.finiteAffineValue_const_sub line 563
theorem OAI.Thomason.Construction.SubdivisionBarycentric.supported_common_mass_bounds line 568
theorem OAI.Thomason.Construction.SubdivisionBarycentric.supported_common_mass_dist line 598
theorem OAI.Thomason.Construction.subdivision_simplex_representation line 625
def OAI.Thomason.Construction.simplexDoubleFirst line 661
def OAI.Thomason.Construction.simplexDoubleLast line 665
def OAI.Thomason.Construction.simplexMaximumMap line 671
Source documentation
The ordinal map given by the maxima of the vertices of a simplex in the chain-poset nerve.
```
def simplexMaximumMap {m n : SimplexCategory}
    (s : SSet.stdSimplex.{0}.obj m ⟶ SimplexCategory.sd.obj n) : m ⟶ n :=
…
```
theorem OAI.Thomason.Construction.simplexMaximumMap_fac line 682

theorem OAI.Thomason.Construction.simplexMaximumMap_chain_le line 692

Source documentation

Every maximum contributed by a smaller chain belongs to the greatest chain in the simplex. This is the key ordered comparison.

theorem simplexMaximumMap_chain_le {m n : SimplexCategory}
    (s : SSet.stdSimplex.{0}.obj m ⟶ SimplexCategory.sd.obj n)
    (B : NonemptyFiniteChains (ULift.{0} (Fin (m.len + 1)))) :
    NonemptyFiniteChains.orderHomMap
        (SimplexCategory.toPartOrd.map (simplexMaximumMap s)).hom B ≤
      (SSet.yonedaEquiv s).obj (chainMaximum B).down := by
…

Mentions: OAI.Thomason.Construction.simplexMaximumMap, OAI.Thomason.Construction.chainMaximum

theorem OAI.Thomason.Construction.simplexLastVertex_zero_comp line 710
theorem OAI.Thomason.Construction.simplexDoubleFirst_le line 720
def OAI.Thomason.Construction.simplexDoubleHomotopy line 756
def OAI.Thomason.Construction.simplexDoublePrism line 760
theorem OAI.Thomason.Construction.simplexDoublePrism_zero line 764
theorem OAI.Thomason.Construction.simplexDoublePrism_one line 767
theorem OAI.Thomason.Construction.simplexDoubleFirst_naturality line 770
theorem OAI.Thomason.Construction.simplexDoubleLast_naturality line 788
theorem OAI.Thomason.Construction.simplexDoubleHomotopy_naturality line 793
theorem OAI.Thomason.Construction.lastVertex_standard_formula line 804
theorem OAI.Thomason.Construction.simplexDoubleFirst_conjugate line 811
theorem OAI.Thomason.Construction.simplexDoubleLast_conjugate line 823

def OAI.Thomason.Construction.standardDoubleHomotopy line 835

Source documentation

The comparison on the double subdivision of a standard simplex.

def standardDoubleHomotopy (n : SimplexCategory) :
    SSet.Homotopy (SSet.sd.map (lastVertex.app (SSet.stdSimplex.obj n)))
      (lastVertex.app (SSet.sd.obj (SSet.stdSimplex.obj n))) where
…

theorem OAI.Thomason.Construction.standardDoubleHomotopy_naturality line 863

def OAI.Thomason.Construction.doubleLastVertexPiece line 888

Source documentation

The compatible comparison prism attached to each original simplex.

def doubleLastVertexPiece (K : SSet.{0}) (j : CostructuredArrow SSet.stdSimplex K) :
    SSet.sd.obj (SSet.sd.obj (SSet.stdSimplex.obj j.left)) ⊗ Δ[1] ⟶ SSet.sd.obj K :=
…

theorem OAI.Thomason.Construction.doubleLastVertexPiece_naturality line 892
def OAI.Thomason.Construction.subdivisionLastVertexHomotopy line 902
Source documentation
The two canonical last-vertex maps from double subdivision are actually simplicially homotopic, for every small simplicial set.
```
def subdivisionLastVertexHomotopy (K : SSet.{0}) :
    SSet.Homotopy (SSet.sd.map (lastVertex.app K))
      (lastVertex.app (SSet.sd.obj K)) := by
…
```
theorem OAI.Thomason.Construction.canonicalExtension_weak line 938
Source documentation
The actual Goerss--Jardine canonical extension map is weak on every small simplicial set, for the geometric-realization weak equivalences.
```
theorem canonicalExtension_weak (K : SSet.{0}) :
    realizationWeakEquivalences (canonicalExtension.app K) :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.extension_realization_weak_iff line 956
Source documentation
Extension preserves and reflects the weak equivalences of actual geometric realizations, using the weak canonical coaugmentation.
```
theorem extension_realization_weak_iff {X Y : SSet.{0}} (f : X ⟶ Y) :
    realizationWeakEquivalences (SSet.ex.map f) ↔ realizationWeakEquivalences f :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.extension_twice_realization_weak_iff line 962
Source documentation
Both extension stages in the Thomason right adjoint preserve and reflect the actual geometric weak-equivalence test.
```
theorem extension_twice_realization_weak_iff {X Y : SSet.{0}} (f : X ⟶ Y) :
    realizationWeakEquivalences ((SSet.ex ⋙ SSet.ex).map f) ↔
      realizationWeakEquivalences f :=
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
def OAI.Thomason.Construction.constructedExtensionLocalizer line 969
Source documentation
The extension functor on the actual realization localizer uses no model-category input.
```
noncomputable def constructedExtensionLocalizer :
    LocalizerMorphism realizationWeakEquivalences realizationWeakEquivalences where
…
```
Mentions: OAI.Thomason.Construction.realizationWeakEquivalences
theorem OAI.Thomason.Construction.constructedExtensionLocalizer_isLocalizedEquivalence line 978
Source documentation
The coaugmentation constructs the inverse of extension after localization, without assuming Kan--Quillen or Street localization.
```
theorem constructedExtensionLocalizer_isLocalizedEquivalence :
    constructedExtensionLocalizer.IsLocalizedEquivalence := by
…
```