DeterminantalStabilization.lean

1 import PaperXII.DeterminantalIdeals
2 
3 /-! Exact preservation under elementary stabilization of a presentation matrix. -/
4 noncomputable section
5 namespace PaperXII.DeterminantalIdeals
6 open Matrix
7 variable {R : Type*} [CommRing R] {m n m' n' : Type*}
8 
9 /-- Reindexing rows or columns does not change the determinantal ideal. -/
10 theorem minorIdeal_submatrix_equiv (A : Matrix m n R) (e : m' ≃ m) (f : n' ≃ n)
11     (k : ℕ) : minorIdeal (A.submatrix e f) k = minorIdeal A k := by
12   apply le_antisymm
13   · apply (minorIdeal_le_iff _ _ _).2
14     intro r c
15     exact minor_mem A k (e ∘ r) (f ∘ c)
16   · apply (minorIdeal_le_iff _ _ _).2
17     intro r c
18     simpa only [Matrix.submatrix_submatrix, Function.comp_def, Equiv.apply_symm_apply]
19       using minor_mem (A.submatrix e f) k (e.symm ∘ r) (f.symm ∘ c)
20 
21 theorem det_submatrix_zero_of_not_injective_rows (A : Matrix m n R) {k : ℕ}
22     (r : Fin k → m) (c : Fin k → n) (h : ¬ Function.Injective r) :
23     (A.submatrix r c).det = 0 := by
24   obtain ⟨i,j,hij,hne⟩ := Function.not_injective_iff.mp h
25   exact Matrix.det_zero_of_row_eq hne (by ext t; simp [Matrix.submatrix_apply, hij])
26 
27 theorem det_submatrix_zero_of_not_injective_cols (A : Matrix m n R) {k : ℕ}
28     (r : Fin k → m) (c : Fin k → n) (h : ¬ Function.Injective c) :
29     (A.submatrix r c).det = 0 := by
30   obtain ⟨i,j,hij,hne⟩ := Function.not_injective_iff.mp h
31   exact Matrix.det_zero_of_column_eq hne (by intro t; simp [Matrix.submatrix_apply, hij])
32 
33 /-- Adding one generator together with its defining relation. -/
34 def stabilize (A : Matrix m n R) : Matrix (Option m) (Option n) R
35   | none, none => 1
36   | some i, some j => A i j
37   | _, _ => 0
38 
39 @[simp] theorem stabilize_none_none (A : Matrix m n R) : stabilize A none none = 1 := rfl
40 @[simp] theorem stabilize_none_some (A : Matrix m n R) (j : n) : stabilize A none (some j) = 0 := rfl
41 @[simp] theorem stabilize_some_none (A : Matrix m n R) (i : m) : stabilize A (some i) none = 0 := rfl
42 @[simp] theorem stabilize_some_some (A : Matrix m n R) (i : m) (j : n) :
43     stabilize A (some i) (some j) = A i j := rfl
44 
45 private theorem option_factor {α β : Type*} (r : α → Option β) (h : ∀ i, r i ≠ none) :
46     ∃ s : α → β, ∀ i, r i = some (s i) := by
47   choose s hs using fun i => Option.ne_none_iff_exists'.mp (h i)
48   exact ⟨s,hs⟩
49 
50 /-- Appending an identity corner shifts minor order by exactly one. -/
51 theorem minorIdeal_stabilize (A : Matrix m n R) (k : ℕ) :
52     minorIdeal (stabilize A) (k+1) = minorIdeal A k := by
53   classical
54   apply le_antisymm
55   · apply (minorIdeal_le_iff _ _ _).2
56     intro r c
57     by_cases hr : Function.Injective r
58     · by_cases hc : Function.Injective c
59       · by_cases hnone : ∃ i, r i = none
60         · obtain ⟨i,hi⟩ := hnone
61           rw [Matrix.det_succ_row _ i]
62           apply Ideal.sum_mem
63           intro j _
64           cases hj : c j with
65           | some t => simp [Matrix.submatrix_apply, hi, hj]
66           | none =>
67             obtain ⟨r',hr'⟩ := option_factor (r ∘ i.succAbove) (by
68               intro a h
69               exact Fin.succAbove_ne i a (hr (h.trans hi.symm)))
70             obtain ⟨c',hc'⟩ := option_factor (c ∘ j.succAbove) (by
71               intro b h
72               exact Fin.succAbove_ne j b (hc (h.trans hj.symm)))
73             have hsub : ((stabilize A).submatrix r c).submatrix i.succAbove j.succAbove =
74                 A.submatrix r' c' := by
75               ext a b
76               simp only [Matrix.submatrix_apply]
77               change stabilize A ((r ∘ i.succAbove) a) ((c ∘ j.succAbove) b) = _
78               rw [hr' a, hc' b]
79               rfl
80             rw [hsub]
81             exact Ideal.mul_mem_left _ _ (minor_mem A k r' c')
82         · have hrnone : ∀ i, r i ≠ none := by simpa using hnone
83           obtain ⟨r',hr'⟩ := option_factor r hrnone
84           by_cases hcnone : ∃ j, c j = none
85           · obtain ⟨j,hj⟩ := hcnone
86             have hz : ((stabilize A).submatrix r c).det = 0 :=
87               Matrix.det_eq_zero_of_column_eq_zero j (by intro i; simp [Matrix.submatrix_apply,hr' i,hj])
88             rw [hz]
89             exact Ideal.zero_mem _
90           · obtain ⟨c',hc'⟩ := option_factor c (by simpa using hcnone)
91             have hsub : (stabilize A).submatrix r c = A.submatrix r' c' := by
92               ext i j
93               simp [Matrix.submatrix_apply,hr' i,hc' j]
94             rw [hsub]
95             exact minorIdeal_succ_le A k (minor_mem A (k+1) r' c')
96       · rw [det_submatrix_zero_of_not_injective_cols _ r c hc]
97         exact Ideal.zero_mem _
98     · rw [det_submatrix_zero_of_not_injective_rows _ r c hr]
99       exact Ideal.zero_mem _
100   · apply (minorIdeal_le_iff _ _ _).2
101     intro r c
102     let r' : Fin (k+1) → Option m := Fin.cons none (fun i => some (r i))
103     let c' : Fin (k+1) → Option n := Fin.cons none (fun i => some (c i))
104     have heq : ((stabilize A).submatrix r' c').det = (A.submatrix r c).det := by
105       rw [Matrix.det_succ_row_zero, Fin.sum_univ_succ]
106       simp [r',c',Matrix.submatrix_apply,Matrix.submatrix_submatrix,
107         Function.comp_def,Fin.succAbove_zero]; rfl
108     rw [← heq]
109     exact minor_mem (stabilize A) (k+1) r' c'
110 
111 /-- The usual reversed-index Fitting ideal of a specified presentation matrix. -/
112 def presentationIdeal [Fintype m] (A : Matrix m n R) (j : ℕ) : Ideal R :=
113   minorIdeal A (Fintype.card m - j)
114 
115 /-- The natural-number boundary is handled explicitly: indices above generator rank give top. -/
116 theorem presentationIdeal_eq_top [Fintype m] (A : Matrix m n R) {j : ℕ}
117     (h : Fintype.card m ≤ j) : presentationIdeal A j = ⊤ := by
118   simp [presentationIdeal, Nat.sub_eq_zero_of_le h]
119 
120 theorem presentationIdeal_stabilize [Fintype m] (A : Matrix m n R) (j : ℕ) :
121     presentationIdeal (stabilize A) j = presentationIdeal A j := by
122   by_cases h : j ≤ Fintype.card m
123   · simp only [presentationIdeal, Fintype.card_option]
124     have hn : Fintype.card m + 1 - j = (Fintype.card m - j) + 1 := by omega
125     rw [hn, minorIdeal_stabilize]
126   · have h₁ : Fintype.card m ≤ j := by omega
127     have h₂ : Fintype.card (Option m) ≤ j := by simp only [Fintype.card_option]; omega
128     rw [presentationIdeal_eq_top _ h₁, presentationIdeal_eq_top _ h₂]
129 
130 end PaperXII.DeterminantalIdeals

Back to source controls