Dehn invariant

AbbreviationDehn group#✓fully proved

The Dehn group is the tensor product \(\mathbb{R} \otimes_{\mathbb{Z}} (\mathbb{R} / 2\pi\mathbb{Z})\) of abelian groups; it is the target of the Dehn invariant.

abbrev DehnGroup : Type := ℝ ⊗[ℤ] AddCircle (2 * π)

Used by 9

Used byDehn invariant · Additivity of the Dehn invariant under concatenation · The Dehn invariant splits off the first edge · The Dehn invariant of the cube is zero · Conditionally, the cube and the regular tetrahedron have different Dehn invariants · Dehn invariant of the empty edge list · Dehn invariant of a repeated edge · Nonzero Dehn invariant of the regular tetrahedron, conditional on irrationality · Nonvanishing of an edge term in the Dehn group

StructureEdge of a polyhedron#✓fully proved

An edge, as recorded for the Dehn invariant, is a pair of real numbers: its length and its dihedral angle in radians. No positivity or range condition is imposed on either.

structure Edge where
  /-- The length of the edge. -/
  length : ℝ
  /-- The dihedral angle at the edge, in radians. -/
  angle : ℝ

Used by 9

Used byEdge list of a cube · Dehn invariant · Additivity of the Dehn invariant under concatenation · The Dehn invariant splits off the first edge · The Dehn invariant of the cube is zero · Dehn invariant of the empty edge list · Dehn invariant of a repeated edge · Nonzero Dehn invariant of the regular tetrahedron, conditional on irrationality · Edge list of the regular tetrahedron

DefinitionDehn invariant#✓fully proved

The Dehn invariant of a list of edges is the sum, over the edges, of \(\ell \otimes \theta\) in the Dehn group, where \(\ell\) is the length of the edge and \(\theta\) its dihedral angle taken modulo \(2\pi\).

noncomputable def dehnInvariant (edges : List Edge) : DehnGroup :=
  (edges.map (fun e => e.length ⊗ₜ[ℤ] (↑e.angle : AddCircle (2 * π)))).sum

Uses 2 · Used by 7

Statement usesDehn group · Edge of a polyhedron

Used byAdditivity of the Dehn invariant under concatenation · The Dehn invariant splits off the first edge · The Dehn invariant of the cube is zero · Conditionally, the cube and the regular tetrahedron have different Dehn invariants · Dehn invariant of the empty edge list · Dehn invariant of a repeated edge · Nonzero Dehn invariant of the regular tetrahedron, conditional on irrationality

DefinitionDihedral angle of the regular tetrahedron#✓fully proved

The real number \(\arccos(1/3)\), the dihedral angle of a regular tetrahedron in radians.

noncomputable def tetrahedralAngle : ℝ := arccos (1 / 3)

Used by 3

Used byConditionally, the cube and the regular tetrahedron have different Dehn invariants · Nonzero Dehn invariant of the regular tetrahedron, conditional on irrationality · Edge list of the regular tetrahedron

DefinitionEdge list of a cube#✓fully proved

For a real number \(\ell\), the edge list of a cube of side \(\ell\) consists of \(12\) edges, each of length \(\ell\) with dihedral angle \(\pi / 2\).

noncomputable def cubeEdges (ℓ : ℝ) : List Edge := List.replicate 12 ⟨ℓ, π / 2⟩

Uses 1 · Used by 2

Statement usesEdge of a polyhedron

Used byThe Dehn invariant of the cube is zero · Conditionally, the cube and the regular tetrahedron have different Dehn invariants

DefinitionEdge list of the regular tetrahedron#✓fully proved

For a real number \(\ell\), the edge list of a regular tetrahedron with edge length \(\ell\) is the list of \(6\) edges, each of length \(\ell\) and dihedral angle \(\arccos(1/3)\).

noncomputable def tetrahedronEdges (ℓ : ℝ) : List Edge :=
  List.replicate 6 ⟨ℓ, tetrahedralAngle⟩

Uses 2 · Used by 2

Statement usesEdge of a polyhedron · Dihedral angle of the regular tetrahedron

Used byConditionally, the cube and the regular tetrahedron have different Dehn invariants · Nonzero Dehn invariant of the regular tetrahedron, conditional on irrationality

TheoremDehn invariant of the empty edge list#✓fully proved

The empty list of edges has Dehn invariant \(0\).

@[simp]
theorem dehnInvariant_nil : dehnInvariant [] = 0

Uses 3

Statement usesDehn group · Edge of a polyhedron · Dehn invariant

TheoremThe Dehn invariant splits off the first edge#✓fully proved

Let \(e\) be an edge of length \(\ell\) and dihedral angle \(\theta\), and let \(L\) be a list of edges. Then the Dehn invariant of the list obtained by putting \(e\) in front of \(L\) equals \(\ell \otimes \theta\) plus the Dehn invariant of \(L\), where \(\theta\) is taken modulo \(2\pi\).

@[simp]
theorem dehnInvariant_cons (e : Edge) (edges : List Edge) :
    dehnInvariant (e :: edges) =
      e.length ⊗ₜ[ℤ] (↑e.angle : AddCircle (2 * π)) + dehnInvariant edges

Uses 3

Statement usesDehn group · Edge of a polyhedron · Dehn invariant

TheoremAdditivity of the Dehn invariant under concatenation#✓fully proved

For lists of edges \(L_1\) and \(L_2\), the Dehn invariant of the concatenation of \(L_1\) and \(L_2\) is the sum of the Dehn invariants of \(L_1\) and \(L_2\).

@[simp]
theorem dehnInvariant_append (edges₁ edges₂ : List Edge) :
    dehnInvariant (edges₁ ++ edges₂) = dehnInvariant edges₁ + dehnInvariant edges₂

Uses 3

Statement usesDehn group · Edge of a polyhedron · Dehn invariant

TheoremDehn invariant of a repeated edge#✓fully proved

For a natural number \(n\) and an edge of length \(\ell\) and dihedral angle \(\theta\), the Dehn invariant of the list consisting of \(n\) copies of that edge is \(n \cdot (\ell \otimes \theta)\) in the Dehn group, where \(\theta\) is taken modulo \(2\pi\).

theorem dehnInvariant_replicate (n : ℕ) (e : Edge) :
    dehnInvariant (List.replicate n e) =
      n • (e.length ⊗ₜ[ℤ] (↑e.angle : AddCircle (2 * π)))

Uses 3 · Used by 2

Statement usesDehn group · Edge of a polyhedron · Dehn invariant

Used byThe Dehn invariant of the cube is zero · Nonzero Dehn invariant of the regular tetrahedron, conditional on irrationality

TheoremA \(\mathbb{Q}\)-linear functional separating \(\alpha\) from \(\pi\)#✓fully proved

Let \(\alpha\) be a real number such that \(\alpha / \pi\) is irrational. Then there is a \(\mathbb{Q}\)-linear map \(f : \mathbb{R} \to \mathbb{R}\) with \(f(\pi) = 0\) and \(f(\alpha) \neq 0\).

The idea of the proof: \(\alpha\) lies outside the \(\mathbb{Q}\)-span of \(\pi\), and a linear functional on the quotient separates it.

theorem exists_linearMap_of_irrational {α : ℝ} (hirr : Irrational (α / π)) :
    ∃ f : ℝ →ₗ[ℚ] ℝ, f π = 0 ∧ f α ≠ 0

Used by 1

Used byNonvanishing of an edge term in the Dehn group

TheoremNonvanishing of an edge term in the Dehn group#✓fully proved

Let \(\ell\) and \(\alpha\) be real numbers with \(\ell \neq 0\) and \(\alpha / \pi\) irrational. Then the pure tensor \(\ell \otimes [\alpha]\) is nonzero in the Dehn group \(\mathbb{R} \otimes_{\mathbb{Z}} (\mathbb{R} / 2\pi\mathbb{Z})\), where \([\alpha]\) is the class of \(\alpha\) modulo \(2\pi\).

The proof applies a \(\mathbb{Q}\)-linear functional that vanishes at \(\pi\) but not at \(\alpha\).

theorem tmul_ne_zero_of_irrational {α : ℝ} {ℓ : ℝ}
    (hℓ : ℓ ≠ 0) (hirr : Irrational (α / π)) :
    ℓ ⊗ₜ[ℤ] (↑α : AddCircle (2 * π)) ≠ (0 : DehnGroup)

Uses 2 · Used by 1

Statement usesDehn group

Proof usesA \(\mathbb{Q}\)-linear functional separating \(\alpha\) from \(\pi\)

Used byNonzero Dehn invariant of the regular tetrahedron, conditional on irrationality

TheoremThe Dehn invariant of the cube is zero#✓fully proved

For every real number \(\ell\), the edge list of a cube of side \(\ell\) (twelve edges of length \(\ell\), each with dihedral angle \(\pi / 2\)) has Dehn invariant \(0\).

The reason is that \(12 \cdot (\pi / 2) = 3 \cdot 2\pi\) vanishes in \(\mathbb{R} / 2\pi\mathbb{Z}\).

theorem dehnInvariant_cubeEdges (ℓ : ℝ) : dehnInvariant (cubeEdges ℓ) = 0

Uses 5 · Used by 1

Statement usesDehn group · Edge list of a cube · Dehn invariant

Proof usesEdge of a polyhedron · Dehn invariant of a repeated edge

Used byConditionally, the cube and the regular tetrahedron have different Dehn invariants

TheoremNonzero Dehn invariant of the regular tetrahedron, conditional on irrationality#✓fully proved

Suppose that \(\arccos(1/3) / \pi\) is irrational. Then for every nonzero real number \(\ell\), the edge list of a regular tetrahedron of side \(\ell\) (six edges of length \(\ell\), each with dihedral angle \(\arccos(1/3)\)) has nonzero Dehn invariant.

theorem dehnInvariant_tetrahedronEdges_ne_zero {ℓ : ℝ} (hℓ : ℓ ≠ 0)
    (hirr : Irrational (tetrahedralAngle / π)) :
    dehnInvariant (tetrahedronEdges ℓ) ≠ 0

Uses 7 · Used by 1

Statement usesDehn group · Dehn invariant · Dihedral angle of the regular tetrahedron · Edge list of the regular tetrahedron

Proof usesEdge of a polyhedron · Dehn invariant of a repeated edge · Nonvanishing of an edge term in the Dehn group

Used byConditionally, the cube and the regular tetrahedron have different Dehn invariants

TheoremConditionally, the cube and the regular tetrahedron have different Dehn invariants#✓fully proved

Suppose that \(\arccos(1/3) / \pi\) is irrational. Then for all real numbers \(\ell\) and \(\ell'\) with \(\ell' \ne 0\), the edge list of a cube of side \(\ell\) and the edge list of a regular tetrahedron of side \(\ell'\) have different Dehn invariants.

Since scissors-congruent polyhedra have equal Dehn invariants, under this hypothesis a cube and a regular tetrahedron of equal volume are not scissors-congruent.

theorem dehnInvariant_cube_ne_dehnInvariant_tetrahedron {ℓ ℓ' : ℝ} (hℓ' : ℓ' ≠ 0)
    (hirr : Irrational (tetrahedralAngle / π)) :
    dehnInvariant (cubeEdges ℓ) ≠ dehnInvariant (tetrahedronEdges ℓ')

Uses 7

Statement usesDehn group · Edge list of a cube · Dehn invariant · Dihedral angle of the regular tetrahedron · Edge list of the regular tetrahedron

Proof usesThe Dehn invariant of the cube is zero · Nonzero Dehn invariant of the regular tetrahedron, conditional on irrationality

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.