The four colours used in the Sabidussi proof

This file contains the elementary algebra over F₂² used by the proof. We use an explicit product so that the three admissible local frames can be given by concrete formulas.

@[reducible, inline]

abbrev Sabidussi.F₂ : Type

The field with two elements.

Equations

• Sabidussi.F₂ = ZMod 2

@[reducible, inline]

abbrev Sabidussi.Color : Type

The four-element colour space.

Equations

• Sabidussi.Color = (Sabidussi.F₂ × Sabidussi.F₂)

@[simp]

theorem Sabidussi.F₂_add_self (x : F₂) : x + x = 0

@[simp]

theorem Sabidussi.color_add_self (x : Color) : x + x = 0

theorem Sabidussi.F₂_add_shuffle (a b : F₂) : a + (b + (a + b)) = 0

def Sabidussi.bracket (x y : Color) : F₂

The alternating form polarizing quadratic.

Equations

• Sabidussi.bracket x y = x.1 * y.2 + x.2 * y.1

def Sabidussi.quadratic (x : Color) : F₂

The quadratic form detecting the colour (1, 1).

Equations

• Sabidussi.quadratic x = x.1 * x.2

@[simp]

theorem Sabidussi.bracket_apply (x y : Color) : bracket x y = x.1 * y.2 + x.2 * y.1

@[simp]

theorem Sabidussi.quadratic_apply (x : Color) : quadratic x = x.1 * x.2

theorem Sabidussi.bracket_zero_left (x : Color) : bracket 0 x = 0

theorem Sabidussi.bracket_zero_right (x : Color) : bracket x 0 = 0

theorem Sabidussi.bracket_add_left (x y z : Color) : bracket (x + y) z = bracket x z + bracket y z

theorem Sabidussi.bracket_add_right (x y z : Color) : bracket x (y + z) = bracket x y + bracket x z

def Sabidussi.bracketRightHom (x : Color) : Color →+ F₂

Bracketing with a fixed left argument, as an additive homomorphism.

Equations

• Sabidussi.bracketRightHom x = { toFun := Sabidussi.bracket x, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Sabidussi.bracketRightHom_apply (x y : Color) : (bracketRightHom x) y = bracket x y

theorem Sabidussi.sum_bracket_right {I : Type u_1} [Fintype I] (x : Color) (f : I → Color) : ∑ i : I, bracket x (f i) = bracket x (∑ i : I, f i)

theorem Sabidussi.bracket_comm (x y : Color) : bracket x y = bracket y x

theorem Sabidussi.bracket_self (x : Color) : bracket x x = 0

theorem Sabidussi.quadratic_add (x y : Color) : quadratic (x + y) = quadratic x + quadratic y + bracket x y

def Sabidussi.tripleDifference (t : Color) : Fin 3 → Color

The three locally admissible difference vectors at a 6-valent vertex.

Equations

• Sabidussi.tripleDifference t ⟨0, isLt⟩ = t
• Sabidussi.tripleDifference t ⟨1, isLt⟩ = (t.2, t.1 + t.2)
• Sabidussi.tripleDifference t ⟨2, isLt⟩ = (t.1 + t.2, t.1)

@[simp]

theorem Sabidussi.tripleDifference_zero (t : Color) : tripleDifference t 0 = t

@[simp]

theorem Sabidussi.tripleDifference_one (t : Color) : tripleDifference t 1 = (t.2, t.1 + t.2)

@[simp]

theorem Sabidussi.tripleDifference_two (t : Color) : tripleDifference t 2 = (t.1 + t.2, t.1)

theorem Sabidussi.sum_tripleDifference (t : Color) : ∑ i : Fin 3, tripleDifference t i = 0

theorem Sabidussi.tripleDifference_ne_zero (t : Color) (ht : t ≠ 0) (i : Fin 3) : tripleDifference t i ≠ 0

def Sabidussi.doubleDifference (t : Color) : Fin 2 → Color

At a 4-valent vertex the two local differences coincide.

Equations

• Sabidussi.doubleDifference t ⟨0, isLt⟩ = t
• Sabidussi.doubleDifference t ⟨1, isLt⟩ = t

theorem Sabidussi.sum_doubleDifference (t : Color) : ∑ i : Fin 2, doubleDifference t i = 0

theorem Sabidussi.doubleDifference_ne_zero (t : Color) (ht : t ≠ 0) (i : Fin 2) : doubleDifference t i ≠ 0

theorem Sabidussi.double_local_quadratic (t : Color) : (∑ i : Fin 2, quadratic (doubleDifference t i) + ∑ i : Fin 2, ∑ j : Fin 2, if j < i then bracket (doubleDifference t i) (doubleDifference t j) else 0) = 0

The local quadratic contribution from two equal nonzero differences vanishes.

theorem Sabidussi.triple_local_quadratic (t : Color) : (∑ i : Fin 3, quadratic (tripleDifference t i) + ∑ i : Fin 3, ∑ j : Fin 3, if j < i then bracket (tripleDifference t i) (tripleDifference t j) else 0) = 0

The local quadratic contribution from the three tripleDifferences vanishes.