PolynomialMonic.lean

1 import PaperIRelease.PolynomialModule
2 set_option autoImplicit false
3 noncomputable section
4 open Polynomial
5 namespace Komorebi.PaperIRelease.PolynomialModule
6 universe u v
7 variable (k : Type u) [Field k]
8 abbrev MonicIrreducibles := {p : k[X] // p.Monic ∧ Irreducible p}
9 def monicToSpec (p : MonicIrreducibles k) : IsDedekindDomain.HeightOneSpectrum k[X] where
10   asIdeal := Ideal.span {p.val}
11   isPrime := Ideal.isPrime_span_singleton_of_prime p.property.2.prime
12   ne_bot := fun h => p.property.2.ne_zero (Ideal.span_singleton_eq_bot.mp h)
13 
14 theorem monicToSpec_injective : Function.Injective (monicToSpec k) := by
15   intro p q hpq
16   apply Subtype.ext
17   apply Polynomial.eq_of_monic_of_associated p.property.1 q.property.1
18   apply Ideal.span_singleton_eq_span_singleton.mp
19   exact congrArg IsDedekindDomain.HeightOneSpectrum.asIdeal hpq
20 
21 theorem monicToSpec_surjective : Function.Surjective (monicToSpec k) := by
22   classical
23   intro P
24   obtain ⟨p, hp, hP⟩ := (Ideal.isPrime_iff_of_isPrincipalIdealRing P.ne_bot).mp P.isPrime
25   let q : MonicIrreducibles k := ⟨normalize p, Polynomial.monic_normalize hp.ne_zero,
26     (normalize_associated p).irreducible_iff.mpr hp.irreducible⟩
27   refine ⟨q, IsDedekindDomain.HeightOneSpectrum.ext ?_⟩
28   change Ideal.span {normalize p} = P.asIdeal
29   rw [hP]
30   exact Ideal.span_singleton_eq_span_singleton.mpr (normalize_associated p)
31 
32 def monicSpectrumEquiv : MonicIrreducibles k ≃ IsDedekindDomain.HeightOneSpectrum k[X] :=
33   Equiv.ofBijective (monicToSpec k) ⟨monicToSpec_injective k, monicToSpec_surjective k⟩
34 
35 variable (M : Type v) [AddCommGroup M] [Module k M] [Module k[X] M]
36   [IsScalarTower k k[X] M]
37 open Komorebi.PaperICompletion4.IntrinsicPrimary
38 local instance : DecidableEq (MonicIrreducibles k) := Classical.decEq _
39 theorem monic_primary_internal_decomposition [FiniteDimensional k M] :
40     DirectSum.IsInternal (fun p : MonicIrreducibles k => primarySubmodule M p.val) := by
41   have hfamily : (fun p : MonicIrreducibles k => primarySubmodule M p.val) =
42       (fun p : MonicIrreducibles k => (monicToSpec k p).asIdeal.primaryComponent M) := by
43     funext p
44     exact primarySubmodule_eq_idealPrimary M p.val
45   rw [hfamily]
46   apply DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
47   · exact (Ideal.iSupIndep_primaryComponent k[X] M).comp (monicToSpec_injective k)
48   · exact ((monicToSpec_surjective k).iSup_comp
49       (fun P : IsDedekindDomain.HeightOneSpectrum k[X] => P.asIdeal.primaryComponent M)).trans
50       (Ideal.iSup_primaryComponent_eq_top (polynomialModule_isTorsion k M))
51 
52 theorem finitely_many_monic_primary_components [FiniteDimensional k M] :
53     Set.Finite {p : MonicIrreducibles k | primarySubmodule M p.val ≠ ⊥} := by
54   let : IsNoetherian k[X] M := isNoetherian_of_tower k (inferInstance : IsNoetherian k M)
55   apply Submodule.finite_ne_bot_of_iSupIndep
56   have h := (Ideal.iSupIndep_primaryComponent k[X] M).comp (monicToSpec_injective k)
57   change iSupIndep (fun p : MonicIrreducibles k => (Ideal.span {p.val}).primaryComponent M) at h
58   simpa only [primarySubmodule_eq_idealPrimary] using h
59 end Komorebi.PaperIRelease.PolynomialModule
60 #print axioms Komorebi.PaperIRelease.PolynomialModule.monic_primary_internal_decomposition
61 #print axioms Komorebi.PaperIRelease.PolynomialModule.finitely_many_monic_primary_components

Back to source controls