LocalResidue.lean

1 import PaperICompletion7.ModuleTop
2 import Mathlib.RingTheory.LocalRing.Basic
3 import Mathlib.RingTheory.Ideal.Quotient.Basic
4 import Mathlib.LinearAlgebra.Basis.VectorSpace
5 
6 /-!
7 The noncommutative local-ring specialization. The division-ring structure on
8 R / Jac(R) is derived from IsLocalRing R. It is not assumed, and no CommRing
9 or commutative residue-field convenience API is used.
10 -/
11 set_option autoImplicit false
12 
13 namespace Komorebi.PaperICompletion7.LocalResidue
14 
15 open Komorebi.SeedRankBasics
16 open Komorebi.PaperICompletion7.Nakayama
17 open Komorebi.PaperICompletion7.ModuleTop
18 
19 universe u v w
20 variable {R : Type u} [Ring R] [IsLocalRing R]
21 
22 /-- Two proper left ideals of a local ring cannot sum to the whole ring. -/
23 theorem proper_sup_ne_top (I J : Ideal R) (hI : I ≠ ⊤) (hJ : J ≠ ⊤) :
24     I ⊔ J ≠ ⊤ := by
25   intro h
26   have hone : (1 : R) ∈ I ⊔ J := by rw [h]; trivial
27   obtain ⟨a, ha, b, hb, hab⟩ := Submodule.mem_sup.mp hone
28   rcases IsLocalRing.isUnit_or_isUnit_of_add_one hab with hu | hu
29   · exact hI (I.eq_top_of_isUnit_mem ha hu)
30   · exact hJ (J.eq_top_of_isUnit_mem hb hu)
31 
32 /-- Uniqueness of the maximal left ideal, without commutativity. -/
33 theorem maximal_left_ideal_unique (I J : Ideal R)
34     (hI : I.IsMaximal) (hJ : J.IsMaximal) : I = J := by
35   by_contra h
36   exact proper_sup_ne_top I J hI.ne_top hJ.ne_top (hI.coprime_of_ne hJ h)
37 
38 /-- The actual ring Jacobson radical is maximal as a left ideal. -/
39 theorem jacobson_isMaximal : (Ring.jacobson R).IsMaximal := by
40   obtain ⟨m, hm⟩ := Ideal.exists_maximal R
41   have heq : Ring.jacobson R = m := by
42     rw [Ring.jacobson_eq_sInf_isMaximal]
43     apply le_antisymm (sInf_le hm)
44     exact le_sInf fun I hI ↦ (maximal_left_ideal_unique m I hm hI).le
45   exact heq.symm ▸ hm
46 
47 /-- The division-ring structure is constructed on the actual radical quotient. -/
48 noncomputable abbrev residueDivisionRing (R : Type u) [Ring R] [IsLocalRing R] :
49     DivisionRing (R ⧸ Ring.jacobson R) :=
50   letI := jacobson_isMaximal (R := R)
51   Ideal.Quotient.divisionRing (Ring.jacobson R)
52 
53 variable {M : Type v} [AddCommGroup M] [Module R M]
54 
55 /-- The printed local formula, with left dimension over the residue division ring. -/
56 theorem seedRank_eq_residue_dimension [Module.Finite R M] :
57     letI := residueDivisionRing R
58     seedRank R M = Module.rank (R ⧸ Ring.jacobson R) (RadicalTop R M) := by
59   let := residueDivisionRing R
60   exact seedRank_eq_radicalTop.trans Submodule.rank_eq_spanRank_of_free.symm
61 
62 /-- The natural-valued version uses the same constructed division-ring action. -/
63 theorem seedFinrank_eq_residue_finrank [Module.Finite R M] :
64     letI := residueDivisionRing R
65     seedFinrank R M = Module.finrank (R ⧸ Ring.jacobson R) (RadicalTop R M) := by
66   let := residueDivisionRing R
67   exact seedFinrank_eq_radicalTop.trans Module.finrank_eq_spanFinrank_of_free.symm
68 
69 end Komorebi.PaperICompletion7.LocalResidue

Back to source controls