ArtinData.lean

1 import Mathlib.RingTheory.Artinian.Ring
2 import Mathlib.RingTheory.Localization.AtPrime.Basic
3 import Mathlib.RingTheory.Idempotents
4 
5 set_option autoImplicit false
6 
7 /-! The exact canonical algebraic input of Paper XII, external Fact 8.1.
8 The supplied equivalence is a ring decomposition, not a module decomposition
9 or a localization equivalence for the representation. Those are outputs of
10 the subsequent packet theorems. The R-algebra structure fixes every canonical
11 localization coordinate. No new axiom is introduced. -/
12 namespace PaperXII.ArtinData
13 
14 open scoped BigOperators
15 
16 variable {R : Type*} [CommRing R]
17 
18 /-- The canonical ring decomposition supplied by external Fact 8.1. -/
19 abbrev Decomposition (R : Type*) [CommRing R] :=
20   R ≃ₐ[R] (∀ m : MaximalSpectrum R, Localization.AtPrime m.asIdeal)
21 
22 /-- The actual central idempotent indexed by a maximal ideal. -/
23 noncomputable def idempotent (D : Decomposition R) (m : MaximalSpectrum R) : R := by
24   classical
25   exact D.symm (Pi.single m 1)
26 
27 /-- Every coordinate is the canonical localization map, by R-algebra linearity. -/
28 theorem coordinate (D : Decomposition R) (r : R) (m : MaximalSpectrum R) :
29     D r m = algebraMap R (Localization.AtPrime m.asIdeal) r := by
30   have h := D.commutes r
31   exact congrFun h m
32 
33 /-- The canonical coordinate maps determine the decomposition uniquely. -/
34 theorem decomposition_unique (D₁ D₂ : Decomposition R) : D₁ = D₂ := by
35   ext r m
36   rw [coordinate, coordinate]
37 
38 /-- The coordinate-vector identity determines the idempotent uniquely. -/
39 theorem map_idempotent [DecidableEq (MaximalSpectrum R)]
40     (D : Decomposition R) (m : MaximalSpectrum R) :
41     D (idempotent D m) = Pi.single m 1 := by
42   simp only [idempotent, AlgEquiv.apply_symm_apply]
43   congr 1
44   exact Subsingleton.elim _ _
45 
46 theorem idem (D : Decomposition R) (m : MaximalSpectrum R) :
47     IsIdempotentElem (idempotent D m) := by
48   classical
49   apply D.injective
50   simp only [map_mul, map_idempotent, ← Pi.single_mul, one_mul]
51 
52 theorem complete [Fintype (MaximalSpectrum R)] (D : Decomposition R) :
53     CompleteOrthogonalIdempotents (idempotent D) := by
54   classical
55   exact (CompleteOrthogonalIdempotents.single
56     (fun m : MaximalSpectrum R => Localization.AtPrime m.asIdeal)).map D.symm.toRingHom
57 
58 theorem algebraMap_idempotent_self (D : Decomposition R) (m : MaximalSpectrum R) :
59     algebraMap R (Localization.AtPrime m.asIdeal) (idempotent D m) = 1 := by
60   classical
61   rw [← coordinate, map_idempotent]
62   exact Pi.single_eq_same _ _
63 
64 theorem algebraMap_idempotent_other (D : Decomposition R) (m n : MaximalSpectrum R)
65     (h : m ≠ n) :
66     algebraMap R (Localization.AtPrime n.asIdeal) (idempotent D m) = 0 := by
67   classical
68   rw [← coordinate, map_idempotent]
69   exact Pi.single_eq_of_ne h.symm _
70 
71 theorem idempotent_not_mem (D : Decomposition R) (m : MaximalSpectrum R) :
72     idempotent D m ∉ m.asIdeal := by
73   have h : IsUnit (algebraMap R (Localization.AtPrime m.asIdeal) (idempotent D m)) := by
74     rw [algebraMap_idempotent_self]
75     exact isUnit_one
76   exact (IsLocalization.AtPrime.isUnit_to_map_iff
77     (Localization.AtPrime m.asIdeal) m.asIdeal _).mp h
78 
79 /-- Vanishing in the localized ring is exactly vanishing after multiplication
80 by the corresponding canonical idempotent. -/
81 theorem mul_idempotent_eq_zero_iff (D : Decomposition R) (m : MaximalSpectrum R) (r : R) :
82     r * idempotent D m = 0 ↔
83       algebraMap R (Localization.AtPrime m.asIdeal) r = 0 := by
84   classical
85   constructor
86   · intro h
87     have hh := congrArg (algebraMap R (Localization.AtPrime m.asIdeal)) h
88     simpa [map_mul, algebraMap_idempotent_self] using hh
89   · intro h
90     apply D.injective
91     ext n
92     by_cases hn : m = n
93     · subst n
94       simp [map_mul, coordinate, algebraMap_idempotent_self, h]
95     · simp [map_mul, coordinate, algebraMap_idempotent_other D m n hn]
96 
97 end PaperXII.ArtinData

Back to source controls