Simplex.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Affine simplex chains, mesh geometry, and universal subdivision.

instance OAI.Kaplansky.simplexMetricSpace line 15

def OAI.Kaplansky.simplexCombination line 21

Source documentation

Affine interpolation of vertices in an actual standard simplex.

def simplexCombination {ι κ : Type} [Fintype ι] [Fintype κ]
    (v : ι → StdSimplex ℝ κ) (t : StdSimplex ℝ ι) : StdSimplex ℝ κ :=
…

theorem OAI.Kaplansky.simplexCombination_coe line 26

def OAI.Kaplansky.simplexCombinationMap line 35

Source documentation

Interpolation is continuous in the barycentric coordinates.

def simplexCombinationMap {ι κ : Type} [Fintype ι] [Fintype κ]
    (v : ι → StdSimplex ℝ κ) : C(StdSimplex ℝ ι, StdSimplex ℝ κ) :=
…

theorem OAI.Kaplansky.simplexCombination_vertex line 46
theorem OAI.Kaplansky.simplexCombination_vertices line 52

theorem OAI.Kaplansky.simplexCombination_reindex line 58

Source documentation

Interpolation intertwines vertex reindexing with the genuine standard-simplex map, including all cofaces.

theorem simplexCombination_reindex {ι κ μ : Type} [Fintype ι] [Fintype κ] [Fintype μ]
    (v : κ → StdSimplex ℝ μ) (f : ι → κ) (t : StdSimplex ℝ ι) :
    simplexCombination (v ∘ f) t = simplexCombination v (StdSimplex.map f t) := by
…

Mentions: OAI.Kaplansky.simplexCombination

theorem OAI.Kaplansky.simplexCombination_map line 64

Source documentation

Affine maps of the target simplex commute with interpolation.

theorem simplexCombination_map {ι κ μ : Type} [Fintype ι] [Fintype κ] [Fintype μ]
    (v : ι → StdSimplex ℝ κ) (f : κ → μ) (t : StdSimplex ℝ ι) :
    StdSimplex.map f (simplexCombination v t) =
      simplexCombination (StdSimplex.map f ∘ v) t := by
…

Mentions: OAI.Kaplansky.simplexCombination

def OAI.Kaplansky.simplexTupleCenter line 71

Source documentation

Barycenter of a tuple in the ambient standard simplex.

def simplexTupleCenter {κ : Type} [Fintype κ] (n : ℕ)
    (v : Fin (n+2) → StdSimplex ℝ κ) : StdSimplex ℝ κ :=
…

theorem OAI.Kaplansky.simplexTupleCenter_map line 76

theorem OAI.Kaplansky.simplexCombination_dist_le line 83

Source documentation

A convex combination stays within any common distance bound from a point.

theorem simplexCombination_dist_le {ι κ : Type} [Fintype ι] [Fintype κ]
    (v : ι → StdSimplex ℝ κ) (t : StdSimplex ℝ ι) (p : StdSimplex ℝ κ)
    (D : ℝ) (hv : ∀ i, dist (v i) p ≤ D) :
    dist (simplexCombination v t) p ≤ D := by
…

Mentions: OAI.Kaplansky.simplexCombination

theorem OAI.Kaplansky.simplexCombination_pair_dist_le line 106

Source documentation

Affine interpolation cannot increase a bound on pairwise vertex distances.

theorem simplexCombination_pair_dist_le {ι κ : Type} [Fintype ι] [Fintype κ]
    (v : ι → StdSimplex ℝ κ) (s t : StdSimplex ℝ ι)
    (D : ℝ) (hv : ∀ i j, dist (v i) (v j) ≤ D) :
    dist (simplexCombination v s) (simplexCombination v t) ≤ D := by
…

Mentions: OAI.Kaplansky.simplexCombination

theorem OAI.Kaplansky.simplexTupleCenter_vertex_dist_le line 117

Source documentation

Averaging N vertices has distance at most (N-1)/N times the original mesh from every vertex. This includes repeated vertices.

theorem simplexTupleCenter_vertex_dist_le {κ : Type} [Fintype κ]
    (n : ℕ) (v : Fin (n+2) → StdSimplex ℝ κ) (D : ℝ)
    (hv : ∀ i j, dist (v i) (v j) ≤ D) (j : Fin (n+2)) :
    dist (simplexTupleCenter n v) (v j) ≤ ((n+1 : ℝ) / (n+2)) * D := by
…

Mentions: OAI.Kaplansky.simplexTupleCenter

theorem OAI.Kaplansky.simplexTupleCenter_combination_dist_le line 157

Source documentation

Every point of the old affine simplex is close to its barycenter with the strict dimension-dependent contraction factor.

theorem simplexTupleCenter_combination_dist_le {κ : Type} [Fintype κ]
    (n : ℕ) (v : Fin (n+2) → StdSimplex ℝ κ) (t : StdSimplex ℝ (Fin (n+2)))
    (D : ℝ) (hv : ∀ i j, dist (v i) (v j) ≤ D) :
    dist (simplexTupleCenter n v) (simplexCombination v t) ≤ ((n+1 : ℝ) / (n+2)) * D := by
…

Mentions: OAI.Kaplansky.simplexTupleCenter, OAI.Kaplansky.simplexCombination

abbrev OAI.Kaplansky.standardSimplexSpace line 166

def OAI.Kaplansky.singularSimplexOfMap line 170

Source documentation

A continuous simplex as an element of the library singular set.

def singularSimplexOfMap {X : TopCat.{0}} {n : ℕ}
    (f : C(StdSimplex ℝ (Fin (n+1)), X)) : (TopCat.toSSet.obj X) _⦋n⦌ :=
…

abbrev OAI.Kaplansky.singularGen line 174

theorem OAI.Kaplansky.singularChains_hom_ext line 179

Source documentation

Maps from singular chains are determined by their values on singular simplices.

theorem singularChains_hom_ext {X : TopCat.{0}} {n : ℕ} {T : ModuleCat.{0} ℤ}
    {f g : (integralSingularChains.obj X).X n ⟶ T}
    (h : ∀ σ : (TopCat.toSSet.obj X) _⦋n⦌, singularGen σ ≫ f = singularGen σ ≫ g) :
    f = g := SSet.chainComplex_hom_ext h

Mentions: OAI.Kaplansky.singularGen

def OAI.Kaplansky.simplexAffineSSet line 185
Source documentation
Interpolation into actual singular simplices, in every degree.
```
def simplexAffineSSet (k : ℕ) :
    tupleSSet (StdSimplex ℝ (Fin (k+1))) ⟶ TopCat.toSSet.obj (standardSimplexSpace k) where
…
```
Mentions: OAI.Kaplansky.tupleSSet, OAI.Kaplansky.standardSimplexSpace
abbrev OAI.Kaplansky.simplexAffineChains line 198
theorem OAI.Kaplansky.tupleGen_affine line 204
def OAI.Kaplansky.standardSimplexMap line 210
theorem OAI.Kaplansky.simplexAffineSSet_naturality line 215
Source documentation
Interpolation is natural in affine maps of ambient simplex coordinates.
```
theorem simplexAffineSSet_naturality {k l : ℕ} (f : Fin (k+1) → Fin (l+1)) :
    tupleSSetMap (StdSimplex.map f) ≫ simplexAffineSSet l =
      simplexAffineSSet k ≫ TopCat.toSSet.map (standardSimplexMap f) := by
…
```
Mentions: OAI.Kaplansky.tupleSSetMap, OAI.Kaplansky.simplexAffineSSet, OAI.Kaplansky.standardSimplexMap
theorem OAI.Kaplansky.simplexAffineChains_naturality line 230
theorem OAI.Kaplansky.tupleGen_vertices_affine line 239
Source documentation
The identity simplex is the interpolation of its actual vertices.
```
theorem tupleGen_vertices_affine (n : ℕ) :
    tupleGen (StdSimplex.single (R := ℝ) (X := Fin (n+1))) ≫ (simplexAffineChains n).f n =
…
```
Mentions: OAI.Kaplansky.tupleGen, OAI.Kaplansky.simplexAffineChains
def OAI.Kaplansky.simplexSubdivisionChains line 254
Source documentation
Barycentric subdivision followed by actual affine singular interpolation.
```
def simplexSubdivisionChains (k : ℕ) :
    tupleChains (StdSimplex ℝ (Fin (k+1))) ⟶
      integralSingularChains.obj (standardSimplexSpace k) :=
…
```
Mentions: OAI.Kaplansky.tupleChains, OAI.Kaplansky.standardSimplexSpace
def OAI.Kaplansky.simplexSubdivisionPrism line 260
Source documentation
The corresponding interpolated chain homotopy components.
```
def simplexSubdivisionPrism (k n : ℕ) :
    (tupleChains (StdSimplex ℝ (Fin (k+1)))).X n ⟶
      (integralSingularChains.obj (standardSimplexSpace k)).X (n+1) :=
…
```
Mentions: OAI.Kaplansky.tupleChains, OAI.Kaplansky.standardSimplexSpace
theorem OAI.Kaplansky.simplexSubdivisionChains_naturality line 266
theorem OAI.Kaplansky.simplexSubdivisionPrism_naturality line 281
def OAI.Kaplansky.universalSubdivision line 292
Source documentation
The subdivided universal identity simplex, as a chain in that same simplex.
```
def universalSubdivision (n : ℕ) : ModuleCat.of ℤ ℤ ⟶
    (integralSingularChains.obj (standardSimplexSpace n)).X n :=
…
```
Mentions: OAI.Kaplansky.standardSimplexSpace
def OAI.Kaplansky.universalSubdivisionPrism line 296
theorem OAI.Kaplansky.universalSubdivision_boundary line 301
theorem OAI.Kaplansky.universalSubdivision_zero line 321
theorem OAI.Kaplansky.universalSubdivisionPrism_zero line 327

theorem OAI.Kaplansky.universalSubdivisionPrism_boundary line 333

Source documentation

The boundary of the universal prism includes the lower-dimensional prisms on every oriented face.

theorem universalSubdivisionPrism_boundary (n : ℕ) :
    universalSubdivisionPrism (n+1) ≫
      (integralSingularChains.obj (standardSimplexSpace (n+1))).d (n+2) (n+1) =
      singularGen (singularSimplexOfMap (ContinuousMap.id _)) - universalSubdivision (n+1) -
      ∑ i : Fin (n+2), (-1 : ℤ)^i.val •
        (universalSubdivisionPrism n ≫
          (integralSingularChains.map (standardSimplexMap i.succAbove)).f (n+1)) := by
…

Mentions: OAI.Kaplansky.universalSubdivisionPrism, OAI.Kaplansky.standardSimplexSpace, OAI.Kaplansky.singularGen, OAI.Kaplansky.singularSimplexOfMap, OAI.Kaplansky.universalSubdivision, OAI.Kaplansky.standardSimplexMap