FittingBaseChange.lean

1 import PaperXII.IntrinsicFitting
2 import Mathlib.LinearAlgebra.TensorProduct.Pi
3 import Mathlib.LinearAlgebra.TensorProduct.RightExactness
4 
5 /-! Intrinsic Fitting ideals commute with arbitrary coefficient base change. -/
6 noncomputable section
7 namespace PaperXII
8 open Matrix TensorProduct DeterminantalIdeals
9 variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
10 variable {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
11 
12 /-- The actual tensor base change of a relation map has the coefficient-mapped matrix. -/
13 theorem baseChange_matrix_coordinates (A : Matrix m n R) :
14     (A.map (algebraMap R S)).mulVecLin.comp (piScalarRight R S S n).toLinearMap =
15       (piScalarRight R S S m).toLinearMap.comp (A.mulVecLin.baseChange S) := by
16   apply LinearMap.ext
17   intro z
18   induction z with
19   | zero => simp
20   | tmul s x =>
21     ext i
22     simp [LinearMap.comp_apply,piScalarRight_apply,piScalarRightHom_tmul,
23       Matrix.mulVec,dotProduct,Algebra.smul_def,
24       map_sum,map_mul]
25     simp only [Finset.sum_mul,mul_assoc]
26   | add x y hx hy => simp only [map_add,hx,hy]
27 
28 variable {M : Type*} [AddCommGroup M] [Module R M]
29 
30 /-- The actual quotient map after tensor base change and free-coordinate identification. -/
31 def baseChangeQuotient (π : (m → R) →ₗ[R] M) : (m → S) →ₗ[S] S ⊗[R] M :=
32   (π.baseChange S).comp (piScalarRight R S S m).symm.toLinearMap
33 
34 /-- Right exactness supplies a genuine presentation after arbitrary base change; no flatness. -/
35 theorem presents_baseChange (A : Matrix m n R) (π : (m → R) →ₗ[R] M)
36     (h : Presents A π) : Presents (A.map (algebraMap R S)) (baseChangeQuotient (S := S) π) := by
37   refine ⟨(π.baseChange_surjective S h.surjective).comp
38     (piScalarRight R S S m).symm.surjective, ?_⟩
39   have hex : Function.Exact (A.mulVecLin.baseChange S) (π.baseChange S) :=
40     lTensor_exact S (LinearMap.exact_iff.mpr h.range_eq_ker.symm) h.surjective
41   have hc := baseChange_matrix_coordinates (S := S) A
42   have hq : (baseChangeQuotient (S := S) π).comp (piScalarRight R S S m).toLinearMap =
43       (LinearEquiv.refl S (S ⊗[R] M)).toLinearMap.comp (π.baseChange S) := by
44     apply LinearMap.ext
45     intro x
46     change (π.baseChange S) ((piScalarRight R S S m).symm ((piScalarRight R S S m) x)) =
47       (π.baseChange S) x
48     rw [LinearEquiv.symm_apply_apply]
49   exact ((Function.Exact.iff_of_ladder_linearEquiv hc hq).mpr hex).linearMap_ker_eq.symm
50 
51 /-- Paper XII, Claim 6.5: intrinsic Fitting ideals commute with arbitrary base change. -/
52 theorem fittingIdeal_baseChange [Module.FinitePresentation R M] (j : ℕ) :
53     fittingIdeal S (S ⊗[R] M) j = Ideal.map (algebraMap R S) (fittingIdeal R M j) := by
54   let P := chosenPresentation R M
55   rw [fittingIdeal_eq_presentation (P.matrix.map (algebraMap R S))
56     (baseChangeQuotient P.quotient) (presents_baseChange P.matrix P.quotient P.presents) j,
57     fittingIdeal_eq_presentation P.matrix P.quotient P.presents j]
58   exact minorIdeal_map (algebraMap R S) P.matrix _
59 
60 end PaperXII

Back to source controls