DetBij / Perm: the bijection theorem

From LowestUnit and LowestBound: for every field of 1-wings A x at the ones of g there is a permutation σ of the ones of g such that the agreement set of σ x and x is disjoint from A (σ x) for every x, and #{x : (σ x)_j = x_j} ≤ bdry g j for every j simultaneously.

This is the bijection theorem (Theorem 3.1 of the paper) for the inverse σ of the bijection τ of the paper; Bijection.lean states it for τ. The proof is that of the paper: a monomial of det Q' with exponents at most bdry g j (exists_lowest_Qmat, by the argument of Lemma 3.8 (iii)), and the Leibniz formula for det Q' (exists_perm_of_mem_support).

theorem AaronsonAmbainis.DetBij.exists_isLowest {ι : Type} [Fintype ι] (q : MvPolynomial ι ℤ) (hq : q ≠ 0) : ∃ (m : ι →₀ ℕ), IsLowest q m

A nonzero polynomial has a monomial of least total degree.

theorem AaronsonAmbainis.DetBij.det_Pmat_mul_det_agMatrix {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) (hA : ∀ (x : Ones g), IsWing g (↑x) (A ↑x)) : (Pmat g A).det * (agMatrix g).det = (Umat g A).det * (Qmat g A).det

det P * det M = det U * det Q'.

theorem AaronsonAmbainis.DetBij.exists_lowest_Qmat {ι : Type} [Fintype ι] [DecidableEq ι] (hU : LowestUnit) (hB : LowestBound) (g : Cube ι → Bool) (A : Cube ι → Finset ι) (hA : ∀ (x : Ones g), IsWing g (↑x) (A ↑x)) : ∃ m ∈ (Qmat g A).det.support, ∀ (j : ι), m j ≤ bdry g j

det Q' has a monomial m with m j ≤ bdry g j for all j.

theorem AaronsonAmbainis.DetBij.Qmat_prod_eq {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) (σ : Equiv.Perm (Ones g)) : ∏ x : Ones g, Qmat g A (σ x) x = if ∀ (x : Ones g), Disjoint (agSet ↑(σ x) ↑x) (A ↑(σ x)) then (MvPolynomial.monomial (∑ x : Ones g, agExp ↑(σ x) ↑x)) 1 else 0

A product of entries of Q' along a permutation is 0 or a single monomial.

theorem AaronsonAmbainis.DetBij.coeff_units_smul_ne_zero {ι : Type} (m : ι →₀ ℕ) (u : ℤˣ) (p : MvPolynomial ι ℤ) (h : (u • p).coeff m ≠ 0) : p.coeff m ≠ 0

A sign does not change whether a coefficient vanishes.

theorem AaronsonAmbainis.DetBij.exists_perm_of_mem_support {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) (m : ι →₀ ℕ) (hm : m ∈ (Qmat g A).det.support) : ∃ (σ : Equiv.Perm (Ones g)), (∀ (x : Ones g), Disjoint (agSet ↑(σ x) ↑x) (A ↑(σ x))) ∧ m = ∑ x : Ones g, agExp ↑(σ x) ↑x

Leibniz: every monomial of det Q' comes from a permutation all of whose entries are nonzero.

theorem AaronsonAmbainis.DetBij.sum_agExp_apply {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (σ : Equiv.Perm (Ones g)) (j : ι) : (∑ x : Ones g, agExp ↑(σ x) ↑x) j = {x : Ones g | ↑(σ x) j = ↑x j}.card

theorem AaronsonAmbainis.DetBij.exists_perm {ι : Type} [Fintype ι] [DecidableEq ι] (hU : LowestUnit) (hB : LowestBound) (g : Cube ι → Bool) (A : Cube ι → Finset ι) (hA : ∀ (x : Ones g), IsWing g (↑x) (A ↑x)) : ∃ (σ : Equiv.Perm (Ones g)), (∀ (x : Ones g), Disjoint (agSet ↑(σ x) ↑x) (A ↑(σ x))) ∧ ∀ (j : ι), {x : Ones g | ↑(σ x) j = ↑x j}.card ≤ bdry g j

The bijection theorem (Theorem 3.1 of the paper, for the inverse σ of the bijection τ of the paper), from LowestUnit and LowestBound.