IntrinsicFitting.lean

1 import PaperXII.PresentationIndependence
2 import Mathlib.Algebra.Module.FinitePresentation
3 
4 /-! Intrinsic Fitting ideals, with independence proved rather than supplied. -/
5 noncomputable section
6 namespace PaperXII
7 open Matrix DeterminantalIdeals
8 variable (R : Type*) [CommRing R] (M : Type*) [AddCommGroup M] [Module R M]
9 
10 /-- Actual finite free relations, generators, and a surjective quotient map. -/
11 structure FiniteMatrixPresentation where
12   generators : ℕ
13   relations : ℕ
14   matrix : Matrix (Fin generators) (Fin relations) R
15   quotient : (Fin generators → R) →ₗ[R] M
16   presents : Presents matrix quotient
17 
18 instance finiteMatrixPresentation_nonempty [Module.FinitePresentation R M] : Nonempty (FiniteMatrixPresentation R M) := by
19   classical
20   obtain ⟨n,m,f,g,hf,hgf⟩ := Module.FinitePresentation.exists_fin' R M
21   refine ⟨⟨n,m,LinearMap.toMatrix' g,f,⟨hf,?_⟩⟩⟩
22   simpa only [← Matrix.toLin'_apply',Matrix.toLin'_toMatrix'] using hgf.linearMap_ker_eq.symm
23 
24 /-- A chosen finite presentation. Its choice is removed by `fittingIdeal_eq_presentation`. -/
25 def chosenPresentation [Module.FinitePresentation R M] : FiniteMatrixPresentation R M :=
26   Classical.choice inferInstance
27 
28 /-- The intrinsic j-th Fitting ideal of a finitely presented module. -/
29 def fittingIdeal [Module.FinitePresentation R M] (j : ℕ) : Ideal R :=
30   presentationIdeal (chosenPresentation R M).matrix j
31 
32 variable {R M}
33 
34 /-- The intrinsic ideal equals the minors computed from any actual finite presentation. -/
35 theorem fittingIdeal_eq_presentation [Module.FinitePresentation R M]
36     {m n : Type*} [Fintype m] [Fintype n]
37     (A : Matrix m n R) (π : (m → R) →ₗ[R] M) (h : Presents A π) (j : ℕ) :
38     fittingIdeal R M j = presentationIdeal A j :=
39   presentationIdeal_independent _ _ _ _ (chosenPresentation R M).presents h j
40 
41 /-- Explicit generators give the upper-index normalization, without hidden subtraction assumptions. -/
42 theorem fittingIdeal_eq_top_of_generator_bound [Module.FinitePresentation R M]
43     {m n : Type*} [Fintype m] [Fintype n]
44     (A : Matrix m n R) (π : (m → R) →ₗ[R] M) (h : Presents A π)
45     {j : ℕ} (hj : Fintype.card m ≤ j) : fittingIdeal R M j = ⊤ := by
46   rw [fittingIdeal_eq_presentation A π h j,presentationIdeal_eq_top _ hj]
47 
48 variable {N : Type*} [AddCommGroup N] [Module R N]
49 
50 /-- The same relation matrix presents the actual transported module. -/
51 theorem presents_comp_equiv {m n : Type*} [Fintype n]
52     (A : Matrix m n R) (π : (m → R) →ₗ[R] M) (h : Presents A π)
53     (e : M ≃ₗ[R] N) : Presents A (e.toLinearMap.comp π) := by
54   refine ⟨e.surjective.comp h.surjective,?_⟩
55   rw [h.range_eq_ker]
56   ext x
57   change π x = 0 ↔ e (π x) = 0
58   exact (e.map_eq_zero_iff).symm
59 
60 /-- Intrinsic Fitting ideals are invariant under actual module isomorphisms. -/
61 theorem fittingIdeal_linearEquiv [Module.FinitePresentation R M]
62     [Module.FinitePresentation R N] (e : M ≃ₗ[R] N) (j : ℕ) :
63     fittingIdeal R M j = fittingIdeal R N j := by
64   let P := chosenPresentation R M
65   rw [fittingIdeal_eq_presentation P.matrix P.quotient P.presents j,
66     fittingIdeal_eq_presentation P.matrix (e.toLinearMap.comp P.quotient)
67       (presents_comp_equiv P.matrix P.quotient P.presents e) j]
68 
69 end PaperXII

Back to source controls