The full-dimensional standard simplex

The simplex with nonnegative coordinates whose sum is at most one is an integration domain in Euclidean space. Its homeomorphism with Mathlib's barycentric Convexity.StdSimplex adds the zeroth weight, equal to one minus the sum of the coordinates. The face inclusions are transported from Mathlib's maps of barycentric simplices. The bridge reuses AbstractSimplicialComplex.realizationTopHomeomorphCoordinateSimplex and AbstractSimplicialComplex.realizationTopHomeomorphStdSimplex; finRotate moves the omitted last coordinate to the zeroth position. Every map of barycentric simplices induced by a map of vertices, read on full-dimensional simplices, is the restriction of the continuous affine map simplexMapAmbient of the ambient Euclidean spaces; the face inclusions are the case of the coface vertex maps Fin.succAbove. In coordinates, the face map omitting the vertex e_j inserts a zero j-th coordinate, and the face map omitting the origin puts the missing barycentric weight in front; a permutation of the vertices induces an affine symmetry of the simplex. Cycling the vertices relates the two readings of the face opposite the origin: through the coordinates other than the j-th one, and through the last coordinates as the face map does. The simplex is a compact convex set with nonempty interior, so derivatives within it are unique at every point (TauCeti.uniqueDiffOn_fullSimplex); this is what makes it a domain for derivatives and integrals of forms. The face maps are injective, hence closed embeddings of the ambient Euclidean spaces (TauCeti.isClosedEmbedding_simplexMapAmbient_succAbove), so pulling back along them preserves compact supports.

This is the full-dimensional simplex convention used in Lee, Introduction to Smooth Manifolds, Chapter 18. The barycentric simplex, its topology, and its maps are those of Mathlib.

noncomputable def TauCeti.fullSimplex (p : ℕ) : Set (EuclideanSpace ℝ (Fin p))

The full-dimensional standard simplex in Euclidean p-space.

@[simp]

theorem TauCeti.mem_fullSimplex_iff {p : ℕ} {x : EuclideanSpace ℝ (Fin p)} : x ∈ fullSimplex p ↔ (∀ (i : Fin p), 0 ≤ x.ofLp i) ∧ ∑ i : Fin p, x.ofLp i ≤ 1

Membership in the full-dimensional simplex is coordinate nonnegativity and a sum bound.

theorem TauCeti.zero_mem_fullSimplex (p : ℕ) : 0 ∈ fullSimplex p

The origin is the zeroth vertex of the full-dimensional simplex.

theorem TauCeti.convex_fullSimplex (p : ℕ) : Convex ℝ (fullSimplex p)

The full-dimensional simplex is convex.

theorem TauCeti.isClosed_fullSimplex (p : ℕ) : IsClosed (fullSimplex p)

The full-dimensional simplex is closed.

theorem TauCeti.isCompact_fullSimplex (p : ℕ) : IsCompact (fullSimplex p)

The full-dimensional simplex is compact.

theorem TauCeti.nonempty_interior_fullSimplex (p : ℕ) : (interior (fullSimplex p)).Nonempty

The full-dimensional simplex has nonempty interior in its Euclidean space.

theorem TauCeti.closure_interior_fullSimplex (p : ℕ) : closure (interior (fullSimplex p)) = fullSimplex p

The full-dimensional simplex is the closure of its interior.

theorem TauCeti.uniqueDiffOn_fullSimplex (p : ℕ) : UniqueDiffOn ℝ (fullSimplex p)

Derivatives within the full-dimensional simplex are unique at each of its points, including the points of its faces and corners.

theorem TauCeti.toLp_insertNth_mem_fullSimplex_iff {p : ℕ} (j : Fin (p + 1)) (t : ℝ) (y : Fin p → ℝ) : WithLp.toLp 2 (j.insertNth t y) ∈ fullSimplex (p + 1) ↔ y ∈ coordinateSimplex (Fin p) ∧ t ∈ Set.Icc 0 (1 - ∑ k : Fin p, y k)

The point of ℝᵖ⁺¹ obtained by inserting t as the j-th coordinate of y lies in the full-dimensional simplex exactly when y lies in the coordinate simplex and t lies between 0 and the unused part 1 - ∑ k, y k of the coordinate sum.

noncomputable def TauCeti.fullSimplexEquivStdSimplex (p : ℕ) : ↑(fullSimplex p) ≃ₜ Convexity.StdSimplex ℝ (Fin (p + 1))

Adding the missing zeroth weight identifies the full-dimensional and barycentric simplices.

@[simp]

theorem TauCeti.fullSimplexEquivStdSimplex_weights_succ {p : ℕ} (x : ↑(fullSimplex p)) (i : Fin p) : ((fullSimplexEquivStdSimplex p) x).weights i.succ = (↑x).ofLp i

The positive-index weights are precisely the original Euclidean coordinates.

@[simp]

theorem TauCeti.fullSimplexEquivStdSimplex_weights_zero {p : ℕ} (x : ↑(fullSimplex p)) : ((fullSimplexEquivStdSimplex p) x).weights 0 = 1 - ∑ i : Fin p, (↑x).ofLp i

The zeroth weight is the unused part of the coordinate sum.

@[simp]

theorem TauCeti.fullSimplexEquivStdSimplex_symm_apply {p : ℕ} (w : Convexity.StdSimplex ℝ (Fin (p + 1))) (i : Fin p) : (↑((fullSimplexEquivStdSimplex p).symm w)).ofLp i = w.weights i.succ

The inverse bridge forgets the zeroth barycentric coordinate.

noncomputable def TauCeti.simplexFace (p : ℕ) (i : Fin (p + 2)) : ↑(fullSimplex p) → ↑(fullSimplex (p + 1))

The i-th face inclusion, obtained by inserting a zero barycentric weight at i.

theorem TauCeti.fullSimplexEquivStdSimplex_simplexFace {p : ℕ} (i : Fin (p + 2)) (x : ↑(fullSimplex p)) : (fullSimplexEquivStdSimplex (p + 1)) (simplexFace p i x) = Convexity.StdSimplex.map i.succAbove ((fullSimplexEquivStdSimplex p) x)

The bridge intertwines a face inclusion with the barycentric coface map.

@[simp]

theorem TauCeti.fullSimplexEquivStdSimplex_simplexFace_succAbove {p : ℕ} (i : Fin (p + 2)) (x : ↑(fullSimplex p)) (j : Fin (p + 1)) : ((fullSimplexEquivStdSimplex (p + 1)) (simplexFace p i x)).weights (i.succAbove j) = ((fullSimplexEquivStdSimplex p) x).weights j

The face inclusion preserves the weights away from its missing vertex.

@[simp]

theorem TauCeti.fullSimplexEquivStdSimplex_simplexFace_self {p : ℕ} (i : Fin (p + 2)) (x : ↑(fullSimplex p)) : ((fullSimplexEquivStdSimplex (p + 1)) (simplexFace p i x)).weights i = 0

The weight at the missing vertex of a face is zero.

theorem TauCeti.continuous_simplexFace (p : ℕ) (i : Fin (p + 2)) : Continuous (simplexFace p i)

Every face inclusion is continuous in the full-dimensional topology.

noncomputable def TauCeti.simplexMapAmbient {m n : ℕ} (f : Fin (m + 1) → Fin (n + 1)) : EuclideanSpace ℝ (Fin m) →ᴬ[ℝ] EuclideanSpace ℝ (Fin n)

The affine extension to the whole Euclidean ambient space of the map of full-dimensional simplices induced by a map of vertices f. It extends the barycentric weights affinely, pushes them forward along f with FunOnFinite.linearMap, and then drops the zeroth coordinate.

theorem TauCeti.simplexMapAmbient_apply {m n : ℕ} (f : Fin (m + 1) → Fin (n + 1)) (x : EuclideanSpace ℝ (Fin m)) (j : Fin n) : ((simplexMapAmbient f) x).ofLp j = ∑ i : Fin (m + 1) with f i = j.succ, Fin.cons (1 - ∑ k : Fin m, x.ofLp k) (fun (k : Fin m) => x.ofLp k) i

Each coordinate of the ambient extension is the sum of the affinely extended barycentric weights over the vertices sent to the corresponding vertex.

theorem TauCeti.simplexMapAmbient_coe {m n : ℕ} (f : Fin (m + 1) → Fin (n + 1)) (x : ↑(fullSimplex m)) : (simplexMapAmbient f) ↑x = ↑((fullSimplexEquivStdSimplex n).symm (Convexity.StdSimplex.map f ((fullSimplexEquivStdSimplex m) x)))

The affine ambient extension restricts to the map of full-dimensional simplices induced by f.

theorem TauCeti.simplexMapAmbient_succAbove_coe {p : ℕ} (i : Fin (p + 2)) (x : ↑(fullSimplex p)) : (simplexMapAmbient i.succAbove) ↑x = ↑(simplexFace p i x)

The ambient extension of the i-th coface vertex map restricts to the face inclusion.

theorem TauCeti.mapsTo_simplexMapAmbient {m n : ℕ} (f : Fin (m + 1) → Fin (n + 1)) : Set.MapsTo (⇑(simplexMapAmbient f)) (fullSimplex m) (fullSimplex n)

The ambient extension of a vertex map carries the full-dimensional simplex into the full-dimensional simplex.

theorem TauCeti.simplexMapAmbient_apply_of_injective {m n : ℕ} {f : Fin (m + 1) → Fin (n + 1)} (hf : Function.Injective f) (x : EuclideanSpace ℝ (Fin m)) {i : Fin (m + 1)} {j : Fin n} (h : f i = j.succ) : ((simplexMapAmbient f) x).ofLp j = Fin.cons (1 - ∑ k : Fin m, x.ofLp k) (fun (k : Fin m) => x.ofLp k) i

For an injective vertex map f, a coordinate of the ambient extension is the affinely extended barycentric weight of the unique vertex sent to the corresponding vertex.

theorem TauCeti.simplexMapAmbient_apply_of_forall_ne {m n : ℕ} {f : Fin (m + 1) → Fin (n + 1)} (x : EuclideanSpace ℝ (Fin m)) {j : Fin n} (h : ∀ (i : Fin (m + 1)), f i ≠ j.succ) : ((simplexMapAmbient f) x).ofLp j = 0

A coordinate of the ambient extension whose vertex is not in the range of the vertex map vanishes.

theorem TauCeti.image_simplexMapAmbient_perm {m : ℕ} (σ : Equiv.Perm (Fin (m + 1))) : ⇑(simplexMapAmbient ⇑σ) '' fullSimplex m = fullSimplex m

The ambient extension of a permutation of the vertices maps the full-dimensional simplex onto itself.

The faces in coordinates

theorem TauCeti.simplexMapAmbient_succAbove_succ {p : ℕ} (j : Fin (p + 1)) (y : EuclideanSpace ℝ (Fin p)) : (simplexMapAmbient j.succ.succAbove) y = WithLp.toLp 2 (j.insertNth 0 y.ofLp)

The face map of Δᵖ⁺¹ omitting the vertex e_j inserts a zero j-th coordinate.

theorem TauCeti.simplexMapAmbient_succAbove_zero {p : ℕ} (y : EuclideanSpace ℝ (Fin p)) : (simplexMapAmbient (Fin.succAbove 0)) y = WithLp.toLp 2 (Fin.cons (1 - ∑ k : Fin p, y.ofLp k) y.ofLp)

The face map of Δᵖ⁺¹ omitting the origin keeps the coordinates of y as the last p coordinates and puts the missing barycentric weight 1 - ∑ k, y k in front.

theorem TauCeti.simplexMapAmbient_cycleRange_symm {p : ℕ} (j : Fin (p + 1)) (y : EuclideanSpace ℝ (Fin p)) : (simplexMapAmbient ⇑(Equiv.symm j.cycleRange)) y = WithLp.toLp 2 fun (k : Fin p) => j.insertNth (1 - ∑ k : Fin p, y.ofLp k) y.ofLp k.succ

The affine symmetry of Δᵖ cycling the vertices 0, …, j reads the face of Δᵖ⁺¹ opposite the origin in the coordinates obtained by deleting the j-th one.

theorem TauCeti.toLp_insertNth_eq_simplexMapAmbient {p : ℕ} (j : Fin (p + 1)) (y : EuclideanSpace ℝ (Fin p)) : WithLp.toLp 2 (j.insertNth (1 - ∑ k : Fin p, y.ofLp k) y.ofLp) = (simplexMapAmbient (Fin.succAbove 0)) ((simplexMapAmbient ⇑(Equiv.symm j.cycleRange)) y)

The point of the face of Δᵖ⁺¹ opposite the origin whose coordinates other than the j-th are those of y is the image under the face map of the cycled point of Δᵖ.

theorem TauCeti.contLinear_simplexMapAmbient_succAbove_succ {p : ℕ} (j : Fin (p + 1)) (k : Fin p) : (simplexMapAmbient j.succ.succAbove).contLinear (EuclideanSpace.single k 1) = EuclideanSpace.single (j.succAbove k) 1

The linear part of the face map omitting the vertex e_j sends e_k to e_{j.succAbove k}.

theorem TauCeti.contLinear_simplexMapAmbient_succAbove_zero {p : ℕ} (k : Fin p) : (simplexMapAmbient (Fin.succAbove 0)).contLinear (EuclideanSpace.single k 1) = EuclideanSpace.single k.succ 1 - EuclideanSpace.single 0 1

The linear part of the face map omitting the origin sends e_k to the edge vector e_{k+1} - e_0.

theorem TauCeti.simplexMapAmbient_succAbove_injective {p : ℕ} (i : Fin (p + 2)) : Function.Injective ⇑(simplexMapAmbient i.succAbove)

The face maps of Δᵖ⁺¹ are injective.

theorem TauCeti.isClosedEmbedding_simplexMapAmbient_succAbove {p : ℕ} (i : Fin (p + 2)) : Topology.IsClosedEmbedding ⇑(simplexMapAmbient i.succAbove)

The face maps of Δᵖ⁺¹ are closed embeddings, so preimages of compact sets under them are compact.

theorem TauCeti.isCompact_inter_preimage_simplexMapAmbient_succAbove {p : ℕ} (i : Fin (p + 2)) {K : Set (EuclideanSpace ℝ (Fin (p + 1)))} (hK : IsCompact K) : IsCompact (↑⊤ ∩ ⇑(simplexMapAmbient i.succAbove) ⁻¹' K)

Preimages of compact sets under the face maps of Δᵖ⁺¹ are compact, so the face maps are proper from all of ℝᵖ and pull test forms back to test forms.