The image of a convex body under a continuous linear map

A continuous linear map f : V →L[ℝ] W sends convex, compact, nonempty sets to convex, compact, nonempty sets, so it pushes a convex body K of V forward to the convex body K.map f of W with carrier f '' K. This is how a convex body is carried along a change of coordinates, for instance to transport the successive minima of a lattice with respect to a body along a linear equivalence.

Main definitions

• ConvexBody.map f K: the image of the convex body K under the continuous linear map f.

def ConvexBody.map {V : Type u_1} {W : Type u_2} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [TopologicalSpace W] [AddCommGroup W] [Module ℝ W] (f : V →L[ℝ] W) (K : ConvexBody V) : ConvexBody W

The image of a convex body under a continuous linear map, as a convex body.

@[simp]

theorem ConvexBody.coe_map {V : Type u_1} {W : Type u_2} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [TopologicalSpace W] [AddCommGroup W] [Module ℝ W] (f : V →L[ℝ] W) (K : ConvexBody V) : ↑(map f K) = ⇑f '' ↑K

@[simp]

theorem ConvexBody.mem_map {V : Type u_1} {W : Type u_2} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [TopologicalSpace W] [AddCommGroup W] [Module ℝ W] {f : V →L[ℝ] W} {K : ConvexBody V} {y : W} : y ∈ map f K ↔ ∃ x ∈ K, f x = y

@[simp]

theorem ConvexBody.map_id {V : Type u_1} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] (K : ConvexBody V) : map (ContinuousLinearMap.id ℝ V) K = K

theorem ConvexBody.map_comp {V : Type u_1} {W : Type u_2} {X : Type u_3} [TopologicalSpace V] [AddCommGroup V] [Module ℝ V] [TopologicalSpace W] [AddCommGroup W] [Module ℝ W] [TopologicalSpace X] [AddCommGroup X] [Module ℝ X] (g : W →L[ℝ] X) (f : V →L[ℝ] W) (K : ConvexBody V) : map (g ∘SL f) K = map g (map f K)