Dev/MonadicDependence/CliqueCrossing/Contract.lean
| 1 | import Mathlib.Combinatorics.SimpleGraph.Maps |
| 2 | import Dev.MonadicDependence.Flip.Contract |
| 3 | import Dev.MonadicDependence.StarCrossing.Contract |
| 4 | |
| 5 | namespace Dev.MonadicDependence.CliqueCrossing |
| 6 | |
| 7 | open Dev.MonadicDependence.Subdivision |
| 8 | open Dev.MonadicDependence.Flip |
| 9 | open Dev.MonadicDependence.StarCrossing |
| 10 | |
| 11 | /-- The clique `r`-crossing of order `n` (Mählmann p. 14). Obtained from |
| 12 | the star `r`-crossing (`starCrossing n r`) by turning each root's |
| 13 | adjacent path-endpoint set into a clique: |
| 14 | |
| 15 | * for every `i : Fin n` and distinct `j, j' : Fin n`, add the edge |
| 16 | `π_{i,j,1} — π_{i,j',1}` (left end, at root `a_i`); |
| 17 | * for every `j : Fin n` and distinct `i, i' : Fin n`, add the edge |
| 18 | `π_{i,j,r} — π_{i',j,r}` (right end, at root `b_j`). |
| 19 | |
| 20 | The interior path vertices `π_{i,j,ℓ}` for `2 ≤ ℓ ≤ r − 1` keep the same |
| 21 | neighborhoods as in the star crossing. `SimpleGraph.fromRel` adds the |
| 22 | `x ≠ y` guard, so the distinct-edge requirement (`j ≠ j'` for the left |
| 23 | clique, `i ≠ i'` for the right) is automatic. -/ |
| 24 | def cliqueCrossing (n r : ℕ) : SimpleGraph (SubdividedBicliqueVert n r) := |
| 25 | starCrossing n r ⊔ |
| 26 | (SimpleGraph.fromRel fun x y => |
| 27 | match x, y with |
| 28 | | .inr ⟨⟨i, _⟩, k⟩, .inr ⟨⟨i', _⟩, k'⟩ => |
| 29 | (i = i' ∧ k.val = 0 ∧ k'.val = 0) |
| 30 | | _, _ => False) ⊔ |
| 31 | (SimpleGraph.fromRel fun x y => |
| 32 | match x, y with |
| 33 | | .inr ⟨⟨_, j⟩, k⟩, .inr ⟨⟨_, j'⟩, k'⟩ => |
| 34 | (j = j' ∧ k.val = r - 1 ∧ k'.val = r - 1) |
| 35 | | _, _ => False) |
| 36 | |
| 37 | /-- A graph `H` is a *flipped clique `r`-crossing of order `n`* |
| 38 | (Mählmann p. 14) iff it is isomorphic to `flip (cliqueCrossing n r) layer |
| 39 | F Fsymm` for some symmetric relation `F` on the `r + 2` layers. The |
| 40 | layer partition is shared with the star `r`-crossing |
| 41 | (`Dev.MonadicDependence.StarCrossing.layer`). -/ |
| 42 | def IsFlippedCliqueCrossing {V : Type*} (H : SimpleGraph V) (n r : ℕ) : Prop := |
| 43 | ∃ (F : Fin (r + 2) → Fin (r + 2) → Prop) (Fsymm : Symmetric F), |
| 44 | Nonempty (H ≃g flip (cliqueCrossing n r) layer F Fsymm) |
| 45 | |
| 46 | end Dev.MonadicDependence.CliqueCrossing |
| 47 |