Completeness of the six-colour cube varieties

@[reducible, inline]

abbrev MacMahon.NonzeroColour : Type

The six physical face colours; zero is reserved for invalid tableau entries.

Equations

• MacMahon.NonzeroColour = { c : Fin 7 // c ≠ 0 }

def MacMahon.colourEquiv : Fin 6 ≃ NonzeroColour

Identify the six indices with the six nonzero face colours.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MacMahon.Colouring : Type

Arbitrary assignments using each of the six colours exactly once.

Equations

• MacMahon.Colouring = (Fin 6 ≃ MacMahon.NonzeroColour)

@[reducible, inline]

abbrev MacMahon.Variety : Type

The thirty off-diagonal entries of Conway's tableau.

Equations

• MacMahon.Variety = { p : MacMahon.Pair // p.1 ≠ p.2 }

noncomputable def MacMahon.orientedColouring (p : Variety × Fin 24) : Colouring

The face colouring of a tableau variety after a proper rotation.

Equations

• MacMahon.orientedColouring p = Equiv.ofBijective (fun (f : Fin 6) => ⟨MacMahon.faceColours (↑p.1).1 (↑p.1).2 (MacMahon.rotations p.2 f), ⋯⟩) ⋯

theorem MacMahon.orientedColouring_injective : Function.Injective orientedColouring

theorem MacMahon.card_variety : Fintype.card Variety = 30

theorem MacMahon.card_colourings : Fintype.card Colouring = 720

theorem MacMahon.all_colourings : Function.Bijective orientedColouring

Every six-colour face assignment has a unique labelled variety and rotation.