The topology on the standard simplex

In this file, we define a topology on the standard simplex StdSimplex R M. When M is finite, this is the topology that is induced by the embedding StdSimplex R M → (M → R). In general, we use the supremum of the coinduced topologies for the maps StdSimplex.map f : StdSimplex R ι → StdSimplex R M where f : ι → M is a map from a finite set ι.

@[instance_reducible]

noncomputable instance Convexity.StdSimplex.topologicalSpace (R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] (M : Type v) : TopologicalSpace (StdSimplex R M)

This is the topology on StdSimplex R M when M is a possibly infinite type. The lemma StdSimplex.continuous_iff shows that this topology is characterized by the fact that a map f from StdSimplex R M is continuous iff for any map g : ι → M with a finite ι, the composition f ∘ map g : StdSimplex R ι → _ is continuous, where StdSimplex R ι is equipped with the topology that is induced by the embedding StdSimplex R ι → (ι → R).

Equations

• Convexity.StdSimplex.topologicalSpace R M = ⨆ (ι : Type ?u.1), ⨆ (_ : Finite ι), ⨆ (f : ι → M), TopologicalSpace.coinduced (Convexity.StdSimplex.map f) inferInstance

theorem Convexity.StdSimplex.continuous_iff {R : Type u} [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] {M : Type v} {T : Type u_1} [TopologicalSpace T] (f : StdSimplex R M → T) : Continuous f ↔ ∀ (ι : Type v) [Finite ι] (g : ι → M), Continuous (f ∘ map g)

theorem Convexity.StdSimplex.continuous_map (R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] {M : Type u_1} {N : Type v} (f : M → N) : Continuous (map f)

theorem Convexity.StdSimplex.continuous_iff' (R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] {M : Type u_1} {T : Type u_2} [TopologicalSpace T] (f : StdSimplex R M → T) : Continuous f ↔ ∀ (s : Finset M), Continuous (f ∘ map Subtype.val)

Same as StdSimplex.continuous_iff but we only consider inclusions of finite subsets of M instead of all maps ι → M for arbitrary finite types ι.

theorem Convexity.StdSimplex.continuous_weights_apply (R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] {M : Type u_1} (m : M) : Continuous fun (t : StdSimplex R M) => t.weights m

theorem Convexity.StdSimplex.isEmbedding_toFun_comp_weights (R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] (M : Type u_1) [Finite M] : Topology.IsEmbedding fun (t : StdSimplex R M) => ⇑t.weights

theorem Convexity.StdSimplex.isClosedEmbedding_toFun_comp_weights (R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] [OrderClosedTopology R] (M : Type u_1) [Finite M] : Topology.IsClosedEmbedding fun (t : StdSimplex R M) => ⇑t.weights