OnePlusIntersection110.lean

1 import PaperXI.OnePlusIndex110
2 
3 /-! Common-ideal quotient towers for exact one-plus groups. The primary
4 statement stays in the original integral-order ring and only needs nested
5 unit groups. It does not assume that a conjugate lattice is an ideal in the
6 full endomorphism algebra, or that a common integral order exists. -/
7 set_option autoImplicit false
8 noncomputable section
9 namespace PaperXI.OnePlusIntersection110
10 open OnePlusIndex110
11 
12 variable {R : Type*} [Ring R]
13 
14 /-- The ambient units congruent to one modulo a left ideal. -/
15 def idealUnits (I : Ideal R) : Subgroup Rˣ :=
16   (congruence I (⊤ : Subgroup Rˣ)).comap Subgroup.topEquiv.symm.toMonoidHom
17 
18 @[simp] theorem mem_idealUnits (I : Ideal R) (g : Rˣ) :
19     g ∈ idealUnits I ↔ (g : R) - 1 ∈ I := Iff.rfl
20 
21 theorem mem_of_offset (L : AddSubgroup R) (K : Subgroup Rˣ)
22     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R))
23     (g : Rˣ) (hg : (g : R) - 1 ∈ L) : g ∈ K := by
24   obtain ⟨u, hu⟩ := hL ⟨(g : R) - 1, hg⟩
25   have he : (u : Rˣ) = g := by
26     apply Units.ext
27     rw [hu]
28     change 1 + ((g : R) - 1) = (g : R)
29     noncomm_ring
30   exact he ▸ u.property
31 
32 theorem idealUnits_le (I : Ideal R) (L : AddSubgroup R) (K : Subgroup Rˣ)
33     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R))
34     (hIL : I.toAddSubgroup ≤ L) : idealUnits I ≤ K := by
35   intro g hg
36   exact mem_of_offset L K hL g (hIL ((mem_idealUnits I g).mp hg))
37 
38 theorem idealUnits_relIndex (I : Ideal R) (L : AddSubgroup R) (K : Subgroup Rˣ)
39     (hK : ∀ g : K, ((g : Rˣ) : R) - 1 ∈ L)
40     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R)) :
41     (idealUnits I).relIndex K = I.toAddSubgroup.relIndex L := by
42   change ((idealUnits I).subgroupOf K).index = _
43   have he : (idealUnits I).subgroupOf K = congruence I K := by
44     ext g
45     rfl
46   rw [he]
47   exact index_eq_additive_relIndex I L K hK hL
48 
49 /-- Nesting of exact one-plus unit groups forces nesting of offset lattices. -/
50 theorem offset_le_of_group_le (L M : AddSubgroup R) (K H : Subgroup Rˣ)
51     (hK : ∀ g : K, ((g : Rˣ) : R) - 1 ∈ L)
52     (hM : ∀ x : M, ∃ g : H, ((g : Rˣ) : R) = 1 + (x : R))
53     (hHK : H ≤ K) : M ≤ L := by
54   intro x hx
55   obtain ⟨g, hg⟩ := hM ⟨x, hx⟩
56   have h := hK ⟨g, hHK g.property⟩
57   rw [hg] at h
58   simpa only [add_sub_cancel_left] using h
59 
60 /-- Finite positive quotient towers remove the common deep ideal. No final
61 multiplicative/additive index identity is an input. -/
62 theorem nested_relIndex_eq (I : Ideal R) (L M : AddSubgroup R)
63     (K H : Subgroup Rˣ)
64     (hK : ∀ g : K, ((g : Rˣ) : R) - 1 ∈ L)
65     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R))
66     (hH : ∀ g : H, ((g : Rˣ) : R) - 1 ∈ M)
67     (hM : ∀ x : M, ∃ g : H, ((g : Rˣ) : R) = 1 + (x : R))
68     (hHK : H ≤ K) (hIM : I.toAddSubgroup ≤ M)
69     [Finite (L ⧸ I.toAddSubgroup.addSubgroupOf L)] :
70     H.relIndex K = M.relIndex L := by
71   have hML := offset_le_of_group_le L M K H hK hM hHK
72   have hCH := idealUnits_le I M H hM hIM
73   have hm := Subgroup.relIndex_mul_relIndex (idealUnits I) H K hCH hHK
74   rw [idealUnits_relIndex I M H hH hM, idealUnits_relIndex I L K hK hL] at hm
75   have ha := AddSubgroup.relIndex_mul_relIndex I.toAddSubgroup M L hIM hML
76   have hIL : I.toAddSubgroup.relIndex L ≠ 0 := by
77     change (I.toAddSubgroup.addSubgroupOf L).index ≠ 0
78     exact AddSubgroup.index_ne_zero_of_finite
79   have hIMpos : I.toAddSubgroup.relIndex M ≠ 0 := by
80     intro hz
81     rw [hz, zero_mul] at ha
82     exact hIL ha.symm
83   exact Nat.eq_of_mul_eq_mul_left (Nat.pos_of_ne_zero hIMpos) (hm.trans ha.symm)
84 
85 
86 section ExternalRing
87 variable {S : Type*} [Ring S]
88 
89 /-- Actual unit conjugation as a ring equivalence of the external algebra. -/
90 def innerRing (y : Sˣ) : S ≃+* S where
91   toFun x := (y : S) * x * (y⁻¹ : Sˣ)
92   invFun x := (y⁻¹ : Sˣ) * x * (y : S)
93   left_inv x := by simp [mul_assoc]
94   right_inv x := by simp [mul_assoc]
95   map_mul' x z := by simp [mul_assoc]
96   map_add' x z := by simp [mul_add, add_mul]
97 
98 /-- The literal image group has the literal image offset lattice. -/
99 theorem mapped_offsets (f : R →+* S) (L : AddSubgroup R) (K : Subgroup Rˣ)
100     (hK : ∀ g : K, ((g : Rˣ) : R) - 1 ∈ L) :
101     ∀ g : K.map (Units.map f.toMonoidHom),
102       ((g : Sˣ) : S) - 1 ∈ L.map f.toAddMonoidHom := by
103   intro g
104   obtain ⟨u, hu, he⟩ := Subgroup.mem_map.mp g.property
105   apply AddSubgroup.mem_map.mpr
106   refine ⟨(u : R) - 1, hK ⟨u, hu⟩, ?_⟩
107   change f ((u : R) - 1) = ((g : Sˣ) : S) - 1
108   rw [map_sub, map_one]
109   exact congrArg (fun z : Sˣ => (z : S) - 1) he
110 
111 theorem mapped_onePlus (f : R →+* S) (L : AddSubgroup R) (K : Subgroup Rˣ)
112     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R)) :
113     ∀ x : L.map f.toAddMonoidHom,
114       ∃ g : K.map (Units.map f.toMonoidHom), ((g : Sˣ) : S) = 1 + (x : S) := by
115   intro x
116   obtain ⟨a, ha, he⟩ := AddSubgroup.mem_map.mp x.property
117   obtain ⟨u, hu⟩ := hL ⟨a, ha⟩
118   refine ⟨⟨Units.map f.toMonoidHom (u : Rˣ),
119     Subgroup.mem_map.mpr ⟨u, u.property, rfl⟩⟩, ?_⟩
120   change f ((u : Rˣ) : R) = 1 + (x : S)
121   rw [hu, map_add, map_one]
122   exact congrArg (fun z : S => 1 + z) he
123 
124 def pullbackGroup (f : R →+* S) (K : Subgroup Rˣ) (K' : Subgroup Sˣ) :
125     Subgroup Rˣ := K ⊓ K'.comap (Units.map f.toMonoidHom)
126 
127 def pullbackLattice (f : R →+* S) (L : AddSubgroup R) (L' : AddSubgroup S) :
128     AddSubgroup R := L ⊓ L'.comap f.toAddMonoidHom
129 
130 theorem pullback_offsets (f : R →+* S) (L : AddSubgroup R) (L' : AddSubgroup S)
131     (K : Subgroup Rˣ) (K' : Subgroup Sˣ)
132     (hK : ∀ g : K, ((g : Rˣ) : R) - 1 ∈ L)
133     (hK' : ∀ g : K', ((g : Sˣ) : S) - 1 ∈ L') :
134     ∀ g : pullbackGroup f K K',
135       ((g : Rˣ) : R) - 1 ∈ pullbackLattice f L L' := by
136   intro g
137   refine ⟨hK ⟨g, g.property.1⟩, ?_⟩
138   have h := hK' ⟨Units.map f.toMonoidHom (g : Rˣ), g.property.2⟩
139   change f (((g : Rˣ) : R)) - 1 ∈ L' at h
140   change f (((g : Rˣ) : R) - 1) ∈ L'
141   simpa only [map_sub, map_one] using h
142 
143 theorem pullback_onePlus (f : R →+* S) (L : AddSubgroup R) (L' : AddSubgroup S)
144     (K : Subgroup Rˣ) (K' : Subgroup Sˣ)
145     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R))
146     (hL' : ∀ x : L', ∃ g : K', ((g : Sˣ) : S) = 1 + (x : S)) :
147     ∀ x : pullbackLattice f L L',
148       ∃ g : pullbackGroup f K K', ((g : Rˣ) : R) = 1 + (x : R) := by
149   intro x
150   obtain ⟨u, hu⟩ := hL ⟨x, x.property.1⟩
151   have hoff : ((Units.map f.toMonoidHom (u : Rˣ) : Sˣ) : S) - 1 = f (x : R) := by
152     change f ((u : Rˣ) : R) - 1 = f (x : R)
153     rw [hu, map_add, map_one]
154     simp only [add_sub_cancel_left]
155   have hmem : Units.map f.toMonoidHom (u : Rˣ) ∈ K' :=
156     mem_of_offset L' K' hL' _ (hoff ▸ x.property.2)
157   exact ⟨⟨u, ⟨u.property, hmem⟩⟩, hu⟩
158 
159 /-- A common deep left ideal in the original ring suffices for an intersection
160 with a group in an external ring. No common ambient order is required. -/
161 theorem pullback_intersection_relIndex_eq (f : R →+* S) (I : Ideal R)
162     (L : AddSubgroup R) (L' : AddSubgroup S) (K : Subgroup Rˣ) (K' : Subgroup Sˣ)
163     (hK : ∀ g : K, ((g : Rˣ) : R) - 1 ∈ L)
164     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R))
165     (hK' : ∀ g : K', ((g : Sˣ) : S) - 1 ∈ L')
166     (hL' : ∀ x : L', ∃ g : K', ((g : Sˣ) : S) = 1 + (x : S))
167     (hI : I.toAddSubgroup ≤ pullbackLattice f L L')
168     [Finite (L ⧸ I.toAddSubgroup.addSubgroupOf L)] :
169     K'.relIndex (K.map (Units.map f.toMonoidHom)) =
170       L'.relIndex (L.map f.toAddMonoidHom) := by
171   have he := nested_relIndex_eq I L (pullbackLattice f L L') K
172     (pullbackGroup f K K') hK hL (pullback_offsets f L L' K K' hK hK')
173     (pullback_onePlus f L L' K K' hL hL') inf_le_left hI
174   simpa only [pullbackGroup, pullbackLattice, Subgroup.inf_relIndex_left,
175     AddSubgroup.inf_relIndex_left, Subgroup.relIndex_comap, AddSubgroup.relIndex_comap] using he
176 
177 /-- Literal conjugation in S, with the deep ideal and finite quotient kept in
178 R. Both the conjugated group and conjugated lattice are constructed. -/
179 theorem conjugate_intersection_relIndex_eq (f : R →+* S) (y : Sˣ) (I : Ideal R)
180     (L : AddSubgroup R) (K : Subgroup Rˣ)
181     (hK : ∀ g : K, ((g : Rˣ) : R) - 1 ∈ L)
182     (hL : ∀ x : L, ∃ g : K, ((g : Rˣ) : R) = 1 + (x : R))
183     (hI : I.toAddSubgroup ≤ pullbackLattice f L
184       (L.map ((innerRing y).toRingHom.comp f).toAddMonoidHom))
185     [Finite (L ⧸ I.toAddSubgroup.addSubgroupOf L)] :
186     (K.map (Units.map ((innerRing y).toRingHom.comp f).toMonoidHom)).relIndex
187         (K.map (Units.map f.toMonoidHom)) =
188       (L.map ((innerRing y).toRingHom.comp f).toAddMonoidHom).relIndex
189         (L.map f.toAddMonoidHom) := by
190   exact pullback_intersection_relIndex_eq f I L
191     (L.map ((innerRing y).toRingHom.comp f).toAddMonoidHom) K
192     (K.map (Units.map ((innerRing y).toRingHom.comp f).toMonoidHom)) hK hL
193     (mapped_offsets ((innerRing y).toRingHom.comp f) L K hK)
194     (mapped_onePlus ((innerRing y).toRingHom.comp f) L K hL) hI
195 
196 end ExternalRing
197 end PaperXI.OnePlusIntersection110

Back to source controls