Dev/MonadicDependence/Flip/Full.lean

1	import Mathlib.Combinatorics.SimpleGraph.Basic
2
3	namespace Dev.MonadicDependence.Flip
4
5	variable {V α : Type*}
6
7	/-- The flip `G ⊕ F` of a graph `G` by a coloring `κ : V → α` and a
8	symmetric relation `F : α → α → Prop` (Mählmann p. 22). For distinct
9	`u, v ∈ V`, the pair is adjacent in the flip iff `G`'s adjacency is
10	toggled exactly when `(κ u, κ v) ∈ F`:
11
12	- if `F (κ u) (κ v)`, then `uv ∈ E(flip)` iff `uv ∉ E(G)`;
13	- otherwise, `uv ∈ E(flip)` iff `uv ∈ E(G)`.
14
15	The coloring `κ : V → α` encodes the partition `𝓚` of Mählmann's
16	definition as the preimages of colors; `α` plays the role of the set of
17	parts. The `k`-flip concept (partition with at most `k` parts) is left
18	implicit: downstream uses only the concrete flip operation, applied to
19	specific layer partitions of the `r`-crossings. -/
20	def flip (G : SimpleGraph V) (κ : V → α) (F : α → α → Prop)
21	(Fsymm : Symmetric F) : SimpleGraph V where
22	Adj u v := u ≠ v ∧ (G.Adj u v ↔ ¬ F (κ u) (κ v))
23	symm u v := by
24	rintro ⟨hne, h⟩
25	refine ⟨Ne.symm hne, ?_⟩
26	rw [SimpleGraph.adj_comm,
27	not_congr (show F (κ v) (κ u) ↔ F (κ u) (κ v) from
28	⟨fun h => Fsymm h, fun h => Fsymm h⟩)]
29	exact h
30	loopless := ⟨fun _ ⟨hne, _⟩ => hne rfl⟩
31
32	end Dev.MonadicDependence.Flip
33