Isometries of the Complex Plane

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

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

References

• Isometries of the Complex Plane

def rotation : { x // x ∈ circle } →* ℂ ≃ₗᵢ[ℝ] ℂ

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem rotation_apply (a : { x // x ∈ circle }) (z : ℂ) : ↑(↑rotation a) z = ↑a * z

@[simp]

theorem rotation_symm (a : { x // x ∈ circle }) : LinearIsometryEquiv.symm (↑rotation a) = ↑rotation a⁻¹

@[simp]

theorem rotation_trans (a : { x // x ∈ circle }) (b : { x // x ∈ circle }) : LinearIsometryEquiv.trans (↑rotation a) (↑rotation b) = ↑rotation (b * a)

theorem rotation_ne_conjLie (a : { x // x ∈ circle }) : ↑rotation a ≠ Complex.conjLie

@[simp]

theorem rotationOf_coe (e : ℂ ≃ₗᵢ[ℝ] ℂ) : ↑(rotationOf e) = ↑e 1 / ↑(↑Complex.abs (↑e 1))

def rotationOf (e : ℂ ≃ₗᵢ[ℝ] ℂ) : { x // x ∈ circle }

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

Equations

• rotationOf e = { val := ↑e 1 / ↑(↑Complex.abs (↑e 1)), property := (_ : ↑e 1 / ↑(↑Complex.abs (↑e 1)) ∈ circle) }

@[simp]

theorem rotationOf_rotation (a : { x // x ∈ circle }) : rotationOf (↑rotation a) = a

theorem rotation_injective : Function.Injective ↑rotation

theorem LinearIsometry.re_apply_eq_re_of_add_conj_eq (f : ℂ →ₗᵢ[ℝ] ℂ) (h₃ : ∀ (z : ℂ), z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)) (z : ℂ) : (↑f z).re = z.re

theorem LinearIsometry.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 LinearIsometry.im_apply_eq_im {f : ℂ →ₗᵢ[ℝ] ℂ} (h : ↑f 1 = 1) (z : ℂ) : z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)

theorem LinearIsometry.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 = LinearIsometryEquiv.refl ℝ ℂ ∨ f = Complex.conjLie

theorem linear_isometry_complex (f : ℂ ≃ₗᵢ[ℝ] ℂ) : ∃ a, f = ↑rotation a ∨ f = LinearIsometryEquiv.trans Complex.conjLie (↑rotation a)

theorem toMatrix_rotation (a : { x // x ∈ circle }) : ↑(LinearMap.toMatrix Complex.basisOneI Complex.basisOneI) ↑(↑rotation a).toLinearEquiv = ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im (_ : (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0))

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 : { x // x ∈ circle }) : ↑LinearMap.det ↑(↑rotation a).toLinearEquiv = 1

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

@[simp]

theorem linearEquiv_det_rotation (a : { x // x ∈ circle }) : ↑LinearEquiv.det (↑rotation a).toLinearEquiv = 1

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