IntrinsicPrimary.lean

1 import PaperICompletion4.ResidueQuotient
2 import Mathlib.Algebra.Module.Torsion.PrimaryComponent
3 
4 /-! # The intrinsic primary component and its literal quotient
5 The primary component consists exactly of vectors killed by some power of p.
6 Its inclusion induces an isomorphism with M/pM for Artinian modules.
7 -/
8 set_option autoImplicit false
9 noncomputable section
10 open scoped Pointwise
11 namespace Komorebi.PaperICompletion4.IntrinsicPrimary
12 open Komorebi.PaperICompletion4.ResidueQuotient
13 universe u v w
14 variable {R : Type u} [CommRing R]
15 variable (M : Type v) [AddCommGroup M] [Module R M]
16 
17 /-- A higher power also kills a vector killed by a lower power. -/
18 theorem power_kills_of_le (p : R) {m n : ℕ} (h : m ≤ n) (x : M)
19     (hx : p ^ m • x = 0) : p ^ n • x = 0 := by
20   obtain ⟨r, rfl⟩ := Nat.exists_eq_add_of_le h
21   rw [pow_add, mul_comm, mul_smul, hx, smul_zero]
22 
23 /-- The intrinsic p-primary submodule, without any presentation choices. -/
24 def primarySubmodule (p : R) : Submodule R M where
25   carrier := {x | ∃ n : ℕ, p ^ n • x = 0}
26   zero_mem' := ⟨0, smul_zero _⟩
27   add_mem' := by
28     rintro x y ⟨m, hm⟩ ⟨n, hn⟩
29     refine ⟨max m n, ?_⟩
30     rw [smul_add, power_kills_of_le M p (le_max_left m n) x hm,
31       power_kills_of_le M p (le_max_right m n) y hn, add_zero]
32   smul_mem' := by
33     rintro a x ⟨n, hn⟩
34     exact ⟨n, by rw [smul_comm, hn, smul_zero]⟩
35 
36 /-- Membership is the actual annihilation-by-a-power condition. -/
37 theorem mem_primarySubmodule (p : R) (x : M) :
38     x ∈ primarySubmodule M p ↔ ∃ n : ℕ, p ^ n • x = 0 := Iff.rfl
39 
40 /-- This is also Mathlib's ideal-primary component for the principal ideal (p). -/
41 theorem primarySubmodule_eq_idealPrimary (p : R) :
42     primarySubmodule M p = (Ideal.span {p}).primaryComponent M := by
43   ext x
44   simp only [mem_primarySubmodule, Ideal.primaryComponent_mem,
45     Ideal.span_singleton_pow, Submodule.torsionBySet_ideal_span_singleton_eq,
46     Submodule.mem_torsionBy_iff]
47 
48 /-- The literal inclusion followed by quotienting the whole module by pM. -/
49 def primaryToGlobal (p : R) :
50     primarySubmodule M p →ₗ[R] ScalarQuotient M p :=
51   (p • (⊤ : Submodule R M)).mkQ.comp (primarySubmodule M p).subtype
52 
53 /-- Its kernel is exactly p times the primary submodule, not a supplied certificate. -/
54 theorem primaryToGlobal_ker (p : R) :
55     (primaryToGlobal M p).ker =
56       p • (⊤ : Submodule R (primarySubmodule M p)) := by
57   ext x
58   change Submodule.Quotient.mk (x : M) = (0 : ScalarQuotient M p) ↔ _
59   rw [Submodule.Quotient.mk_eq_zero, mem_scalarImage_iff, mem_scalarImage_iff]
60   constructor
61   · rintro ⟨y, hy⟩
62     obtain ⟨n, hn⟩ := x.property
63     have hyprim : y ∈ primarySubmodule M p := by
64       refine ⟨n + 1, ?_⟩
65       rw [pow_succ, mul_smul, hy]
66       exact hn
67     exact ⟨⟨y, hyprim⟩, Subtype.ext hy⟩
68   · rintro ⟨y, hy⟩
69     exact ⟨y, congrArg Subtype.val hy⟩
70 
71 /-- In an Artinian module, every class modulo pM has a primary representative. -/
72 theorem primaryToGlobal_surjective [IsArtinian R M] (p : R) :
73     Function.Surjective (primaryToGlobal M p) := by
74   let f : Module.End R M := DistribSMul.toLinearMap R M p
75   obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.range (f ^ n) = LinearMap.range (f ^ m)⟩ :=
76     IsArtinian.monotone_stabilizes f.iterateRange
77   have hpow : ∀ n : ℕ, ∀ x : M, (f ^ n) x = p ^ n • x := by
78     intro n
79     induction n with
80     | zero => intro x; simp
81     | succ n ih =>
82       intro x
83       rw [pow_succ, Module.End.mul_apply, ih, pow_succ, mul_smul]
84       rfl
85   intro z
86   obtain ⟨x, rfl⟩ := (p • (⊤ : Submodule R M)).mkQ_surjective z
87   have hx : (f ^ n) x ∈ LinearMap.range (f ^ (n + 1)) := by
88     rw [← hn (n + 1) (Nat.le_succ n)]
89     exact LinearMap.mem_range_self _ x
90   obtain ⟨y, hy⟩ := hx
91   have hy' : p ^ n • (p • y) = p ^ n • x := by
92     rw [hpow, hpow, pow_succ, mul_smul] at hy
93     exact hy
94   have hprimary : x - p • y ∈ primarySubmodule M p := by
95     exact ⟨n, by rw [smul_sub, hy', sub_self]⟩
96   refine ⟨⟨x - p • y, hprimary⟩, ?_⟩
97   change Submodule.Quotient.mk (x - p • y) =
98     (Submodule.Quotient.mk x : ScalarQuotient M p)
99   have hz : Submodule.Quotient.mk (p • y) = (0 : ScalarQuotient M p) := by
100     exact (Submodule.Quotient.mk_eq_zero _).mpr
101       ((mem_scalarImage_iff p _).mpr ⟨y, rfl⟩)
102   rw [Submodule.Quotient.mk_sub, hz, sub_zero]
103 
104 /-- The primary quotient equals the global quotient over the residue ring itself. -/
105 def primaryQuotientEquivGlobal [IsArtinian R M] (p : R) :
106     ScalarQuotient (primarySubmodule M p) p ≃ₗ[R ⧸ Ideal.span {p}]
107       ScalarQuotient M p :=
108   scalarQuotientEquiv p (primaryToGlobal M p)
109     (primaryToGlobal_surjective M p) (primaryToGlobal_ker M p)
110 
111 /-- The equivalence is induced by inclusion, with no arbitrary reassignment of classes. -/
112 theorem primaryQuotientEquivGlobal_mk [IsArtinian R M] (p : R)
113     (x : primarySubmodule M p) :
114     primaryQuotientEquivGlobal M p (Submodule.Quotient.mk x) =
115       Submodule.Quotient.mk (x : M) :=
116   scalarQuotientEquiv_mk p _ _ _ x
117 
118 end Komorebi.PaperICompletion4.IntrinsicPrimary

Back to source controls