Faces of the standard simplex

Complements to Mathlib's Convexity.StdSimplex about the maps StdSimplex.map f. An arbitrary map adds weights over its fibres. An injective map embeds a standard simplex as a face of a larger one and keeps the weights of a point, so it is injective; a point supported on its range comes from the smaller simplex (StdSimplex.comap). For f = j.succAbove its image is the facet on which the j-th weight vanishes; for the last vertex this facet is the smaller simplex with a zero last weight appended. A function taking a constant value on every facet takes that value wherever some weight vanishes. Two facets, opposite j < k, meet in the codimension-two face opposite both: a common point of the two facets comes from that face through both composites of face maps, the two sides of the simplicial identity SimplexCategory.δ_comp_δ.

The prefix sums TauCeti.prefixSum N x.weights of the weights of a point x of StdSimplex R (Fin n) lie between 0 and 1.

theorem Convexity.StdSimplex.ext_fin_three {R : Type u_1} [LE R] [AddCommMonoid R] [One R] {x y : StdSimplex R (Fin 3)} (h0 : x.weights 0 = y.weights 0) (h1 : x.weights 1 = y.weights 1) (h2 : x.weights 2 = y.weights 2) : x = y

A point of the triangle StdSimplex R (Fin 3) is determined by its three weights.

@[simp]

theorem Convexity.StdSimplex.total_fin_three {R : Type u_1} [LE R] [AddCommMonoid R] [One R] (x : StdSimplex R (Fin 3)) : x.weights 0 + x.weights 1 + x.weights 2 = 1

The three weights of a point of the standard 2-simplex add up to 1.

theorem Convexity.StdSimplex.weights_one_add_weights_two_le_one {R : Type u_1} [LE R] [AddCommMonoid R] [One R] [AddRightMono R] (x : StdSimplex R (Fin 3)) : x.weights 1 + x.weights 2 ≤ 1

The weights of the last two vertices of a point of the standard 2-simplex add up to at most 1.

theorem Convexity.StdSimplex.weights_map_apply {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Fintype X] [DecidableEq Y] (f : X → Y) (x : StdSimplex R X) (y : Y) : (map f x).weights y = ∑ i : X with f i = y, x.weights i

Mapping a standard simplex adds the weights over each fibre of the map.

theorem Convexity.StdSimplex.weights_map_apply_of_injective {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {f : X → Y} (hf : Function.Injective f) (x : StdSimplex R X) (a : X) : (map f x).weights (f a) = x.weights a

Along an injective map, the weight at the image of a point is the weight at that point.

theorem Convexity.StdSimplex.map_injective {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {f : X → Y} (hf : Function.Injective f) : Function.Injective (map f)

The map of standard simplices along an injective map is injective.

theorem Convexity.StdSimplex.sum_filter_weights_map {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] (f : X → Y) (x : StdSimplex R X) (P : Y → Prop) [DecidablePred P] : ∑ y : Y with P y, (map f x).weights y = ∑ a : X with P (f a), x.weights a

Sums of the weights of a mapped standard simplex over a set are sums of the weights over its preimage.

noncomputable def Convexity.StdSimplex.comap {R : Type u_1} [PartialOrder R] [Semiring R] {X : Type u_2} {Y : Type u_3} {f : X → Y} (hf : Function.Injective f) (y : StdSimplex R Y) (h : ↑y.support ⊆ Set.range f) : StdSimplex R X

A point of StdSimplex R Y whose weights are supported on the range of an injective map f : X → Y, pulled back to StdSimplex R X: a right inverse of StdSimplex.map f on its range (StdSimplex.map_comap), and a left inverse of it (StdSimplex.comap_map).

theorem Convexity.StdSimplex.weights_comap {R : Type u_1} [PartialOrder R] [Semiring R] {X : Type u_2} {Y : Type u_3} {f : X → Y} (hf : Function.Injective f) (y : StdSimplex R Y) (h : ↑y.support ⊆ Set.range f) : (comap hf y h).weights = Finsupp.comapDomain f y.weights ⋯

The weights of a pulled back point are the pulled back weights.

@[simp]

theorem Convexity.StdSimplex.weights_comap_apply {R : Type u_1} [PartialOrder R] [Semiring R] {X : Type u_2} {Y : Type u_3} {f : X → Y} (hf : Function.Injective f) (y : StdSimplex R Y) (h : ↑y.support ⊆ Set.range f) (a : X) : (comap hf y h).weights a = y.weights (f a)

The weight of a pulled back point at a is the weight of the point at f a.

@[simp]

theorem Convexity.StdSimplex.map_comap {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {f : X → Y} (hf : Function.Injective f) (y : StdSimplex R Y) (h : ↑y.support ⊆ Set.range f) : map f (comap hf y h) = y

Pulling back a point along an injective map whose range contains its support, and then mapping forward again, recovers the point.

@[simp]

theorem Convexity.StdSimplex.comap_map {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {f : X → Y} (hf : Function.Injective f) (x : StdSimplex R X) (h : ↑(map f x).support ⊆ Set.range f) : comap hf (map f x) h = x

Mapping a point forward along an injective map and pulling it back again recovers the point.

theorem Convexity.StdSimplex.mem_range_map_succAbove_iff {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {n : ℕ} (j : Fin (n + 1)) (x : StdSimplex R (Fin (n + 1))) : x ∈ Set.range (map j.succAbove) ↔ x.weights j = 0

A point of a standard simplex lies on the facet opposite j exactly when its j-th weight vanishes.

theorem Convexity.StdSimplex.weights_map_succAbove_self {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {n : ℕ} (j : Fin (n + 1)) (x : StdSimplex R (Fin n)) : (map j.succAbove x).weights j = 0

The j-th weight vanishes on the facet opposite j.

theorem Convexity.StdSimplex.weights_map_succAbove_of_eq {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {n : ℕ} {j k : Fin (n + 1)} {i : Fin n} (h : j.succAbove i = k) (x : StdSimplex R (Fin n)) : (map j.succAbove x).weights k = x.weights i

On the facet opposite j, the weight at j.succAbove i is the i-th weight of the facet.

theorem Convexity.StdSimplex.range_snoc_weights_zero {R : Type u_1} [PartialOrder R] [Semiring R] (n : ℕ) : (Set.range fun (s : StdSimplex R (Fin n)) => Fin.snoc (⇑s.weights) 0) = {y : Fin (n + 1) → R | (y ∈ Set.range fun (s : StdSimplex R (Fin (n + 1))) => ⇑s.weights) ∧ y (Fin.last n) = 0}

The facet of the standard simplex on Fin (n + 1) opposite its last vertex, the points with vanishing last weight, is the standard simplex on Fin n with a zero last weight appended.

theorem Convexity.StdSimplex.apply_eq_of_weights_eq_zero {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {n : ℕ} {Z : Type u_4} {φ : StdSimplex R (Fin (n + 1)) → Z} {z : Z} (hφ : ∀ (i : Fin (n + 1)) (w : StdSimplex R (Fin n)), φ (map i.succAbove w) = z) {b : StdSimplex R (Fin (n + 1))} {k : Fin (n + 1)} (hb : b.weights k = 0) : φ b = z

A function on a standard simplex which takes the value z on every facet takes the value z at every point with a vanishing weight.

theorem Convexity.StdSimplex.exists_map_succAbove_of_map_succAbove_eq {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {n : ℕ} {j k : Fin (n + 2)} (hjk : j < k) {y z : StdSimplex R (Fin (n + 1))} (h : map j.succAbove y = map k.succAbove z) : ∃ (w : StdSimplex R (Fin n)), y = map (k.pred ⋯).succAbove w ∧ z = map (j.castPred ⋯).succAbove w

The facets of a standard simplex opposite j < k meet in the codimension-two face opposite both: a common point is the image of a point w of that face, and the corresponding points of the two facets are the images of w under the face maps given by the simplicial identity.

theorem Convexity.StdSimplex.prefixSum_weights_nonneg {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {n : ℕ} (x : StdSimplex R (Fin n)) (N : ℕ) : 0 ≤ TauCeti.prefixSum N ⇑x.weights

The prefix sums of the weights of a point of a standard simplex on Fin n are nonnegative.

theorem Convexity.StdSimplex.prefixSum_weights_le_one {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {n : ℕ} (x : StdSimplex R (Fin n)) (N : ℕ) : TauCeti.prefixSum N ⇑x.weights ≤ 1

The prefix sums of the weights of a point of a standard simplex on Fin n are at most 1.