Dev/MonadicDependence/HalfGraphCrossing/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.HalfGraphCrossing
6
7	open Dev.MonadicDependence.Subdivision
8	open Dev.MonadicDependence.Flip
9	open Dev.MonadicDependence.StarCrossing
10
11	/-- The half-graph `r`-crossing of order `n` (Mählmann p. 14). Same
12	vertex set as the star `r`-crossing (`SubdividedBicliqueVert n r`).
13	Edges:
14
15	* interior path edges
16	`π_{i,j,ℓ} — π_{i,j,ℓ+1}` for every `(i, j) ∈ [n]²` and `ℓ ∈ [r − 1]`;
17	* left half-graph ends `a_i — π_{i',j,1}` for every `i ≤ i'` and
18	`j ∈ [n]`;
19	* right half-graph ends `b_j — π_{i,j',r}` for every `j ≤ j'` and
20	`i ∈ [n]`.
21
22	No other edges. Intended for `r ≥ 1`; for `r = 0` the definition yields
23	the empty graph on `SubdividedBicliqueVert n 0 ≃ Fin n ⊕ Fin n` (no
24	path vertices, no root edges), which lies outside Mählmann's scope. -/
25	def halfGraphCrossing (n r : ℕ) : SimpleGraph (SubdividedBicliqueVert n r) :=
26	SimpleGraph.fromRel fun x y =>
27	match x, y with
28	\| .inr ⟨e, k⟩, .inr ⟨e', k'⟩ => e = e' ∧ k.val + 1 = k'.val
29	\| .inl (.inl i), .inr ⟨⟨i', _⟩, k⟩ => i ≤ i' ∧ k.val = 0
30	\| .inl (.inr j), .inr ⟨⟨_, j'⟩, k⟩ => j ≤ j' ∧ k.val = r - 1
31	\| _, _ => False
32
33	/-- A graph `H` is a flipped half-graph `r`-crossing of order `n`
34	(Mählmann p. 14) iff it is isomorphic to `flip (halfGraphCrossing n r)
35	layer F Fsymm` for some symmetric relation `F` on the `r + 2` layers.
36	The layer partition is shared with the star `r`-crossing
37	(`Dev.MonadicDependence.StarCrossing.layer`). -/
38	def IsFlippedHalfGraphCrossing {V : Type*} (H : SimpleGraph V) (n r : ℕ) : Prop :=
39	∃ (F : Fin (r + 2) → Fin (r + 2) → Prop) (Fsymm : Symmetric F),
40	Nonempty (H ≃g flip (halfGraphCrossing n r) layer F Fsymm)
41
42	end Dev.MonadicDependence.HalfGraphCrossing
43