Documentation

Mathlib.Analysis.Complex.Isometry

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 #

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.
Instances For
    @[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 : circle) (b : circle) :
    (rotation a).trans (rotation b) = rotation (b * a)
    @[simp]
    theorem rotationOf_coe (e : ≃ₗᵢ[] ) :
    (rotationOf e) = e 1 / (Complex.abs (e 1))

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

    Equations
    Instances For
      @[simp]
      theorem rotationOf_rotation (a : circle) :
      rotationOf (rotation a) = a
      theorem LinearIsometry.re_apply_eq_re_of_add_conj_eq (f : →ₗᵢ[] ) (h₃ : ∀ (z : ), z + (starRingEnd ) z = f z + (starRingEnd ) (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 ) (f z)
      theorem LinearIsometry.re_apply_eq_re {f : →ₗᵢ[] } (h : f 1 = 1) (z : ) :
      (f z).re = z.re
      theorem linear_isometry_complex (f : ≃ₗᵢ[] ) :
      ∃ (a : circle), f = rotation a f = Complex.conjLIE.trans (rotation a)
      theorem toMatrix_rotation (a : circle) :
      (LinearMap.toMatrix Complex.basisOneI Complex.basisOneI) (rotation a).toLinearEquiv = (Matrix.planeConformalMatrix (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) :
      LinearMap.det (rotation a).toLinearEquiv = 1

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

      @[simp]
      theorem linearEquiv_det_rotation (a : circle) :
      LinearEquiv.det (rotation a).toLinearEquiv = 1

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