FittingBoundaryChecks.lean

1 import PaperXII.FittingTransport
2 
3 /-! Kernel-checked normalization checks, including zero and empty-rank boundaries. -/
4 noncomputable section
5 namespace PaperXII
6 open Matrix DeterminantalIdeals
7 variable {R : Type*} [CommRing R]
8 
9 /-- Positive-order minors of the zero relation matrix all vanish. -/
10 theorem minorIdeal_zero_matrix {m n : Type*} {k : ℕ} (hk : 0 < k) :
11     minorIdeal (0 : Matrix m n R) k = ⊥ := by
12   apply le_antisymm _ bot_le
13   apply (minorIdeal_le_iff _ _ _).mpr
14   intro r c
15   have : Nonempty (Fin k) := ⟨⟨0,hk⟩⟩
16   simp
17 
18 /-- For a finite free module, low-index Fitting ideals are zero and high-index ones are the unit ideal. -/
19 theorem fittingIdeal_free (n j : ℕ) :
20     fittingIdeal R (Fin n → R) j = if n ≤ j then ⊤ else ⊥ := by
21   classical
22   have hp : Presents (0 : Matrix (Fin n) (Fin 0) R) (LinearMap.id : (Fin n → R) →ₗ[R] _) := by
23     refine ⟨Function.surjective_id, ?_⟩
24     simp [Matrix.mulVecLin]
25   rw [fittingIdeal_eq_presentation _ _ hp]
26   by_cases h : n ≤ j
27   · simp only [h,ite_true]
28     exact presentationIdeal_eq_top _ (by simpa using h)
29   · simp only [h,ite_false,presentationIdeal,Fintype.card_fin]
30     exact minorIdeal_zero_matrix (by omega)
31 
32 /-- The zero module has unit zeroth Fitting ideal, not the zero ideal. -/
33 theorem fittingIdeal_zero_module (j : ℕ) : fittingIdeal R (Fin 0 → R) j = ⊤ := by
34   simp [fittingIdeal_free]
35 
36 /-- The first normalization distinguishes the free rank-one module from the zero module. -/
37 theorem fittingIdeal_free_rank_one_zero : fittingIdeal R (Fin 1 → R) 0 = ⊥ := by
38   simp [fittingIdeal_free]
39 
40 /-- A one-by-one presentation records its actual relation coefficient. -/
41 theorem one_by_one_presentationIdeal (a : R) :
42     presentationIdeal (Matrix.of fun (_ : Fin 1) (_ : Fin 1) => a) 0 = Ideal.span ({a} : Set R) := by
43   change minorIdeal (Matrix.of fun (_ : Fin 1) (_ : Fin 1) => a) 1 = _
44   unfold minorIdeal
45   congr 1
46   ext x
47   constructor
48   · rintro ⟨⟨r,c⟩,hx⟩
49     change (Matrix.of (fun (_ : Fin 1) (_ : Fin 1) => a)).det = x at hx
50     rw [Matrix.det_fin_one] at hx
51     exact hx.symm
52   · intro hx
53     have h : x = a := Set.mem_singleton_iff.mp hx
54     subst x
55     refine ⟨(id,id),?_⟩
56     change (Matrix.of (fun (_ : Fin 1) (_ : Fin 1) => a)).det = a
57     rw [Matrix.det_fin_one]
58     rfl
59 
60 /-- The empty matrix boundary and a genuine 1-by-1 relation both survive non-flat coefficient maps. -/
61 theorem one_by_one_baseChange {S : Type*} [CommRing S] (f : R →+* S) (a : R) :
62     presentationIdeal (Matrix.of fun (_ : Fin 1) (_ : Fin 1) => f a) 0 =
63       Ideal.map f (presentationIdeal (Matrix.of fun (_ : Fin 1) (_ : Fin 1) => a) 0) :=
64   minorIdeal_map f (Matrix.of fun (_ : Fin 1) (_ : Fin 1) => a) _
65 
66 end PaperXII

Back to source controls