Finite coordinate simplices

The subdivision construction uses a simplex as a subset of a finite coordinate space. The equivalence below identifies these coordinates with Mathlib's finitely supported simplex without changing their pointwise values.

def SphereOddDegree.finiteSimplex (R : Type u_1) (X : Type u_2) [Semiring R] [PartialOrder R] [Fintype X] : Set (X → R)

Nonnegative finite coordinate functions whose coordinates sum to one.

Equations

• SphereOddDegree.finiteSimplex R X = {f : X → R | (∀ (x : X), 0 ≤ f x) ∧ ∑ x : X, f x = 1}

@[instance_reducible]

instance SphereOddDegree.FiniteSimplex.instFunLikeElemForallFiniteSimplex {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] : FunLike (↑(finiteSimplex S X)) X S

Equations

• SphereOddDegree.FiniteSimplex.instFunLikeElemForallFiniteSimplex = { coe := fun (s : ↑(SphereOddDegree.finiteSimplex S X)) => ↑s, coe_injective := ⋯ }

@[simp]

theorem SphereOddDegree.FiniteSimplex.mk_apply {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] (f : X → S) (h : f ∈ finiteSimplex S X) (x : X) : ⟨f, h⟩ x = f x

Applying a coordinate subtype reads its underlying function.

theorem SphereOddDegree.FiniteSimplex.ext {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] {s t : ↑(finiteSimplex S X)} (h : ⇑s = ⇑t) : s = t

Coordinate equality determines a point of the finite simplex.

theorem SphereOddDegree.FiniteSimplex.ext_iff {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] {s t : ↑(finiteSimplex S X)} : s = t ↔ ⇑s = ⇑t

noncomputable def SphereOddDegree.FiniteSimplex.equivalence {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] : ↑(finiteSimplex S X) ≃ Convexity.StdSimplex S X

Conversion to finitely supported weights preserves every coordinate.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SphereOddDegree.FiniteSimplex.equivalence_weights {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] (s : ↑(finiteSimplex S X)) (x : X) : (equivalence s).weights x = s x

The finitely supported representation has the same coordinates.

@[simp]

theorem SphereOddDegree.FiniteSimplex.equivalence_symm_apply {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] (s : Convexity.StdSimplex S X) (x : X) : (equivalence.symm s) x = s.weights x

Returning to finite coordinates reads the original finitely supported weights.

@[simp]

theorem SphereOddDegree.FiniteSimplex.zero_le {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] (s : ↑(finiteSimplex S X)) (x : X) : 0 ≤ s x

Every coordinate of a finite simplex point is nonnegative.

@[simp]

theorem SphereOddDegree.FiniteSimplex.sum_eq_one {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] (s : ↑(finiteSimplex S X)) : ∑ x : X, s x = 1

The coordinates of a finite simplex point sum to one.

instance SphereOddDegree.FiniteSimplex.instSubsingletonElemForallFiniteSimplex {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [Subsingleton X] : Subsingleton ↑(finiteSimplex S X)

theorem SphereOddDegree.FiniteSimplex.le_one {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] (s : ↑(finiteSimplex S X)) (x : X) : s x ≤ 1

Each nonnegative coordinate is bounded by the total mass.

theorem SphereOddDegree.FiniteSimplex.image_linearMap {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] (f : X → Y) : ⇑(FunOnFinite.linearMap S S f) '' finiteSimplex S X ⊆ finiteSimplex S Y

Summing coordinates along fibers preserves nonnegativity and total mass.

noncomputable def SphereOddDegree.FiniteSimplex.map {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] (f : X → Y) (s : ↑(finiteSimplex S X)) : ↑(finiteSimplex S Y)

Push a finite simplex point forward by summing weights over each fiber.

Equations

• SphereOddDegree.FiniteSimplex.map f s = ⟨(FunOnFinite.linearMap S S f) ⇑s, ⋯⟩

@[simp]

theorem SphereOddDegree.FiniteSimplex.map_coe {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] (f : X → Y) (s : ↑(finiteSimplex S X)) : ⇑(map f s) = (FunOnFinite.linearMap S S f) ⇑s

The underlying coordinate function is the finite fiber-sum linear map.

theorem SphereOddDegree.FiniteSimplex.map_comp_apply {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Fintype X] [Fintype Y] [Fintype Z] [IsOrderedRing S] (f : X → Y) (g : Y → Z) (x : ↑(finiteSimplex S X)) : map g (map f x) = map (g ∘ f) x

Pushing weights through two maps agrees with pushing them through their composition.

theorem SphereOddDegree.FiniteSimplex.single_mem {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [DecidableEq X] (x : X) : Pi.single x 1 ∈ finiteSimplex S X

Unit mass at one coordinate lies in the finite simplex.

@[reducible, inline]

abbrev SphereOddDegree.FiniteSimplex.vertex {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [DecidableEq X] (x : X) : ↑(finiteSimplex S X)

The finite simplex vertex carrying unit mass at the chosen coordinate.

Equations

• SphereOddDegree.FiniteSimplex.vertex x = ⟨Pi.single x 1, ⋯⟩

@[simp]

theorem SphereOddDegree.FiniteSimplex.vertex_coe {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [DecidableEq X] (x : X) : ⇑(vertex x) = Pi.single x 1

A vertex has its unit-coordinate function as underlying coordinates.

@[simp]

theorem SphereOddDegree.FiniteSimplex.map_vertex {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] [DecidableEq X] [DecidableEq Y] (f : X → Y) (x : X) : map f (vertex x) = vertex (f x)

A vertex is sent to the vertex indexed by the image coordinate.

theorem SphereOddDegree.FiniteSimplex.continuous_map {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] [TopologicalSpace S] [IsTopologicalSemiring S] (f : X → Y) : Continuous (map f)

Fiber sums give continuous maps between finite coordinate simplices.

def SphereOddDegree.FiniteSimplex.barycenter {𝕜 : Type u_1} {X : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Fintype X] [Nonempty X] : ↑(finiteSimplex 𝕜 X)

The finite simplex point assigning the same mass to every coordinate.

Equations

• SphereOddDegree.FiniteSimplex.barycenter = ⟨fun (x : X) => (↑(Fintype.card X))⁻¹, ⋯⟩

@[simp]

theorem SphereOddDegree.FiniteSimplex.barycenter_apply {𝕜 : Type u_1} {X : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Fintype X] [Nonempty X] (x : X) : ↑barycenter x = (↑(Fintype.card X))⁻¹

Every barycenter coordinate is the reciprocal of the number of vertices.

theorem SphereOddDegree.single_mem_finiteSimplex (S : Type u_1) {X : Type u_2} [Fintype X] [DecidableEq X] [Semiring S] [PartialOrder S] [IsOrderedRing S] (x : X) : Pi.single x 1 ∈ finiteSimplex S X

Unit-coordinate vectors belong to the finite coordinate simplex.

theorem SphereOddDegree.convex_finiteSimplex (S : Type u_1) (X : Type u_2) [Semiring S] [PartialOrder S] [IsOrderedRing S] [Fintype X] : Convex S (finiteSimplex S X)

Convex combinations preserve the nonnegative coordinates and their total mass.

theorem SphereOddDegree.convexHull_range_single_eq_finiteSimplex (R : Type u_1) (X : Type u_2) [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Fintype X] [DecidableEq X] : (convexHull R) (Set.range fun (i : X) => Pi.single i 1) = finiteSimplex R X

The finite coordinate simplex is exactly the convex hull of its unit-coordinate vertices.

theorem SphereOddDegree.isCompact_finiteSimplex (S : Type u_1) (X : Type u_2) [Fintype X] [TopologicalSpace S] [Semiring S] [PartialOrder S] [OrderClosedTopology S] [ContinuousAdd S] [CompactIccSpace S] [IsOrderedRing S] : IsCompact (finiteSimplex S X)

Finite coordinate simplices are compact in an ordered topological semiring.

instance SphereOddDegree.FiniteSimplex.compactSpace (S : Type u_1) (X : Type u_2) [Fintype X] [TopologicalSpace S] [Semiring S] [PartialOrder S] [OrderClosedTopology S] [ContinuousAdd S] [CompactIccSpace S] [IsOrderedRing S] : CompactSpace ↑(finiteSimplex S X)

theorem SphereOddDegree.bounded_finiteSimplex (X : Type u_1) [Fintype X] : Bornology.IsBounded (finiteSimplex ℝ X)

A compact finite coordinate simplex is bounded in real coordinate space.

noncomputable def SphereOddDegree.FiniteSimplex.homeomorphUnitInterval : ↑(finiteSimplex ℝ (Fin 2)) ≃ₜ ↑unitInterval

The one-dimensional finite coordinate simplex is the unit interval.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SphereOddDegree.FiniteSimplex.homeomorphUnitInterval_one : homeomorphUnitInterval (vertex 1) = 1

The last endpoint corresponds to unit mass at coordinate one.

@[simp]

theorem SphereOddDegree.FiniteSimplex.homeomorphUnitInterval_zero : homeomorphUnitInterval (vertex 0) = 0

The first endpoint corresponds to unit mass at coordinate zero.