Definition
A k-division of Fin n partitions it into k nonempty
consecutive intervals in increasing order. A row division and a column
division split a matrix into a grid of k² cells. A cell is vertical if
each of its columns is constant, horizontal if each of its rows is constant,
and mixed if it is neither. The matrix has a k-mixed minor if some pair of
row and column k-divisions makes all k² cells mixed, and its mixed
number is the largest such k.
An ordering of a finite simple graph's vertices turns its adjacency relation into such a matrix. The mixed minor number of the graph is the least mixed number of this matrix over all vertex orderings.
Lean source
| 1 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 2 | import Mathlib.Data.Nat.Lattice |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Mixed minor number |
| 7 | type: definition |
| 8 | --- |
| 9 | A *k*-division of `Fin n` partitions it into *k* nonempty |
| 10 | consecutive intervals in increasing order. A row division and a column |
| 11 | division split a matrix into a grid of *k*² cells. A cell is vertical if |
| 12 | each of its columns is constant, horizontal if each of its rows is constant, |
| 13 | and mixed if it is neither. The matrix has a *k*-mixed minor if some pair of |
| 14 | row and column *k*-divisions makes all *k*² cells mixed, and its mixed |
| 15 | number is the largest such *k*. |
| 16 | |
| 17 | An ordering of a finite simple graph's vertices turns its adjacency relation |
| 18 | into such a matrix. The mixed minor number of the graph is the least mixed |
| 19 | number of this matrix over all vertex orderings. |
| 20 | |
| 21 | # Formalization notes |
| 22 | |
| 23 | Disjointness and convexity of the parts of a `Division` follow from the |
| 24 | ordering and covering fields, so the structure does not carry them. Matrix |
| 25 | entries are truth values, so constancy of a cell's rows or columns is |
| 26 | propositional equivalence. A *k*-division of `Fin n` forces *k* ≤ *n*, so the |
| 27 | supremum in `matrixMixedNumber` ranges over a bounded set; it takes the value |
| 28 | 0 if the matrix has no mixed minor at all. Vertex |
| 29 | orderings always exist, so the infimum in `mixedMinorNumber` ranges over a |
| 30 | nonempty set. |
| 31 | -/ |
| 32 | |
| 33 | namespace Lax2.MixedMinorNumber |
| 34 | |
| 35 | /-- A division of `Fin n` into `k` nonempty consecutive intervals in |
| 36 | increasing order. Disjointness and convexity of the parts follow from |
| 37 | `part_ordered` and `part_cover`. -/ |
| 38 | structure Division (n k : ℕ) where |
| 39 | /-- The `i`-th part of the division. -/ |
| 40 | part : Fin k → Finset (Fin n) |
| 41 | /-- Every part is nonempty. -/ |
| 42 | part_nonempty : ∀ i, (part i).Nonempty |
| 43 | /-- The parts cover the whole interval. -/ |
| 44 | part_cover : ∀ x : Fin n, ∃ i, x ∈ part i |
| 45 | /-- Earlier-indexed parts lie strictly before later-indexed parts. -/ |
| 46 | part_ordered : |
| 47 | ∀ ⦃i j : Fin k⦄, i < j → |
| 48 | ∀ ⦃a b : Fin n⦄, a ∈ part i → b ∈ part j → a < b |
| 49 | |
| 50 | /-- A matrix cell is vertical when each column is constant within the row |
| 51 | part. -/ |
| 52 | def cellVertical {n m k : ℕ} (M : Fin n → Fin m → Prop) |
| 53 | (R : Division n k) (C : Division m k) (i j : Fin k) : Prop := |
| 54 | ∀ ⦃r₁ r₂ : Fin n⦄, r₁ ∈ R.part i → r₂ ∈ R.part i → |
| 55 | ∀ ⦃c : Fin m⦄, c ∈ C.part j → (M r₁ c ↔ M r₂ c) |
| 56 | |
| 57 | /-- A matrix cell is horizontal when each row is constant within the column |
| 58 | part. -/ |
| 59 | def cellHorizontal {n m k : ℕ} (M : Fin n → Fin m → Prop) |
| 60 | (R : Division n k) (C : Division m k) (i j : Fin k) : Prop := |
| 61 | ∀ ⦃r : Fin n⦄, r ∈ R.part i → |
| 62 | ∀ ⦃c₁ c₂ : Fin m⦄, c₁ ∈ C.part j → c₂ ∈ C.part j → |
| 63 | (M r c₁ ↔ M r c₂) |
| 64 | |
| 65 | /-- A matrix cell is mixed when it is neither vertical nor horizontal. -/ |
| 66 | def cellMixed {n m k : ℕ} (M : Fin n → Fin m → Prop) |
| 67 | (R : Division n k) (C : Division m k) (i j : Fin k) : Prop := |
| 68 | ¬ cellVertical M R C i j ∧ ¬ cellHorizontal M R C i j |
| 69 | |
| 70 | /-- A matrix has a `k`-mixed minor if suitable row and column `k`-divisions |
| 71 | make every induced cell mixed. -/ |
| 72 | def HasMixedMinor {n m : ℕ} (M : Fin n → Fin m → Prop) (k : ℕ) : Prop := |
| 73 | ∃ R : Division n k, ∃ C : Division m k, ∀ i j : Fin k, cellMixed M R C i j |
| 74 | |
| 75 | /-- The largest order of a mixed minor of a matrix. -/ |
| 76 | noncomputable def matrixMixedNumber {n m : ℕ} |
| 77 | (M : Fin n → Fin m → Prop) : ℕ := |
| 78 | sSup {k | HasMixedMinor M k} |
| 79 | |
| 80 | /-- The adjacency matrix of a graph in a chosen vertex order. -/ |
| 81 | def orderedAdjacency {V : Type} {n : ℕ} |
| 82 | (G : SimpleGraph V) (e : Fin n ≃ V) : Fin n → Fin n → Prop := |
| 83 | fun i j => G.Adj (e i) (e j) |
| 84 | |
| 85 | /-- The mixed minor number of a finite simple graph: the least mixed number |
| 86 | of its adjacency matrix over all vertex orderings. -/ |
| 87 | noncomputable def mixedMinorNumber {V : Type} [Fintype V] [DecidableEq V] |
| 88 | (G : SimpleGraph V) : ℕ := |
| 89 | sInf (Set.range fun e : Fin (Fintype.card V) ≃ V => |
| 90 | matrixMixedNumber (orderedAdjacency G e)) |
| 91 | |
| 92 | end Lax2.MixedMinorNumber |
| 93 |
Formalization notes
Disjointness and convexity of the parts of a Division follow from the
ordering and covering fields, so the structure does not carry them. Matrix
entries are truth values, so constancy of a cell's rows or columns is
propositional equivalence. A k-division of Fin n forces k ≤ n, so the
supremum in matrixMixedNumber ranges over a bounded set; it takes the value
0 if the matrix has no mixed minor at all. Vertex
orderings always exist, so the infimum in mixedMinorNumber ranges over a
nonempty set.
Imported
none