Dev/MonadicDependence/Subdivision/Full.lean
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | |
| 3 | namespace Dev.MonadicDependence.Subdivision |
| 4 | |
| 5 | /-- Vertex type of the `r`-subdivision of the complete graph `K_n`. |
| 6 | Either a principal vertex `.inl i` (with `i : Fin n`) or a subdivision |
| 7 | vertex `.inr (e, k)`, where `e : {p : Fin n × Fin n // p.1 < p.2}` |
| 8 | represents the edge `{e.1, e.2}` of `K_n` oriented by `<`, and |
| 9 | `k : Fin r` is its position along the path `e.1 ↝ e.2` (0-indexed). -/ |
| 10 | abbrev SubdividedCliqueVert (n r : ℕ) : Type := |
| 11 | Fin n ⊕ ({p : Fin n × Fin n // p.1 < p.2} × Fin r) |
| 12 | |
| 13 | /-- Vertex type of the `r`-subdivision of the biclique `K_{n,n}`. |
| 14 | Either a root (`.inl (.inl i)` = `aᵢ` or `.inl (.inr j)` = `bⱼ`) or a |
| 15 | subdivision vertex `.inr ((i, j), k)` = `π_{i,j,k+1}`, the `(k+1)`-st |
| 16 | interior vertex on the `a_i ↝ b_j` path (`k : Fin r`). -/ |
| 17 | abbrev SubdividedBicliqueVert (n r : ℕ) : Type := |
| 18 | (Fin n ⊕ Fin n) ⊕ ((Fin n × Fin n) × Fin r) |
| 19 | |
| 20 | /-- The `r`-subdivision of the complete graph on `Fin n`. Each edge |
| 21 | `{i, j}` of `K_n` (represented as the ordered pair `(i, j)` with `i < j`) |
| 22 | is replaced by a path of length `r + 1`: |
| 23 | `i — π₀ — π₁ — ⋯ — π_{r-1} — j`. For `r = 0` the graph equals `K_n` |
| 24 | (the subdivision-vertex component is indexed by `Fin 0 = ∅`, so it is |
| 25 | empty, and the principal-principal clause `r = 0` kicks in). |
| 26 | |
| 27 | `SimpleGraph.fromRel` adds the `x ≠ y` guard and symmetrizes by |
| 28 | disjunction, so the catch-all `False` branch accounts for pattern pairs |
| 29 | whose reverse is handled by an earlier clause. -/ |
| 30 | def subdividedClique (n r : ℕ) : SimpleGraph (SubdividedCliqueVert n r) := |
| 31 | SimpleGraph.fromRel fun x y => |
| 32 | match x, y with |
| 33 | | .inl _, .inl _ => r = 0 |
| 34 | | .inl i, .inr ⟨e, k⟩ => |
| 35 | (i = e.val.1 ∧ k.val = 0) ∨ (i = e.val.2 ∧ k.val = r - 1) |
| 36 | | .inr ⟨e, k⟩, .inr ⟨e', k'⟩ => e = e' ∧ k.val + 1 = k'.val |
| 37 | | _, _ => False |
| 38 | |
| 39 | /-- The `r`-subdivision of the biclique `K_{n,n}`. Each edge `a_i b_j` is |
| 40 | replaced by the `(r+1)`-edge path |
| 41 | `a_i — π_{i,j,1} — ⋯ — π_{i,j,r} — b_j`. For `r = 0` the graph equals |
| 42 | `K_{n,n}` (subdivision-vertex component empty; the root-root clauses |
| 43 | produce the biclique). |
| 44 | |
| 45 | Shares the vertex type with the star/clique/half-graph `r`-crossings |
| 46 | (`Dev.MonadicDependence.StarCrossing`, |
| 47 | `Dev.MonadicDependence.CliqueCrossing`, |
| 48 | `Dev.MonadicDependence.HalfGraphCrossing`), which augment this graph's |
| 49 | adjacency without changing its vertices. -/ |
| 50 | def subdividedBiclique (n r : ℕ) : SimpleGraph (SubdividedBicliqueVert n r) := |
| 51 | SimpleGraph.fromRel fun x y => |
| 52 | match x, y with |
| 53 | | .inl (.inl _), .inl (.inr _) => r = 0 |
| 54 | | .inl (.inl i), .inr ⟨⟨a, _⟩, k⟩ => i = a ∧ k.val = 0 |
| 55 | | .inl (.inr j), .inr ⟨⟨_, b⟩, k⟩ => j = b ∧ k.val = r - 1 |
| 56 | | .inr ⟨e, k⟩, .inr ⟨e', k'⟩ => e = e' ∧ k.val + 1 = k'.val |
| 57 | | _, _ => False |
| 58 | |
| 59 | end Dev.MonadicDependence.Subdivision |
| 60 |