PresentationIndependence.lean

1 import PaperXII.PresentationComparison
2 
3 noncomputable section
4 namespace PaperXII.DeterminantalIdeals
5 open Matrix
6 variable {R : Type*} [CommRing R] {m n p q m' : Type*}
7 
8 /-- Row-coordinate transport of the actual relation submodule. -/
9 theorem mem_range_submatrix_rows [Fintype n] (A : Matrix m n R) (e : m' ≃ m)
10     (v : m' → R) :
11     v ∈ (A.submatrix e id).mulVecLin.range ↔ v ∘ e.symm ∈ A.mulVecLin.range := by
12   have heq (x : n → R) : (A.submatrix e id) *ᵥ x = (A *ᵥ x) ∘ e := rfl
13   constructor
14   · rintro ⟨x,hx⟩
15     refine ⟨x, ?_⟩
16     ext i
17     have hi := congrFun hx (e.symm i)
18     simpa [Matrix.mulVecLin_apply,heq,Function.comp_def] using hi
19   · rintro ⟨x,hx⟩
20     refine ⟨x, ?_⟩
21     ext i
22     have hi := congrFun hx (e i)
23     simpa [Matrix.mulVecLin_apply,heq,Function.comp_def] using hi
24 
25 variable {M : Type*} [AddCommGroup M] [Module R M]
26 
27 /-- Independence from both the generators and the relations of a finite presentation. -/
28 theorem presentationIdeal_independent [Fintype m] [Fintype n] [Fintype p] [Fintype q]
29     (A : Matrix m n R) (B : Matrix q p R)
30     (π : (m → R) →ₗ[R] M) (ρ : (q → R) →ₗ[R] M)
31     (hA : Presents A π) (hB : Presents B ρ) (j : ℕ) :
32     presentationIdeal A j = presentationIdeal B j := by
33   classical
34   obtain ⟨c,hc⟩ := Module.projective_lifting_property π ρ hA.surjective
35   obtain ⟨d,hd⟩ := Module.projective_lifting_property ρ π hB.surjective
36   let C : Matrix m q R := LinearMap.toMatrix' c
37   let D : Matrix q m R := LinearMap.toMatrix' d
38   have hC : π.comp C.mulVecLin = ρ := by
39     simpa only [C, ← Matrix.toLin'_apply', Matrix.toLin'_toMatrix'] using hc
40   have hD : ρ.comp D.mulVecLin = π := by
41     simpa only [D, ← Matrix.toLin'_apply', Matrix.toLin'_toMatrix'] using hd
42   let B' := (augment B D).submatrix (Equiv.sumComm m q) id
43   have hkerA := range_augment_eq_ker A π ρ C hA.range_eq_ker hC
44   have hkerB := range_augment_eq_ker B ρ π D hB.range_eq_ker hD
45   have hrange : (augment A C).mulVecLin.range = B'.mulVecLin.range := by
46     ext v
47     rw [hkerA]
48     change v ∈ (commonMap π ρ).ker ↔
49       v ∈ ((augment B D).submatrix (Equiv.sumComm m q) id).mulVecLin.range
50     rw [mem_range_submatrix_rows, hkerB]
51     change π (v ∘ Sum.inl) + ρ (v ∘ Sum.inr) = 0 ↔
52       ρ ((v ∘ (Equiv.sumComm m q).symm) ∘ Sum.inl) +
53       π ((v ∘ (Equiv.sumComm m q).symm) ∘ Sum.inr) = 0
54     simp [Function.comp_def,add_comm]
55   calc
56     presentationIdeal A j = presentationIdeal (augment A C) j :=
57       (presentationIdeal_augment A C j).symm
58     _ = presentationIdeal B' j := minorIdeal_eq_of_range_eq _ _ hrange _
59     _ = presentationIdeal (augment B D) j :=
60       presentationIdeal_submatrix_equiv _ (Equiv.sumComm m q) (Equiv.refl (p ⊕ m)) j
61     _ = presentationIdeal B j := presentationIdeal_augment B D j
62 
63 end PaperXII.DeterminantalIdeals

Back to source controls