Mazur-Ulam Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Mazur-Ulam theorem states that an isometric bijection between two normed affine spaces over ℝ is affine. We formalize it in three definitions:

isometry_equiv.to_real_linear_isometry_equiv_of_map_zero : given E ≃ᵢ F sending 0 to 0, returns E ≃ₗᵢ[ℝ] F with the same to_fun and inv_fun;
isometry_equiv.to_real_linear_isometry_equiv : given f : E ≃ᵢ F, returns a linear isometry equivalence g : E ≃ₗᵢ[ℝ] F with g x = f x - f 0.
isometry_equiv.to_real_affine_isometry_equiv : given f : PE ≃ᵢ PF, returns an affine isometry equivalence g : PE ≃ᵃⁱ[ℝ] PF whose underlying isometry_equiv is f

The formalization is based on Jussi Väisälä, A Proof of the Mazur-Ulam Theorem.

Tags #

isometry, affine map, linear map

source

theorem isometry_equiv.midpoint_fixed {E : Type u_1} {PE : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] [metric_space PE] [normed_add_torsor E PE] {x y : PE} (e : PE ≃ᵢ PE) :

⇑e x = x → ⇑e y = y → ⇑e (midpoint ℝ x y) = midpoint ℝ x y

If an isometric self-homeomorphism of a normed vector space over ℝ fixes x and y, then it fixes the midpoint of [x, y]. This is a lemma for a more general Mazur-Ulam theorem, see below.

source

theorem isometry_equiv.map_midpoint {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] [metric_space PE] [normed_add_torsor E PE] [normed_add_comm_group F] [normed_space ℝ F] [metric_space PF] [normed_add_torsor F PF] (f : PE ≃ᵢ PF) (x y : PE) :

⇑f (midpoint ℝ x y) = midpoint ℝ (⇑f x) (⇑f y)

A bijective isometry sends midpoints to midpoints.

Since f : PE ≃ᵢ PF sends midpoints to midpoints, it is an affine map. We define a conversion to a continuous_linear_equiv first, then a conversion to an affine_map.

source

noncomputable def isometry_equiv.to_real_linear_isometry_equiv_of_map_zero {E : Type u_1} {F : Type u_3} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] (f : E ≃ᵢ F) (h0 : ⇑f 0 = 0) :

E ≃ₗᵢ[ℝ ] F

Mazur-Ulam Theorem: if f is an isometric bijection between two normed vector spaces over ℝ and f 0 = 0, then f is a linear isometry equivalence.

Equations

f.to_real_linear_isometry_equiv_of_map_zero h0 = {to_linear_equiv := {to_fun := ((add_monoid_hom.of_map_midpoint ℝ ℝ ⇑f h0 _).to_real_linear_map _).to_linear_map.to_fun, map_add' := _, map_smul' := _, inv_fun := f.to_equiv.inv_fun, left_inv := _, right_inv := _}, norm_map' := _}

source

@[simp]

theorem isometry_equiv.coe_to_real_linear_equiv_of_map_zero {E : Type u_1} {F : Type u_3} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] (f : E ≃ᵢ F) (h0 : ⇑f 0 = 0) :

⇑(f.to_real_linear_isometry_equiv_of_map_zero h0) = ⇑f

source

@[simp]

theorem isometry_equiv.coe_to_real_linear_equiv_of_map_zero_symm {E : Type u_1} {F : Type u_3} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] (f : E ≃ᵢ F) (h0 : ⇑f 0 = 0) :

⇑((f.to_real_linear_isometry_equiv_of_map_zero h0).symm) = ⇑(f.symm)

source

noncomputable def isometry_equiv.to_real_linear_isometry_equiv {E : Type u_1} {F : Type u_3} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] (f : E ≃ᵢ F) :

E ≃ₗᵢ[ℝ ] F

Mazur-Ulam Theorem: if f is an isometric bijection between two normed vector spaces over ℝ, then x ↦ f x - f 0 is a linear isometry equivalence.

Equations

f.to_real_linear_isometry_equiv = (f.trans (isometry_equiv.add_right (⇑f 0)).symm).to_real_linear_isometry_equiv_of_map_zero _

source

@[simp]

theorem isometry_equiv.to_real_linear_equiv_apply {E : Type u_1} {F : Type u_3} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] (f : E ≃ᵢ F) (x : E) :

⇑(f.to_real_linear_isometry_equiv) x = ⇑f x - ⇑f 0

source

@[simp]

theorem isometry_equiv.to_real_linear_isometry_equiv_symm_apply {E : Type u_1} {F : Type u_3} [normed_add_comm_group E] [normed_space ℝ E] [normed_add_comm_group F] [normed_space ℝ F] (f : E ≃ᵢ F) (y : F) :

⇑(f.to_real_linear_isometry_equiv.symm) y = ⇑(f.symm) (y + ⇑f 0)

source

noncomputable def isometry_equiv.to_real_affine_isometry_equiv {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] [metric_space PE] [normed_add_torsor E PE] [normed_add_comm_group F] [normed_space ℝ F] [metric_space PF] [normed_add_torsor F PF] (f : PE ≃ᵢ PF) :

PE ≃ᵃⁱ[ℝ ] PF

Mazur-Ulam Theorem: if f is an isometric bijection between two normed add-torsors over normed vector spaces over ℝ, then f is an affine isometry equivalence.

Equations

f.to_real_affine_isometry_equiv = affine_isometry_equiv.mk' ⇑f ((isometry_equiv.vadd_const (classical.arbitrary PE)).trans (f.trans (isometry_equiv.vadd_const (⇑f (classical.arbitrary PE))).symm)).to_real_linear_isometry_equiv (classical.arbitrary PE) _

source

@[simp]

theorem isometry_equiv.coe_fn_to_real_affine_isometry_equiv {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] [metric_space PE] [normed_add_torsor E PE] [normed_add_comm_group F] [normed_space ℝ F] [metric_space PF] [normed_add_torsor F PF] (f : PE ≃ᵢ PF) :

⇑(f.to_real_affine_isometry_equiv) = ⇑f

source

@[simp]

theorem isometry_equiv.coe_to_real_affine_isometry_equiv {E : Type u_1} {PE : Type u_2} {F : Type u_3} {PF : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] [metric_space PE] [normed_add_torsor E PE] [normed_add_comm_group F] [normed_space ℝ F] [metric_space PF] [normed_add_torsor F PF] (f : PE ≃ᵢ PF) :

f.to_real_affine_isometry_equiv.to_isometry_equiv = f