PolynomialModule.lean

1 import PaperICompletion4.OperatorIntrinsicFormula
2 set_option autoImplicit false
3 noncomputable section
4 namespace Komorebi.PaperIRelease.PolynomialModule
5 open Polynomial
6 open Komorebi.PaperICompletion3.PrimarySeedFormula
7 open Komorebi.PaperICompletion4.IntrinsicPrimary Komorebi.PaperICompletion4.GroupedPrimary
8 universe u v
9 variable (k : Type u) [Field k] (M : Type v) [AddCommGroup M]
10 variable [Module k M] [Module k[X] M] [IsScalarTower k k[X] M]
11 
12 /-- Multiplication by X in an existing polynomial module. -/
13 def variableAction : Module.End k M where
14   toFun m := (X : k[X]) • m
15   map_add' := smul_add _
16   map_smul' c m := by
17     change (X : k[X]) • (c • m) = c • ((X : k[X]) • m)
18     exact smul_comm _ _ _
19 
20 /-- Every pre-existing polynomial-module action is its variable-action evaluation module. -/
21 def evaluationEquiv : Module.AEval' (variableAction k M) ≃ₗ[k[X]] M :=
22   LinearEquiv.ofAEval (variableAction k M) (LinearEquiv.refl k M) (fun _ => rfl)
23 
24 /-- Finite-dimensional existing polynomial modules are torsion. -/
25 theorem polynomialModule_isTorsion [FiniteDimensional k M] : Module.IsTorsion k[X] M := by
26   intro m
27   obtain ⟨p, hp⟩ := operatorModule_isTorsion (variableAction k M)
28     (x := (evaluationEquiv k M).symm m)
29   refine ⟨p, ?_⟩
30   change (p : k[X]) • (evaluationEquiv k M).symm m = 0 at hp
31   change (p : k[X]) • m = 0
32   have h := congrArg (evaluationEquiv k M) hp
33   rw [(evaluationEquiv k M).map_smul, LinearEquiv.apply_symm_apply, map_zero] at h
34   exact h
35 
36 /-- Positive elementary divisors for the existing module, without a supplied operator presentation. -/
37 theorem exists_positive_primary_decomposition [FiniteDimensional k M] :
38     ∃ (ι : Type u) (_ : Fintype ι) (p : ι → k[X])
39       (_ : ∀ i, Irreducible (p i)) (e : ι → ℕ) (_ : ∀ i, 0 < e i),
40       Nonempty (M ≃ₗ[k[X]] ((i : ι) → k[X] ⧸ Ideal.span {p i ^ e i})) := by
41   obtain ⟨ι, hι, p, hp, e, he, ⟨f⟩⟩ := exists_positive_primaryProduct_equiv (variableAction k M)
42   exact ⟨ι, hι, p, hp, e, he, ⟨(evaluationEquiv k M).symm.trans f⟩⟩
43 
44 local instance : DecidableEq (IsDedekindDomain.HeightOneSpectrum k[X]) := Classical.decEq _
45 
46 /-- The actual ideal-primary subspaces sum internally to the given module. -/
47 theorem primary_internal_decomposition [FiniteDimensional k M] :
48     DirectSum.IsInternal (fun p : IsDedekindDomain.HeightOneSpectrum k[X] => p.asIdeal.primaryComponent M) := by
49   apply DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
50   · exact Ideal.iSupIndep_primaryComponent k[X] M
51   · exact Ideal.iSup_primaryComponent_eq_top (polynomialModule_isTorsion k M)
52 
53 /-- Only finitely many intrinsic prime-ideal components are nonzero. -/
54 theorem finitely_many_primary_components [FiniteDimensional k M] :
55     Set.Finite {p : IsDedekindDomain.HeightOneSpectrum k[X] |
56       p.asIdeal.primaryComponent M ≠ ⊥} := by
57   let : IsNoetherian k[X] M := isNoetherian_of_tower k (inferInstance : IsNoetherian k M)
58   exact Submodule.finite_ne_bot_of_iSupIndep (Ideal.iSupIndep_primaryComponent k[X] M)
59 
60 /-- Every intrinsic primary component has the matching finite elementary-divisor presentation. -/
61 theorem exists_grouped_primary_decomposition [FiniteDimensional k M] :
62     ∃ (ι : Type u) (_ : Fintype ι) (q : ι → k[X])
63       (_ : ∀ i, Irreducible (q i)) (e : ι → ℕ) (_ : ∀ i, 0 < e i),
64       ∀ p : k[X], Irreducible p → Nonempty
65         (primarySubmodule M p ≃ₗ[k[X]]
66           ((i : {i : ι // Ideal.span {q i} = Ideal.span {p}}) →
67             k[X] ⧸ Ideal.span {q i.val ^ e i.val})) := by
68   obtain ⟨ι, hι, q, hq, e, he, ⟨f⟩⟩ := exists_positive_primary_decomposition k M
69   exact ⟨ι, hι, q, hq, e, he, fun p hp =>
70     ⟨(primaryCongr p f).trans (groupedPrimaryEquiv q hq e p hp)⟩⟩
71 
72 
73 /-- Literal finite direct-sum presentation by powers of the specified irreducible. -/
74 theorem intrinsic_primary_finite_power_sum [FiniteDimensional k M]
75     (p : k[X]) (hp : Irreducible p) :
76     ∃ (ι : Type u) (_ : Fintype ι) (e : ι → ℕ), (∀ i, 0 < e i) ∧
77       Nonempty (primarySubmodule M p ≃ₗ[k[X]]
78         DirectSum ι (fun i => k[X] ⧸ Ideal.span {p ^ e i})) := by
79   classical
80   obtain ⟨ι, hι, q, hq, e, he, hcomponents⟩ := exists_grouped_primary_decomposition k M
81   let J := {i : ι // Ideal.span {q i} = Ideal.span {p}}
82   let f (i : J) : (k[X] ⧸ Ideal.span {q i.val ^ e i.val}) ≃ₗ[k[X]]
83       (k[X] ⧸ Ideal.span {p ^ e i.val}) := Submodule.quotEquivOfEq _ _ (by
84         simpa only [Ideal.span_singleton_pow] using
85           congrArg (fun I : Ideal k[X] => I ^ e i.val) i.property)
86   refine ⟨J, inferInstance, fun i => e i.val, fun i => he i.val, ?_⟩
87   exact ⟨((hcomponents p hp).some.trans (LinearEquiv.piCongrRight f)).trans
88     (DirectSum.linearEquivFunOnFintype k[X] J _).symm⟩
89 
90 end Komorebi.PaperIRelease.PolynomialModule

Back to source controls