GroupedPrimary.lean

1 import PaperICompletion4.IntrinsicPrimary
2 
3 /-! # Grouped elementary divisors are the actual intrinsic primary component -/
4 set_option autoImplicit false
5 noncomputable section
6 open scoped Pointwise
7 namespace Komorebi.PaperICompletion4.GroupedPrimary
8 open Komorebi.PaperICompletion3.PrimarySeedFormula
9 open Komorebi.PaperICompletion4.ResidueQuotient
10 open Komorebi.PaperICompletion4.IntrinsicPrimary
11 universe u v w
12 variable {R : Type u} [CommRing R]
13 
14 /-- Coprimality makes scalar multiplication injective as well as surjective. -/
15 theorem eq_zero_of_coprime_smul (p q : R) (hc : IsCoprime p q)
16     (x : R ⧸ Ideal.span {q}) (hx : p • x = 0) : x = 0 := by
17   obtain ⟨a, b, hab⟩ := hc
18   have hq : q • x = 0 := by
19     rw [Algebra.smul_def]
20     change Ideal.Quotient.mk (Ideal.span {q}) q * x = 0
21     rw [Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span (Set.mem_singleton q)),
22       zero_mul]
23   calc
24     x = (1 : R) • x := (one_smul R x).symm
25     _ = (a * p + b * q) • x := by rw [hab]
26     _ = 0 := by rw [add_smul, mul_smul, mul_smul, hx, hq, smul_zero, smul_zero, add_zero]
27 
28 section Equivalence
29 variable {M : Type v} [AddCommGroup M] [Module R M]
30 variable {N : Type w} [AddCommGroup N] [Module R N]
31 
32 /-- An actual module equivalence preserves the intrinsic primary condition. -/
33 theorem primary_equiv_mem_iff (p : R) (f : M ≃ₗ[R] N) (x : M) :
34     f x ∈ primarySubmodule N p ↔ x ∈ primarySubmodule M p := by
35   change (∃ n : ℕ, p ^ n • f x = 0) ↔ ∃ n : ℕ, p ^ n • x = 0
36   simp only [← f.map_smul, map_eq_zero_iff f f.injective]
37 
38 /-- Restriction to intrinsic primary components, not an unrelated presentation witness. -/
39 def primaryCongr (p : R) (f : M ≃ₗ[R] N) :
40     primarySubmodule M p ≃ₗ[R] primarySubmodule N p where
41   toFun x := ⟨f x, (primary_equiv_mem_iff p f x).mpr x.property⟩
42   invFun y := ⟨f.symm y, (primary_equiv_mem_iff p f.symm y).mpr y.property⟩
43   left_inv x := Subtype.ext (f.symm_apply_apply x)
44   right_inv y := Subtype.ext (f.apply_symm_apply y)
45   map_add' x y := Subtype.ext (f.map_add x y)
46   map_smul' a x := Subtype.ext (f.map_smul a x)
47 end Equivalence
48 
49 section Product
50 variable [IsDomain R] [IsPrincipalIdealRing R]
51 variable {ι : Type v} [Fintype ι]
52 variable (q : ι → R) (hq : ∀ i, Irreducible (q i)) (e : ι → ℕ)
53 
54 include hq in
55 /-- The intrinsic primary component consists exactly of the matching coordinates. -/
56 theorem primaryProduct_mem_iff (p : R) (hp : Irreducible p)
57     (x : (i : ι) → R ⧸ Ideal.span {q i ^ e i}) :
58     x ∈ primarySubmodule ((i : ι) → R ⧸ Ideal.span {q i ^ e i}) p ↔
59       ∀ i, Ideal.span {q i} ≠ Ideal.span {p} → x i = 0 := by
60   classical
61   constructor
62   · rintro ⟨n, hn⟩ i hi
63     have hc := coprime_primePower_ideals p (q i) hp (hq i) (Ne.symm hi) n (e i)
64     exact eq_zero_of_coprime_smul (p ^ n) (q i ^ e i)
65       ((Ideal.isCoprime_span_singleton_iff _ _).mp hc) (x i) (congrFun hn i)
66   · intro hx
67     refine ⟨Finset.univ.sup e, ?_⟩
68     ext i
69     by_cases hi : Ideal.span {q i} = Ideal.span {p}
70     · have hid : Ideal.span {q i ^ e i} = Ideal.span {p ^ e i} := by
71         simpa only [Ideal.span_singleton_pow] using
72           congrArg (fun I : Ideal R ↦ I ^ e i) hi
73       have hz : p ^ e i • x i = 0 := by
74         rw [Algebra.smul_def]
75         change Ideal.Quotient.mk (Ideal.span {q i ^ e i}) (p ^ e i) * x i = 0
76         have hpq : p ^ e i ∈ Ideal.span {q i ^ e i} := by
77           rw [hid]
78           exact Ideal.subset_span (Set.mem_singleton _)
79         rw [Ideal.Quotient.eq_zero_iff_mem.mpr hpq, zero_mul]
80       exact power_kills_of_le _ p (Finset.le_sup (f := e) (Finset.mem_univ i)) (x i) hz
81     · simp only [Pi.smul_apply, Pi.zero_apply, hx i hi, smul_zero]
82 
83 /-- The grouped product is equivalent to the literal intrinsic primary submodule. -/
84 def groupedPrimaryEquiv (p : R) (hp : Irreducible p) :
85     primarySubmodule ((i : ι) → R ⧸ Ideal.span {q i ^ e i}) p ≃ₗ[R]
86       ((i : {i : ι // Ideal.span {q i} = Ideal.span {p}}) →
87         R ⧸ Ideal.span {q i ^ e i}) := by
88   classical
89   let f : primarySubmodule ((i : ι) → R ⧸ Ideal.span {q i ^ e i}) p →ₗ[R]
90       ((i : {i : ι // Ideal.span {q i} = Ideal.span {p}}) →
91         R ⧸ Ideal.span {q i ^ e i}) :=
92     (LinearMap.pi fun i ↦ LinearMap.proj i.val).comp (primarySubmodule _ p).subtype
93   apply LinearEquiv.ofBijective f
94   constructor
95   · intro x y hxy
96     apply Subtype.ext
97     funext i
98     by_cases hi : Ideal.span {q i} = Ideal.span {p}
99     · exact congrFun hxy ⟨i, hi⟩
100     · rw [(primaryProduct_mem_iff q hq e p hp x).mp x.property i hi,
101         (primaryProduct_mem_iff q hq e p hp y).mp y.property i hi]
102   · intro y
103     let x : (i : ι) → R ⧸ Ideal.span {q i ^ e i} :=
104       fun i ↦ if hi : Ideal.span {q i} = Ideal.span {p} then y ⟨i, hi⟩ else 0
105     have hx : x ∈ primarySubmodule _ p := by
106       apply (primaryProduct_mem_iff q hq e p hp x).mpr
107       intro i hi
108       simp [x, hi]
109     refine ⟨⟨x, hx⟩, ?_⟩
110     ext i
111     change x i.val = y i
112     simp [x, i.property]
113 end Product
114 end Komorebi.PaperICompletion4.GroupedPrimary

Back to source controls