Determinantal ideals of a generic matrix

This file defines minors of the generic matrix Matrix.mvPolynomialX and the ideal generated by all minors of a fixed size.

noncomputable def Matrix.mvPolynomialMinor (R : Type u_1) [CommRing R] {m : Type u_3} {n : Type u_4} {t : Type u_5} [Fintype t] [DecidableEq t] (row : t → m) (col : t → n) : MvPolynomial (m × n) R

The minor of the generic matrix selected by row and column functions.

Equations

• Matrix.mvPolynomialMinor R row col = ((Matrix.mvPolynomialX m n R).submatrix row col).det

theorem Matrix.mvPolynomialMinor_eq_det_submatrix {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} {t : Type u_5} [Fintype t] [DecidableEq t] (row : t → m) (col : t → n) : mvPolynomialMinor R row col = ((mvPolynomialX m n R).submatrix row col).det

@[simp]

theorem Matrix.mvPolynomialMinor_zero {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} {t : Type u_5} [Fintype t] [DecidableEq t] [IsEmpty t] (row : t → m) (col : t → n) : mvPolynomialMinor R row col = 1

A generic minor indexed by an empty type is 1.

@[simp]

theorem Matrix.mvPolynomialMinor_one {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} {t : Type u_5} [Fintype t] [DecidableEq t] [Unique t] (row : t → m) (col : t → n) : mvPolynomialMinor R row col = MvPolynomial.X (row default, col default)

A generic minor indexed by a unique type is the corresponding variable.

@[simp]

theorem Matrix.aeval_mvPolynomialMinor (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] {m : Type u_3} {n : Type u_4} {t : Type u_5} [Fintype t] [DecidableEq t] [Algebra R S] (A : Matrix m n S) (row : t → m) (col : t → n) : (MvPolynomial.aeval fun (ij : m × n) => A ij.1 ij.2) (mvPolynomialMinor R row col) = (A.submatrix row col).det

Evaluating a generic minor at a concrete matrix gives the corresponding concrete minor.

theorem Matrix.map_mvPolynomialMinor {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {m : Type u_3} {n : Type u_4} {t : Type u_5} [Fintype t] [DecidableEq t] (f : R →+* S) (row : t → m) (col : t → n) : (MvPolynomial.map f) (mvPolynomialMinor R row col) = mvPolynomialMinor S row col

Mapping coefficients sends a generic minor to the corresponding generic minor.

noncomputable def MvPolynomial.determinantalMinors (R : Type u_1) [CommRing R] (m : Type u_3) (n : Type u_4) (t : Type u_5) [Fintype t] [DecidableEq t] : Set (MvPolynomial (m × n) R)

The set of all minors of the generic matrix indexed by t.

Equations

• MvPolynomial.determinantalMinors R m n t = (fun (I : (t → m) × (t → n)) => Matrix.mvPolynomialMinor R I.1 I.2) '' Set.univ

theorem MvPolynomial.mem_determinantalMinors {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} {t : Type u_5} [Fintype t] [DecidableEq t] {f : MvPolynomial (m × n) R} : f ∈ determinantalMinors R m n t ↔ ∃ (row : t → m) (col : t → n), Matrix.mvPolynomialMinor R row col = f

Membership in the set of all generic minors.

noncomputable def MvPolynomial.determinantalIdeal (R : Type u_1) [CommRing R] (m : Type u_3) (n : Type u_4) (t : Type u_5) [Fintype t] [DecidableEq t] : Ideal (MvPolynomial (m × n) R)

The ideal generated by all minors of the generic matrix indexed by t.

Equations

• MvPolynomial.determinantalIdeal R m n t = Ideal.span (MvPolynomial.determinantalMinors R m n t)

theorem MvPolynomial.mvPolynomialMinor_mem_determinantalIdeal {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} {t : Type u_5} [Fintype t] [DecidableEq t] (row : t → m) (col : t → n) : Matrix.mvPolynomialMinor R row col ∈ determinantalIdeal R m n t

Every generic minor indexed by t belongs to the corresponding determinantal ideal.

theorem MvPolynomial.determinantalIdeal_le_iff {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} {t : Type u_5} [Fintype t] [DecidableEq t] {J : Ideal (MvPolynomial (m × n) R)} : determinantalIdeal R m n t ≤ J ↔ ∀ (row : t → m) (col : t → n), Matrix.mvPolynomialMinor R row col ∈ J

A determinantal ideal is contained in J iff every generating minor belongs to J.

theorem MvPolynomial.determinantalIdeal_eq_span_determinantalMinors (R : Type u_1) [CommRing R] (m : Type u_3) (n : Type u_4) (t : Type u_5) [Fintype t] [DecidableEq t] : determinantalIdeal R m n t = Ideal.span (determinantalMinors R m n t)

The determinantal ideal is the span of the set of generic minors.

theorem MvPolynomial.fg_determinantalIdeal (R : Type u_1) [CommRing R] (m : Type u_3) (n : Type u_4) (t : Type u_5) [Fintype t] [DecidableEq t] [Finite m] [Finite n] : (determinantalIdeal R m n t).FG

Determinantal ideals are finitely generated.

theorem MvPolynomial.map_determinantalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (m : Type u_3) (n : Type u_4) (t : Type u_5) [Fintype t] [DecidableEq t] (f : R →+* S) : Ideal.map (map f) (determinantalIdeal R m n t) = determinantalIdeal S m n t

Determinantal ideals commute with coefficient-wise base change.