RadicalOnePlus111.lean

1 import PaperXI.OnePlusIntersection110
2 import Mathlib.RingTheory.Jacobson.Ideal
3 
4 /-! Exact one-plus groups from actual radical ideals in the original order.
5 The order may be noncommutative. No arbitrary additive lattice is declared
6 to be a group or an ideal of the full field endomorphism algebra. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.RadicalOnePlus111
10 open PaperXI.OnePlusIntersection110
11 
12 variable {R : Type*} [Ring R]
13 
14 /-- A two-sided inverse follows from the left-Jacobson property alone.
15 No commutativity or desired invertibility premise is used. -/
16 theorem isUnit_of_sub_one_mem_jacobson (r : R)
17     (hr : r - 1 ∈ Ideal.jacobson (⊥ : Ideal R)) : IsUnit r := by
18   obtain ⟨s, hs⟩ := Ideal.exists_mul_sub_mem_of_sub_one_mem_jacobson r hr
19   have hsr : s * r = 1 := by simpa only [Ideal.mem_bot, sub_eq_zero] using hs
20   have hsrad : s - 1 ∈ Ideal.jacobson (⊥ : Ideal R) := by
21     have h := (Ideal.jacobson (⊥ : Ideal R)).neg_mem
22       ((Ideal.jacobson (⊥ : Ideal R)).mul_mem_left s hr)
23     have he : -(s * (r - 1)) = s - 1 := by rw [mul_sub, mul_one, hsr]; abel
24     rwa [he] at h
25   obtain ⟨t, ht⟩ := Ideal.exists_mul_sub_mem_of_sub_one_mem_jacobson s hsrad
26   have hts : t * s = 1 := by simpa only [Ideal.mem_bot, sub_eq_zero] using ht
27   have htr : t = r := by
28     calc t = t * (s * r) := by rw [hsr, mul_one]
29          _ = (t * s) * r := (mul_assoc _ _ _).symm
30          _ = r := by rw [hts, one_mul]
31   exact ⟨⟨r, s, by simpa only [htr] using hts, hsr⟩, rfl⟩
32 
33 /-- The actual subgroup of units whose offset belongs to I. -/
34 def onePlus (I : Ideal R) : Subgroup Rˣ := idealUnits I
35 
36 theorem onePlus_offsets (I : Ideal R) :
37     ∀ g : onePlus I, ((g : Rˣ) : R) - 1 ∈ I.toAddSubgroup := fun g => g.property
38 
39 /-- Every actual ideal element has its literal unit 1+x in the subgroup. -/
40 theorem onePlus_surjective (I : Ideal R)
41     (hI : I ≤ Ideal.jacobson (⊥ : Ideal R)) :
42     ∀ x : I.toAddSubgroup, ∃ g : onePlus I, ((g : Rˣ) : R) = 1 + (x : R) := by
43   intro x
44   have hu : IsUnit (1 + (x : R)) :=
45     isUnit_of_sub_one_mem_jacobson _ (by simpa using hI x.property)
46   obtain ⟨g, hg⟩ := hu
47   refine ⟨⟨g, ?_⟩, hg⟩
48   change (g : R) - 1 ∈ I
49   rw [hg]
50   simp
51 
52 /-- The ideal itself is the offset carrier, via the actual unit-valued map. -/
53 def offsetEquiv (I : Ideal R) (hI : I ≤ Ideal.jacobson (⊥ : Ideal R)) :
54     onePlus I ≃ I.toAddSubgroup :=
55   PaperXI.OnePlusIndex110.offsetEquiv I.toAddSubgroup (onePlus I)
56     (onePlus_offsets I) (onePlus_surjective I hI)
57 
58 end PaperXI.RadicalOnePlus111

Back to source controls