Classification of plane isometries

AbbreviationThe Euclidean plane#✓fully proved

The Euclidean plane is the real vector space \(\mathbb{R}^2\) with its standard inner product \(\langle x, y \rangle = x_1 y_1 + x_2 y_2\).

abbrev Plane := EuclideanSpace ℝ (Fin 2)

Used by 6

Used byGlide reflection · Reflection · Rotation · Translation · Linear determinant of a plane isometry · Classification of plane isometries

DefinitionLinear determinant of a plane isometry#✓fully proved

The linear determinant of an isometry \(f\) of the Euclidean plane is the determinant of the linear part of \(f\).

noncomputable def linearDet (f : Plane ≃ᵃⁱ[ℝ] Plane) : ℝ :=
  LinearMap.det (f.linear.toLinearMap)

Uses 1 · Used by 4

Statement usesThe Euclidean plane

Used byGlide reflection · Reflection · Rotation · Classification of plane isometries

DefinitionTranslation#✓fully proved

An isometry \(f\) of the Euclidean plane is a translation if there is a vector \(v\) such that \(f(x) = x + v\) for every point \(x\).

def IsTranslation (f : Plane ≃ᵃⁱ[ℝ] Plane) : Prop :=
  ∃ v : Plane, ∀ x : Plane, f x = v +ᵥ x

Uses 1 · Used by 2

Statement usesThe Euclidean plane

Used byRotation · Classification of plane isometries

DefinitionRotation#✓fully proved

An isometry \(f\) of the Euclidean plane is a rotation if it fixes some point \(p\), the determinant of its linear part is \(1\), and \(f\) is not a translation.

def IsRotation (f : Plane ≃ᵃⁱ[ℝ] Plane) : Prop :=
  ∃ p : Plane, f p = p ∧ linearDet f = 1 ∧ ¬IsTranslation f

Uses 3 · Used by 1

Statement usesTranslation · The Euclidean plane · Linear determinant of a plane isometry

Used byClassification of plane isometries

DefinitionReflection#✓fully proved

An isometry \(f\) of the Euclidean plane is a reflection if there is a line \(L\) such that \(f(x) = x\) for every point \(x\) of \(L\), and the determinant of the linear part of \(f\) is \(-1\).

def IsReflection (f : Plane ≃ᵃⁱ[ℝ] Plane) : Prop :=
  ∃ L : AffineSubspace ℝ Plane,
    Module.finrank ℝ L.direction = 1 ∧
    (∀ x : Plane, x ∈ L → f x = x) ∧
    linearDet f = -1

Uses 2 · Used by 1

Statement usesThe Euclidean plane · Linear determinant of a plane isometry

Used byClassification of plane isometries

DefinitionGlide reflection#✓fully proved

An isometry \(f\) of the Euclidean plane is a glide reflection if the determinant of its linear part is \(-1\) and there are a line \(L\) and a nonzero vector \(v\) parallel to \(L\) such that \(f(x) = x + v\) for every point \(x\) of \(L\).

def IsGlideReflection (f : Plane ≃ᵃⁱ[ℝ] Plane) : Prop :=
  linearDet f = -1 ∧
    ∃ (L : AffineSubspace ℝ Plane),
      Module.finrank ℝ L.direction = 1 ∧
        ∃ (v : Plane), v ∈ L.direction ∧ v ≠ 0 ∧
          ∀ x ∈ L, (f x : Plane) = v +ᵥ x

Uses 2 · Used by 1

Statement usesThe Euclidean plane · Linear determinant of a plane isometry

Used byClassification of plane isometries

TheoremClassification of plane isometries#✓fully proved

Every isometry of the Euclidean plane is a translation, a rotation, a reflection, or a glide reflection.

theorem plane_isometry_classification (f : Plane ≃ᵃⁱ[ℝ] Plane) :
    IsTranslation f ∨ IsRotation f ∨ IsReflection f ∨ IsGlideReflection f

Uses 6

Statement usesGlide reflection · Reflection · Rotation · Translation · The Euclidean plane

Proof usesLinear determinant of a plane isometry

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.