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.

source

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

Instances For

source

@[instance_reducible]

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 := ⋯ }

source

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

source

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

source

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

source

@[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 := ⋯ }

Instances For

source

@[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

source

@[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 := ⋯ }

Instances For

source

@[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✝

source

@[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

source

@[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

source

@[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

source

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₃)

source

@[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 := ⋯ }

Instances For

source

@[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

Documentation

Mathlib.Geometry.Convex.ConvexSpace.AffineMap

Bundled affine maps between convex spaces #