Dev/MonadicDependence/Biclique/Contract.lean
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | |
| 3 | namespace Dev.MonadicDependence.Biclique |
| 4 | |
| 5 | /-- The biclique of order `k` is the complete bipartite graph `K_{k,k}` |
| 6 | on vertex set `Fin k ⊕ Fin k`: sides `a_1,…,a_k` (the `Sum.inl i`) and |
| 7 | `b_1,…,b_k` (the `Sum.inr j`), with `a_i` adjacent to `b_j` for all |
| 8 | `i, j ∈ Fin k`. |
| 9 | |
| 10 | "`G` contains the biclique of order `k` as a subgraph" (Mählmann, p. 22; |
| 11 | see `statement.tex`) is `(biclique k).IsContained G` — i.e., an injective |
| 12 | graph homomorphism `biclique k →g G`, equivalently `2k` distinct vertices |
| 13 | of `G` forming the bipartite edge pattern, with no constraint on other |
| 14 | adjacencies. Mathlib exposes this relation via the scoped notation |
| 15 | `biclique k ⊑ G` and supplies `completeBipartiteGraph_isContained_iff` |
| 16 | for a finset-level characterization. -/ |
| 17 | abbrev biclique (k : ℕ) : SimpleGraph (Fin k ⊕ Fin k) := |
| 18 | completeBipartiteGraph (Fin k) (Fin k) |
| 19 | |
| 20 | end Dev.MonadicDependence.Biclique |
| 21 |