Lax49.MixedMinorNumber

Mixed minor number

concepts/Lax49/MixedMinorNumber.lean · lax-49

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

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 view on GitHub

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 Lax49.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 Lax49.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.

Builds on

none

Used by

From Mathlib

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

Mixed minor number

Flags

Flag this concept