Dev/MonadicDependence/StarCrossing/Contract.lean

1	import Mathlib.Combinatorics.SimpleGraph.Maps
2	import Dev.MonadicDependence.Subdivision.Contract
3	import Dev.MonadicDependence.Flip.Contract
4
5	namespace Dev.MonadicDependence.StarCrossing
6
7	open Dev.MonadicDependence.Subdivision
8	open Dev.MonadicDependence.Flip
9
10	/-- The star `r`-crossing of order `n` (Mählmann p. 14): the
11	`r`-subdivided biclique. It has `2n` roots `a_i, b_j` and, for every
12	`(i, j) ∈ [n]²`, an internal `r`-vertex path
13	`a_i — π_{i,j,1} — ⋯ — π_{i,j,r} — b_j`; no other edges are present.
14	Definitionally equal to `subdividedBiclique n r`. -/
15	abbrev starCrossing (n r : ℕ) : SimpleGraph (SubdividedBicliqueVert n r) :=
16	subdividedBiclique n r
17
18	/-- The layer partition of the star / clique / half-graph `r`-crossing
19	vertex set (`SubdividedBicliqueVert n r`), indexed by `Fin (r + 2)`:
20	layer `0` = left roots `a_i` (`.inl (.inl _)`); layer `ℓ + 1` for
21	`ℓ : Fin r` = path vertices `π_{i,j,ℓ+1}` (`.inr ⟨_, ℓ⟩`); layer `r + 1`
22	= right roots `b_j` (`.inl (.inr _)`). Shared across the three crossing
23	types. -/
24	def layer {n r : ℕ} : SubdividedBicliqueVert n r → Fin (r + 2)
25	\| .inl (.inl _) => ⟨0, by omega⟩
26	\| .inr ⟨_, ℓ⟩ => ⟨ℓ.val + 1, by omega⟩
27	\| .inl (.inr _) => ⟨r + 1, by omega⟩
28
29	/-- A graph `H` is a flipped star `r`-crossing of order `n`
30	(Mählmann p. 14) iff it is isomorphic to `flip (starCrossing n r) layer
31	F Fsymm` for some symmetric relation `F` on the `r + 2` layers. Taking
32	`F = ⊥` recovers the unflipped star `r`-crossing as a special case. -/
33	def IsFlippedStarCrossing {V : Type*} (H : SimpleGraph V) (n r : ℕ) : Prop :=
34	∃ (F : Fin (r + 2) → Fin (r + 2) → Prop) (Fsymm : Symmetric F),
35	Nonempty (H ≃g flip (starCrossing n r) layer F Fsymm)
36
37	end Dev.MonadicDependence.StarCrossing
38