Documentation

Mathlib.Geometry.Convex.ConvexSpace.AffineMapCone

The cone of an affine map from the standard simplex #

Given an affine map s : StdSimplex R (Fin n) → Y and y : Y, we define an affine map s.cone : StdSimplex R (Fin (n + 1)) → Y which sends the vertex 0 to y and the vertex i.succ to the image by s of the ith vertex of the standard simplex.

source
noncomputable def Convexity.ConvexSpace.AffineMap.cone {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {Y : Type u_2} [ConvexSpace R Y] {n : ℕ} (s : ConvexSpace.AffineMap R (StdSimplex R (Fin n)) Y) (y : Y) :
ConvexSpace.AffineMap R (StdSimplex R (Fin (n + 1))) Y

The cone of an affine map from the standard simplex. If s is an affine map StdSimplex R (Fin n) → Y and y : Y, then s.cone y is the affine map StdSimplex R (Fin (n + 1)) → Y which sends the vertex 0 to y and the vertex i.succ to the image by s of the ith vertex of the standard simplex.

Equations
Instances For
    source
    theorem Convexity.ConvexSpace.AffineMap.cone_def {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {Y : Type u_2} [ConvexSpace R Y] {n : ℕ} (s : ConvexSpace.AffineMap R (StdSimplex R (Fin n)) Y) (y : Y) :
    s.cone y = StdSimplex.affineMapMk fun (i : Fin (n + 1)) => Fin.cases y (fun (i : Fin n) => s (StdSimplex.single i)) i
    source
    @[simp]
    theorem Convexity.ConvexSpace.AffineMap.cone_single_zero {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {Y : Type u_2} [ConvexSpace R Y] {n : ℕ} (s : ConvexSpace.AffineMap R (StdSimplex R (Fin n)) Y) (y : Y) :
    (s.cone y) (StdSimplex.single 0) = y
    source
    @[simp]
    theorem Convexity.ConvexSpace.AffineMap.cone_single_succ {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {Y : Type u_2} [ConvexSpace R Y] {n : ℕ} (s : ConvexSpace.AffineMap R (StdSimplex R (Fin n)) Y) (y : Y) (j : Fin n) :
    (s.cone y) (StdSimplex.single j.succ) = s (StdSimplex.single j)
    source
    @[simp]
    theorem Convexity.ConvexSpace.AffineMap.cone_mk₁ {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {Y : Type u_2} [ConvexSpace R Y] (y y₀ : Y) :
    (StdSimplex.affineMapMk ![y₀]).cone y = StdSimplex.affineMapMk ![y, y₀]
    source
    @[simp]
    theorem Convexity.ConvexSpace.AffineMap.cone_mk₂ {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {Y : Type u_2} [ConvexSpace R Y] (y y₀ y₁ : Y) :
    (StdSimplex.affineMapMk ![y₀, y₁]).cone y = StdSimplex.affineMapMk ![y, y₀, y₁]
    source
    theorem Convexity.ConvexSpace.AffineMap.cone_comp {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {Y : Type u_2} {Z : Type u_3} [ConvexSpace R Y] [ConvexSpace R Z] {n : ℕ} (φ : ConvexSpace.AffineMap R Y Z) (ψ : ConvexSpace.AffineMap R (StdSimplex R (Fin (n + 1))) Y) (y : Y) :
    (φ.comp ψ).cone (φ y) = φ.comp (ψ.cone y)