Discrete groups of plane isometries

AbbreviationThe Euclidean plane for discrete isometry groups#✓fully proved

\(E_2\) is the Euclidean plane: the real vector space \(\mathbb{R}^2\) of pairs of real numbers with the standard Euclidean inner product and norm.

abbrev E2 := EuclideanSpace ℝ (Fin 2)

Used by 15

Used byCarrier of the translation lattice subgroup · Conjugating a translation by a plane isometry · Classification of discrete additive subgroups of the plane · Separation criterion for groups of plane isometries · Linear part of a plane isometry · Isometry group of the Euclidean plane · Membership in the translation lattice subgroup · The point group preserves the translation lattice · Point group of a group of plane isometries · Translation homomorphism · Translations are determined by their vectors · Translation lattice · Classification of translation lattices · Translation lattice as an additive subgroup · The translation lattice of a discrete isometry group is discrete

AbbreviationIsometry group of the Euclidean plane#✓fully proved

\(M_2\) is the group, under composition, of affine isometries of the Euclidean plane onto itself.

abbrev M₂ := E2 ≃ᵃⁱ[ℝ] E2

Uses 1 · Used by 13

Statement usesThe Euclidean plane for discrete isometry groups

Used byCarrier of the translation lattice subgroup · Conjugating a translation by a plane isometry · Separation criterion for groups of plane isometries · Linear part of a plane isometry · Membership in the translation lattice subgroup · The point group preserves the translation lattice · Point group of a group of plane isometries · Translation homomorphism · Translations are determined by their vectors · Translation lattice · Classification of translation lattices · Translation lattice as an additive subgroup · The translation lattice of a discrete isometry group is discrete

DefinitionLinear part of a plane isometry#✓fully proved

The linear part of an affine isometry \(f\) of the Euclidean plane is the linear isometry \(A\) of the plane such that \(f(x + v) = f(x) + A v\) for every point \(x\) and every vector \(v\).

noncomputable def linearPart (f : M₂) : E2 ≃ₗᵢ[ℝ] E2 := f.linearIsometryEquiv

Uses 2 · Used by 4

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane

Used bySeparation criterion for groups of plane isometries · The point group preserves the translation lattice · Point group of a group of plane isometries · The translation lattice of a discrete isometry group is discrete

DefinitionPoint group of a group of plane isometries#✓fully proved

The point group of a group \(G\) of affine isometries of the Euclidean plane is the set of linear parts of the elements of \(G\).

noncomputable def pointGroupSet (G : Subgroup M₂) : Set (E2 ≃ₗᵢ[ℝ] E2) :=
  {A | ∃ f ∈ G, linearPart f = A}

Uses 3 · Used by 1

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane · Linear part of a plane isometry

Used byThe point group preserves the translation lattice

DefinitionTranslation lattice#✓fully proved

The translation lattice of a subgroup \(G\) of the group \(M_2\) of affine isometries of the Euclidean plane \(E_2\) is the set of vectors \(v \in E_2\) such that the translation \(x \mapsto v + x\) belongs to \(G\).

noncomputable def translationLattice (G : Subgroup M₂) : Set E2 :=
  {v : E2 | (AffineIsometryEquiv.constVAdd ℝ E2 v : M₂) ∈ G}

Uses 2 · Used by 3

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane

Used byCarrier of the translation lattice subgroup · Membership in the translation lattice subgroup · The point group preserves the translation lattice

DefinitionTranslation homomorphism#✓fully proved

The group homomorphism from the additive group of the Euclidean plane \(\mathbb{R}^2\) (written multiplicatively) to the group of affine isometries of the plane that sends a vector \(v\) to translation by \(v\), the isometry \(x \mapsto v + x\).

noncomputable def translationHom : Multiplicative E2 →* M₂ where
  toFun v := AffineIsometryEquiv.constVAdd ℝ E2 (Multiplicative.toAdd v)
  map_one' := by
    apply AffineIsometryEquiv.ext
    intro x
    change (0 : E2) + x = x
    exact zero_add x
  map_mul' v w := by
    apply AffineIsometryEquiv.ext
    intro x
    change (Multiplicative.toAdd v + Multiplicative.toAdd w) + x =
      Multiplicative.toAdd v + (Multiplicative.toAdd w + x)
    exact add_assoc _ _ _

Uses 2 · Used by 2

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane

Used byTranslations are determined by their vectors · Translation lattice as an additive subgroup

DefinitionTranslation lattice as an additive subgroup#✓fully proved

For a group \(G\) of affine isometries of the Euclidean plane \(\mathbb{R}^2\), the additive subgroup of \(\mathbb{R}^2\) consisting of the vectors \(v\) such that translation by \(v\) belongs to \(G\); it is the preimage of \(G\) under the translation homomorphism \(v \mapsto (x \mapsto v + x)\).

noncomputable def translationLatticeSubgroup (G : Subgroup M₂) : AddSubgroup E2 :=
  Subgroup.toAddSubgroup' (G.comap translationHom)

Uses 3 · Used by 4

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane · Translation homomorphism

Used byCarrier of the translation lattice subgroup · Membership in the translation lattice subgroup · Classification of translation lattices · The translation lattice of a discrete isometry group is discrete

TheoremMembership in the translation lattice subgroup#✓fully proved

For every group \(G\) of affine isometries of the Euclidean plane and every vector \(v\) of the plane, \(v\) belongs to the translation lattice subgroup of \(G\) if and only if \(v\) belongs to the translation lattice of \(G\).

@[simp] theorem mem_translationLatticeSubgroup (G : Subgroup M₂) (v : E2) :
    v ∈ translationLatticeSubgroup G ↔ v ∈ translationLattice G

Uses 4

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane · Translation lattice · Translation lattice as an additive subgroup

TheoremCarrier of the translation lattice subgroup#✓fully proved

For every group \(G\) of affine isometries of the Euclidean plane, the underlying set of the translation lattice subgroup of \(G\) is the translation lattice of \(G\).

@[simp] theorem coe_translationLatticeSubgroup (G : Subgroup M₂) :
    (translationLatticeSubgroup G : Set E2) = translationLattice G

Uses 4

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane · Translation lattice · Translation lattice as an additive subgroup

TheoremTranslations are determined by their vectors#✓fully proved

For vectors \(v\) and \(w\) of the Euclidean plane \(\mathbb{R}^2\), if translation by \(v\) and translation by \(w\) are the same affine isometry, then \(v = w\). Equivalently, the translation homomorphism \(v \mapsto (x \mapsto v + x)\) from the additive group of the plane to the group of affine isometries of the plane is injective.

theorem translationHom_injective : Function.Injective translationHom

Uses 3

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane · Translation homomorphism

DefinitionSeparation criterion for groups of plane isometries#✓fully proved

A group \(G\) of affine isometries of the Euclidean plane satisfies the separation criterion if there is \(\varepsilon > 0\) such that every element \(f \ne \mathrm{id}\) of \(G\) whose linear part is the identity satisfies \(\|f(0)\| \ge \varepsilon\), and every element \(f\) of \(G\) whose linear part \(A\) is not the identity satisfies \(\|A - I\| \ge \varepsilon\), where \(I\) is the identity map and the norm is the operator norm.

Its linear-part condition measures operator-norm separation from the identity, rather than the numerical rotation angle.

def IsDiscrete (G : Subgroup M₂) : Prop :=
  ∃ ε > 0,
    (∀ f ∈ G, linearPart f = LinearIsometryEquiv.refl ℝ E2 → f ≠ 1 → ε ≤ ‖f 0‖) ∧
    (∀ f ∈ G, linearPart f ≠ LinearIsometryEquiv.refl ℝ E2 →
      ε ≤ ‖(linearPart f).toLinearIsometry.toContinuousLinearMap -
        ContinuousLinearMap.id ℝ E2‖)

Uses 3 · Used by 2

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane · Linear part of a plane isometry

Used byClassification of translation lattices · The translation lattice of a discrete isometry group is discrete

TheoremThe translation lattice of a discrete isometry group is discrete#✓fully proved

Let \(G\) be a group of affine isometries of the Euclidean plane \(\mathbb{R}^2\), and suppose there is \(\varepsilon > 0\) such that every non-identity translation in \(G\) moves the origin by at least \(\varepsilon\), and every element of \(G\) whose linear part \(A\) is not the identity satisfies \(\|A - I\| \ge \varepsilon\) in operator norm. Then the translation lattice of \(G\), the additive subgroup of vectors \(v\) such that translation by \(v\) lies in \(G\), is discrete in the subspace topology of \(\mathbb{R}^2\).

theorem translationLatticeSubgroup_discreteTopology (G : Subgroup M₂) (hG : IsDiscrete G) :
    DiscreteTopology (translationLatticeSubgroup G)

Uses 5 · Used by 1

Statement usesThe Euclidean plane for discrete isometry groups · Separation criterion for groups of plane isometries · Isometry group of the Euclidean plane · Translation lattice as an additive subgroup

Proof usesLinear part of a plane isometry

Used byClassification of translation lattices

LemmaConjugating a translation by a plane isometry#✓fully proved

Let \(g\) be an affine isometry of the Euclidean plane with linear part \(A\), let \(v\) be a vector, and write \(\tau_w\) for translation by a vector \(w\). Then \(g \circ \tau_v \circ g^{-1} = \tau_{A v}\).

lemma conj_translation (g : M₂) (v : E2) :
    g * (AffineIsometryEquiv.constVAdd ℝ E2 v) * g⁻¹ =
    AffineIsometryEquiv.constVAdd ℝ E2 (g.linearIsometryEquiv v)

Uses 2 · Used by 1

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane

Used byThe point group preserves the translation lattice

TheoremThe point group preserves the translation lattice#✓fully proved

Let \(G\) be a group of affine isometries of the Euclidean plane. If \(A\) belongs to the point group of \(G\), that is, \(A\) is the linear part of some element of \(G\), and \(v\) belongs to the translation lattice of \(G\), then \(A v\) belongs to the translation lattice of \(G\).

theorem point_group_preserves_lattice (G : Subgroup M₂)
    (A : E2 ≃ₗᵢ[ℝ] E2) (hA : A ∈ pointGroupSet G)
    (v : E2) (hv : v ∈ translationLattice G) :
    A v ∈ translationLattice G

Uses 6

Statement usesThe Euclidean plane for discrete isometry groups · Isometry group of the Euclidean plane · Point group of a group of plane isometries · Translation lattice

Proof usesConjugating a translation by a plane isometry · Linear part of a plane isometry

TheoremClassification of discrete additive subgroups of the plane#✓fully proved

Every discrete additive subgroup G of ℝ² is trivial, cyclic (generated by a single nonzero vector), or a rank-two lattice (generated by two ℝ-linearly independent vectors).

theorem discrete_subgroup_R2_classification
    (G : AddSubgroup E2) [DiscreteTopology G] :
    G = ⊥ ∨
    (∃ α : E2, α ≠ 0 ∧ G = AddSubgroup.zmultiples α) ∨
    (∃ a b : E2, LinearIndependent ℝ ![a, b] ∧
      G = AddSubgroup.zmultiples a ⊔ AddSubgroup.zmultiples b)

Uses 1 · Used by 1

Statement usesThe Euclidean plane for discrete isometry groups

Used byClassification of translation lattices

TheoremClassification of translation lattices#✓fully proved

Let \(G\) be a group of affine isometries of the Euclidean plane \(\mathbb{R}^2\), and suppose there is \(\varepsilon > 0\) such that every non-identity translation in \(G\) moves the origin by at least \(\varepsilon\), and every element of \(G\) whose linear part \(A\) is not the identity satisfies \(\|A - I\| \ge \varepsilon\) in operator norm. Let \(L\) be the translation lattice of \(G\), the additive subgroup of vectors \(v\) such that translation by \(v\) lies in \(G\). Then either \(L = \{0\}\), or \(L = \mathbb{Z}\alpha\) for some nonzero vector \(\alpha\), or \(L = \mathbb{Z}a + \mathbb{Z}b\) for some \(\mathbb{R}\)-linearly independent vectors \(a\) and \(b\).

theorem translation_lattice_classification (G : Subgroup M₂) (hG : IsDiscrete G) :
    translationLatticeSubgroup G = ⊥ ∨
    (∃ α : E2, α ≠ 0 ∧ translationLatticeSubgroup G = AddSubgroup.zmultiples α) ∨
    (∃ a b : E2, LinearIndependent ℝ ![a, b] ∧
      translationLatticeSubgroup G = AddSubgroup.zmultiples a ⊔ AddSubgroup.zmultiples b)

Uses 6

Statement usesThe Euclidean plane for discrete isometry groups · Separation criterion for groups of plane isometries · Isometry group of the Euclidean plane · Translation lattice as an additive subgroup

Proof usesClassification of discrete additive subgroups of the plane · The translation lattice of a discrete isometry group is discrete

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.