Dev.MonadicDependence.Flip
Definition
Let \(G\) be a graph, \(\mathcal{K}\) a partition of \(V(G)\), and \(F \subseteq \mathcal{K}^2\) a symmetric relation. For a vertex \(v \in V(G)\), let \(\mathcal{K}(v) \in \mathcal{K}\) denote the unique part containing \(v\).
The flip of \(G\) by \((\mathcal{K}, F)\), denoted \(G \oplus F\) (leaving \(\mathcal{K}\) implicit when clear from context), is the graph with vertex set \(V(G)\) and with edges defined, for every pair of distinct vertices \(u, v \in V(G)\), by \[uv \in E(G \oplus F) \;\Longleftrightarrow\; \begin{cases} uv \notin E(G) & \text{if } (\mathcal{K}(u), \mathcal{K}(v)) \in F, \\ uv \in E(G) & \text{otherwise.} \end{cases}\]
We call \(G \oplus F\) a \(\mathcal{K}\)-flip of \(G\).
For \(k \in \mathbb{N}\), a graph \(H\) is a \(k\)-flip of \(G\) if there exists a partition \(\mathcal{K}\) of \(V(G)\) with \(|\mathcal{K}| \leq k\) and a symmetric relation \(F \subseteq \mathcal{K}^2\) such that \(H = G \oplus F\).
In particular, taking \(F = \emptyset\) yields \(G \oplus \emptyset = G\), so every graph \(G\) is a \(1\)-flip of itself (via the trivial one-part partition).
Review notes
Partition encoded as a coloring. Mählmann’s definition is stated in terms of a partition \(\mathcal{K}\) of \(V(G)\) and a symmetric relation \(F \subseteq \mathcal{K}^2\). We encode the partition as a coloring \(\kappa : V \to \alpha\) with \(\alpha\) the (implicit) type of colors; \(\kappa\) maps each vertex to its part, and \(F\) becomes a symmetric relation on \(\alpha\). This is equivalent to the source data: the set of parts is \(\{\kappa(v) : v \in V(G)\}\) and each part is a preimage \(\kappa^{-1}(\{c\})\). The coloring presentation is closer to Mathlib’s idioms and avoids working with partitions as sets-of-sets.
\(k\)-flip omitted. Mählmann additionally defines “\(k\)-flip” as a flip whose partition has at most \(k\) parts (p. 22). We expose only the raw flip operation; the \(k\)-flip bound is not used anywhere in the target scope (Definition MonadicDependence quantifies over all symmetric \(F\) on the fixed layer partition). We can add it later if downstream work needs it.
Symmetry is explicit. The symmetry hypothesis
Fsymm : Symmetric F is threaded through the Lean definition
(SimpleGraph’s symm field uses it). Mählmann assumes
\(F\) is symmetric but does not carry the witness; in Lean we must, so
that the resulting adjacency relation is symmetric and therefore a
genuine SimpleGraph.
Sign of the flip. The adjacency equation is
\[(\texttt{flip } G\ \kappa\ F).\text{Adj}\ u\ v
\;\Longleftrightarrow\;
u \neq v \land
(G.\text{Adj}\ u\ v \leftrightarrow \neg F\ (\kappa u)\ (\kappa v)).\]
This matches the source: when \(F\ (\kappa u)\ (\kappa v)\) holds,
adjacency is inverted; otherwise it is preserved. The framing with
\(\neg F\) on the right of the ↔︎ (rather than introducing a
case split) is compact and plays nicely with Lean’s decidability
machinery when F is a decidable relation.
Trivial flip. Taking \(F = \bot\) (the always-false relation) yields \(\texttt{flip } G\ \kappa\ \bot \cong G\) (edge-for-edge), matching Mählmann’s “\(F = \emptyset\) gives \(G \oplus \emptyset = G\)”. This is used in the proof of Lemma WeaklySparseMonDepIsNowhereDense: an unflipped star \(r'\)-crossing is a flipped star \(r'\)-crossing via the trivial flip.
Dev/MonadicDependence/Flip/Contract.lean (full)
| 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 |