PresentationComparison.lean

1 import PaperXII.DeterminantalBlockStabilization
2 import Mathlib.LinearAlgebra.Matrix.ToLin
3 import Mathlib.Algebra.Module.Projective
4 
5 noncomputable section
6 namespace PaperXII.DeterminantalIdeals
7 open Matrix
8 variable {R : Type*} [CommRing R] {m n p q : Type*}
9 
10 /-- A relation-submodule inclusion constructs a matrix factorization. -/
11 theorem exists_factor_of_range_le [Fintype n] [Fintype p]
12     (U : Matrix m n R) (V : Matrix m p R)
13     (hUV : U.mulVecLin.range ≤ V.mulVecLin.range) :
14     ∃ C : Matrix p n R, V * C = U := by
15   classical
16   let f : (n → R) →ₗ[R] V.mulVecLin.range :=
17     U.mulVecLin.codRestrict _ (fun x => hUV (LinearMap.mem_range_self _ x))
18   have hs : Function.Surjective V.mulVecLin.rangeRestrict := by
19     rintro ⟨v,x,hx⟩
20     exact ⟨x, Subtype.ext hx⟩
21   obtain ⟨g,hg⟩ := Module.projective_lifting_property V.mulVecLin.rangeRestrict f hs
22   refine ⟨LinearMap.toMatrix' g, ?_⟩
23   apply Matrix.toLin'.injective
24   apply LinearMap.ext
25   intro x
26   ext i
27   have hgi := congrArg (fun z : V.mulVecLin.range => z.val i) (LinearMap.congr_fun hg x)
28   simpa [Matrix.toLin'_mul, f, Matrix.toLin'_apply'] using hgi
29 
30 /-- Equality of generated relation submodules gives equality of all minor ideals. -/
31 theorem minorIdeal_eq_of_range_eq [Fintype n] [Fintype p]
32     (A : Matrix m n R) (B : Matrix m p R)
33     (h : A.mulVecLin.range = B.mulVecLin.range) (k : ℕ) :
34     minorIdeal A k = minorIdeal B k := by
35   obtain ⟨C,hC⟩ := exists_factor_of_range_le A B h.le
36   obtain ⟨D,hD⟩ := exists_factor_of_range_le B A h.ge
37   exact minorIdeal_eq_of_mutual_factorization A B C D hC hD k
38 
39 /-- The relation matrix after adjoining generators lifted by C. -/
40 def augment [DecidableEq q] (A : Matrix m n R) (C : Matrix m q R) :
41     Matrix (m ⊕ q) (n ⊕ q) R := Matrix.fromBlocks A (-C) 0 1
42 
43 theorem presentationIdeal_augment [Fintype m] [Fintype q] [DecidableEq q]
44     (A : Matrix m n R) (C : Matrix m q R) (j : ℕ) :
45     presentationIdeal (augment A C) j = presentationIdeal A j := by
46   classical
47   let U : Matrix (m ⊕ q) (m ⊕ q) R := Matrix.fromBlocks 1 (-C) 0 1
48   let V : Matrix (m ⊕ q) (m ⊕ q) R := Matrix.fromBlocks 1 C 0 1
49   have hVU : V * U = 1 := by
50     simp [V,U,Matrix.fromBlocks_multiply,← Matrix.fromBlocks_one]
51   have hmul : U * stabilizeBlock A q = augment A C := by
52     simp [U,stabilizeBlock,augment,Matrix.fromBlocks_multiply]
53     ext a b
54     simp [Matrix.one_apply]
55   rw [← hmul]
56   unfold presentationIdeal
57   rw [minorIdeal_mul_left_eq U V hVU]
58   exact presentationIdeal_stabilizeBlock A q j
59 
60 variable {M : Type*} [AddCommGroup M] [Module R M]
61 
62 /-- An exact finite relation matrix with its actual quotient map. -/
63 structure Presents [Fintype n] (A : Matrix m n R) (π : (m → R) →ₗ[R] M) : Prop where
64   surjective : Function.Surjective π
65   range_eq_ker : A.mulVecLin.range = π.ker
66 
67 /-- Add two finite generating families into their common free carrier. -/
68 def commonMap (π : (m → R) →ₗ[R] M) (ρ : (q → R) →ₗ[R] M) :
69     ((m ⊕ q) → R) →ₗ[R] M where
70   toFun v := π (v ∘ Sum.inl) + ρ (v ∘ Sum.inr)
71   map_add' := by
72     intro x y
73     change π ((x ∘ Sum.inl) + (y ∘ Sum.inl)) + ρ ((x ∘ Sum.inr) + (y ∘ Sum.inr)) = _
74     rw [map_add,map_add]
75     abel
76   map_smul' := by
77     intro a x
78     change π (a • (x ∘ Sum.inl)) + ρ (a • (x ∘ Sum.inr)) = _
79     rw [map_smul,map_smul,smul_add]
80     rfl
81 
82 theorem range_augment_eq_ker [Fintype n] [Fintype q] [DecidableEq q]
83     (A : Matrix m n R) (π : (m → R) →ₗ[R] M) (ρ : (q → R) →ₗ[R] M)
84     (C : Matrix m q R) (hA : A.mulVecLin.range = π.ker)
85     (hC : π.comp C.mulVecLin = ρ) :
86     (augment A C).mulVecLin.range = (commonMap π ρ).ker := by
87   classical
88   have hπA (x : n → R) : π (A *ᵥ x) = 0 := by
89     have hx := LinearMap.mem_range_self A.mulVecLin x
90     rw [hA] at hx
91     exact hx
92   have hπC (x : q → R) : π (C *ᵥ x) = ρ x := LinearMap.congr_fun hC x
93   ext v
94   constructor
95   · rintro ⟨x,rfl⟩
96     change (commonMap π ρ) ((augment A C) *ᵥ x) = 0
97     rw [augment,Matrix.fromBlocks_mulVec]
98     change π (A *ᵥ (x ∘ Sum.inl) + (-C) *ᵥ (x ∘ Sum.inr)) +
99       ρ ((0 : Matrix q n R) *ᵥ (x ∘ Sum.inl) + (1 : Matrix q q R) *ᵥ (x ∘ Sum.inr)) = 0
100     simp [Matrix.neg_mulVec,hπA,hπC]
101   · intro hv
102     have hv' : π (v ∘ Sum.inl) + ρ (v ∘ Sum.inr) = 0 := hv
103     have hk : v ∘ Sum.inl + C *ᵥ (v ∘ Sum.inr) ∈ A.mulVecLin.range := by
104       rw [hA]
105       change π (v ∘ Sum.inl + C *ᵥ (v ∘ Sum.inr)) = 0
106       simpa [map_add,hπC] using hv'
107     obtain ⟨x,hx⟩ := hk
108     refine ⟨Sum.elim x (v ∘ Sum.inr), ?_⟩
109     change (augment A C) *ᵥ Sum.elim x (v ∘ Sum.inr) = v
110     rw [augment,Matrix.fromBlocks_mulVec]
111     ext i
112     rcases i with i | i
113     · have hxi := congrFun hx i
114       simp only [Matrix.mulVecLin_apply,Pi.add_apply] at hxi
115       simp only [Sum.elim_inl,Function.comp_def,Matrix.neg_mulVec,
116         Pi.add_apply,Pi.neg_apply]
117       change (A *ᵥ x) i + -(C *ᵥ (v ∘ Sum.inr)) i = v (.inl i)
118       rw [hxi]
119       abel
120     · simp
121 
122 end PaperXII.DeterminantalIdeals

Back to source controls