Bundled affine maps between convex spaces

If X and Y are convex spaces (over R), we introduce the type ConvexSpace.AffineMap R X Y of bundled affine maps from X to Y.

structure Convexity.ConvexSpace.AffineMap (R : Type u_1) [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (X : Type u_2) (Y : Type u_3) [ConvexSpace R X] [ConvexSpace R Y] : Type (max u_2 u_3)

The type of (bundled) affine maps between two convex spaces.

• toFun : X → Y

  The underlying map of an affine map between convex spaces.

• isAffineMap_toFun : IsAffineMap R self.toFun

@[instance_reducible, macro_inline]

instance Convexity.ConvexSpace.AffineMap.instFunLike {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [ConvexSpace R X] [ConvexSpace R Y] : FunLike (ConvexSpace.AffineMap R X Y) X Y

Equations

• Convexity.ConvexSpace.AffineMap.instFunLike = { coe := Convexity.ConvexSpace.AffineMap.toFun, coe_injective := ⋯ }

@[simp]

theorem Convexity.ConvexSpace.AffineMap.coe_mk {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [ConvexSpace R X] [ConvexSpace R Y] (toFun : X → Y) (isAffineMap_toFun : IsAffineMap R toFun) : ⇑{ toFun := toFun, isAffineMap_toFun := isAffineMap_toFun } = toFun

theorem Convexity.ConvexSpace.AffineMap.ext {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [ConvexSpace R X] [ConvexSpace R Y] {f g : ConvexSpace.AffineMap R X Y} (h : ⇑f = ⇑g) : f = g

theorem Convexity.ConvexSpace.AffineMap.ext_iff {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [ConvexSpace R X] [ConvexSpace R Y] {f g : ConvexSpace.AffineMap R X Y} : f = g ↔ ⇑f = ⇑g

theorem Convexity.ConvexSpace.AffineMap.isAffineMap {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [ConvexSpace R X] [ConvexSpace R Y] (f : ConvexSpace.AffineMap R X Y) : IsAffineMap R ⇑f

@[implicit_reducible]

def Convexity.ConvexSpace.AffineMap.id {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (X : Type u_2) [ConvexSpace R X] : ConvexSpace.AffineMap R X X

The identity map, as a bundled affine map of convex spaces.

Equations

• Convexity.ConvexSpace.AffineMap.id X = { toFun := id, isAffineMap_toFun := ⋯ }

@[simp]

theorem Convexity.ConvexSpace.AffineMap.id_apply {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (X : Type u_2) [ConvexSpace R X] (a : X) : (id X) a = _root_.id a

@[implicit_reducible]

def Convexity.ConvexSpace.AffineMap.comp {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [ConvexSpace R X] [ConvexSpace R Y] [ConvexSpace R Z] (g : ConvexSpace.AffineMap R Y Z) (f : ConvexSpace.AffineMap R X Y) : ConvexSpace.AffineMap R X Z

The composition of bundled affine maps between convex spaces.

Equations

• g.comp f = { toFun := ⇑g ∘ ⇑f, isAffineMap_toFun := ⋯ }

@[simp]

theorem Convexity.ConvexSpace.AffineMap.comp_apply {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [ConvexSpace R X] [ConvexSpace R Y] [ConvexSpace R Z] (g : ConvexSpace.AffineMap R Y Z) (f : ConvexSpace.AffineMap R X Y) (a✝ : X) : (g.comp f) a✝ = (⇑g ∘ ⇑f) a✝

@[simp]

theorem Convexity.ConvexSpace.AffineMap.coe_comp {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [ConvexSpace R X] [ConvexSpace R Y] [ConvexSpace R Z] (g : ConvexSpace.AffineMap R Y Z) (f : ConvexSpace.AffineMap R X Y) : ⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

theorem Convexity.ConvexSpace.AffineMap.id_comp {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [ConvexSpace R X] [ConvexSpace R Y] (f : ConvexSpace.AffineMap R X Y) : (id Y).comp f = f

@[simp]

theorem Convexity.ConvexSpace.AffineMap.comp_id {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [ConvexSpace R X] [ConvexSpace R Y] (f : ConvexSpace.AffineMap R X Y) : f.comp (id X) = f

theorem Convexity.ConvexSpace.AffineMap.assoc {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {T : Type u_5} [ConvexSpace R X] [ConvexSpace R Y] [ConvexSpace R Z] [ConvexSpace R T] (f₁ : ConvexSpace.AffineMap R Z T) (f₂ : ConvexSpace.AffineMap R Y Z) (f₃ : ConvexSpace.AffineMap R X Y) : (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃)

@[implicit_reducible]

def Convexity.ConvexSpace.AffineMap.const {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [ConvexSpace R X] [ConvexSpace R Y] (y : Y) : ConvexSpace.AffineMap R X Y

A constant map between convex spaces, as a bundled affine map.

Equations

• Convexity.ConvexSpace.AffineMap.const y = { toFun := fun (x : X) => y, isAffineMap_toFun := ⋯ }

@[simp]

theorem Convexity.ConvexSpace.AffineMap.const_apply {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [ConvexSpace R X] [ConvexSpace R Y] (y : Y) (x✝ : X) : (const y) x✝ = y

theorem Convexity.StdSimplex.affineMap_ext {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [ConvexSpace R Y] {f g : ConvexSpace.AffineMap R (StdSimplex R M) Y} (h : ∀ (i : M), f (single i) = g (single i)) : f = g

theorem Convexity.StdSimplex.affineMap_ext_iff {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [ConvexSpace R Y] {f g : ConvexSpace.AffineMap R (StdSimplex R M) Y} : f = g ↔ ∀ (i : M), f (single i) = g (single i)

noncomputable def Convexity.StdSimplex.affineMap {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} (f : M → N) : ConvexSpace.AffineMap R (StdSimplex R M) (StdSimplex R N)

The (bundled) affine map StdSimplex R M → StdSimplex R N induced by a map f : M → N.

Equations

• Convexity.StdSimplex.affineMap f = { toFun := Convexity.StdSimplex.map f, isAffineMap_toFun := ⋯ }

@[simp]

theorem Convexity.StdSimplex.coe_affineMap {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} (f : M → N) : ⇑(affineMap f) = map f

@[simp]

theorem Convexity.StdSimplex.affineMap_id {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (M : Type u_2) : affineMap id = ConvexSpace.AffineMap.id (StdSimplex R M)

noncomputable def Convexity.StdSimplex.affineMapMk {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {X : Type u_3} [ConvexSpace R X] (f : M → X) : ConvexSpace.AffineMap R (StdSimplex R M) X

Given a map f : M → X where X is a convex space over R, this is the affine map StdSimplex R M → X which sends the vertex corresponding to m : M to f m.

Equations

• Convexity.StdSimplex.affineMapMk f = { toFun := fun (x : Convexity.StdSimplex R M) => Convexity.iConvexComb x f, isAffineMap_toFun := ⋯ }

theorem Convexity.StdSimplex.affineMapMk_apply {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [ConvexSpace R Y] (f : M → Y) (s : StdSimplex R M) : (affineMapMk f) s = iConvexComb s f

@[simp]

theorem Convexity.StdSimplex.affineMapMk_single {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [ConvexSpace R Y] (f : M → Y) (m : M) : (affineMapMk f) (single m) = f m

theorem Convexity.StdSimplex.affineMapMk_surjective {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [ConvexSpace R Y] (s : ConvexSpace.AffineMap R (StdSimplex R M) Y) : ∃ (f : M → Y), affineMapMk f = s

theorem Convexity.StdSimplex.comp_affineMapMk {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} {Z : Type u_4} [ConvexSpace R Y] [ConvexSpace R Z] (f : ConvexSpace.AffineMap R Y Z) (g : M → Y) : f.comp (affineMapMk g) = affineMapMk (⇑f ∘ g)