hex

32.5. Latin-square isotopy as graph isomorphism🔗

The nauty introduction begins from a broad principle: finite objects built from finite sets and relations can often be encoded as coloured graphs. Its Latin-square example asks about isotopy: two squares are isotopic when one can be obtained from the other by independently permuting the rows, the columns, and the symbols.

Before mentioning graphs, we can state that question directly in Lean. We package the Latin property as bijectivity of every row and column, and define isotopy using three independent permutations.

open Hex.GraphIso.Mathlib namespace LatinSquareExample structure LatinSquare where entry : Fin 3 → Fin 3 → Fin 3 rows : ∀ i, Function.Bijective (entry i) columns : ∀ j, Function.Bijective (fun i => entry i j) def Isotopic (L M : LatinSquare) : Prop := ∃ r c s : Equiv.Perm (Fin 3), ∀ i j, M.entry (r i) (c j) = s (L.entry i j)

The introduction illustrates the construction with exactly this square:

1 3 2
2 1 3
3 2 1

The definitions below use the zero-based elements of Fin 3. The second square is obtained by exchanging the first two rows and then exchanging the symbols 1 and 2.

def nautySquare : LatinSquare where entry | 0, 0 => 0 | 0, 1 => 2 | 0, 2 => 1 | 1, 0 => 1 | 1, 1 => 0 | 1, 2 => 2 | 2, 0 => 2 | 2, 1 => 1 | 2, 2 => 0 rows := ⊢ ∀ (i : Fin 3), Function.Bijective fun x => match i, x with | 0, 0 => 0 | 0, 1 => 2 | 0, 2 => 1 | 1, 0 => 1 | 1, 1 => 0 | 1, 2 => 2 | 2, 0 => 2 | 2, 1 => 1 | 2, 2 => 0 All goals completed! 🐙 columns := ⊢ ∀ (j : Fin 3), Function.Bijective fun i => match i, j with | 0, 0 => 0 | 0, 1 => 2 | 0, 2 => 1 | 1, 0 => 1 | 1, 1 => 0 | 1, 2 => 2 | 2, 0 => 2 | 2, 1 => 1 | 2, 2 => 0 All goals completed! 🐙 def cyclicSquare : LatinSquare where entry i j := ⟨(i + j) % 3, i:Fin 3j:Fin 3⊢ (↑i + ↑j) % 3 < 3 All goals completed! 🐙⟩ rows := ⊢ ∀ (i : Fin 3), Function.Bijective fun j => ⟨(↑i + ↑j) % 3, ⋯⟩ All goals completed! 🐙 columns := ⊢ ∀ (j : Fin 3), Function.Bijective fun i => ⟨(↑i + ↑j) % 3, ⋯⟩ All goals completed! 🐙

Following the nauty introduction, we make a graph with four colours of vertices: one vertex for each row, column, symbol, and position. A position vertex is joined to its row, its column, and the symbol written there. The resulting graph has 18 vertices and 27 edges.

inductive Vertex | row : Fin 3 → Vertex | column : Fin 3 → Vertex | symbol : Fin 3 → Vertex | position : Fin 3 × Fin 3 → Vertex deriving DecidableEq, Fintype private def incidence (L : LatinSquare) (x y : Vertex) : Prop := match x, y with | .position (i, _), .row i' => i = i' | .position (_, j), .column j' => j = j' | .position (i, j), .symbol k => L.entry i j = k | _, _ => False private instance (L : LatinSquare) : DecidableRel (incidence L) := fun x y => L:LatinSquarex:Vertexy:Vertex⊢ Decidable (incidence L x y) L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.row a✝) y)L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.column a✝) y)L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝) y)L:LatinSquarey:Vertexa✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.position a✝) y) L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.row a✝) y)L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.column a✝) y)L:LatinSquarey:Vertexa✝:Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝) y)L:LatinSquarey:Vertexa✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.position a✝) y) L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.row a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.column a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.symbol a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.position a✝)) L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.row a✝¹) (Vertex.row a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.row a✝¹) (Vertex.column a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.row a✝¹) (Vertex.symbol a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.row a✝¹) (Vertex.position a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.column a✝¹) (Vertex.row a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.column a✝¹) (Vertex.column a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.column a✝¹) (Vertex.symbol a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.column a✝¹) (Vertex.position a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝¹) (Vertex.row a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝¹) (Vertex.column a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝¹) (Vertex.symbol a✝))L:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.symbol a✝¹) (Vertex.position a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.row a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.column a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.symbol a✝))L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3 × Fin 3⊢ Decidable (incidence L (Vertex.position a✝¹) (Vertex.position a✝)) L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3 × Fin 3⊢ Decidable False L:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3a✝:Fin 3 × Fin 3⊢ Decidable FalseL:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (a✝¹.1 = a✝)L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (a✝¹.2 = a✝)L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3⊢ Decidable (L.entry a✝¹.1 a✝¹.2 = a✝)L:LatinSquarea✝¹:Fin 3 × Fin 3a✝:Fin 3 × Fin 3⊢ Decidable False All goals completed! 🐙 private def graph (L : LatinSquare) : SimpleGraph Vertex := SimpleGraph.fromRel (incidence L) private def color : Vertex → Fin 4 | .row _ => 0 | .column _ => 1 | .symbol _ => 2 | .position _ => 3 def encode (L : LatinSquare) : Hex.GraphIso.Mathlib.Colored Vertex 4 where graph := graph L color := color onto := L:LatinSquare⊢ Function.Surjective color All goals completed! 🐙 private instance (L : LatinSquare) : DecidableRel (encode L).graph.Adj := fun x y => L:LatinSquarex:Vertexy:Vertex⊢ Decidable ((encode L).graph.Adj x y) L:LatinSquarex:Vertexy:Vertex⊢ Decidable (x ≠ y ∧ (incidence L x y ∨ incidence L y x)) All goals completed! 🐙

It remains to justify the reduction. A colour-preserving graph isomorphism restricts to a permutation on each of the row, column, and symbol vertices. The three edges incident to a position vertex then force those permutations to satisfy the isotopy equation. The generic componentPerm extracts all three permutations, keeping the reflection proof itself short.

variable {L M : LatinSquare} private def component : Fin 3 → Fin 3 → Vertex | 0 => Vertex.row | 1 => Vertex.column | 2 => Vertex.symbol private def index : Vertex → Fin 3 | .row i | .column i | .symbol i => i | .position _ => 0 private def componentMap (f : (encode L).Iso (encode M)) (kind i : Fin 3) : Fin 3 := index (f.graphIso (component kind i)) private theorem map_component (f : (encode L).Iso (encode M)) (kind i : Fin 3) : f.graphIso (component kind i) = component kind (componentMap f kind i) := L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3i:Fin 3⊢ f.graphIso (component kind i) = component kind (componentMap f kind i) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3i:Fin 3hc:(encode M).color (f.graphIso (component kind i)) = (encode L).color (component kind i)⊢ f.graphIso (component kind i) = component kind (componentMap f kind i) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3i:Fin 3v:Vertexh:f.graphIso (component kind i) = vhc:(encode M).color v = (encode L).color (component kind i)⊢ v = component kind (componentMap f kind i) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3v:Vertexh:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = vhc:(encode M).color v = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ v = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.row a✝hc:(encode M).color (Vertex.row a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.row a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.column a✝hc:(encode M).color (Vertex.column a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.column a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.symbol a✝hc:(encode M).color (Vertex.symbol a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.symbol a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3 × Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.position a✝hc:(encode M).color (Vertex.position a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.position a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = Vertex.row a✝hc:(encode M).color (Vertex.row a✝) = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ Vertex.row a✝ = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = Vertex.column a✝hc:(encode M).color (Vertex.column a✝) = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ Vertex.column a✝ = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = Vertex.symbol a✝hc:(encode M).color (Vertex.symbol a✝) = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ Vertex.symbol a✝ = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3 × Fin 3h:f.graphIso (component ((fun i => i) ⟨0, ⋯⟩) i) = Vertex.position a✝hc:(encode M).color (Vertex.position a✝) = (encode L).color (component ((fun i => i) ⟨0, ⋯⟩) i)⊢ Vertex.position a✝ = component ((fun i => i) ⟨0, ⋯⟩) (componentMap f ((fun i => i) ⟨0, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = Vertex.row a✝hc:(encode M).color (Vertex.row a✝) = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ Vertex.row a✝ = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = Vertex.column a✝hc:(encode M).color (Vertex.column a✝) = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ Vertex.column a✝ = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = Vertex.symbol a✝hc:(encode M).color (Vertex.symbol a✝) = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ Vertex.symbol a✝ = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3 × Fin 3h:f.graphIso (component ((fun i => i) ⟨1, ⋯⟩) i) = Vertex.position a✝hc:(encode M).color (Vertex.position a✝) = (encode L).color (component ((fun i => i) ⟨1, ⋯⟩) i)⊢ Vertex.position a✝ = component ((fun i => i) ⟨1, ⋯⟩) (componentMap f ((fun i => i) ⟨1, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.row a✝hc:(encode M).color (Vertex.row a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.row a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.column a✝hc:(encode M).color (Vertex.column a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.column a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.symbol a✝hc:(encode M).color (Vertex.symbol a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.symbol a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i)L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3a✝:Fin 3 × Fin 3h:f.graphIso (component ((fun i => i) ⟨2, ⋯⟩) i) = Vertex.position a✝hc:(encode M).color (Vertex.position a✝) = (encode L).color (component ((fun i => i) ⟨2, ⋯⟩) i)⊢ Vertex.position a✝ = component ((fun i => i) ⟨2, ⋯⟩) (componentMap f ((fun i => i) ⟨2, ⋯⟩) i) All goals completed! 🐙 private noncomputable def componentPerm (f : (encode L).Iso (encode M)) (kind : Fin 3) : Equiv.Perm (Fin 3) := Equiv.ofBijective (componentMap f kind) <| L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3⊢ Function.Bijective (componentMap f kind) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3⊢ Function.Injective (componentMap f kind) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3i:Fin 3j:Fin 3h:componentMap f kind i = componentMap f kind j⊢ i = j L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)kind:Fin 3i:Fin 3j:Fin 3h:componentMap f kind i = componentMap f kind jhc:component kind i = component kind j⊢ i = j L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨0, ⋯⟩) i = componentMap f ((fun i => i) ⟨0, ⋯⟩) jhc:component ((fun i => i) ⟨0, ⋯⟩) i = component ((fun i => i) ⟨0, ⋯⟩) j⊢ i = jL:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨1, ⋯⟩) i = componentMap f ((fun i => i) ⟨1, ⋯⟩) jhc:component ((fun i => i) ⟨1, ⋯⟩) i = component ((fun i => i) ⟨1, ⋯⟩) j⊢ i = jL:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨2, ⋯⟩) i = componentMap f ((fun i => i) ⟨2, ⋯⟩) jhc:component ((fun i => i) ⟨2, ⋯⟩) i = component ((fun i => i) ⟨2, ⋯⟩) j⊢ i = j L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨0, ⋯⟩) i = componentMap f ((fun i => i) ⟨0, ⋯⟩) jhc:component ((fun i => i) ⟨0, ⋯⟩) i = component ((fun i => i) ⟨0, ⋯⟩) j⊢ i = jL:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨1, ⋯⟩) i = componentMap f ((fun i => i) ⟨1, ⋯⟩) jhc:component ((fun i => i) ⟨1, ⋯⟩) i = component ((fun i => i) ⟨1, ⋯⟩) j⊢ i = jL:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3h:componentMap f ((fun i => i) ⟨2, ⋯⟩) i = componentMap f ((fun i => i) ⟨2, ⋯⟩) jhc:component ((fun i => i) ⟨2, ⋯⟩) i = component ((fun i => i) ⟨2, ⋯⟩) j⊢ i = j All goals completed! 🐙 private theorem map_entry (f : (encode L).Iso (encode M)) (i j : Fin 3) : M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j) := L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position p⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.row i))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.row i))hc:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.column j))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.row i))hc:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.column j))hs:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.symbol (L.entry i j)))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (Vertex.position p) (component 0 (componentMap f 0 i))hc:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.column j))hs:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.symbol (L.entry i j)))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (Vertex.position p) (component 0 (componentMap f 0 i))hc:(encode M).graph.Adj (Vertex.position p) (component 1 (componentMap f 1 j))hs:(encode M).graph.Adj (f.graphIso (Vertex.position (i, j))) (f.graphIso (Vertex.symbol (L.entry i j)))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:(encode M).graph.Adj (Vertex.position p) (component 0 (componentMap f 0 i))hc:(encode M).graph.Adj (Vertex.position p) (component 1 (componentMap f 1 j))hs:(encode M).graph.Adj (Vertex.position p) (component 2 (componentMap f 2 (L.entry i j)))⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j) L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)i:Fin 3j:Fin 3p:Fin 3 × Fin 3hp:f.graphIso (Vertex.position (i, j)) = Vertex.position phr:p.1 = componentMap f 0 ihc:p.2 = componentMap f 1 jhs:M.entry p.1 p.2 = componentMap f 2 (L.entry i j)⊢ M.entry (componentMap f 0 i) (componentMap f 1 j) = componentMap f 2 (L.entry i j) All goals completed! 🐙 theorem isotopic_of_isomorphic : (encode L).Isomorphic (encode M) → Isotopic L M := L:LatinSquareM:LatinSquare⊢ (encode L).Isomorphic (encode M) → Isotopic L M L:LatinSquareM:LatinSquaref:(encode L).Iso (encode M)⊢ Isotopic L M All goals completed! 🐙

With that bridge established, the promised proof of a statement about Latin squares is just the reduction followed by graph_iso:

example : Isotopic nautySquare cyclicSquare := L:LatinSquareM:LatinSquare⊢ Isotopic nautySquare cyclicSquare L:LatinSquareM:LatinSquare⊢ (encode nautySquare).Isomorphic (encode cyclicSquare) All goals completed! 🐙 end LatinSquareExample

The same encoding turns the automorphism surface into a statement about one square rather than a pair. A colour-preserving automorphism of the incidence graph is an isotopy of the square onto itself, so the group autos reports is the isotopy group. Spelling the encoding out on Colored 18 4 rather than reusing the Vertex type above keeps this example Mathlib-free: vertices 0, 1, 2 are the rows, 3, 4, 5 the columns, 6, 7, 8 the symbols, and 9 + 3 * i + j the position (i, j), each joined to its row, its column and the symbol (i + j) % 3 written there.

namespace LatinAutomorphismExample def incidenceEdges : List (Nat × Nat) := (List.range 3).flatMap fun i => (List.range 3).flatMap fun j => [(i, 9 + 3 * i + j), (3 + j, 9 + 3 * i + j), (6 + (i + j) % 3, 9 + 3 * i + j)] def incidence : Colored 18 4 where graph := (Graph.ofEdges? 18 incidenceEdges).getD (Graph.empty 18) coloring := (Coloring.ofVector? (Hex.Vector.ofFn' fun v => if v.val < 3 then 0 else if v.val < 6 then 1 else if v.val < 9 then 2 else 3)).getD (Coloring.mod 18 4) -- the cyclic square of order three: eighteen isotopies, and four -- orbits, one on each of the rows, the columns, the symbols and the -- positions #guard (autos incidence).order = 18 #guard (autos incidence).numOrbits = 4 #guard (autos incidence).orbits = #[0, 0, 0, 3, 3, 3, 6, 6, 6, 9, 9, 9, 9, 9, 9, 9, 9, 9] example (p : Perm 18) (h : p ∈ (autos incidence).gens) : IsIso incidence incidence p := autos_isIso h end LatinAutomorphismExample

An isotopy is recovered from a generator by reading its action on the three colour classes: the restriction to 0, 1, 2 is the row permutation, the restriction to 3, 4, 5 the column permutation, and the restriction to 6, 7, 8 the symbol permutation. The position class is determined by the other three, which is why the group order counts isotopies and not vertex permutations. The eighteen agree with a direct count: an isotopy of the cyclic square is a triple (α, β, γ) with α i + β j = γ (i + j), forcing α i = a i + p, β j = a j + q and γ k = a k + p + q for a unit a and residues p, q, so there are 2 * 3 * 3 = 18 of them. Each colour class is one orbit, since the translations already act transitively on rows, on columns and on symbols.