mathlib3 documentation

analysis.complex.isometry

Isometries of the Complex Plane #

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

The lemma linear_isometry_complex states the classification of isometries in the complex plane. Specifically, isometries with rotations but without translation. The proof involves:

creating a linear isometry g with two fixed points, g(0) = 0, g(1) = 1
applying linear_isometry_complex_aux to g The proof of linear_isometry_complex_aux is separated in the following parts:
show that the real parts match up: linear_isometry.re_apply_eq_re
show that I maps to either I or -I
every z is a linear combination of a + b * I

References #

Isometries of the Complex Plane

noncomputable def rotation :

↥circle →* ℂ ≃ₗᵢ[ℝ ] ℂ

An element of the unit circle defines a linear_isometry_equiv from ℂ to itself, by rotation.

Equations

rotation = {to_fun := λ (a : ↥circle), {to_linear_equiv := {to_fun := (distrib_mul_action.to_linear_equiv ℝ ℂ a).to_fun, map_add' := _, map_smul' := _, inv_fun := (distrib_mul_action.to_linear_equiv ℝ ℂ a).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}, map_one' := rotation._proof_7, map_mul' := rotation._proof_8}

@[simp]

theorem rotation_apply (a : ↥circle) (z : ℂ) :

⇑(⇑rotation a) z = ↑a * z

@[simp]

theorem rotation_symm (a : ↥circle) :

(⇑rotation a).symm = ⇑rotation a⁻¹

@[simp]

theorem rotation_trans (a b : ↥circle) :

(⇑rotation a).trans (⇑rotation b) = ⇑rotation (b * a)

theorem rotation_ne_conj_lie (a : ↥circle) :

⇑rotation a ≠ complex.conj_lie

@[simp]

theorem rotation_of_coe (e : ℂ ≃ₗᵢ[ℝ ] ℂ) :

↑(rotation_of e) = ⇑e 1 / ↑(⇑complex.abs (⇑e 1))

noncomputable def rotation_of (e : ℂ ≃ₗᵢ[ℝ ] ℂ) :

Takes an element of ℂ ≃ₗᵢ[ℝ] ℂ and checks if it is a rotation, returns an element of the unit circle.

Equations

rotation_of e = ⟨⇑e 1 / ↑(⇑complex.abs (⇑e 1)), _⟩

@[simp]

theorem rotation_of_rotation (a : ↥circle) :

rotation_of (⇑rotation a) = a

theorem rotation_injective :

function.injective ⇑rotation

theorem linear_isometry.re_apply_eq_re_of_add_conj_eq (f : ℂ →ₗᵢ[ℝ ] ℂ) (h₃ : ∀ (z : ℂ), z + ⇑(star_ring_end ℂ) z = ⇑f z + ⇑(star_ring_end ℂ) (⇑f z)) (z : ℂ) :

(⇑f z).re = z.re

theorem linear_isometry.im_apply_eq_im_or_neg_of_re_apply_eq_re {f : ℂ →ₗᵢ[ℝ ] ℂ} (h₂ : ∀ (z : ℂ), (⇑f z).re = z.re) (z : ℂ) :

(⇑f z).im = z.im ∨ (⇑f z).im = -z.im

theorem linear_isometry.im_apply_eq_im {f : ℂ →ₗᵢ[ℝ ] ℂ} (h : ⇑f 1 = 1) (z : ℂ) :

z + ⇑(star_ring_end ℂ) z = ⇑f z + ⇑(star_ring_end ℂ) (⇑f z)

theorem linear_isometry.re_apply_eq_re {f : ℂ →ₗᵢ[ℝ ] ℂ} (h : ⇑f 1 = 1) (z : ℂ) :

(⇑f z).re = z.re

theorem linear_isometry_complex_aux {f : ℂ ≃ₗᵢ[ℝ ] ℂ} (h : ⇑f 1 = 1) :

f = linear_isometry_equiv.refl ℝ ℂ ∨ f = complex.conj_lie

theorem linear_isometry_complex (f : ℂ ≃ₗᵢ[ℝ ] ℂ) :

∃ (a : ↥circle), f = ⇑rotation a ∨ f = complex.conj_lie.trans (⇑rotation a)

theorem to_matrix_rotation (a : ↥circle) :

⇑(linear_map.to_matrix complex.basis_one_I complex.basis_one_I) ↑((⇑rotation a).to_linear_equiv) = ⇑(matrix.plane_conformal_matrix ↑a.re ↑a.im _)

The matrix representation of rotation a is equal to the conformal matrix !![re a, -im a; im a, re a].

@[simp]

theorem det_rotation (a : ↥circle) :

⇑linear_map.det ↑((⇑rotation a).to_linear_equiv) = 1

The determinant of rotation (as a linear map) is equal to 1.

@[simp]

theorem linear_equiv_det_rotation (a : ↥circle) :

⇑linear_equiv.det (⇑rotation a).to_linear_equiv = 1

The determinant of rotation (as a linear equiv) is equal to 1.