Colour groups of sphere triangulations

DefinitionTriangles of a sphere triangulation#✓fully proved

For a finite simplicial 2-sphere \(X\) in \(\mathbb{R}^3\), the triangles of \(X\) are its faces with exactly three vertices, that is, its 2-dimensional faces.

def triangles (X : FiniteSimplicialSphere 3) : Set (Finset (EuclideanSpace ℝ (Fin 3))) :=
  {t | t ∈ X.K.faces ∧ t.card = 3}

Uses 1 · Used by 3

Statement usesFinite simplicial sphere

Used byColour group of a 2-coloured sphere triangulation · Proper colourings of the triangles of a sphere triangulation · Kourovka Problem 17.35 (statement)

DefinitionProper colourings of the triangles of a sphere triangulation#✓fully proved

Let \(X\) be a finite simplicial 2-sphere in \(\mathbb{R}^3\), and let a colouring assign white or black to every finite set of points of \(\mathbb{R}^3\). The colouring is proper on \(X\) if any two distinct triangles of \(X\) (faces with exactly three vertices) that have exactly two vertices in common receive different colours.

def IsProperTriangleColouring (X : FiniteSimplicialSphere 3)
    (white : Finset (EuclideanSpace ℝ (Fin 3)) → Bool) : Prop :=
  ∀ t ∈ triangles X, ∀ s ∈ triangles X, t ≠ s → (t ∩ s).card = 2 → white t ≠ white s

Uses 2 · Used by 1

Statement usesFinite simplicial sphere · Triangles of a sphere triangulation

Used byKourovka Problem 17.35 (statement)

AbbreviationColour group of a 2-coloured sphere triangulation#✓fully proved

Let \(X\) be a finite simplicial 2-sphere in \(\mathbb{R}^3\), let a colouring assign white or black to every finite set of points of \(\mathbb{R}^3\), and let \(c\) be one of the two colours. The colour group of \(X\) for \(c\) is the abelian group generated by the vertices of \(X\) with the relations \(u + v + w = 0\) for each triangle \(\{u, v, w\}\) of \(X\) (a face with exactly three vertices) of colour \(c\); that is, the free abelian group \(\mathbb{Z}^{(V)}\) on the vertex set \(V\) of \(X\) modulo the subgroup generated by the indicator functions of the triangles of \(X\) of colour \(c\).

abbrev colourGroup (X : FiniteSimplicialSphere 3)
    (white : Finset (EuclideanSpace ℝ (Fin 3)) → Bool) (c : Bool) : Type :=
  (X.K.vertices →₀ ℤ) ⧸ AddSubgroup.closure {f : X.K.vertices →₀ ℤ | ∃ t ∈ triangles X,
    white t = c ∧ ∀ v : X.K.vertices, f v = if (v : EuclideanSpace ℝ (Fin 3)) ∈ t then 1 else 0}

Uses 2 · Used by 1

Statement usesFinite simplicial sphere · Triangles of a sphere triangulation

Used byKourovka Problem 17.35 (statement)

DefinitionKourovka Problem 17.35 (statement)#✓fully proved

The statement that for every finite simplicial 2-sphere \(X\) in \(\mathbb{R}^3\) and every colouring of the finite sets of points of \(\mathbb{R}^3\) white or black such that any two distinct triangles of \(X\) (faces with exactly three vertices) with exactly two vertices in common receive different colours, the groups \(G_W\) and \(G_B\) are isomorphic. Here \(G_W\) is the abelian group generated by the vertices of \(X\) with the relations \(u + v + w = 0\) for each white triangle \(\{u, v, w\}\) of \(X\), and \(G_B\) is defined in the same way from the black triangles.

def sphereTriangulationColourGroupsIso : Prop :=
  ∀ (X : FiniteSimplicialSphere 3) (white : Finset (EuclideanSpace ℝ (Fin 3)) → Bool),
    IsProperTriangleColouring X white →
      Nonempty (colourGroup X white true ≃+ colourGroup X white false)

Uses 4 · Used by 1

Statement usesFinite simplicial sphere · Proper colourings of the triangles of a sphere triangulation · Colour group of a 2-coloured sphere triangulation · Triangles of a sphere triangulation

Used byBlackburn–McCourt theorem (Kourovka Problem 17.35)

TheoremBlackburn–McCourt theorem (Kourovka Problem 17.35)#●ready to prove

Let \(X\) be a finite simplicial 2-sphere in \(\mathbb{R}^3\), and let a colouring assign white or black to every finite set of points of \(\mathbb{R}^3\) so that any two distinct triangles of \(X\) (faces with exactly three vertices) with exactly two vertices in common receive different colours. Let \(G_W\) be the abelian group generated by the vertices of \(X\) with the relations \(u + v + w = 0\) for each white triangle \(\{u, v, w\}\) of \(X\), and let \(G_B\) be defined in the same way from the black triangles. Then \(G_W\) and \(G_B\) are isomorphic.

public theorem_wanted sphereTriangulationColourGroupsIso_holds : sphereTriangulationColourGroupsIso

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 17.35 (I. M. Wanless, N. J. Cavenagh); resolution: S. R. Blackburn and T. A. McCourt, Triangulations of the sphere, bitrades and abelian groups, Combinatorica 34 (2014), 527-546, Theorem 1 (for any finite triangulation of the sphere with properly black-white coloured faces, A_W ≅ A_B); Kourovka Archive, Problem 17.35 (Conjecture is proved), https://arxiv.org/abs/1112.5423.

Uses 1

Statement usesKourovka Problem 17.35 (statement)

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.