Matrix entries lying in an ideal

A two-sided ideal containing every entry of a matrix contains every entry of any two-sided product formed from it, and an ideal contains every entry of any linear combination of matrices whose entries it contains: each such entry is an S-combination of entries of the original matrices.

Nothing here needs invertibility, a square shape, or a diagonal target — only that the products are conformable — so the statements are rectangular. Both hold over any Semiring; the two-sided product statement asks the ideal to be two-sided (Ideal.IsTwoSided), which is automatic over a commutative semiring. They are the membership computations a defining-ideal closure proof performs when it propagates a relation through a matrix identity.

Main results

• Matrix.mul_mul_apply_mem: every entry of P * A * Q lies in a two-sided ideal containing every entry of A.
• Matrix.sum_smul_apply_mem: every entry of ∑ a, c a • F a lies in an ideal containing every entry of every F a.

theorem Matrix.mul_mul_apply_mem {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {S : Type u_6} [Semiring S] [Fintype m] [Fintype n] {A : Matrix m n S} {I : Ideal S} [I.IsTwoSided] (hA : ∀ (i : m) (j : n), A i j ∈ I) (P : Matrix l m S) (Q : Matrix n o S) (i : l) (j : o) : (P * A * Q) i j ∈ I

A two-sided ideal containing the entries of a matrix contains the entries of any two-sided product formed from it. Each entry of P * A * Q is an S-combination of entries of A.

theorem Matrix.sum_smul_apply_mem {m : Type u_2} {n : Type u_3} {ι : Type u_5} {S : Type u_6} [Semiring S] [Fintype ι] {F : ι → Matrix m n S} {I : Ideal S} (hF : ∀ (a : ι) (i : m) (j : n), F a i j ∈ I) (c : ι → S) (i : m) (j : n) : (∑ a : ι, c a • F a) i j ∈ I

An ideal containing the entries of a family of matrices contains the entries of every linear combination of them.