diff --git a/Archive.lean b/Archive.lean index 8ca03e8bc806d9..1b282c6a2ddf5d 100644 --- a/Archive.lean +++ b/Archive.lean @@ -61,6 +61,8 @@ import Archive.Imo.Imo2024Q5 import Archive.Imo.Imo2024Q6 import Archive.Imo.Imo2025Q3 import Archive.Kuratowski +import Archive.LangerGraph +import Archive.PrimitiveGraphs import Archive.MinimalSheffer import Archive.MiuLanguage.Basic import Archive.MiuLanguage.DecisionNec diff --git a/Archive/LangerGraph.lean b/Archive/LangerGraph.lean new file mode 100644 index 00000000000000..9d3e87c814c5f8 --- /dev/null +++ b/Archive/LangerGraph.lean @@ -0,0 +1,536 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +import Mathlib.Data.ZMod.Basic +import Mathlib.Data.Matrix.Basic +import Mathlib.Data.Fin.VecNotation +import Mathlib.Combinatorics.SimpleGraph.Basic +import Mathlib.Combinatorics.SimpleGraph.Action +import Mathlib.Combinatorics.SimpleGraph.Representation + +/-! +# The Langer graph, the Tutte 12-cage, and the GH(2,2) ecosystem + +The **Langer graph** is the collinearity graph of the split Cayley hexagon GH(2,2), +the unique generalized 6-gon over 𝔽₂. It has 63 vertices (the points of the parabolic +quadric Q(6,2) in PG(6,2)), is 6-regular with 189 edges, and is the unique +distance-regular graph with intersection array {6, 4, 4; 1, 1, 3}. + +The **Tutte 12-cage** is the incidence graph of GH(2,2): 126 vertices +(63 points + 63 lines), 189 edges, girth 12. It is semisymmetric — edge-transitive +but not vertex-transitive — because no polarity exists for GH(2,2) over 𝔽₂. + +The main result `langer_eq_tutte12_distance2` proves that the Langer graph (defined +algebraically via the Zorn product on Q(6,2)) equals the distance-2 graph of the +Tutte 12-cage restricted to points (defined combinatorially from the edge list). +The proof uses G₂(2) transitivity: both graphs are invariant under two generators +of G₂(2), so they agree everywhere if they agree at vertex 0. + +## Main definitions + +* `langerSimpleGraph` — the Langer graph on `Fin 63`, via Zorn product +* `tutte12CageGraph` — the Tutte 12-cage on `Fin 126`, via edge list +* `Q62form` — the quadratic form Q(x) = x₀x₄ + x₁x₅ + x₂x₆ + x₃² on 𝔽₂⁷ +* `Q62_H` — the 7 × 63 parity-check matrix from Q(6,2) + +## Main results + +* `Q62_self_orthogonal` — H · Hᵀ = 0 over 𝔽₂ +* `langer_regular` — the Langer graph is 6-regular +* `tutte12_bipartite` — the Tutte 12-cage is bipartite +* `langer_eq_tutte12_distance2'` — algebraic Langer = geometric distance-2 + (structural proof via G₂(2) transitivity) + +## Visualizations + +* [The Langer graph](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/langer-63v.jpg) — symmetry-aware drawing with 6-fold rotational layout +* [The Tutte 12-cage](https://raw.githubusercontent.com/RaggedR/symmetric-graphs/main/lean/named_graphs/tutte-12cage.jpg) — incidence graph of GH(2,2) + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798 +* Benson, *Minimal regular graphs of girth 8 and 12*, Canad. J. Math. 18 (1966) +* Springer–Veldkamp, *Octonions, Jordan Algebras and Exceptional Groups*, §1.8 +-/ + +set_option linter.style.nativeDecide false + +open Matrix + +/-! ## Part 1: The quadratic form Q(6,2) -/ + +/-- The quadratic form Q(x) = x₀x₄ + x₁x₅ + x₂x₆ + x₃² on 𝔽₂⁷. +Points of Q(6,2) are the nonzero vectors with Q(x) = 0. -/ +def Q62form (x : Fin 7 → ZMod 2) : ZMod 2 := + x 0 * x 4 + x 1 * x 5 + x 2 * x 6 + x 3 * x 3 + +/-- Convert a natural number (1..127) to its bit vector in 𝔽₂⁷. -/ +def toBitVec (n : Fin 128) : Fin 7 → ZMod 2 := + fun i => if n.val / (2 ^ i.val) % 2 = 0 then 0 else 1 + +/-- The list of indices (1..127) whose bit vectors lie on Q(6,2). -/ +def q62Indices : List (Fin 128) := + (List.finRange 128).tail.filter fun n => Q62form (toBitVec n) = 0 + +/-- Q(6,2) has exactly 63 points. -/ +theorem q62_card : q62Indices.length = 63 := by native_decide + +/-- Get the n-th point of Q(6,2) (as an index into Fin 128). -/ +def q62Point (j : Fin 63) : Fin 128 := + q62Indices.get (j.cast (by native_decide)) + +/-- The parity-check matrix: H[i][j] = (j-th Q(6,2) point)[i-th coordinate]. -/ +def Q62_H : Matrix (Fin 7) (Fin 63) (ZMod 2) := + fun i j => toBitVec (q62Point j) i + +/-- **Self-orthogonality of Q(6,2)**: H · Hᵀ = 0 over 𝔽₂. +The CSS condition: the code C = ker(H) contains its dual C⊥ = rowspan(H). -/ +theorem Q62_self_orthogonal : Q62_H * Q62_Hᵀ = (0 : Matrix (Fin 7) (Fin 7) (ZMod 2)) := by + native_decide + +/-! ## Part 2: The Langer graph via Zorn product -/ + +/-- Adjacency test for the Langer graph via the Zorn product criterion. +Returns `true` iff `i ≠ j` and all eight entries of M_x · M_y vanish, +where M_x is the Zorn vector matrix of the split octonion algebra over 𝔽₂. -/ +def langerAdjBool (i j : Fin 63) : Bool := + if i == j then false else + let x := toBitVec (q62Point i) + let y := toBitVec (q62Point j) + let α := x 3; let γ := y 3 + (α * γ + x 0 * y 4 + x 1 * y 5 + x 2 * y 6 == 0) && + (α * γ + x 4 * y 0 + x 5 * y 1 + x 6 * y 2 == 0) && + (γ * x 0 + α * y 0 + x 5 * y 6 + x 6 * y 5 == 0) && + (γ * x 1 + α * y 1 + x 6 * y 4 + x 4 * y 6 == 0) && + (γ * x 2 + α * y 2 + x 4 * y 5 + x 5 * y 4 == 0) && + (γ * x 4 + α * y 4 + x 1 * y 2 + x 2 * y 1 == 0) && + (γ * x 5 + α * y 5 + x 2 * y 0 + x 0 * y 2 == 0) && + (γ * x 6 + α * y 6 + x 0 * y 1 + x 1 * y 0 == 0) + +/-- The **Langer graph**: collinearity graph of the split Cayley hexagon GH(2,2) +on the 63 points of Q(6,2). 6-regular, 189 edges, distance-regular with +intersection array {6, 4, 4; 1, 1, 3}. Aut ≅ G₂(2) of order 12096. -/ +def langerSimpleGraph : SimpleGraph (Fin 63) where + Adj i j := langerAdjBool i j + symm i j := by simp only [langerAdjBool]; revert i j; native_decide + loopless := ⟨fun i => by simp only [langerAdjBool]; revert i; native_decide⟩ + +instance langerDecAdj : DecidableRel langerSimpleGraph.Adj := + fun i j => inferInstanceAs (Decidable (langerAdjBool i j)) + +/-- The Langer graph is 6-regular. -/ +theorem langer_regular : + ∀ v : Fin 63, (Finset.univ.filter fun w => langerSimpleGraph.Adj v w).card = 6 := by + native_decide + +/-- The Langer graph has 189 undirected edges. -/ +theorem langer_edges : + (Finset.univ.filter fun p : Fin 63 × Fin 63 => + p.1 < p.2 ∧ langerSimpleGraph.Adj p.1 p.2).card = 189 := by + native_decide + +/-! ## Part 3: The Tutte 12-cage -/ + +/-- Edge list for the Tutte 12-cage (189 edges, 0-indexed). +Vertices 0–62 are points of GH(2,2), vertices 63–125 are lines. +Every edge connects a point to a line (bipartite). -/ +private def tutte12Edges : Array (Fin 126 × Fin 126) := #[ + (0,63), (0,64), (0,65), (1,66), (1,67), (1,68), + (2,69), (2,70), (2,71), (3,72), (3,73), (3,74), + (4,75), (4,76), (4,77), (5,78), (5,79), (5,80), + (6,81), (6,82), (6,83), (7,66), (7,72), (7,78), + (8,66), (8,84), (8,85), (9,72), (9,86), (9,87), + (10,78), (10,88), (10,89), (11,90), (11,91), (11,92), + (12,93), (12,94), (12,95), (13,96), (13,97), (13,98), + (14,99), (14,100), (14,101), (15,63), (15,73), (15,75), + (16,63), (16,102), (16,103), (17,73), (17,90), (17,96), + (18,75), (18,104), (18,105), (19,86), (19,106), (19,107), + (20,99), (20,108), (20,109), (21,87), (21,110), (21,111), + (22,93), (22,112), (22,113), (23,69), (23,74), (23,81), + (24,69), (24,114), (24,115), (25,74), (25,93), (25,99), + (26,81), (26,116), (26,117), (27,96), (27,118), (27,119), + (28,87), (28,120), (28,121), (29,90), (29,122), (29,123), + (30,86), (30,124), (30,125), (31,64), (31,67), (31,70), + (32,64), (32,106), (32,108), (33,67), (33,91), (33,94), + (34,70), (34,118), (34,120), (35,84), (35,102), (35,114), + (36,100), (36,103), (36,124), (37,85), (37,112), (37,122), + (38,97), (38,110), (38,115), (39,68), (39,76), (39,82), + (40,68), (40,97), (40,100), (41,76), (41,107), (41,113), + (42,82), (42,121), (42,123), (43,94), (43,104), (43,125), + (44,91), (44,111), (44,116), (45,85), (45,105), (45,117), + (46,84), (46,109), (46,119), (47,65), (47,79), (47,83), + (48,65), (48,110), (48,112), (49,79), (49,92), (49,101), + (50,83), (50,119), (50,125), (51,88), (51,108), (51,123), + (52,98), (52,106), (52,117), (53,89), (53,103), (53,116), + (54,95), (54,102), (54,121), (55,71), (55,77), (55,80), + (56,71), (56,122), (56,124), (57,77), (57,109), (57,111), + (58,80), (58,95), (58,98), (59,101), (59,105), (59,120), + (60,89), (60,113), (60,118), (61,88), (61,104), (61,115), + (62,92), (62,107), (62,114)] + +private def tutte12AdjBool (u v : Fin 126) : Bool := + tutte12Edges.any fun (a, b) => (u == a && v == b) || (u == b && v == a) + +/-- The **Tutte 12-cage**: incidence graph of GH(2,2) on 126 vertices. +3-regular, 189 edges, girth 12. Semisymmetric (edge-transitive, not vertex-transitive). -/ +def tutte12CageGraph : SimpleGraph (Fin 126) where + Adj u v := tutte12AdjBool u v + symm u v := by simp only [tutte12AdjBool]; revert u v; native_decide + loopless := ⟨fun u => by simp only [tutte12AdjBool]; revert u; native_decide⟩ + +instance tutte12DecAdj : DecidableRel tutte12CageGraph.Adj := + fun u v => inferInstanceAs (Decidable (tutte12AdjBool u v)) + +/-- The Tutte 12-cage is 3-regular. -/ +theorem tutte12_regular : + ∀ v : Fin 126, (Finset.univ.filter fun w => tutte12CageGraph.Adj v w).card = 3 := by + native_decide + +/-- The bipartition: point (< 63) or line (≥ 63). -/ +def tutte12Side (v : Fin 126) : Fin 2 := + if v.val < 63 then 0 else 1 + +/-- The Tutte 12-cage is bipartite: every edge connects a point to a line. -/ +theorem tutte12_bipartite : + ∀ u v : Fin 126, tutte12CageGraph.Adj u v → tutte12Side u ≠ tutte12Side v := by + native_decide + +/-! ## Part 4: Distance-2 adjacency on points -/ + +/-- Distance-2 adjacency on points: p ~ q iff they share a line vertex +in the Tutte 12-cage. -/ +def tutte12Distance2Bool (p q : Fin 63) : Bool := + p != q && + let pv : Fin 126 := ⟨p.val, by omega⟩ + let qv : Fin 126 := ⟨q.val, by omega⟩ + (List.finRange 63).any fun l => + let lv : Fin 126 := ⟨l.val + 63, by omega⟩ + tutte12AdjBool pv lv && tutte12AdjBool qv lv + +/-! ## Part 5: G₂(2) generators and invariance -/ + +private def g2gen1Fwd : Array (Fin 63) := #[ + ⟨1, by omega⟩, ⟨3, by omega⟩, ⟨5, by omega⟩, ⟨2, by omega⟩, ⟨0, by omega⟩, + ⟨6, by omega⟩, ⟨4, by omega⟩, ⟨23, by omega⟩, ⟨25, by omega⟩, ⟨24, by omega⟩, + ⟨26, by omega⟩, ⟨28, by omega⟩, ⟨30, by omega⟩, ⟨27, by omega⟩, ⟨29, by omega⟩, + ⟨31, by omega⟩, ⟨33, by omega⟩, ⟨34, by omega⟩, ⟨32, by omega⟩, ⟨35, by omega⟩, + ⟨37, by omega⟩, ⟨38, by omega⟩, ⟨36, by omega⟩, ⟨55, by omega⟩, ⟨58, by omega⟩, + ⟨56, by omega⟩, ⟨57, by omega⟩, ⟨60, by omega⟩, ⟨61, by omega⟩, ⟨59, by omega⟩, + ⟨62, by omega⟩, ⟨7, by omega⟩, ⟨8, by omega⟩, ⟨9, by omega⟩, ⟨10, by omega⟩, + ⟨12, by omega⟩, ⟨11, by omega⟩, ⟨14, by omega⟩, ⟨13, by omega⟩, ⟨15, by omega⟩, + ⟨17, by omega⟩, ⟨16, by omega⟩, ⟨18, by omega⟩, ⟨19, by omega⟩, ⟨21, by omega⟩, + ⟨20, by omega⟩, ⟨22, by omega⟩, ⟨39, by omega⟩, ⟨40, by omega⟩, ⟨42, by omega⟩, + ⟨41, by omega⟩, ⟨45, by omega⟩, ⟨46, by omega⟩, ⟨44, by omega⟩, ⟨43, by omega⟩, + ⟨47, by omega⟩, ⟨49, by omega⟩, ⟨48, by omega⟩, ⟨50, by omega⟩, ⟨51, by omega⟩, + ⟨53, by omega⟩, ⟨52, by omega⟩, ⟨54, by omega⟩] + +private def g2gen1Inv : Array (Fin 63) := #[ + ⟨4, by omega⟩, ⟨0, by omega⟩, ⟨3, by omega⟩, ⟨1, by omega⟩, ⟨6, by omega⟩, + ⟨2, by omega⟩, ⟨5, by omega⟩, ⟨31, by omega⟩, ⟨32, by omega⟩, ⟨33, by omega⟩, + ⟨34, by omega⟩, ⟨36, by omega⟩, ⟨35, by omega⟩, ⟨38, by omega⟩, ⟨37, by omega⟩, + ⟨39, by omega⟩, ⟨41, by omega⟩, ⟨40, by omega⟩, ⟨42, by omega⟩, ⟨43, by omega⟩, + ⟨45, by omega⟩, ⟨44, by omega⟩, ⟨46, by omega⟩, ⟨7, by omega⟩, ⟨9, by omega⟩, + ⟨8, by omega⟩, ⟨10, by omega⟩, ⟨13, by omega⟩, ⟨11, by omega⟩, ⟨14, by omega⟩, + ⟨12, by omega⟩, ⟨15, by omega⟩, ⟨18, by omega⟩, ⟨16, by omega⟩, ⟨17, by omega⟩, + ⟨19, by omega⟩, ⟨22, by omega⟩, ⟨20, by omega⟩, ⟨21, by omega⟩, ⟨47, by omega⟩, + ⟨48, by omega⟩, ⟨50, by omega⟩, ⟨49, by omega⟩, ⟨54, by omega⟩, ⟨53, by omega⟩, + ⟨51, by omega⟩, ⟨52, by omega⟩, ⟨55, by omega⟩, ⟨57, by omega⟩, ⟨56, by omega⟩, + ⟨58, by omega⟩, ⟨59, by omega⟩, ⟨61, by omega⟩, ⟨60, by omega⟩, ⟨62, by omega⟩, + ⟨23, by omega⟩, ⟨25, by omega⟩, ⟨26, by omega⟩, ⟨24, by omega⟩, ⟨29, by omega⟩, + ⟨27, by omega⟩, ⟨28, by omega⟩, ⟨30, by omega⟩] + +private def g2gen2Fwd : Array (Fin 63) := #[ + ⟨10, by omega⟩, ⟨20, by omega⟩, ⟨29, by omega⟩, ⟨49, by omega⟩, ⟨55, by omega⟩, + ⟨36, by omega⟩, ⟨44, by omega⟩, ⟨14, by omega⟩, ⟨25, by omega⟩, ⟨59, by omega⟩, + ⟨40, by omega⟩, ⟨0, by omega⟩, ⟨19, by omega⟩, ⟨50, by omega⟩, ⟨35, by omega⟩, + ⟨5, by omega⟩, ⟨7, by omega⟩, ⟨47, by omega⟩, ⟨58, by omega⟩, ⟨18, by omega⟩, + ⟨24, by omega⟩, ⟨34, by omega⟩, ⟨41, by omega⟩, ⟨11, by omega⟩, ⟨17, by omega⟩, + ⟨62, by omega⟩, ⟨33, by omega⟩, ⟨6, by omega⟩, ⟨28, by omega⟩, ⟨48, by omega⟩, + ⟨45, by omega⟩, ⟨51, by omega⟩, ⟨61, by omega⟩, ⟨32, by omega⟩, ⟨42, by omega⟩, + ⟨3, by omega⟩, ⟨8, by omega⟩, ⟨22, by omega⟩, ⟨27, by omega⟩, ⟨57, by omega⟩, + ⟨46, by omega⟩, ⟨4, by omega⟩, ⟨21, by omega⟩, ⟨52, by omega⟩, ⟨31, by omega⟩, + ⟨12, by omega⟩, ⟨23, by omega⟩, ⟨53, by omega⟩, ⟨60, by omega⟩, ⟨16, by omega⟩, + ⟨26, by omega⟩, ⟨38, by omega⟩, ⟨43, by omega⟩, ⟨1, by omega⟩, ⟨9, by omega⟩, + ⟨56, by omega⟩, ⟨37, by omega⟩, ⟨2, by omega⟩, ⟨30, by omega⟩, ⟨54, by omega⟩, + ⟨39, by omega⟩, ⟨13, by omega⟩, ⟨15, by omega⟩] + +private def g2gen2Inv : Array (Fin 63) := #[ + ⟨11, by omega⟩, ⟨53, by omega⟩, ⟨57, by omega⟩, ⟨35, by omega⟩, ⟨41, by omega⟩, + ⟨15, by omega⟩, ⟨27, by omega⟩, ⟨16, by omega⟩, ⟨36, by omega⟩, ⟨54, by omega⟩, + ⟨0, by omega⟩, ⟨23, by omega⟩, ⟨45, by omega⟩, ⟨61, by omega⟩, ⟨7, by omega⟩, + ⟨62, by omega⟩, ⟨49, by omega⟩, ⟨24, by omega⟩, ⟨19, by omega⟩, ⟨12, by omega⟩, + ⟨1, by omega⟩, ⟨42, by omega⟩, ⟨37, by omega⟩, ⟨46, by omega⟩, ⟨20, by omega⟩, + ⟨8, by omega⟩, ⟨50, by omega⟩, ⟨38, by omega⟩, ⟨28, by omega⟩, ⟨2, by omega⟩, + ⟨58, by omega⟩, ⟨44, by omega⟩, ⟨33, by omega⟩, ⟨26, by omega⟩, ⟨21, by omega⟩, + ⟨14, by omega⟩, ⟨5, by omega⟩, ⟨56, by omega⟩, ⟨51, by omega⟩, ⟨60, by omega⟩, + ⟨10, by omega⟩, ⟨22, by omega⟩, ⟨34, by omega⟩, ⟨52, by omega⟩, ⟨6, by omega⟩, + ⟨30, by omega⟩, ⟨40, by omega⟩, ⟨17, by omega⟩, ⟨29, by omega⟩, ⟨3, by omega⟩, + ⟨13, by omega⟩, ⟨31, by omega⟩, ⟨43, by omega⟩, ⟨47, by omega⟩, ⟨59, by omega⟩, + ⟨4, by omega⟩, ⟨55, by omega⟩, ⟨39, by omega⟩, ⟨18, by omega⟩, ⟨9, by omega⟩, + ⟨48, by omega⟩, ⟨32, by omega⟩, ⟨25, by omega⟩] + +private theorem g2gen1Fwd_size : g2gen1Fwd.size = 63 := by native_decide +private theorem g2gen1Inv_size : g2gen1Inv.size = 63 := by native_decide +private theorem g2gen2Fwd_size : g2gen2Fwd.size = 63 := by native_decide +private theorem g2gen2Inv_size : g2gen2Inv.size = 63 := by native_decide + +/-- First generator of G₂(2): order 7, from companion matrix of x³ + x + 1. -/ +def g2gen1 : Equiv.Perm (Fin 63) where + toFun i := g2gen1Fwd[i.val]'(by have := g2gen1Fwd_size; omega) + invFun i := g2gen1Inv[i.val]'(by have := g2gen1Inv_size; omega) + left_inv := by intro i; revert i; native_decide + right_inv := by intro i; revert i; native_decide + +/-- Second generator of G₂(2): order 6, maps vertex 0 → 10. -/ +def g2gen2 : Equiv.Perm (Fin 63) where + toFun i := g2gen2Fwd[i.val]'(by have := g2gen2Fwd_size; omega) + invFun i := g2gen2Inv[i.val]'(by have := g2gen2Inv_size; omega) + left_inv := by intro i; revert i; native_decide + right_inv := by intro i; revert i; native_decide + +/-- σ₁ preserves Langer adjacency. -/ +theorem g2gen1_langer_inv : + ∀ i j : Fin 63, + langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (g2gen1 i) (g2gen1 j) := by + native_decide + +/-- σ₂ preserves Langer adjacency. -/ +theorem g2gen2_langer_inv : + ∀ i j : Fin 63, + langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (g2gen2 i) (g2gen2 j) := by + native_decide + +/-- σ₁ preserves distance-2 adjacency. -/ +theorem g2gen1_dist2_inv : + ∀ p q : Fin 63, + tutte12Distance2Bool p q = tutte12Distance2Bool (g2gen1 p) (g2gen1 q) := by + native_decide + +/-- σ₂ preserves distance-2 adjacency. -/ +theorem g2gen2_dist2_inv : + ∀ p q : Fin 63, + tutte12Distance2Bool p q = tutte12Distance2Bool (g2gen2 p) (g2gen2 q) := by + native_decide + +/-! ## Part 6: Word induction (structural, no native_decide) -/ + +/-- The four generator actions: σ₁, σ₁⁻¹, σ₂, σ₂⁻¹. -/ +def applyGen : Fin 4 → Equiv.Perm (Fin 63) + | 0 => g2gen1 + | 1 => g2gen1.symm + | 2 => g2gen2 + | 3 => g2gen2.symm + +/-- Apply a generator word (left-to-right). -/ +def applyWord : List (Fin 4) → Equiv.Perm (Fin 63) + | [] => Equiv.refl _ + | g :: gs => (applyGen g).trans (applyWord gs) + +private theorem symm_preserves_langer (σ : Equiv.Perm (Fin 63)) + (h : ∀ i j : Fin 63, + langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (σ i) (σ j)) + (i j : Fin 63) : + langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (σ.symm i) (σ.symm j) := by + have := h (σ.symm i) (σ.symm j) + simp only [Equiv.apply_symm_apply] at this + exact this.symm + +private theorem applyGen_langer_inv (g : Fin 4) (i j : Fin 63) : + langerSimpleGraph.Adj i j ↔ langerSimpleGraph.Adj (applyGen g i) (applyGen g j) := by + fin_cases g <;> simp only [applyGen] + · exact g2gen1_langer_inv i j + · exact symm_preserves_langer g2gen1 (g2gen1_langer_inv) i j + · exact g2gen2_langer_inv i j + · exact symm_preserves_langer g2gen2 (g2gen2_langer_inv) i j + +/-- Any generator word preserves Langer adjacency (structural induction). -/ +theorem applyWord_langer_inv (w : List (Fin 4)) : + ∀ i j : Fin 63, langerSimpleGraph.Adj i j ↔ + langerSimpleGraph.Adj (applyWord w i) (applyWord w j) := by + induction w with + | nil => intro i j; simp [applyWord] + | cons g gs ih => + intro i j + simp only [applyWord, Equiv.trans_apply] + rw [applyGen_langer_inv g i j] + exact ih (applyGen g i) (applyGen g j) + +private theorem symm_preserves_dist2 (σ : Equiv.Perm (Fin 63)) + (h : ∀ p q : Fin 63, tutte12Distance2Bool p q = tutte12Distance2Bool (σ p) (σ q)) + (p q : Fin 63) : + tutte12Distance2Bool p q = tutte12Distance2Bool (σ.symm p) (σ.symm q) := by + have := h (σ.symm p) (σ.symm q) + simp only [Equiv.apply_symm_apply] at this + exact this.symm + +private theorem applyGen_dist2_inv (g : Fin 4) (p q : Fin 63) : + tutte12Distance2Bool p q = tutte12Distance2Bool (applyGen g p) (applyGen g q) := by + fin_cases g <;> simp only [applyGen] + · exact g2gen1_dist2_inv p q + · exact symm_preserves_dist2 g2gen1 (g2gen1_dist2_inv) p q + · exact g2gen2_dist2_inv p q + · exact symm_preserves_dist2 g2gen2 (g2gen2_dist2_inv) p q + +/-- Any generator word preserves distance-2 adjacency (structural induction). -/ +theorem applyWord_dist2_inv (w : List (Fin 4)) : + ∀ p q : Fin 63, tutte12Distance2Bool p q = + tutte12Distance2Bool (applyWord w p) (applyWord w q) := by + induction w with + | nil => intro p q; simp [applyWord] + | cons g gs ih => + intro p q + simp only [applyWord, Equiv.trans_apply] + rw [applyGen_dist2_inv g p q] + exact ih (applyGen g p) (applyGen g q) + +/-! ## Part 7: Transitivity witnesses and main theorem -/ + +private def witnessWordData : Array (List (Fin 4)) := #[ + [], [0], [0,0,0], [0,0], [1], + [1,1,1], [1,1], [3,3,1], [3,1,2], [0,2,2,1], + [2], [3], [0,0,3,0], [1,1,3,1], [0,0,3,3], + [1,1,1,3], [1,3,0], [2,1,1], [2,1,2,0], [0,0,3,1], + [0,2], [2,1,3], [1,3,3], [3,3], [0,2,2], + [1,2,2,1], [2,0], [1,1,3], [3,0], [0,0,0,2], + [0,2,1,3], [0,3,0,2], [2,0,2,2], [2,0,2], [2,1], + [0,0,3], [3,1], [0,2,0], [1,1,3,3], [0,3,1,2], + [2,2], [1,3], [2,1,2], [0,0,3,1,1], [0,3,0], + [0,2,1], [2,2,2], [0,3,3], [2,2,1], [0,0,2], + [1,3,1], [0,2,1,1], [2,2,2,1], [0,3], [0,2,2,1,3], + [1,2], [1,2,2], [2,0,0], [0,2,2,0], [0,0,0,2,0], + [0,3,1], [3,0,0], [0,2,1,3,0]] + +private theorem witnessWordData_size : witnessWordData.size = 63 := by native_decide + +/-- BFS witness words: `witnessWord v` is a generator word mapping 0 → v. -/ +def witnessWord (v : Fin 63) : List (Fin 4) := + witnessWordData[v.val]'(by have := witnessWordData_size; omega) + +/-- Each witness word correctly maps 0 to its target vertex. -/ +theorem witnessWord_correct : + ∀ v : Fin 63, applyWord (witnessWord v) 0 = v := by + native_decide + +/-- The Langer graph and distance-2 graph agree at vertex 0. -/ +theorem graphs_agree_at_zero : + ∀ v : Fin 63, + langerSimpleGraph.Adj 0 v ↔ (tutte12Distance2Bool 0 v = true) := by + native_decide + +private theorem transport_langer (w : List (Fin 4)) (q : Fin 63) : + langerSimpleGraph.Adj (applyWord w 0) q ↔ + langerSimpleGraph.Adj 0 ((applyWord w).symm q) := by + conv_lhs => rw [← Equiv.apply_symm_apply (applyWord w) q] + exact ((applyWord_langer_inv w) 0 ((applyWord w).symm q)).symm + +private theorem transport_dist2 (w : List (Fin 4)) (q : Fin 63) : + tutte12Distance2Bool (applyWord w 0) q = + tutte12Distance2Bool 0 ((applyWord w).symm q) := by + conv_lhs => rw [← Equiv.apply_symm_apply (applyWord w) q] + exact ((applyWord_dist2_inv w) 0 ((applyWord w).symm q)).symm + +/-- **The Langer graph equals the distance-2 graph of the Tutte 12-cage +restricted to points** — proved structurally via G₂(2) transitivity. + +The argument: +1. Let σ = applyWord (witnessWord p), so σ(0) = p +2. Adj p q ↔ Adj 0 (σ⁻¹ q) [by transport_langer] +3. dist2 p q = dist2 0 (σ⁻¹ q) [by transport_dist2] +4. Adj 0 (σ⁻¹ q) ↔ dist2 0 (σ⁻¹ q) [by graphs_agree_at_zero] -/ +theorem langer_eq_tutte12_distance2' : + ∀ p q : Fin 63, + langerSimpleGraph.Adj p q ↔ (tutte12Distance2Bool p q = true) := by + intro p q + rw [← witnessWord_correct p] + rw [transport_langer, transport_dist2] + exact graphs_agree_at_zero _ + +/-! ## The Langer graph is a Sabidussi coset graph + +G₂(2) = ⟨σ₁, σ₂⟩ acts vertex-transitively on the 63 points of GH(2,2), +so by the Sabidussi representation theorem: + `langerSimpleGraph ≃g cosetGraph(Stab_G₂(0), connectionSet G₂ langer 0)` -/ + +/-- The two G₂(2) generators as a `Fin 2`-indexed family. -/ +def langerGens : Fin 2 → Equiv.Perm (Fin 63) + | 0 => g2gen1 + | 1 => g2gen2 + +/-- G₂(2) as a subgroup of Sym(63), generated by σ₁ and σ₂. -/ +def langerG : Subgroup (Equiv.Perm (Fin 63)) := + Subgroup.closure (Set.range langerGens) + +private theorem applyGen_mem (i : Fin 4) : applyGen i ∈ langerG := by + unfold langerG + match i with + | 0 => exact Subgroup.subset_closure ⟨0, rfl⟩ + | 1 => exact Subgroup.inv_mem _ (Subgroup.subset_closure ⟨0, rfl⟩) + | 2 => exact Subgroup.subset_closure ⟨1, rfl⟩ + | 3 => exact Subgroup.inv_mem _ (Subgroup.subset_closure ⟨1, rfl⟩) + +private theorem applyWord_mem (w : List (Fin 4)) : applyWord w ∈ langerG := by + induction w with + | nil => exact Subgroup.one_mem _ + | cons i rest ih => exact langerG.mul_mem ih (applyGen_mem i) + +noncomputable instance langerMulAction : MulAction langerG (Fin 63) := + MulAction.compHom (Fin 63) langerG.subtype + +noncomputable instance langerGraphAction : + GraphAction langerG (Fin 63) langerSimpleGraph where + adj_smul := by + intro ⟨σ, hσ⟩ u v hadj + change langerSimpleGraph.Adj (σ u) (σ v) + revert u v; change ∀ u v, langerSimpleGraph.Adj u v → langerSimpleGraph.Adj (σ u) (σ v) + refine Subgroup.closure_induction + (p := fun σ _ => ∀ u v, langerSimpleGraph.Adj u v → langerSimpleGraph.Adj (σ u) (σ v)) + ?_ ?_ ?_ ?_ hσ + · intro x ⟨i, hi⟩; subst hi + match i with + | 0 => exact fun u v h => (g2gen1_langer_inv u v).mp h + | 1 => exact fun u v h => (g2gen2_langer_inv u v).mp h + · intro u v h; simpa + · intro x y _ _ hx hy u v hadj + simp only [Equiv.Perm.mul_apply]; exact hx _ _ (hy u v hadj) + · intro x _ hx u v hadj + let f : { p : Fin 63 × Fin 63 // langerSimpleGraph.Adj p.1 p.2 } → + { p : Fin 63 × Fin 63 // langerSimpleGraph.Adj p.1 p.2 } := + fun ⟨⟨a, b⟩, hab⟩ => ⟨⟨x a, x b⟩, hx a b hab⟩ + have hf_surj : Function.Surjective f := Finite.surjective_of_injective (by + intro ⟨⟨a₁, b₁⟩, _⟩ ⟨⟨a₂, b₂⟩, _⟩ h + simp only [f, Subtype.mk.injEq, Prod.mk.injEq] at h + exact Subtype.ext (Prod.ext (x.injective h.1) (x.injective h.2))) + obtain ⟨⟨⟨a, b⟩, hab⟩, heq⟩ := hf_surj ⟨⟨u, v⟩, hadj⟩ + simp only [f, Subtype.mk.injEq, Prod.mk.injEq] at heq + rw [show a = x⁻¹ u from by rw [← heq.1]; simp, + show b = x⁻¹ v from by rw [← heq.2]; simp] at hab + exact hab + +noncomputable instance langerPretransitive : + MulAction.IsPretransitive langerG (Fin 63) where + exists_smul_eq := by + intro x y + let σ_x := applyWord (witnessWord x) + let σ_y := applyWord (witnessWord y) + have hmem : σ_x.symm.trans σ_y ∈ langerG := + langerG.mul_mem (applyWord_mem _) (langerG.inv_mem (applyWord_mem _)) + exact ⟨⟨σ_x.symm.trans σ_y, hmem⟩, by + change (σ_x.symm.trans σ_y) x = y + simp only [Equiv.trans_apply] + rw [show σ_x.symm x = 0 from by + rw [Equiv.symm_apply_eq]; exact (witnessWord_correct x).symm] + exact witnessWord_correct y⟩ + +/-- **The Langer graph is a Sabidussi coset graph.** + + `langerSimpleGraph ≃g Sab(G₂(2), H₁₉₂, D)` + +where H₁₉₂ = Stab(0) has order 192. -/ +noncomputable def langerSabidussiIso : + langerSimpleGraph ≃g SimpleGraph.cosetGraph + (MulAction.stabilizer langerG (0 : Fin 63)) + (connectionSet langerG langerSimpleGraph 0) + (connectionSet.isConnectionSet 0) := + sabidussiIso 0 diff --git a/Archive/PrimitiveGraphs.lean b/Archive/PrimitiveGraphs.lean new file mode 100644 index 00000000000000..33f47e62b7bb4d --- /dev/null +++ b/Archive/PrimitiveGraphs.lean @@ -0,0 +1,511 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +import Archive.LangerGraph + +/-! +# Primitive and imprimitive cubic arc-transitive graphs + +Four results connecting primitivity, imprimitivity, and covering structure +for cubic arc-transitive graphs in the Foster census: + +1. **Langer graph primitivity** — The G₂(2) action on 63 vertices is primitive + (Atkinson's algorithm). The point stabiliser H₁₉₂ is maximal in G₂(2). + +2. **Zhou-6 graph primitivity** — The PSL(2,13) action on 91 vertices (via + the subgroup D₁₂) is primitive. The stabiliser D₁₂ is maximal in PSL(2,13). + +3. **Zhou-3 → Zhou-6 covering** — The Zhou-3 graph (F182A, cubic, 182 vertices) + is a positive double cover of Zhou-6 (91 vertices, 6-regular) via the block + system S₃ < D₁₂ in PSL(2,13). + +4. **No cubic double cover of Langer** — The Tutte 12-cage (126 vertices, cubic) + cannot cover the Langer graph because its point subgraph is edgeless. + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798 +* M.D. Atkinson, *An algorithm for finding the blocks of a permutation group*, + Math. Comp. 29 (1975), 911–913 +* C.-X. Zhou, Y.-Q. Feng, *Automorphism groups of connected cubic Cayley graphs + of order 2pq*, Algebra Colloq. (2007) +-/ + +set_option linter.style.nativeDecide false + +/-! ## Section 1: Atkinson's algorithm (generic) and Langer primitivity -/ + +/-! ### Atkinson's algorithm for Fin 63 (Langer / G₂(2)) -/ + +private def mergeRep63 (f : Fin 63 → Fin 63) (lo hi : Fin 63) : Fin 63 → Fin 63 := + fun i => let fi := f i; if fi = hi then lo else fi + +private def atkinson63 (gens : List (Equiv.Perm (Fin 63))) + (queue : List (Fin 63 × Fin 63)) (part : Fin 63 → Fin 63) : + Nat → Fin 63 → Fin 63 + | 0 => part + | fuel + 1 => + match queue with + | [] => part + | (x, y) :: rest => + let (newPairs, part') := gens.foldl + (fun (acc : List (Fin 63 × Fin 63) × (Fin 63 → Fin 63)) g => + let (pairs, p) := acc + let rgx := p (g x) + let rgy := p (g y) + if rgx = rgy then (pairs, p) + else + let lo := min rgx rgy + let hi := max rgx rgy + ((lo, hi) :: pairs, mergeRep63 p lo hi)) ([], part) + atkinson63 gens (rest ++ newPairs) part' fuel + +private def blockIsFull63 (v : Fin 63) : Bool := + let gens := [g2gen1, g2gen1.symm, g2gen2, g2gen2.symm] + let initPart : Fin 63 → Fin 63 := fun i => if i = v then 0 else i + let finalPart := atkinson63 gens [(0, v)] initPart 300 + decide (∀ w : Fin 63, finalPart w = 0) + +/-- **Primitivity of the G₂(2) action on the 63 points of GH(2,2).** + +For every vertex `v ≠ 0`, Atkinson's algorithm starting from `0 ~ v` +merges all 63 vertices into a single equivalence class. This means +no non-trivial block system exists, so the point stabiliser H₁₉₂ ≤ G₂(2) +is a **maximal subgroup** — there is no subgroup K with H₁₉₂ < K < G₂(2). -/ +theorem langer_action_primitive : + ∀ v : Fin 63, v ≠ 0 → blockIsFull63 v = true := by + native_decide + +/-! ## Section 2: The Zhou-6 graph and its primitivity -/ + +/-- Edge list for the Zhou-6 graph (91 vertices, 6-regular, 273 edges). +This is the quotient of Zhou-3 (F182A) by the block system S₃ < D₁₂ +in PSL(2,13). Equivalently, Sab(PSL(2,13), D₁₂). -/ +private def zhou6Edges : Array (Fin 91 × Fin 91) := #[ + (0, 48), (0, 54), (0, 59), (0, 63), (0, 65), (0, 69), + (1, 26), (1, 35), (1, 62), (1, 71), (1, 75), (1, 81), + (2, 24), (2, 31), (2, 82), (2, 83), (2, 86), (2, 87), + (3, 38), (3, 53), (3, 57), (3, 73), (3, 84), (3, 87), + (4, 39), (4, 44), (4, 53), (4, 54), (4, 77), (4, 89), + (5, 34), (5, 45), (5, 46), (5, 54), (5, 78), (5, 90), + (6, 35), (6, 38), (6, 46), (6, 47), (6, 61), (6, 79), + (7, 39), (7, 43), (7, 45), (7, 52), (7, 58), (7, 79), + (8, 25), (8, 34), (8, 59), (8, 61), (8, 74), (8, 80), + (9, 37), (9, 52), (9, 60), (9, 65), (9, 75), (9, 82), + (10, 18), (10, 24), (10, 40), (10, 58), (10, 66), (10, 74), + (11, 51), (11, 55), (11, 67), (11, 68), (11, 75), (11, 89), + (12, 20), (12, 24), (12, 52), (12, 69), (12, 72), (12, 90), + (13, 53), (13, 58), (13, 68), (13, 70), (13, 76), (13, 85), + (14, 29), (14, 30), (14, 60), (14, 67), (14, 76), (14, 80), + (15, 18), (15, 20), (15, 63), (15, 64), (15, 73), (15, 81), + (16, 36), (16, 51), (16, 74), (16, 81), (16, 85), (16, 88), + (17, 29), (17, 35), (17, 56), (17, 73), (17, 83), (17, 90), + (18, 33), (18, 37), (18, 66), (18, 73), + (19, 26), (19, 28), (19, 29), (19, 34), (19, 86), (19, 89), + (20, 32), (20, 52), (20, 64), (20, 80), + (21, 32), (21, 41), (21, 44), (21, 66), (21, 83), (21, 88), + (22, 36), (22, 42), (22, 45), (22, 60), (22, 70), (22, 84), + (23, 25), (23, 28), (23, 39), (23, 47), (23, 62), (23, 87), + (24, 69), (24, 74), (24, 87), + (25, 39), (25, 49), (25, 56), (25, 59), + (26, 34), (26, 50), (26, 57), (26, 71), + (27, 37), (27, 38), (27, 42), (27, 44), (27, 51), (27, 78), + (28, 29), (28, 47), (28, 48), (28, 88), + (29, 60), (29, 73), + (30, 46), (30, 49), (30, 66), (30, 67), (30, 71), + (31, 43), (31, 50), (31, 64), (31, 67), (31, 83), + (32, 55), (32, 80), (32, 84), (32, 88), + (33, 37), (33, 43), (33, 48), (33, 61), (33, 77), + (34, 45), (34, 74), + (35, 61), (35, 75), (35, 83), + (36, 60), (36, 72), (36, 77), (36, 81), + (37, 78), (37, 82), + (38, 51), (38, 57), (38, 79), + (39, 44), (39, 52), + (40, 50), (40, 55), (40, 56), (40, 58), (40, 65), + (41, 57), (41, 59), (41, 66), (41, 68), (41, 72), + (42, 44), (42, 69), (42, 70), (42, 71), + (43, 45), (43, 48), (43, 67), + (44, 83), + (45, 84), + (46, 47), (46, 54), (46, 66), + (47, 64), (47, 70), + (48, 69), (48, 88), + (49, 56), (49, 71), (49, 82), (49, 85), + (50, 57), (50, 64), (50, 65), + (51, 67), (51, 74), + (52, 75), + (53, 54), (53, 73), (53, 85), + (54, 65), + (55, 56), (55, 84), (55, 89), + (56, 90), + (57, 72), + (58, 76), (58, 79), + (59, 63), (59, 68), + (60, 65), + (61, 77), (61, 80), + (62, 76), (62, 78), (62, 81), (62, 87), + (63, 79), (63, 81), (63, 86), + (64, 70), + (68, 70), (68, 75), + (69, 71), + (72, 77), (72, 90), + (76, 78), (76, 80), + (77, 89), + (78, 90), + (79, 86), + (82, 85), (82, 86), + (84, 87), + (85, 88), + (86, 89)] + +private def zhou6AdjBool (u v : Fin 91) : Bool := + zhou6Edges.any fun (a, b) => (u == a && v == b) || (u == b && v == a) + +/-- The **Zhou-6 graph**: 91 vertices, 6-regular, 273 edges. +Quotient of the Zhou-3 graph (F182A) by the block system S₃ < D₁₂. -/ +def zhou6Graph : SimpleGraph (Fin 91) where + Adj u v := zhou6AdjBool u v + symm u v := by simp only [zhou6AdjBool]; revert u v; native_decide + loopless := ⟨fun u => by simp only [zhou6AdjBool]; revert u; native_decide⟩ + +instance zhou6DecAdj : DecidableRel zhou6Graph.Adj := + fun u v => inferInstanceAs (Decidable (zhou6AdjBool u v)) + +/-- The Zhou-6 graph is 6-regular. -/ +theorem zhou6_regular : + ∀ v : Fin 91, (Finset.univ.filter fun w => zhou6Graph.Adj v w).card = 6 := by + native_decide + +/-- The Zhou-6 graph has 273 edges. -/ +theorem zhou6_edges : + (Finset.univ.filter fun p : Fin 91 × Fin 91 => + p.1 < p.2 ∧ zhou6Graph.Adj p.1 p.2).card = 273 := by + native_decide + +/-! ### Zhou-6 generators (PSL(2,13) action on 91 = |PSL(2,13)|/|D₁₂| points) -/ + +private def zhou6Gen1Fwd : Array (Fin 91) := #[ + 1, 3, 5, 7, 9, 11, 13, 14, 16, 17, 8, 18, 19, 20, 21, 23, 24, 4, 25, 27, + 28, 0, 31, 22, 34, 36, 38, 40, 42, 44, 41, 46, 48, 49, 51, 53, 2, 56, 58, 60, + 61, 63, 50, 30, 65, 67, 68, 70, 71, 72, 6, 10, 29, 52, 75, 33, 77, 79, 80, 81, + 83, 85, 84, 62, 47, 35, 59, 66, 15, 26, 64, 57, 86, 39, 74, 73, 32, 82, 55, 76, + 88, 87, 90, 54, 43, 12, 78, 45, 69, 37, 89] + +private def zhou6Gen1Inv : Array (Fin 91) := #[ + 21, 0, 36, 1, 17, 2, 50, 3, 10, 4, 51, 5, 85, 6, 7, 68, 8, 9, 11, 12, + 13, 14, 23, 15, 16, 18, 69, 19, 20, 52, 43, 22, 76, 55, 24, 65, 25, 89, 26, 73, + 27, 30, 28, 84, 29, 87, 31, 64, 32, 33, 42, 34, 53, 35, 83, 78, 37, 71, 38, 66, + 39, 40, 63, 41, 70, 44, 67, 45, 46, 88, 47, 48, 49, 75, 74, 54, 79, 56, 86, 57, + 58, 59, 77, 60, 62, 61, 72, 81, 80, 90, 82] + +private def zhou6Gen2Fwd : Array (Fin 91) := #[ + 2, 4, 6, 8, 10, 12, 0, 15, 9, 3, 1, 13, 17, 16, 22, 19, 11, 5, 26, 7, + 29, 30, 32, 33, 35, 37, 39, 41, 43, 45, 42, 47, 14, 50, 52, 54, 55, 57, 59, 18, + 62, 49, 21, 64, 66, 20, 69, 48, 31, 27, 23, 68, 73, 74, 24, 76, 78, 25, 81, 82, + 84, 65, 77, 86, 28, 87, 71, 70, 85, 83, 88, 44, 56, 34, 75, 53, 36, 40, 72, 63, + 60, 89, 38, 46, 80, 51, 79, 61, 67, 58, 90] + +private def zhou6Gen2Inv : Array (Fin 91) := #[ + 6, 10, 0, 9, 1, 17, 2, 19, 3, 8, 4, 16, 5, 11, 32, 7, 13, 12, 39, 15, + 45, 42, 14, 50, 54, 57, 18, 49, 64, 20, 21, 48, 22, 23, 73, 24, 76, 25, 82, 26, + 77, 27, 30, 28, 71, 29, 83, 31, 47, 41, 33, 85, 34, 75, 35, 36, 72, 37, 89, 38, + 80, 87, 40, 79, 43, 61, 44, 88, 51, 46, 67, 66, 78, 52, 53, 74, 55, 62, 56, 86, + 84, 58, 59, 69, 60, 68, 63, 65, 70, 81, 90] + +private theorem zhou6Gen1Fwd_size : zhou6Gen1Fwd.size = 91 := by native_decide +private theorem zhou6Gen1Inv_size : zhou6Gen1Inv.size = 91 := by native_decide +private theorem zhou6Gen2Fwd_size : zhou6Gen2Fwd.size = 91 := by native_decide +private theorem zhou6Gen2Inv_size : zhou6Gen2Inv.size = 91 := by native_decide + +/-- First generator of PSL(2,13) acting on 91 cosets of D₁₂. -/ +def zhou6Gen1 : Equiv.Perm (Fin 91) where + toFun i := zhou6Gen1Fwd[i.val]'(by have := zhou6Gen1Fwd_size; omega) + invFun i := zhou6Gen1Inv[i.val]'(by have := zhou6Gen1Inv_size; omega) + left_inv := by intro i; revert i; native_decide + right_inv := by intro i; revert i; native_decide + +/-- Second generator of PSL(2,13) acting on 91 cosets of D₁₂. -/ +def zhou6Gen2 : Equiv.Perm (Fin 91) where + toFun i := zhou6Gen2Fwd[i.val]'(by have := zhou6Gen2Fwd_size; omega) + invFun i := zhou6Gen2Inv[i.val]'(by have := zhou6Gen2Inv_size; omega) + left_inv := by intro i; revert i; native_decide + right_inv := by intro i; revert i; native_decide + +/-- σ₁ preserves Zhou-6 adjacency. -/ +theorem zhou6Gen1_adj : + ∀ u v : Fin 91, + zhou6Graph.Adj u v ↔ zhou6Graph.Adj (zhou6Gen1 u) (zhou6Gen1 v) := by + native_decide + +/-- σ₂ preserves Zhou-6 adjacency. -/ +theorem zhou6Gen2_adj : + ∀ u v : Fin 91, + zhou6Graph.Adj u v ↔ zhou6Graph.Adj (zhou6Gen2 u) (zhou6Gen2 v) := by + native_decide + +/-! ### Atkinson's algorithm for Fin 91 (Zhou-6 / PSL(2,13)) -/ + +private def mergeRep91 (f : Fin 91 → Fin 91) (lo hi : Fin 91) : Fin 91 → Fin 91 := + fun i => let fi := f i; if fi = hi then lo else fi + +private def atkinson91 (gens : List (Equiv.Perm (Fin 91))) + (queue : List (Fin 91 × Fin 91)) (part : Fin 91 → Fin 91) : + Nat → Fin 91 → Fin 91 + | 0 => part + | fuel + 1 => + match queue with + | [] => part + | (x, y) :: rest => + let (newPairs, part') := gens.foldl + (fun (acc : List (Fin 91 × Fin 91) × (Fin 91 → Fin 91)) g => + let (pairs, p) := acc + let rgx := p (g x) + let rgy := p (g y) + if rgx = rgy then (pairs, p) + else + let lo := min rgx rgy + let hi := max rgx rgy + ((lo, hi) :: pairs, mergeRep91 p lo hi)) ([], part) + atkinson91 gens (rest ++ newPairs) part' fuel + +private def blockIsFull91 (v : Fin 91) : Bool := + let gens := [zhou6Gen1, zhou6Gen1.symm, zhou6Gen2, zhou6Gen2.symm] + let initPart : Fin 91 → Fin 91 := fun i => if i = v then 0 else i + let finalPart := atkinson91 gens [(0, v)] initPart 400 + decide (∀ w : Fin 91, finalPart w = 0) + +/-- **Primitivity of the PSL(2,13) action on 91 points.** + +For every vertex `v ≠ 0`, Atkinson's algorithm starting from `0 ~ v` +merges all 91 vertices into a single equivalence class. The stabiliser +D₁₂ (order 12) is a **maximal subgroup** of PSL(2,13) (order 1092). -/ +theorem zhou6_action_primitive : + ∀ v : Fin 91, v ≠ 0 → blockIsFull91 v = true := by + native_decide + +/-! ## Section 3: Zhou-3 → Zhou-6 covering -/ + +/-- Edge list for the Zhou-3 graph (F182A, 182 vertices, cubic, 273 edges). +The unique cubic arc-transitive graph on 182 vertices, with +Aut ≅ PSL(2,13) × Z₂ and arc-stabiliser S₃. -/ +private def zhou3Edges : Array (Fin 182 × Fin 182) := #[ + (0, 97), (0, 119), (0, 131), + (1, 108), (1, 126), (1, 139), + (2, 71), (2, 143), (2, 163), + (3, 53), (3, 125), (3, 150), + (4, 62), (4, 165), (4, 175), + (5, 48), (5, 166), (5, 172), + (6, 107), (6, 115), (6, 174), + (7, 77), (7, 147), (7, 169), + (8, 88), (8, 109), (8, 179), + (9, 79), (9, 106), (9, 155), + (10, 90), (10, 92), (10, 181), + (11, 68), (11, 108), (11, 157), + (12, 77), (12, 94), (12, 122), + (13, 70), (13, 93), (13, 158), + (14, 91), (14, 104), (14, 159), + (15, 78), (15, 86), (15, 117), + (16, 51), (16, 123), (16, 149), + (17, 69), (17, 119), (17, 161), + (18, 75), (18, 130), (18, 151), + (19, 105), (19, 121), (19, 165), + (20, 49), (20, 117), (20, 132), + (21, 37), (21, 81), (21, 148), + (22, 134), (22, 136), (22, 179), + (23, 102), (23, 111), (23, 150), + (24, 40), (24, 138), (24, 181), + (25, 48), (25, 104), (25, 145), + (26, 117), (26, 140), (26, 170), + (27, 106), (27, 137), (27, 153), + (28, 59), (28, 135), (28, 152), + (29, 60), (29, 120), (29, 161), + (30, 41), (30, 127), (30, 146), + (31, 36), (31, 128), (31, 163), + (32, 73), (32, 148), (32, 171), + (33, 103), (33, 163), (33, 176), + (34, 70), (34, 113), (34, 146), + (35, 58), (35, 167), (35, 181), + (36, 75), (36, 133), + (37, 66), (37, 147), + (38, 52), (38, 56), (38, 179), + (39, 59), (39, 68), (39, 173), + (40, 129), (40, 161), + (41, 64), (41, 105), + (42, 65), (42, 89), (42, 132), + (43, 82), (43, 166), (43, 176), + (44, 72), (44, 91), (44, 141), + (45, 85), (45, 121), (45, 168), + (46, 57), (46, 79), (46, 124), + (47, 50), (47, 95), (47, 174), + (48, 149), + (49, 139), (49, 174), + (50, 113), (50, 118), + (51, 78), (51, 98), + (52, 115), (52, 142), + (53, 69), (53, 100), + (54, 75), (54, 76), (54, 84), + (55, 89), (55, 102), (55, 156), + (56, 94), (56, 176), + (57, 58), (57, 96), + (58, 121), + (59, 147), + (60, 133), (60, 143), + (61, 93), (61, 98), (61, 134), + (62, 128), (62, 135), + (63, 87), (63, 101), (63, 167), + (64, 110), (64, 177), + (65, 160), (65, 169), + (66, 87), (66, 154), + (67, 74), (67, 96), (67, 123), + (68, 148), + (69, 91), + (70, 151), + (71, 123), (71, 166), + (72, 155), (72, 162), + (73, 120), (73, 144), + (74, 157), (74, 164), + (76, 114), (76, 159), + (77, 103), + (78, 89), + (79, 105), + (80, 100), (80, 113), (80, 116), + (81, 110), (81, 131), + (82, 115), (82, 118), + (83, 133), (83, 137), (83, 144), + (84, 139), (84, 140), + (85, 88), (85, 142), + (86, 97), (86, 134), + (87, 90), + (88, 167), + (90, 169), + (92, 95), (92, 132), + (93, 109), + (94, 141), + (95, 129), + (96, 138), + (97, 177), + (98, 164), + (99, 112), (99, 142), (99, 171), + (100, 129), + (101, 114), (101, 130), + (102, 149), + (103, 135), + (104, 150), + (106, 146), + (107, 108), (107, 171), + (109, 130), + (110, 178), + (111, 112), (111, 168), + (112, 180), + (114, 145), + (116, 152), (116, 158), + (118, 127), + (119, 136), + (120, 131), + (122, 155), (122, 160), + (124, 157), (124, 162), + (125, 152), (125, 175), + (126, 159), (126, 162), + (127, 172), + (128, 140), + (136, 141), + (137, 151), + (138, 143), + (144, 180), + (145, 154), + (153, 156), (153, 160), + (154, 178), + (156, 180), + (158, 173), + (164, 173), + (165, 170), + (168, 175), + (170, 177), + (172, 178)] + +private def zhou3AdjBool (u v : Fin 182) : Bool := + zhou3Edges.any fun (a, b) => (u == a && v == b) || (u == b && v == a) + +/-- The **Zhou-3 graph** (F182A): 182 vertices, cubic (3-regular), 273 edges. +The unique cubic arc-transitive graph on 182 vertices. +Sab(PSL(2,13), S₃) where |PSL(2,13)| = 1092, |S₃| = 6. -/ +def zhou3Graph : SimpleGraph (Fin 182) where + Adj u v := zhou3AdjBool u v + symm u v := by simp only [zhou3AdjBool]; revert u v; native_decide + loopless := ⟨fun u => by simp only [zhou3AdjBool]; revert u; native_decide⟩ + +instance zhou3DecAdj : DecidableRel zhou3Graph.Adj := + fun u v => inferInstanceAs (Decidable (zhou3AdjBool u v)) + +/-- The Zhou-3 graph is 3-regular. -/ +theorem zhou3_regular : + ∀ v : Fin 182, (Finset.univ.filter fun w => zhou3Graph.Adj v w).card = 3 := by + native_decide + +/-- The Zhou-3 graph has 273 edges. -/ +theorem zhou3_edges : + (Finset.univ.filter fun p : Fin 182 × Fin 182 => + p.1 < p.2 ∧ zhou3Graph.Adj p.1 p.2).card = 273 := by + native_decide + +/-! ### The covering map Zhou-3 → Zhou-6 + +The block system for the Z₂ double cover is: vertex `v` of Zhou-3 maps to +vertex `v / 2` of Zhou-6. Each fibre `{2k, 2k+1}` has size 2. -/ + +/-- The covering map from Zhou-3 (Fin 182) to Zhou-6 (Fin 91): `v ↦ v / 2`. -/ +def zhouBlockMap (v : Fin 182) : Fin 91 := + ⟨v.val / 2, by omega⟩ + +/-- The covering map is surjective. -/ +theorem zhouBlockMap_surj : Function.Surjective zhouBlockMap := by + intro ⟨j, hj⟩ + refine ⟨⟨2 * j, by omega⟩, ?_⟩ + simp only [zhouBlockMap, Fin.mk.injEq] + omega + +/-- Every fibre of the covering map has exactly 2 elements. -/ +theorem zhouBlockMap_fibre_size : + ∀ w : Fin 91, + (Finset.univ.filter fun v : Fin 182 => zhouBlockMap v = w).card = 2 := by + native_decide + +/-- The covering map is a graph homomorphism: if `u ~ v` in Zhou-3, then +`zhouBlockMap u ~ zhouBlockMap v` in Zhou-6. -/ +theorem zhouBlockMap_hom : + ∀ u v : Fin 182, + zhou3Graph.Adj u v → zhou6Graph.Adj (zhouBlockMap u) (zhouBlockMap v) := by + native_decide + +/-- **Zhou-6 is the quotient of Zhou-3 under the block map.** + +The Zhou-6 graph equals the image of the Zhou-3 graph under the block map: +two Zhou-6 vertices are adjacent iff some pair of their preimages are adjacent +in Zhou-3. This is the positive double cover construction S₃ < D₁₂ < PSL(2,13). -/ +theorem zhou6_eq_quotient : + ∀ a b : Fin 91, + zhou6Graph.Adj a b ↔ + ∃ u v : Fin 182, + zhouBlockMap u = a ∧ zhouBlockMap v = b ∧ zhou3Graph.Adj u v := by + native_decide + +/-! ## Section 4: No cubic double cover of the Langer graph -/ + +/-- **The Tutte 12-cage has no edges between points.** + +The induced subgraph on vertices 0–62 (points of GH(2,2)) is edgeless. +This obstructs any covering map from the Tutte 12-cage to the Langer graph: +the Langer graph has 189 edges among its 63 vertices, but no point-point +edge exists in the Tutte 12-cage to cover them. + +More fundamentally, the point stabiliser H₁₉₂ in G₂(2) has structure +((C₄ × C₄) ⋊ C₃) ⋊ C₂) ⋊ C₂, with three index-2 subgroups of order 96, +but none yield a size-3 suborbit — the smallest suborbits are size 6 and 12. +No cubic Sabidussi graph over G₂(2) with 126 vertices exists. -/ +theorem tutte12_points_independent : + ∀ p q : Fin 63, + ¬ tutte12CageGraph.Adj ⟨p.val, by omega⟩ ⟨q.val, by omega⟩ := by + native_decide diff --git a/Mathlib.lean b/Mathlib.lean index 51a2d9e682d0ca..100ccd502ff9dd 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3574,6 +3574,7 @@ public import Mathlib.Combinatorics.SetFamily.KruskalKatona public import Mathlib.Combinatorics.SetFamily.LYM public import Mathlib.Combinatorics.SetFamily.Shadow public import Mathlib.Combinatorics.SetFamily.Shatter +public import Mathlib.Combinatorics.SimpleGraph.Action public import Mathlib.Combinatorics.SimpleGraph.Acyclic public import Mathlib.Combinatorics.SimpleGraph.AdjMatrix public import Mathlib.Combinatorics.SimpleGraph.Basic @@ -3591,6 +3592,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph public import Mathlib.Combinatorics.SimpleGraph.Copy +public import Mathlib.Combinatorics.SimpleGraph.CosetGraph public import Mathlib.Combinatorics.SimpleGraph.Dart public import Mathlib.Combinatorics.SimpleGraph.DegreeSum public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges @@ -3619,6 +3621,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Operations public import Mathlib.Combinatorics.SimpleGraph.Partition public import Mathlib.Combinatorics.SimpleGraph.Paths public import Mathlib.Combinatorics.SimpleGraph.Prod +public import Mathlib.Combinatorics.SimpleGraph.QuotientGraph public import Mathlib.Combinatorics.SimpleGraph.Regularity.Bound public import Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk public import Mathlib.Combinatorics.SimpleGraph.Regularity.Energy @@ -3626,9 +3629,11 @@ public import Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise public import Mathlib.Combinatorics.SimpleGraph.Regularity.Increment public import Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma public import Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform +public import Mathlib.Combinatorics.SimpleGraph.Representation public import Mathlib.Combinatorics.SimpleGraph.StronglyRegular public import Mathlib.Combinatorics.SimpleGraph.Subgraph public import Mathlib.Combinatorics.SimpleGraph.Sum +public import Mathlib.Combinatorics.SimpleGraph.Symmetric public import Mathlib.Combinatorics.SimpleGraph.Trails public import Mathlib.Combinatorics.SimpleGraph.Triangle.Basic public import Mathlib.Combinatorics.SimpleGraph.Triangle.Counting diff --git a/Mathlib/Combinatorics/SimpleGraph/Action.lean b/Mathlib/Combinatorics/SimpleGraph/Action.lean new file mode 100644 index 00000000000000..0b7875c8109f46 --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/Action.lean @@ -0,0 +1,129 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Maps +public import Mathlib.GroupTheory.GroupAction.Basic + +/-! +# Group actions on simple graphs + +Given a group `G` acting on a type `V` via `MulAction G V`, and a simple graph `Γ : SimpleGraph V`, +we say the action is a *graph action* if it preserves adjacency: `Γ.Adj u v → Γ.Adj (g • u) (g • v)` +for all `g : G`. + +## Main definitions + +* `GraphAction G Γ` — the action of `G` on `V` preserves the adjacency relation of `Γ` +* `GraphAction.adj_smul_iff` — for groups, adjacency is an iff (not just an implication) +* `GraphAction.toIso` — each `g : G` induces a graph isomorphism `Γ ≃g Γ` +* `IsVertexTransitive G Γ` — the action is a graph action and is transitive +* `IsArcTransitive G Γ` — the action is transitive on ordered adjacent pairs +* `IsLocallyTransitive G Γ v` — the stabilizer of `v` acts transitively on its neighbors + +## Main results + +* `isArcTransitive_of_vertexTransitive_locallyTransitive` — vertex-transitive + locally + transitive implies arc-transitive +-/ + +@[expose] public section + +variable {G V : Type*} + +/-- A group action on `V` is a *graph action* on `Γ : SimpleGraph V` if it preserves adjacency. -/ +class GraphAction (G : Type*) (V : Type*) [Group G] [MulAction G V] + (Γ : SimpleGraph V) : Prop where + /-- The action preserves adjacency. -/ + adj_smul : ∀ (g : G) (u v : V), Γ.Adj u v → Γ.Adj (g • u) (g • v) + +namespace GraphAction + +variable [Group G] [MulAction G V] {Γ : SimpleGraph V} [GraphAction G V Γ] + +/-- For group actions, adjacency is preserved in both directions: +`Γ.Adj (g • u) (g • v) ↔ Γ.Adj u v`. -/ +theorem adj_smul_iff (g : G) (u v : V) : Γ.Adj (g • u) (g • v) ↔ Γ.Adj u v := by + constructor + · intro h + have h' := adj_smul g⁻¹ (g • u) (g • v) h + simp only [inv_smul_smul] at h' + exact h' + · exact adj_smul g u v + +/-- Each group element `g` induces a graph isomorphism `Γ ≃g Γ`. -/ +noncomputable def toIso (g : G) : Γ ≃g Γ where + toEquiv := MulAction.toPerm g + map_rel_iff' := adj_smul_iff g _ _ + +@[simp] +theorem toIso_apply (g : G) (v : V) : (toIso g : Γ ≃g Γ) v = g • v := rfl + +@[simp] +theorem toIso_symm (g : G) : (toIso g : Γ ≃g Γ).symm = toIso g⁻¹ := by + ext v + simp [toIso] + +theorem toIso_mul (g h : G) : + (toIso (g * h) : Γ ≃g Γ) = (toIso h : Γ ≃g Γ).trans (toIso g) := by + ext v + simp [toIso, mul_smul] + +end GraphAction + +/-- A graph `Γ` is *vertex-transitive* under the action of `G` if `G` preserves adjacency +and acts transitively on the vertices. -/ +class IsVertexTransitive (G : Type*) (V : Type*) [Group G] [MulAction G V] + (Γ : SimpleGraph V) : Prop extends GraphAction G V Γ where + /-- The action is transitive on vertices. -/ + pretransitive : MulAction.IsPretransitive G V + +attribute [instance] IsVertexTransitive.pretransitive + +/-- A graph `Γ` is *arc-transitive* under the action of `G` if for any two arcs +`(u₁, v₁)` and `(u₂, v₂)`, there exists `g ∈ G` sending `u₁ ↦ u₂` and `v₁ ↦ v₂`. -/ +class IsArcTransitive (G : Type*) (V : Type*) [Group G] [MulAction G V] + (Γ : SimpleGraph V) : Prop extends GraphAction G V Γ where + /-- The action is transitive on arcs (ordered adjacent pairs). -/ + arc_transitive : ∀ u₁ v₁ u₂ v₂ : V, Γ.Adj u₁ v₁ → Γ.Adj u₂ v₂ → + ∃ g : G, g • u₁ = u₂ ∧ g • v₁ = v₂ + +namespace IsArcTransitive + +variable [Group G] [MulAction G V] {Γ : SimpleGraph V} [IsArcTransitive G V Γ] + +/-- An arc-transitive graph with no isolated vertices is vertex-transitive. -/ +theorem isVertexTransitive (hne : ∀ v : V, ∃ w : V, Γ.Adj v w) : + IsVertexTransitive G V Γ where + pretransitive := ⟨by + intro x y + obtain ⟨x', hx'⟩ := hne x + obtain ⟨y', hy'⟩ := hne y + obtain ⟨g, hg, _⟩ := @arc_transitive G V _ _ Γ _ x x' y y' hx' hy' + exact ⟨g, hg⟩⟩ + +end IsArcTransitive + +/-- A graph is *locally transitive* at `v` if the stabilizer of `v` acts transitively +on the neighbors of `v`. -/ +def IsLocallyTransitive (G : Type*) (V : Type*) [Group G] [MulAction G V] + (Γ : SimpleGraph V) (v : V) : Prop := + ∀ w₁ w₂ : V, Γ.Adj v w₁ → Γ.Adj v w₂ → + ∃ g : G, g • v = v ∧ g • w₁ = w₂ + +/-- A vertex-transitive, locally transitive graph is arc-transitive. -/ +theorem isArcTransitive_of_vertexTransitive_locallyTransitive + [Group G] [MulAction G V] (Γ : SimpleGraph V) [IsVertexTransitive G V Γ] + (hlocal : ∀ v : V, IsLocallyTransitive G V Γ v) : + IsArcTransitive G V Γ where + arc_transitive := by + intro u₁ v₁ u₂ v₂ h₁ h₂ + obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G u₁ u₂ + have hadj : Γ.Adj u₂ (g • v₁) := by + rw [← hg] + exact GraphAction.adj_smul g u₁ v₁ h₁ + obtain ⟨h, hhu₂, hhv⟩ := hlocal u₂ (g • v₁) v₂ hadj h₂ + exact ⟨h * g, by rw [mul_smul, hg, hhu₂], by rw [mul_smul, hhv]⟩ diff --git a/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean b/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean new file mode 100644 index 00000000000000..caebcd8cfdedfe --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/CosetGraph.lean @@ -0,0 +1,173 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Action +public import Mathlib.GroupTheory.GroupAction.Quotient +public import Mathlib.GroupTheory.DoubleCoset +public import Mathlib.Tactic.Group + +/-! +# Coset graphs (Sabidussi construction) + +Given a group `G`, a subgroup `H`, and a *connection set* `D ⊆ G` that is a union of +`(H, H)`-double cosets, is symmetric (`D = D⁻¹`), and is disjoint from `H`, we define the +**coset graph** `Sab(G, H, D)` whose vertices are the left cosets `G ⧸ H` and whose edges +connect `xH` to `yH` whenever `x⁻¹y ∈ D`. + +This is Sabidussi's generalization of Cayley graphs: when `H = ⊥`, the coset graph on +`G ⧸ ⊥ ≃ G` recovers the Cayley graph `Cay(G, D)`. + +## Main definitions + +* `IsConnectionSet H D` — `D` is a union of `(H, H)`-double cosets, closed under inversion, + and disjoint from `H` +* `SimpleGraph.cosetGraph H D` — the coset graph `Sab(G, H, D)` as a `SimpleGraph (G ⧸ H)` + +## Main results + +* `SimpleGraph.cosetGraph.adj_mk` — adjacency is characterized by `x⁻¹y ∈ D` +* `SimpleGraph.cosetGraph.graphAction` — `G` acts on the coset graph preserving adjacency +* `SimpleGraph.cosetGraph.isVertexTransitive` — coset graphs are vertex-transitive + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §2. +* Sabidussi, *Vertex-transitive graphs*, Monatsh. Math. 68 (1964), 426–438. +-/ + +@[expose] public section + +variable {G : Type*} [Group G] + +/-- A set `D ⊆ G` is a *connection set* for the subgroup `H` if it is stable under +left and right multiplication by `H` (i.e., a union of `(H,H)`-double cosets), +is closed under inversion, and is disjoint from `H`. -/ +structure IsConnectionSet (H : Subgroup G) (D : Set G) : Prop where + /-- `D` is stable under left and right multiplication by elements of `H`. -/ + double_coset_stable : ∀ d ∈ D, ∀ h₁ ∈ (H : Set G), ∀ h₂ ∈ (H : Set G), h₁ * d * h₂ ∈ D + /-- `D` is closed under inversion. -/ + inv_mem : ∀ d ∈ D, d⁻¹ ∈ D + /-- `D` is disjoint from `H`. -/ + disjoint : Disjoint D ↑H + +namespace IsConnectionSet + +variable {H : Subgroup G} {D : Set G} + +theorem one_not_mem (hD : IsConnectionSet H D) : (1 : G) ∉ D := + fun h => Set.disjoint_left.mp hD.disjoint h (Subgroup.one_mem H) + +end IsConnectionSet + +/-- The **coset graph** `Sab(G, H, D)`. Vertices are the left cosets `G ⧸ H`, +and two cosets `xH, yH` are adjacent iff `x⁻¹y ∈ D`. + +This is Sabidussi's generalization of Cayley graphs: when `H = ⊥`, +the coset graph on `G ⧸ ⊥ ≃ G` recovers the Cayley graph `Cay(G, D)`. -/ +noncomputable def SimpleGraph.cosetGraph (H : Subgroup G) (D : Set G) + (hD : IsConnectionSet H D) : SimpleGraph (G ⧸ H) where + Adj q₁ q₂ := Quotient.liftOn₂ q₁ q₂ (fun x y => x⁻¹ * y ∈ D) + (fun a₁ b₁ a₂ b₂ h₁ h₂ => by + have ha : a₁⁻¹ * a₂ ∈ (H : Set G) := QuotientGroup.leftRel_apply.mp h₁ + have hb : b₁⁻¹ * b₂ ∈ (H : Set G) := QuotientGroup.leftRel_apply.mp h₂ + apply propext; change a₁⁻¹ * b₁ ∈ D ↔ a₂⁻¹ * b₂ ∈ D; constructor + · intro h + have key : a₂⁻¹ * b₂ = (a₂⁻¹ * a₁) * (a₁⁻¹ * b₁) * (b₁⁻¹ * b₂) := by group + rw [key] + refine hD.double_coset_stable _ h _ ?_ _ hb + have : (a₁⁻¹ * a₂)⁻¹ ∈ (H : Set G) := H.inv_mem ha + rwa [mul_inv_rev, inv_inv] at this + · intro h + have key : a₁⁻¹ * b₁ = (a₁⁻¹ * a₂) * (a₂⁻¹ * b₂) * (b₂⁻¹ * b₁) := by group + rw [key] + refine hD.double_coset_stable _ h _ ha _ ?_ + have : (b₁⁻¹ * b₂)⁻¹ ∈ (H : Set G) := H.inv_mem hb + rwa [mul_inv_rev, inv_inv] at this) + symm := by + intro q₁ q₂ + refine Quotient.inductionOn₂ q₁ q₂ fun x y => ?_ + simp only [Quotient.liftOn₂_mk] + intro h + have hmem := hD.inv_mem _ h + rwa [mul_inv_rev, inv_inv] at hmem + loopless := ⟨by + intro q + refine Quotient.inductionOn q fun x => ?_ + simp only [Quotient.liftOn₂_mk] + show ¬(x⁻¹ * x ∈ D) + rw [inv_mul_cancel] + exact hD.one_not_mem⟩ + +namespace SimpleGraph.cosetGraph + +variable (H : Subgroup G) (D : Set G) (hD : IsConnectionSet H D) + +/-- Adjacency in the coset graph is characterized by membership of `x⁻¹y` in `D`. -/ +@[simp] +theorem adj_mk (x y : G) : + (cosetGraph H D hD).Adj (QuotientGroup.mk x) (QuotientGroup.mk y) ↔ x⁻¹ * y ∈ D := + Iff.rfl + +/-- The left multiplication action of `G` on `G ⧸ H` preserves coset graph adjacency. -/ +instance graphAction : GraphAction G (G ⧸ H) (cosetGraph H D hD) where + adj_smul g q₁ q₂ := by + refine Quotient.inductionOn₂ q₁ q₂ fun x y => ?_ + intro h + change (g * x)⁻¹ * (g * y) ∈ D + rw [mul_inv_rev, mul_assoc, inv_mul_cancel_left] + exact h + +/-- Coset graphs are vertex-transitive under the natural action of `G`. -/ +instance isVertexTransitive : IsVertexTransitive G (G ⧸ H) (cosetGraph H D hD) where + pretransitive := MulAction.isPretransitive_quotient G H + +end SimpleGraph.cosetGraph + +/-! ## Coset projection + +When `H ≤ K`, the natural projection `G ⧸ H → G ⧸ K` sends `gH ↦ gK`. +If `D` is a connection set for both `H` and `K`, this projection is a +graph homomorphism: adjacency in `Sab(G, H, D)` implies adjacency in +`Sab(G, K, D)`. + +This is the Sabidussi analogue of quotient by a block system: the orbits +of `K` on `G ⧸ H` form a system of blocks of size `[K : H]`, and the +quotient graph is `Sab(G, K, D)`. -/ + +/-- The natural projection `G ⧸ H → G ⧸ K` when `H ≤ K`. -/ +def cosetProjection (H K : Subgroup G) (hle : H ≤ K) : + G ⧸ H → G ⧸ K := + Quotient.map id fun _ _ hab => by + change (QuotientGroup.leftRel K).r _ _ + have hab' : (QuotientGroup.leftRel H).r _ _ := hab + rw [QuotientGroup.leftRel_apply] at hab' ⊢ + exact hle hab' + +@[simp] +theorem cosetProjection_mk (H K : Subgroup G) (hle : H ≤ K) + (g : G) : cosetProjection H K hle ⟦g⟧ = ⟦g⟧ := + rfl + +/-- **Coset projection is a graph homomorphism**: if `H ≤ K` and `D` is a + connection set for both, then adjacency in `Sab(G, H, D)` implies + adjacency in `Sab(G, K, D)`. + + The proof is trivial: adjacency is `x⁻¹y ∈ D` in both graphs. + The subgroup only determines the coset equivalence, not the adjacency test. -/ +theorem SimpleGraph.cosetGraph.proj_adj + {H K : Subgroup G} (hle : H ≤ K) {D : Set G} + (hDH : IsConnectionSet H D) (hDK : IsConnectionSet K D) + (q₁ q₂ : G ⧸ H) : + (cosetGraph H D hDH).Adj q₁ q₂ → + (cosetGraph K D hDK).Adj (cosetProjection H K hle q₁) + (cosetProjection H K hle q₂) := + Quotient.inductionOn₂ q₁ q₂ fun _ _ h => h + +/-- The coset projection is surjective. -/ +theorem cosetProjection_surjective (H K : Subgroup G) (hle : H ≤ K) : + Function.Surjective (cosetProjection H K hle) := + fun q => Quotient.inductionOn q fun g => ⟨⟦g⟧, rfl⟩ diff --git a/Mathlib/Combinatorics/SimpleGraph/QuotientGraph.lean b/Mathlib/Combinatorics/SimpleGraph/QuotientGraph.lean new file mode 100644 index 00000000000000..420b6dffab698e --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/QuotientGraph.lean @@ -0,0 +1,134 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Symmetric +public import Mathlib.GroupTheory.GroupAction.Blocks + +/-! +# Quotient graphs and the Lorimer quotient theorem + +The quotient of a symmetric graph `Sab(G, H, HaH)` by a `G`-invariant partition +is again a symmetric graph `Sab(G, K, KaK)` for some overgroup `H ≤ K ≤ G`. + +## Main definitions + +* `SimpleGraph.quotientGraph` — quotient of a graph by a surjection (partition) +* `cosetQuotientMap` — the natural map `G ⧸ H → G ⧸ K` for `H ≤ K` +* `expandConnectionSet` — the expanded connection set `KDK` for an overgroup `K` + +## Main results + +* `quotient_cosetGraph_iso` — the quotient of `Sab(G,H,D)` is isomorphic to `Sab(G,K,KDK)` + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §4. +-/ + +@[expose] public section + +variable {G : Type*} [Group G] + +/-! ### Quotient graph construction -/ + +/-- The **quotient graph** of `Γ` with respect to a surjection `π : V → ι`. -/ +def SimpleGraph.quotientGraph {V ι : Type*} (Γ : SimpleGraph V) (π : V → ι) : + SimpleGraph ι where + Adj i j := i ≠ j ∧ ∃ u v : V, π u = i ∧ π v = j ∧ Γ.Adj u v + symm := by + intro i j ⟨hne, u, v, hui, hvj, hadj⟩ + exact ⟨hne.symm, v, u, hvj, hui, Γ.symm hadj⟩ + loopless := ⟨fun i ⟨hne, _⟩ => hne rfl⟩ + +/-! ### The coset quotient map -/ + +/-- The natural map `G ⧸ H → G ⧸ K` for `H ≤ K`, sending `gH ↦ gK`. -/ +noncomputable def cosetQuotientMap (H K : Subgroup G) (hHK : H ≤ K) : + G ⧸ H → G ⧸ K := + Quotient.map' id (fun _ _ h => QuotientGroup.leftRel_apply.mpr + (hHK (QuotientGroup.leftRel_apply.mp h))) + +@[simp] +theorem cosetQuotientMap_mk (H K : Subgroup G) (hHK : H ≤ K) (g : G) : + cosetQuotientMap H K hHK (QuotientGroup.mk g) = QuotientGroup.mk g := + rfl + +/-! ### Expanded connection set KDK -/ + +/-- The expanded connection set `KDK` for an overgroup `K`. -/ +def expandConnectionSet (K : Subgroup G) (D : Set G) : Set G := + {g : G | ∃ k₁ ∈ (K : Set G), ∃ d ∈ D, ∃ k₂ ∈ (K : Set G), g = k₁ * d * k₂} + +/-- `KDK` is a valid connection set for `K` when `D ∩ K = ∅`. -/ +theorem expandConnectionSet_isConnectionSet (H K : Subgroup G) (D : Set G) + (hD : IsConnectionSet H D) (hDK : Disjoint D ↑K) : + IsConnectionSet K (expandConnectionSet K D) where + double_coset_stable := by + intro d hd m₁ hm₁ m₂ hm₂ + obtain ⟨k₁, hk₁, e, he, k₂, hk₂, rfl⟩ := hd + exact ⟨m₁ * k₁, K.mul_mem hm₁ hk₁, e, he, k₂ * m₂, K.mul_mem hk₂ hm₂, by group⟩ + inv_mem := by + intro d hd + obtain ⟨k₁, hk₁, e, he, k₂, hk₂, rfl⟩ := hd + exact ⟨k₂⁻¹, K.inv_mem hk₂, e⁻¹, hD.inv_mem e he, k₁⁻¹, K.inv_mem hk₁, by group⟩ + disjoint := by + rw [Set.disjoint_left] + intro g hg hgK + obtain ⟨k₁, hk₁, d, hd, k₂, hk₂, rfl⟩ := hg + have : d ∈ (K : Set G) := by + have := K.mul_mem (K.mul_mem (K.inv_mem hk₁) hgK) (K.inv_mem hk₂) + convert this using 1; group + exact Set.disjoint_left.mp hDK hd this + +/-! ### The Lorimer quotient theorem -/ + +/-- **Lorimer's Quotient Theorem**: The quotient of `Sab(G, H, D)` by the overgroup +`K ≥ H` (with `D ∩ K = ∅`) is isomorphic to `Sab(G, K, KDK)`. + +The quotient map `G ⧸ H → G ⧸ K` (sending `gH ↦ gK`) induces a graph +isomorphism from the quotient graph to the coset graph with expanded +connection set. -/ +noncomputable def quotient_cosetGraph_iso (H K : Subgroup G) (D : Set G) + (hD : IsConnectionSet H D) (hHK : H ≤ K) + (hDK : Disjoint D ↑K) : + SimpleGraph.quotientGraph (SimpleGraph.cosetGraph H D hD) (cosetQuotientMap H K hHK) ≃g + SimpleGraph.cosetGraph K (expandConnectionSet K D) + (expandConnectionSet_isConnectionSet H K D hD hDK) where + toEquiv := Equiv.refl _ + map_rel_iff' := by + intro q₁ q₂ + refine Quotient.inductionOn₂ q₁ q₂ fun x y => ?_ + simp only [Equiv.refl_apply] + rw [SimpleGraph.cosetGraph.adj_mk] + constructor + · intro ⟨k₁, hk₁, d, hd, k₂, hk₂, heq⟩ + refine ⟨?_, QuotientGroup.mk (x * k₁), + QuotientGroup.mk (x * k₁ * d), ?_, ?_, ?_⟩ + · intro heq' + have : d ∈ (K : Set G) := by + have hK : k₁ * d * k₂ ∈ (K : Set G) := heq ▸ QuotientGroup.eq.mp heq' + have := K.mul_mem (K.mul_mem (K.inv_mem hk₁) hK) (K.inv_mem hk₂) + convert this using 1; group + exact Set.disjoint_left.mp hDK hd this + · simp only [cosetQuotientMap_mk, QuotientGroup.eq] + have : (x * k₁)⁻¹ * x = k₁⁻¹ := by group + rw [this]; exact K.inv_mem hk₁ + · simp only [cosetQuotientMap_mk, QuotientGroup.eq] + have hy : y = x * (k₁ * d * k₂) := by rw [← heq]; group + have : (x * k₁ * d)⁻¹ * (x * (k₁ * d * k₂)) = k₂ := by group + rw [hy, this]; exact hk₂ + · convert hd using 1 + simp [mul_inv_rev, mul_assoc, inv_mul_cancel_left] + · intro ⟨_, u, v, hu, hv, hadj⟩ + revert hu hv hadj + refine Quotient.inductionOn₂ u v fun x' y' hx' hy' (hadj : x'⁻¹ * y' ∈ D) => ?_ + simp only [cosetQuotientMap_mk] at hx' hy' + have hxK : x⁻¹ * x' ∈ (K : Set G) := by + have := K.inv_mem (QuotientGroup.eq.mp hx' : x'⁻¹ * x ∈ K) + rwa [mul_inv_rev, inv_inv] at this + have hyK : y'⁻¹ * y ∈ (K : Set G) := QuotientGroup.eq.mp hy' + exact ⟨x⁻¹ * x', hxK, x'⁻¹ * y', hadj, y'⁻¹ * y, hyK, by group⟩ diff --git a/Mathlib/Combinatorics/SimpleGraph/Representation.lean b/Mathlib/Combinatorics/SimpleGraph/Representation.lean new file mode 100644 index 00000000000000..b1faf6b2f9bd21 --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/Representation.lean @@ -0,0 +1,163 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.CosetGraph +public import Mathlib.GroupTheory.GroupAction.Quotient +public import Mathlib.Tactic.Group + +/-! +# The Sabidussi representation theorem + +Every vertex-transitive graph is isomorphic to a coset graph. More precisely, +if `G` acts vertex-transitively on a graph `Γ`, then for any basepoint `v`, +the orbit-stabilizer equivalence `V ≃ G ⧸ stabilizer G v` is a graph +isomorphism from `Γ` to `Sab(G, Gᵥ, D)`, where `D = {g ∈ G : Γ.Adj v (g • v)}`. + +## Main definitions + +* `connectionSet G Γ v` — the set of group elements moving `v` to a neighbor +* `connectionSet.isConnectionSet` — the connection set satisfies the axioms +* `sabidussiEquiv` — the equivalence `V ≃ G ⧸ stabilizer G v` for transitive actions +* `sabidussiIso` — the graph isomorphism `Γ ≃g cosetGraph (stabilizer G v) D` + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §2. +* Sabidussi, *Vertex-transitive graphs*, Monatsh. Math. 68 (1964), 426–438. +-/ + +@[expose] public section + +variable {G V : Type*} [Group G] [MulAction G V] {Γ : SimpleGraph V} + +/-! ### The connection set -/ + +/-- The *connection set* of a basepoint `v`: the set of group elements +that move `v` to one of its neighbors. -/ +def connectionSet (G : Type*) [Group G] [MulAction G V] + (Γ : SimpleGraph V) (v : V) : Set G := + {g : G | Γ.Adj v (g • v)} + +namespace connectionSet + +variable [GraphAction G V Γ] (v : V) + +omit [GraphAction G V Γ] in +theorem one_not_mem : (1 : G) ∉ connectionSet G Γ v := by + simp [connectionSet] + +theorem inv_mem {g : G} (hg : g ∈ connectionSet G Γ v) : + g⁻¹ ∈ connectionSet G Γ v := by + simp only [connectionSet, Set.mem_setOf_eq] at hg ⊢ + have h := Γ.symm hg + rwa [← GraphAction.adj_smul_iff g⁻¹, inv_smul_smul] at h + +theorem double_coset_stable {g : G} (hg : g ∈ connectionSet G Γ v) + {h₁ : G} (hh₁ : h₁ ∈ MulAction.stabilizer G v) + {h₂ : G} (hh₂ : h₂ ∈ MulAction.stabilizer G v) : + h₁ * g * h₂ ∈ connectionSet G Γ v := by + simp only [connectionSet, Set.mem_setOf_eq] at hg ⊢ + rw [mul_smul, mul_smul, MulAction.mem_stabilizer_iff.mp hh₂] + have := GraphAction.adj_smul h₁ v (g • v) hg + rwa [MulAction.mem_stabilizer_iff.mp hh₁] at this + +omit [GraphAction G V Γ] in +theorem disjoint_stabilizer : + Disjoint (connectionSet G Γ v) ↑(MulAction.stabilizer G v) := by + rw [Set.disjoint_left] + intro g hg hstab + simp only [connectionSet, Set.mem_setOf_eq] at hg + rw [SetLike.mem_coe, MulAction.mem_stabilizer_iff] at hstab + rw [hstab] at hg + exact (Γ.loopless.irrefl v) hg + +/-- The connection set forms a valid `IsConnectionSet` for the stabilizer subgroup. -/ +theorem isConnectionSet : + IsConnectionSet (MulAction.stabilizer G v) (connectionSet G Γ v) where + double_coset_stable _ hd _ hh₁ _ hh₂ := double_coset_stable v hd hh₁ hh₂ + inv_mem _ hd := inv_mem v hd + disjoint := disjoint_stabilizer v + +end connectionSet + +/-! ### The orbit-stabilizer equivalence -/ + +section SabidussiRepresentation + +variable [GraphAction G V Γ] [MulAction.IsPretransitive G V] (v : V) + +/-- The equivalence `V ≃ G ⧸ stabilizer G v` for a transitive action. + +The forward map sends `u` to the coset `gH` where `g • v = u`. +The inverse map sends `⟦g⟧` to `g • v`. -/ +noncomputable def sabidussiEquiv : V ≃ G ⧸ MulAction.stabilizer G v where + toFun u := QuotientGroup.mk (MulAction.exists_smul_eq G v u).choose + invFun := Quotient.lift (· • v) (by + intro a b hab + have hmem : (a⁻¹ * b) • v = v := + MulAction.mem_stabilizer_iff.mp (QuotientGroup.leftRel_apply.mp hab) + calc a • v = a • ((a⁻¹ * b) • v) := by rw [hmem] + _ = (a * (a⁻¹ * b)) • v := (mul_smul a (a⁻¹ * b) v).symm + _ = b • v := by rw [mul_inv_cancel_left]) + left_inv u := by + simp only + exact (MulAction.exists_smul_eq G v u).choose_spec + right_inv := by + intro q + refine Quotient.inductionOn q fun g => ?_ + simp only [Quotient.lift_mk] + apply QuotientGroup.eq.mpr + rw [MulAction.mem_stabilizer_iff, mul_smul] + set g' := (MulAction.exists_smul_eq G v (g • v)).choose + have hspec : g' • v = g • v := (MulAction.exists_smul_eq G v (g • v)).choose_spec + calc g'⁻¹ • (g • v) = g'⁻¹ • (g' • v) := by rw [hspec] + _ = v := inv_smul_smul g' v + +@[simp] +theorem sabidussiEquiv_smul (g : G) : + sabidussiEquiv v (g • v) = (g : G ⧸ MulAction.stabilizer G v) := by + simp only [sabidussiEquiv] + apply QuotientGroup.eq.mpr + rw [MulAction.mem_stabilizer_iff, mul_smul] + set g' := (MulAction.exists_smul_eq G v (g • v)).choose + have hspec : g' • v = g • v := (MulAction.exists_smul_eq G v (g • v)).choose_spec + calc g'⁻¹ • (g • v) = g'⁻¹ • (g' • v) := by rw [hspec] + _ = v := inv_smul_smul g' v + +@[simp] +theorem sabidussiEquiv_symm_mk (g : G) : + (sabidussiEquiv v).symm (QuotientGroup.mk g) = g • v := by + rfl + +/-- **Sabidussi's Representation Theorem**: Every vertex-transitive graph is +isomorphic to a coset graph. + +The orbit-stabilizer equivalence `V ≃ G ⧸ stabilizer G v` is a graph isomorphism +from `Γ` to `cosetGraph (stabilizer G v) (connectionSet G Γ v)`. -/ +noncomputable def sabidussiIso : + Γ ≃g SimpleGraph.cosetGraph (MulAction.stabilizer G v) + (connectionSet G Γ v) (connectionSet.isConnectionSet v) where + toEquiv := sabidussiEquiv v + map_rel_iff' := by + intro u w + set g₁ := (MulAction.exists_smul_eq G v u).choose + set g₂ := (MulAction.exists_smul_eq G v w).choose + have hu : g₁ • v = u := (MulAction.exists_smul_eq G v u).choose_spec + have hw : g₂ • v = w := (MulAction.exists_smul_eq G v w).choose_spec + change g₁⁻¹ * g₂ ∈ connectionSet G Γ v ↔ Γ.Adj u w + rw [← hu, ← hw] + simp only [connectionSet, Set.mem_setOf_eq, mul_smul] + constructor + · intro h + have := (@GraphAction.adj_smul_iff G V _ _ Γ _ g₁⁻¹ (g₁ • v) (g₂ • v)).mp + (by rwa [inv_smul_smul]) + exact this + · intro h + have := (@GraphAction.adj_smul_iff G V _ _ Γ _ g₁⁻¹ (g₁ • v) (g₂ • v)).mpr h + rwa [inv_smul_smul] at this + +end SabidussiRepresentation diff --git a/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean b/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean new file mode 100644 index 00000000000000..396baa0b54a598 --- /dev/null +++ b/Mathlib/Combinatorics/SimpleGraph/Symmetric.lean @@ -0,0 +1,196 @@ +/- +Copyright (c) 2026 Robin Langer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robin Langer +-/ +module + +public import Mathlib.Combinatorics.SimpleGraph.Representation +public import Mathlib.GroupTheory.DoubleCoset +public import Mathlib.Tactic.Group + +/-! +# Symmetric graphs and Lorimer's theorem + +A *symmetric* (arc-transitive) graph is a coset graph `Sab(G, H, HaH)` where `a` is an +involution not in `H`. This file proves both directions of Lorimer's theorem: +the forward direction shows `Sab(G, H, HaH)` is arc-transitive when `a² = 1` and `a ∉ H`, +and the reverse direction shows every arc-transitive graph's connection set is a single +double coset `HaH` where `a` swaps an arc. + +## Main definitions + +* `doubleCoset_isConnectionSet` — `HaH` is a valid connection set when `a² = 1, a ∉ H` +* `sabidussiSymmetricGraph` — the coset graph `Sab(G, H, HaH)` + +## Main results + +* `lorimer_forward` — `Sab(G, H, HaH)` is arc-transitive when `a² = 1, a ∉ H` +* `connectionSet_eq_doubleCoset` — under arc-transitivity, the connection set is a single + double coset +* `lorimer_reverse` — every arc-transitive graph has an arc-swapping involution `a` with + `a ∉ Gᵥ`, `a² ∈ Gᵥ`, and `D = GᵥaGᵥ` + +## References + +* Robin Langer, *Symmetric Graphs and their Quotients*, arXiv:1306.4798, Chapter 2 §§3–4. +* Lorimer, *Vertex-transitive graphs*, 1984. +-/ + +@[expose] public section + +variable {G : Type*} [Group G] + +private theorem inv_eq_self_of_sq_eq_one {a : G} (ha : a ^ 2 = 1) : a⁻¹ = a := + inv_eq_of_mul_eq_one_left (by rwa [← sq]) + +open DoubleCoset in +/-- `HaH` is a valid connection set when `a² = 1` and `a ∉ H`. -/ +theorem doubleCoset_isConnectionSet (H : Subgroup G) (a : G) + (ha_sq : a ^ 2 = 1) (ha_not : a ∉ H) : + IsConnectionSet H (doubleCoset a (H : Set G) H) where + double_coset_stable := by + intro d hd k₁ hk₁ k₂ hk₂ + obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := mem_doubleCoset.mp hd + exact mem_doubleCoset.mpr + ⟨k₁ * h₁, H.mul_mem hk₁ hh₁, h₂ * k₂, H.mul_mem hh₂ hk₂, by group⟩ + inv_mem := by + intro d hd + obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := mem_doubleCoset.mp hd + have ha_inv := inv_eq_self_of_sq_eq_one ha_sq + refine mem_doubleCoset.mpr ⟨h₂⁻¹, H.inv_mem hh₂, h₁⁻¹, H.inv_mem hh₁, ?_⟩ + calc (h₁ * a * h₂)⁻¹ = h₂⁻¹ * a⁻¹ * h₁⁻¹ := by group + _ = h₂⁻¹ * a * h₁⁻¹ := by rw [ha_inv] + disjoint := by + rw [Set.disjoint_left] + intro g hg hgH + obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := mem_doubleCoset.mp hg + have : a = h₁⁻¹ * (h₁ * a * h₂) * h₂⁻¹ := by group + rw [this] at ha_not + exact ha_not (H.mul_mem (H.mul_mem (H.inv_mem hh₁) hgH) (H.inv_mem hh₂)) + +section Lorimer + +variable (H : Subgroup G) (a : G) (ha_sq : a ^ 2 = 1) (ha_not : a ∉ H) + +/-- The coset graph `Sab(G, H, HaH)` for an involution `a ∉ H`. -/ +noncomputable abbrev sabidussiSymmetricGraph := + SimpleGraph.cosetGraph H (DoubleCoset.doubleCoset a (H : Set G) H) + (doubleCoset_isConnectionSet H a ha_sq ha_not) + +/-- Local transitivity at the identity coset. -/ +private theorem locallyTransitive_at_one : + IsLocallyTransitive G (G ⧸ H) (sabidussiSymmetricGraph H a ha_sq ha_not) + ((1 : G) : G ⧸ H) := by + intro w₁ w₂ hw₁ hw₂ + revert hw₁ hw₂ + refine Quotient.inductionOn₂ w₁ w₂ fun y₁ y₂ hy₁ hy₂ => ?_ + change (1 : G)⁻¹ * y₁ ∈ _ at hy₁; change (1 : G)⁻¹ * y₂ ∈ _ at hy₂ + simp only [inv_one, one_mul] at hy₁ hy₂ + obtain ⟨h₁, hh₁, k₁, hk₁, rfl⟩ := DoubleCoset.mem_doubleCoset.mp hy₁ + obtain ⟨h₂, hh₂, k₂, hk₂, rfl⟩ := DoubleCoset.mem_doubleCoset.mp hy₂ + refine ⟨h₂ * h₁⁻¹, ?_, ?_⟩ + · change (h₂ * h₁⁻¹) • ((1 : G) : G ⧸ H) = (1 : G) + rw [MulAction.Quotient.smul_coe, smul_eq_mul, mul_one] + apply QuotientGroup.eq.mpr + show (h₂ * h₁⁻¹)⁻¹ * 1 ∈ H + simp only [mul_one, mul_inv_rev, inv_inv] + exact H.mul_mem hh₁ (H.inv_mem hh₂) + · change (h₂ * h₁⁻¹) • ((h₁ * a * k₁ : G) : G ⧸ H) = (h₂ * a * k₂ : G) + rw [MulAction.Quotient.smul_coe, smul_eq_mul, QuotientGroup.eq] + have ha_inv := inv_eq_self_of_sq_eq_one ha_sq + suffices h : (h₂ * h₁⁻¹ * (h₁ * a * k₁))⁻¹ * (h₂ * a * k₂) = k₁⁻¹ * k₂ by + rw [h]; exact H.mul_mem (H.inv_mem hk₁) hk₂ + calc (h₂ * h₁⁻¹ * (h₁ * a * k₁))⁻¹ * (h₂ * a * k₂) + = (h₂ * a * k₁)⁻¹ * (h₂ * a * k₂) := by congr 1; group + _ = k₁⁻¹ * a⁻¹ * (h₂⁻¹ * (h₂ * a * k₂)) := by group + _ = k₁⁻¹ * a⁻¹ * (a * k₂) := by rw [show h₂⁻¹ * (h₂ * a * k₂) = a * k₂ from by group] + _ = k₁⁻¹ * (a⁻¹ * a) * k₂ := by group + _ = k₁⁻¹ * k₂ := by rw [ha_inv]; simp [← sq, ha_sq] + +/-- Local transitivity at any vertex, transported from `⟦1⟧`. -/ +private theorem locallyTransitive_everywhere : + ∀ q : G ⧸ H, + IsLocallyTransitive G (G ⧸ H) (sabidussiSymmetricGraph H a ha_sq ha_not) q := by + intro q w₁ w₂ hw₁ hw₂ + set Γ := sabidussiSymmetricGraph H a ha_sq ha_not + obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G ((1 : G) : G ⧸ H) q + have hw₁' : Γ.Adj ((1 : G) : G ⧸ H) (g⁻¹ • w₁) := by + have := (@GraphAction.adj_smul_iff G _ _ _ Γ _ g⁻¹ q w₁).mpr hw₁ + rwa [← hg, inv_smul_smul] at this + have hw₂' : Γ.Adj ((1 : G) : G ⧸ H) (g⁻¹ • w₂) := by + have := (@GraphAction.adj_smul_iff G _ _ _ Γ _ g⁻¹ q w₂).mpr hw₂ + rwa [← hg, inv_smul_smul] at this + obtain ⟨h, hfix, hsend⟩ := + locallyTransitive_at_one H a ha_sq ha_not (g⁻¹ • w₁) (g⁻¹ • w₂) hw₁' hw₂' + refine ⟨g * h * g⁻¹, ?_, ?_⟩ + · calc (g * h * g⁻¹) • q = g • (h • (g⁻¹ • q)) := by simp [mul_smul] + _ = g • (h • ((1 : G) : G ⧸ H)) := by rw [← hg, inv_smul_smul] + _ = g • ((1 : G) : G ⧸ H) := by rw [hfix] + _ = q := hg + · calc (g * h * g⁻¹) • w₁ = g • (h • (g⁻¹ • w₁)) := by simp [mul_smul] + _ = g • (g⁻¹ • w₂) := by rw [hsend] + _ = w₂ := smul_inv_smul g w₂ + +/-- **Lorimer's Theorem (forward direction)**: `Sab(G, H, HaH)` is arc-transitive +when `a² = 1` and `a ∉ H`. -/ +theorem lorimer_forward : + IsArcTransitive G (G ⧸ H) (sabidussiSymmetricGraph H a ha_sq ha_not) := + isArcTransitive_of_vertexTransitive_locallyTransitive _ + (locallyTransitive_everywhere H a ha_sq ha_not) + +end Lorimer + +/-! ### Lorimer's theorem (reverse direction) -/ + +/-- Under arc-transitivity, the stabilizer acts transitively on neighbors. -/ +theorem stabilizer_transitive_on_neighbors {V : Type*} [MulAction G V] + (Γ : SimpleGraph V) [IsArcTransitive G V Γ] + (v : V) {w u : V} (hw : Γ.Adj v w) (hu : Γ.Adj v u) : + ∃ h ∈ MulAction.stabilizer G v, h • w = u := by + obtain ⟨g, hgv, hgw⟩ := @IsArcTransitive.arc_transitive G V _ _ Γ _ v w v u hw hu + exact ⟨g, MulAction.mem_stabilizer_iff.mpr hgv, hgw⟩ + +/-- Under arc-transitivity, the connection set is a single double coset `HaH`. -/ +theorem connectionSet_eq_doubleCoset {V : Type*} [MulAction G V] + (Γ : SimpleGraph V) [IsArcTransitive G V Γ] + (v : V) {a : G} (ha : a ∈ connectionSet G Γ v) : + connectionSet G Γ v = + DoubleCoset.doubleCoset a (MulAction.stabilizer G v : Set G) + (MulAction.stabilizer G v) := by + ext g + constructor + · intro hg + obtain ⟨h, hh, hhw⟩ := @stabilizer_transitive_on_neighbors G _ V _ Γ _ v _ _ ha hg + rw [DoubleCoset.mem_doubleCoset] + exact ⟨h, hh, (g⁻¹ * (h * a))⁻¹, + (MulAction.stabilizer G v).inv_mem (by + rw [MulAction.mem_stabilizer_iff, mul_smul, mul_smul, hhw, inv_smul_smul]), + by group⟩ + · intro hg + obtain ⟨h₁, hh₁, h₂, hh₂, rfl⟩ := DoubleCoset.mem_doubleCoset.mp hg + exact connectionSet.double_coset_stable v ha hh₁ hh₂ + +/-- **Lorimer's Theorem (reverse direction)**: Every arc-transitive graph's connection +set is a single `(H,H)`-double coset, determined by the arc-swapping element. + +Combined with `sabidussiIso`, this shows every arc-transitive graph +is `Sab(G, stabilizer G v, HaH)` where `a` swaps an arc `(v,w)`. -/ +theorem lorimer_reverse {V : Type*} [MulAction G V] + (Γ : SimpleGraph V) [IsArcTransitive G V Γ] + (v w : V) (hvw : Γ.Adj v w) : + ∃ a : G, a • v = w ∧ a • w = v ∧ a ∉ MulAction.stabilizer G v ∧ + a ^ 2 ∈ MulAction.stabilizer G v ∧ + connectionSet G Γ v = + DoubleCoset.doubleCoset a (MulAction.stabilizer G v : Set G) + (MulAction.stabilizer G v) := by + obtain ⟨a, hav, haw⟩ := + @IsArcTransitive.arc_transitive G V _ _ Γ _ v w w v hvw (Γ.symm hvw) + refine ⟨a, hav, haw, ?_, ?_, ?_⟩ + · intro hmem + rw [MulAction.mem_stabilizer_iff] at hmem + rw [hmem] at hav + exact Γ.loopless.irrefl v (hav ▸ hvw) + · rw [MulAction.mem_stabilizer_iff, sq, mul_smul, hav, haw] + · exact connectionSet_eq_doubleCoset Γ v (by + simp only [connectionSet, Set.mem_setOf_eq, hav]; exact hvw)