DeterminantalBlockStabilization.lean

1 import PaperXII.DeterminantalStabilization
2 import Mathlib.Data.Fintype.Option
3 
4 noncomputable section
5 namespace PaperXII.DeterminantalIdeals
6 open Matrix
7 variable {R : Type*} [CommRing R] {m n m' n' : Type*}
8 
9 theorem presentationIdeal_submatrix_equiv [Fintype m] [Fintype m']
10     (A : Matrix m n R) (e : m' ≃ m) (f : n' ≃ n) (j : ℕ) :
11     presentationIdeal (A.submatrix e f) j = presentationIdeal A j := by
12   simp only [presentationIdeal, Fintype.card_congr e, minorIdeal_submatrix_equiv]
13 
14 /-- Stabilization by an arbitrary finite identity block. -/
15 def stabilizeBlock (A : Matrix m n R) (q : Type*) : Matrix (m ⊕ q) (n ⊕ q) R := by
16   classical
17   exact Matrix.fromBlocks A 0 0 1
18 
19 @[simp] theorem stabilizeBlock_inl_inl (A : Matrix m n R) (q : Type*) (i : m) (j : n) :
20     stabilizeBlock A q (.inl i) (.inl j) = A i j := rfl
21 @[simp] theorem stabilizeBlock_inl_inr (A : Matrix m n R) (q : Type*) (i : m) (j : q) :
22     stabilizeBlock A q (.inl i) (.inr j) = 0 := rfl
23 @[simp] theorem stabilizeBlock_inr_inl (A : Matrix m n R) (q : Type*) (i : q) (j : n) :
24     stabilizeBlock A q (.inr i) (.inl j) = 0 := rfl
25 @[simp] theorem stabilizeBlock_inr_inr (A : Matrix m n R) (q : Type*) [DecidableEq q] (i j : q) :
26     stabilizeBlock A q (.inr i) (.inr j) = if i = j then 1 else 0 := by
27   classical
28   simp [stabilizeBlock, Matrix.one_apply]
29 
30 def optionSumEquiv (α β : Type*) : α ⊕ Option β ≃ Option (α ⊕ β) where
31   toFun := fun x => match x with
32     | .inl a => some (.inl a)
33     | .inr none => none
34     | .inr (some b) => some (.inr b)
35   invFun := fun x => match x with
36     | none => .inr none
37     | some (.inl a) => .inl a
38     | some (.inr b) => .inr (some b)
39   left_inv := by intro x; rcases x with a | (_ | b) <;> rfl
40   right_inv := by intro x; rcases x with _ | (a | b) <;> rfl
41 
42 theorem stabilizeBlock_option (A : Matrix m n R) (q : Type*) :
43     stabilizeBlock A (Option q) =
44       (stabilize (stabilizeBlock A q)).submatrix (optionSumEquiv m q) (optionSumEquiv n q) := by
45   classical
46   ext i j
47   rcases i with a | (_ | b) <;> rcases j with c | (_ | d) <;>
48     simp [Matrix.submatrix_apply, optionSumEquiv, stabilize]
49 
50 theorem stabilizeBlock_equiv (A : Matrix m n R) {q q' : Type*} (e : q ≃ q') :
51     (stabilizeBlock A q').submatrix (Equiv.sumCongr (Equiv.refl m) e)
52       (Equiv.sumCongr (Equiv.refl n) e) = stabilizeBlock A q := by
53   classical
54   ext i j
55   rcases i with i | i <;> rcases j with j | j <;>
56     simp [Matrix.submatrix_apply]
57 
58 theorem presentationIdeal_stabilizeBlock [Fintype m] (A : Matrix m n R)
59     (q : Type*) [Fintype q] (j : ℕ) :
60     presentationIdeal (stabilizeBlock A q) j = presentationIdeal A j := by
61   classical
62   refine Fintype.induction_empty_option (P := fun q _ =>
63     presentationIdeal (stabilizeBlock A q) j = presentationIdeal A j) ?_ ?_ ?_ q
64   · intro α β _ e h
65     let : Fintype α := Fintype.ofEquiv β e.symm
66     rw [← presentationIdeal_submatrix_equiv (stabilizeBlock A β)
67       (Equiv.sumCongr (Equiv.refl m) e) (Equiv.sumCongr (Equiv.refl n) e) j,
68       stabilizeBlock_equiv]
69     exact h
70   · have h : stabilizeBlock A PEmpty = A.submatrix (Equiv.sumEmpty m PEmpty)
71         (Equiv.sumEmpty n PEmpty) := by
72       ext i k
73       rcases i with i | i
74       · rcases k with k | k
75         · rfl
76         · exact isEmptyElim k
77       · exact isEmptyElim i
78     rw [h, presentationIdeal_submatrix_equiv]
79   · intro α _ h
80     rw [stabilizeBlock_option, presentationIdeal_submatrix_equiv,
81       presentationIdeal_stabilize, h]
82 
83 end PaperXII.DeterminantalIdeals

Back to source controls