Coefficientwise multihomogeneity for matrix words

The central parameter is a univariate polynomial variable. Its coefficient ring is a multivariate polynomial ring whose variables are grouped into independent triples. The zero polynomial is homogeneous of every degree.

@[reducible, inline]

abbrev KoetheCounterexample.Mortality.HoleRing (k : Type u_1) [CommSemiring k] (N : ℕ) : Type u_1

The polynomial ring in N blocks of three hole variables.

Equations

• KoetheCounterexample.Mortality.HoleRing k N = MvPolynomial (Fin N × Fin 3) k

def KoetheCounterexample.Mortality.blockUnit {N : ℕ} (b : Fin N) : Fin N → ℕ

The multidegree contributed by one occurrence of block b.

Equations

• KoetheCounterexample.Mortality.blockUnit b c = if c = b then 1 else 0

def KoetheCounterexample.Mortality.CoeffHom {k : Type u_1} [CommRing k] {N : ℕ} (p : Polynomial (HoleRing k N)) (e : Fin N → ℕ) : Prop

The coefficients in the central parameter are all multihomogeneous of one and the same specified multidegree.

Equations

• KoetheCounterexample.Mortality.CoeffHom p e = ∀ (j : ℕ), KoetheMultiProjective.IsMultiHomogeneous (p.coeff j) e

theorem KoetheCounterexample.Mortality.multiHom_sum {k : Type u_1} [CommRing k] {N : ℕ} {ι : Type u_2} (s : Finset ι) (f : ι → HoleRing k N) {e : Fin N → ℕ} (hf : ∀ i ∈ s, KoetheMultiProjective.IsMultiHomogeneous (f i) e) : KoetheMultiProjective.IsMultiHomogeneous (∑ i ∈ s, f i) e

theorem KoetheCounterexample.Mortality.multiHom_C {k : Type u_1} [CommRing k] {N : ℕ} (a : k) : KoetheMultiProjective.IsMultiHomogeneous (MvPolynomial.C a) 0

theorem KoetheCounterexample.Mortality.multiHom_X {k : Type u_1} [CommRing k] {N : ℕ} (b : Fin N) (j : Fin 3) : KoetheMultiProjective.IsMultiHomogeneous (MvPolynomial.X (b, j)) (blockUnit b)

@[simp]

theorem KoetheCounterexample.Mortality.coeffHom_zero {k : Type u_1} [CommRing k] {N : ℕ} (e : Fin N → ℕ) : CoeffHom 0 e

theorem KoetheCounterexample.Mortality.coeffHom_C {k : Type u_1} [CommRing k] {N : ℕ} {a : HoleRing k N} {e : Fin N → ℕ} (ha : KoetheMultiProjective.IsMultiHomogeneous a e) : CoeffHom (Polynomial.C a) e

@[simp]

theorem KoetheCounterexample.Mortality.coeffHom_one {k : Type u_1} [CommRing k] {N : ℕ} : CoeffHom 1 0

theorem KoetheCounterexample.Mortality.coeffHom_intCast {k : Type u_1} [CommRing k] {N : ℕ} (z : ℤ) : CoeffHom (↑z) 0

theorem KoetheCounterexample.Mortality.coeffHom_X {k : Type u_1} [CommRing k] {N : ℕ} : CoeffHom Polynomial.X 0

theorem KoetheCounterexample.Mortality.CoeffHom.add {k : Type u_1} [CommRing k] {N : ℕ} {p q : Polynomial (HoleRing k N)} {e : Fin N → ℕ} (hp : CoeffHom p e) (hq : CoeffHom q e) : CoeffHom (p + q) e

theorem KoetheCounterexample.Mortality.CoeffHom.sum {k : Type u_1} [CommRing k] {N : ℕ} {ι : Type u_2} (s : Finset ι) (f : ι → Polynomial (HoleRing k N)) {e : Fin N → ℕ} (hf : ∀ i ∈ s, CoeffHom (f i) e) : CoeffHom (∑ i ∈ s, f i) e

theorem KoetheCounterexample.Mortality.CoeffHom.mul {k : Type u_1} [CommRing k] {N : ℕ} {p q : Polynomial (HoleRing k N)} {e f : Fin N → ℕ} (hp : CoeffHom p e) (hq : CoeffHom q f) : CoeffHom (p * q) (e + f)

theorem KoetheCounterexample.Mortality.CoeffHom.prod {k : Type u_1} [CommRing k] {N : ℕ} {ι : Type u_2} (s : Finset ι) (f : ι → Polynomial (HoleRing k N)) (e : ι → Fin N → ℕ) (hf : ∀ i ∈ s, CoeffHom (f i) (e i)) : CoeffHom (∏ i ∈ s, f i) (∑ i ∈ s, e i)

def KoetheCounterexample.Mortality.MatrixCoeffHom {k : Type u_1} [CommRing k] {N : ℕ} {m : Type u_2} {n : Type u_3} (A : Matrix m n (Polynomial (HoleRing k N))) (e : Fin N → ℕ) : Prop

The common multidegree of every coefficient of every matrix entry.

Equations

• KoetheCounterexample.Mortality.MatrixCoeffHom A e = ∀ (i : m) (j : n), KoetheCounterexample.Mortality.CoeffHom (A i j) e

theorem KoetheCounterexample.Mortality.matrixCoeffHom_one {k : Type u_1} [CommRing k] {N : ℕ} {n : Type u_2} [DecidableEq n] : MatrixCoeffHom 1 0

theorem KoetheCounterexample.Mortality.MatrixCoeffHom.mul {k : Type u_1} [CommRing k] {N : ℕ} {m : Type u_2} {n : Type u_3} {o : Type u_4} [Fintype n] {A : Matrix m n (Polynomial (HoleRing k N))} {B : Matrix n o (Polynomial (HoleRing k N))} {e f : Fin N → ℕ} (hA : MatrixCoeffHom A e) (hB : MatrixCoeffHom B f) : MatrixCoeffHom (A * B) (e + f)

theorem KoetheCounterexample.Mortality.MatrixCoeffHom.det {k : Type u_1} [CommRing k] {N r : ℕ} {A : Matrix (Fin r) (Fin r) (Polynomial (HoleRing k N))} {e : Fin N → ℕ} (hA : MatrixCoeffHom A e) : CoeffHom A.det fun (b : Fin N) => r * e b

theorem KoetheCounterexample.Mortality.matrixCoeffHom_prod {k : Type u_1} [CommRing k] {N : ℕ} {n : Type u_2} {α : Type u_3} [Fintype n] [DecidableEq n] (w : List α) (L : α → Matrix n n (Polynomial (HoleRing k N))) (e : α → Fin N → ℕ) (hw : ∀ a ∈ w, MatrixCoeffHom (L a) (e a)) : MatrixCoeffHom (List.map L w).prod (List.map e w).sum

theorem KoetheCounterexample.Mortality.lift_coeffHom {k : Type u_1} [Field k] {N d : ℕ} (P : Pencil k d) (a : Fin 3 → HoleRing k N) (e : Fin N → ℕ) (ha : ∀ (i : Fin 3), KoetheMultiProjective.IsMultiHomogeneous (a i) e) : MatrixCoeffHom (P.lift a) e