DeterminantalIdeals.lean

1 import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
2 import Mathlib.RingTheory.Ideal.Maps
3 import Mathlib.RingTheory.Ideal.BigOperators
4 import Mathlib.Tactic.Abel
5 import Mathlib.Tactic.Choose
6 
7 /-!
8 # Determinantal ideals for Paper XII
9 
10 These are ideals of actual minors, not supplied invariant ideals. Repeated row or
11 column indices are permitted in the generating family; their determinants vanish.
12 This module is infrastructure, not yet the presentation-independence theorem.
13 -/
14 noncomputable section
15 namespace PaperXII.DeterminantalIdeals
16 open Matrix
17 variable {R S : Type*} [CommRing R] [CommRing S]
18 variable {m n p : Type*}
19 
20 /-- Ideal generated by all size-`k` minors. The empty minor equals one. -/
21 def minorIdeal (A : Matrix m n R) (k : ℕ) : Ideal R :=
22   Ideal.span (Set.range fun rc : (Fin k → m) × (Fin k → n) =>
23     (A.submatrix rc.1 rc.2).det)
24 
25 theorem minor_mem (A : Matrix m n R) (k : ℕ)
26     (r : Fin k → m) (c : Fin k → n) :
27     (A.submatrix r c).det ∈ minorIdeal A k :=
28   Ideal.subset_span ⟨(r,c), rfl⟩
29 
30 theorem minorIdeal_le_iff (A : Matrix m n R) (k : ℕ) (J : Ideal R) :
31     minorIdeal A k ≤ J ↔ ∀ (r : Fin k → m) (c : Fin k → n), (A.submatrix r c).det ∈ J := by
32   rw [minorIdeal, Ideal.span_le]
33   constructor
34   · intro h r c
35     exact h ⟨(r,c),rfl⟩
36   · rintro h _ ⟨⟨r,c⟩,rfl⟩
37     exact h r c
38 
39 @[simp] theorem minorIdeal_zero (A : Matrix m n R) : minorIdeal A 0 = ⊤ := by
40   apply (Ideal.eq_top_iff_one _).mpr
41   simpa using minor_mem A 0 Fin.elim0 Fin.elim0
42 
43 /-- Minors commute with an arbitrary coefficient-ring map. No flatness is used. -/
44 theorem minorIdeal_map (f : R →+* S) (A : Matrix m n R) (k : ℕ) :
45     minorIdeal (A.map f) k = Ideal.map f (minorIdeal A k) := by
46   rw [minorIdeal, minorIdeal, Ideal.map_span]
47   congr 1
48   ext x
49   constructor
50   · rintro ⟨⟨r,c⟩,rfl⟩
51     refine ⟨(A.submatrix r c).det, ⟨(r,c),rfl⟩, ?_⟩
52     exact f.map_det _
53   · rintro ⟨_, ⟨⟨r,c⟩,rfl⟩,rfl⟩
54     exact ⟨(r,c), (f.map_det _).symm⟩
55 
56 @[simp] theorem minorIdeal_transpose (A : Matrix m n R) (k : ℕ) :
57     minorIdeal A.transpose k = minorIdeal A k := by
58   apply le_antisymm
59   · apply (minorIdeal_le_iff _ _ _).2
60     intro r c
61     simpa only [← Matrix.transpose_submatrix, Matrix.det_transpose] using minor_mem A k c r
62   · apply (minorIdeal_le_iff _ _ _).2
63     intro r c
64     simpa only [← Matrix.transpose_submatrix, Matrix.det_transpose,
65       Matrix.transpose_transpose] using minor_mem A.transpose k c r
66 
67 /-- Laplace expansion gives the descending determinantal filtration. -/
68 theorem minorIdeal_succ_le (A : Matrix m n R) (k : ℕ) :
69     minorIdeal A (k+1) ≤ minorIdeal A k := by
70   apply (minorIdeal_le_iff _ _ _).2
71   intro r c
72   rw [Matrix.det_succ_row _ 0]
73   apply Ideal.sum_mem
74   intro j _
75   exact Ideal.mul_mem_left _ _ (minor_mem A k (r ∘ (0 : Fin (k+1)).succAbove)
76     (c ∘ j.succAbove))
77 
78 /-- Rectangular matrix multiplication cannot enlarge the minors ideal of the right factor. -/
79 theorem minorIdeal_mul_le_right [Fintype n] (A : Matrix m n R) (B : Matrix n p R)
80     (k : ℕ) : minorIdeal (A * B) k ≤ minorIdeal B k := by
81   apply (minorIdeal_le_iff _ _ _).2
82   intro r c
83   have hrows : (A * B).submatrix r c =
84       fun i => ∑ t : n, A (r i) t • (fun j => B t (c j)) := by
85     ext i j
86     simp [Matrix.mul_apply, Matrix.submatrix_apply, Pi.smul_apply, Finset.sum_apply]
87   rw [hrows]
88   change (Matrix.detRowAlternating (R := R) (n := Fin k)).toMultilinearMap
89     (fun i => ∑ t : n, A (r i) t • (fun j => B t (c j))) ∈ minorIdeal B k
90   rw [MultilinearMap.map_sum]
91   apply Ideal.sum_mem
92   intro t _
93   change Matrix.detRowAlternating (fun i => A (r i) (t i) • (fun j => B (t i) (c j))) ∈ minorIdeal B k
94   rw [Matrix.detRowAlternating.map_smul_univ]
95   exact (minorIdeal B k).smul_mem _ (minor_mem B k t c)
96 
97 /-- The analogous left-factor inclusion. -/
98 theorem minorIdeal_mul_le_left [Fintype n] (A : Matrix m n R) (B : Matrix n p R)
99     (k : ℕ) : minorIdeal (A * B) k ≤ minorIdeal A k := by
100   have h := minorIdeal_mul_le_right B.transpose A.transpose k
101   simpa only [← Matrix.transpose_mul, minorIdeal_transpose] using h
102 
103 /-- An actual two-sided inverse gives invariance, not merely containment. -/
104 theorem minorIdeal_mul_left_eq [Fintype m] [DecidableEq m] (U V : Matrix m m R)
105     (hVU : V * U = 1) (A : Matrix m n R) (k : ℕ) :
106     minorIdeal (U * A) k = minorIdeal A k := by
107   classical
108   apply le_antisymm (minorIdeal_mul_le_right U A k)
109   have h := minorIdeal_mul_le_right V (U*A) k
110   simpa only [← Matrix.mul_assoc, hVU, Matrix.one_mul] using h
111 
112 theorem minorIdeal_mul_right_eq [Fintype n] [DecidableEq n] (U V : Matrix n n R)
113     (hUV : U * V = 1) (A : Matrix m n R) (k : ℕ) :
114     minorIdeal (A * U) k = minorIdeal A k := by
115   classical
116   apply le_antisymm (minorIdeal_mul_le_left A U k)
117   have h := minorIdeal_mul_le_left (A*U) V k
118   simpa only [Matrix.mul_assoc, hUV, Matrix.mul_one] using h
119 
120 /-- Adding or removing redundant relation columns is harmless if both matrices factor. -/
121 theorem minorIdeal_eq_of_mutual_factorization [Fintype n] [Fintype p]
122     (A : Matrix m n R) (B : Matrix m p R)
123     (C : Matrix p n R) (D : Matrix n p R) (hA : B*C=A) (hB : A*D=B) (k : ℕ) :
124     minorIdeal A k = minorIdeal B k := by
125   apply le_antisymm
126   · rw [← hA]
127     exact minorIdeal_mul_le_left B C k
128   · rw [← hB]
129     exact minorIdeal_mul_le_left A D k
130 
131 end PaperXII.DeterminantalIdeals

Back to source controls