GeneralizedPackets.lean

1 import Mathlib.RingTheory.HopkinsLevitzki
2 import Mathlib.RingTheory.Artinian.Ring
3 import Mathlib.RingTheory.Spectrum.Maximal.Localization
4 import PaperXII.PacketTrace
5 import PaperXII.ArtinData
6 
7 set_option autoImplicit false
8 
9 /-! Paper XII, Corollary 8.3. A maximal ideal specified by generators gives
10 simultaneous generalized eigenspaces in the actual canonical Artin packet.
11 The Artin product equivalence is the external input from Fact 8.1.
12 Nilpotence, separation of different maximal ideals, and the packet equality
13 are proved here, without assuming a semisimple or faithful representation. -/
14 namespace PaperXII.GeneralizedPackets
15 
16 open scoped BigOperators
17 open PaperXII.ArtinData
18 
19 variable {R : Type*} [CommRing R] [IsArtinianRing R]
20 
21 /-- A single positive exponent kills the image of the entire maximal ideal
22 in its Artin localization. -/
23 theorem exists_local_power (m : MaximalSpectrum R) :
24     ∃ N : ℕ, 1 ≤ N ∧ ∀ x ∈ m.asIdeal,
25       (algebraMap R (Localization.AtPrime m.asIdeal) x) ^ N = 0 := by
26   obtain ⟨n, hn⟩ := (isArtinianRing_iff_isNilpotent_maximalIdeal
27     (Localization.AtPrime m.asIdeal)).mp inferInstance
28   refine ⟨n + 1, Nat.le_add_left 1 n, ?_⟩
29   intro x hx
30   have hmem := Ideal.pow_mem_pow
31     ((IsLocalization.AtPrime.to_map_mem_maximal_iff
32       (Localization.AtPrime m.asIdeal) m.asIdeal x).mpr hx) n
33   have hz : (algebraMap R (Localization.AtPrime m.asIdeal) x) ^ n = 0 := by
34     simpa only [hn, Ideal.zero_eq_bot, Ideal.mem_bot] using hmem
35   rw [pow_succ, hz, zero_mul]
36 
37 omit [IsArtinianRing R] in
38 /-- Distinct maximal ideals cannot contain all the generators of each other.
39 This also handles an empty generator type: no distinct maximal ideal can exist. -/
40 theorem exists_generator_outside {ι : Type*} (g : ι → R)
41     (m n : MaximalSpectrum R) (hg : Ideal.span (Set.range g) = m.asIdeal)
42     (hne : n ≠ m) : ∃ i, g i ∉ n.asIdeal := by
43   classical
44   by_contra! h
45   have hle : m.asIdeal ≤ n.asIdeal := by
46     rw [← hg, Ideal.span_le]
47     rintro _ ⟨i, rfl⟩
48     exact h i
49   exact hne (MaximalSpectrum.ext (m.isMaximal.eq_of_le n.isMaximal.ne_top hle).symm)
50 
51 omit [IsArtinianRing R] in
52 /-- An element invertible in one Artin coordinate has a partial inverse whose
53 product with it is exactly the corresponding canonical idempotent. -/
54 theorem exists_partial_inverse (D : Decomposition R) (m : MaximalSpectrum R)
55     (x : R) (hu : IsUnit (algebraMap R (Localization.AtPrime m.asIdeal) x)) :
56     ∃ y : R, y * x = idempotent D m := by
57   classical
58   obtain ⟨u, hu⟩ := hu
59   refine ⟨D.symm (Pi.single m (↑(u⁻¹) : Localization.AtPrime m.asIdeal)), ?_⟩
60   apply D.injective
61   simp only [map_mul, AlgEquiv.apply_symm_apply, map_idempotent]
62   ext n
63   by_cases hn : n = m
64   · subst n
65     simp only [Pi.mul_apply, Pi.single_eq_same, coordinate, ← hu, Units.inv_mul]
66   · simp [Pi.single_eq_of_ne hn]
67 
68 /-- The canonical packet is annihilated by one common positive power of every
69 element of its maximal ideal. This exponent is independent of the module. -/
70 theorem exists_packet_power (D : Decomposition R) (m : MaximalSpectrum R) :
71     ∃ N : ℕ, 1 ≤ N ∧ ∀ x ∈ m.asIdeal, x ^ N * idempotent D m = 0 := by
72   obtain ⟨N, hN, hn⟩ := exists_local_power m
73   refine ⟨N, hN, fun x hx => (mul_idempotent_eq_zero_iff D m _).mpr ?_⟩
74   simpa only [map_pow] using hn x hx
75 
76 variable {V : Type*} [AddCommGroup V] [Module R V]
77 
78 omit [IsArtinianRing R] in
79 /-- On every other Artin packet, a generator of m acts invertibly. Therefore a
80 vector killed by powers of all the generators has zero projection there. -/
81 theorem other_packet_vanishes {ι : Type*} (D : Decomposition R) (g : ι → R)
82     (m n : MaximalSpectrum R) (hg : Ideal.span (Set.range g) = m.asIdeal)
83     (hne : n ≠ m) (N : ℕ) (v : V) (hv : ∀ i, g i ^ N • v = 0) :
84     idempotent D n • v = 0 := by
85   obtain ⟨i, hi⟩ := exists_generator_outside g m n hg hne
86   have hu : IsUnit (algebraMap R (Localization.AtPrime n.asIdeal) (g i ^ N)) := by
87     rw [map_pow]
88     exact ((IsLocalization.AtPrime.isUnit_to_map_iff
89       (Localization.AtPrime n.asIdeal) n.asIdeal (g i)).mpr hi).pow N
90   obtain ⟨y, hy⟩ := exists_partial_inverse D n (g i ^ N) hu
91   rw [← hy, mul_smul, hv i, smul_zero]
92 
93 /-- Exact equality of the actual projector image with simultaneous generalized
94 nilpotence conditions. No finiteness, semisimplicity, or faithfulness condition
95 on the representation is needed. The maximal ideal generators are explicit. -/
96 theorem simultaneous_packet [Fintype (MaximalSpectrum R)] {ι : Type*}
97     (D : Decomposition R) (g : ι → R) (m : MaximalSpectrum R)
98     (hg : Ideal.span (Set.range g) = m.asIdeal) :
99     ∃ N : ℕ, 1 ≤ N ∧ ∀ v : V,
100       (∃ w : V, idempotent D m • w = v) ↔ ∀ i, g i ^ N • v = 0 := by
101   classical
102   obtain ⟨N, hN, hn⟩ := exists_packet_power D m
103   refine ⟨N, hN, fun v => ?_⟩
104   constructor
105   · rintro ⟨w, rfl⟩ i
106     rw [← mul_smul, hn (g i) (hg ▸ Ideal.subset_span ⟨i, rfl⟩), zero_smul]
107   · intro hv
108     refine ⟨v, ?_⟩
109     have hsum : (∑ n : MaximalSpectrum R, idempotent D n • v) = v := by
110       rw [← Finset.sum_smul, (complete D).complete, one_smul]
111     rw [Finset.sum_eq_single m] at hsum
112     · exact hsum
113     · intro n _ hne
114       exact other_packet_vanishes D g m n hg hne N v hv
115     · simp
116 
117 omit [IsArtinianRing R] in
118 /-- Corollary 8.3 in the paper's operator-and-eigenvalue notation. Once the
119 maximal ideal is explicitly given by these differences, algebraic closure and
120 an additional algebra-generation hypothesis are unnecessary. The packet is
121 the actual E-linear image of its canonical Artin idempotent. -/
122 theorem simultaneous_generalized_eigenspaces {E ι : Type*} [Field E]
123     [Algebra E R] [Module.Finite E R] [Module E V] [IsScalarTower E R V]
124     (D : Decomposition R) (T : ι → R) (eigenvalue : ι → E) (m : MaximalSpectrum R)
125     (hm : Ideal.span (Set.range (fun i => T i - algebraMap E R (eigenvalue i))) = m.asIdeal) :
126     ∃ N : ℕ, 1 ≤ N ∧
127       (PaperXII.PacketTrace.packet (E := E) (V := V) (idempotent D m) : Set V) =
128         {v : V | ∀ i, (T i - algebraMap E R (eigenvalue i)) ^ N • v = 0} := by
129   let : IsArtinianRing R := IsArtinianRing.of_finite E R
130   let : Fintype (MaximalSpectrum R) := Fintype.ofFinite _
131   obtain ⟨N, hN, hn⟩ := simultaneous_packet (V := V) D
132     (fun i => T i - algebraMap E R (eigenvalue i)) m hm
133   refine ⟨N, hN, ?_⟩
134   ext v
135   exact hn v
136 
137 end PaperXII.GeneralizedPackets

Back to source controls