DiagonalAutomorphisms.lean

1 import RealizationBoundaries.EndomorphismScalars
2 
3 /-!
4 # Inverses and automorphisms of the original groups
5 
6 An everywhere nonzero diagonal is invertible on the product. For a source with
7 an infinite selector, its inverse also preserves the appropriate original
8 rational-line preimages. This last step is proved; product invertibility alone
9 is not silently identified with invertibility on an arbitrary subspace.
10 -/
11 set_option autoImplicit false
12 set_option backward.isDefEq.respectTransparency false
13 noncomputable section
14 namespace RealizationBoundaries
15 
16 def inverseDiagonal (c : Ambient) : Ambient := fun p => (c p)⁻¹
17 
18 @[simp] theorem inverseDiagonal_apply (c : Ambient) (p : Prime) :
19     inverseDiagonal c p = (c p)⁻¹ := rfl
20 
21 theorem diagonal_inverse_left (c : Ambient) (hc : ∀ p, c p ≠ 0) (x : Ambient) :
22     diagonal (inverseDiagonal c) (diagonal c x) = x := by
23   funext p
24   exact inv_mul_cancel_left₀ (hc p) (x p)
25 
26 theorem diagonal_inverse_right (c : Ambient) (hc : ∀ p, c p ≠ 0) (x : Ambient) :
27     diagonal c (diagonal (inverseDiagonal c) x) = x := by
28   funext p
29   exact mul_inv_cancel_left₀ (hc p) (x p)
30 
31 /-- A topological additive equivalence on the actual infinite product. -/
32 def diagonalAmbientEquiv (c : Ambient) (hc : ∀ p, c p ≠ 0) : Ambient ≃ₜ+ Ambient where
33   toFun := diagonal c
34   invFun := diagonal (inverseDiagonal c)
35   left_inv := diagonal_inverse_left c hc
36   right_inv := diagonal_inverse_right c hc
37   map_add' := map_add (diagonal c)
38   continuous_toFun := diagonal_continuous c
39   continuous_invFun := diagonal_continuous (inverseDiagonal c)
40 
41 theorem diagonalTail_inverse_left (c : Ambient) (hc : ∀ p, c p ≠ 0) (v : TailSpace) :
42     diagonalTail (inverseDiagonal c) (diagonalTail c v) = v := by
43   obtain ⟨x, rfl⟩ := quotientMap_surjective v
44   simp only [diagonalTail_quotient, diagonal_inverse_left c hc]
45 
46 theorem diagonalTail_inverse_right (c : Ambient) (hc : ∀ p, c p ≠ 0) (v : TailSpace) :
47     diagonalTail c (diagonalTail (inverseDiagonal c) v) = v := by
48   obtain ⟨x, rfl⟩ := quotientMap_surjective v
49   simp only [diagonalTail_quotient, diagonal_inverse_right c hc]
50 
51 /-- A zero coordinate of the diagonal kills an actual nonzero prime seed. -/
52 theorem hom_injective_iff_diagonal_nonzero (U V : Submodule ℚ TailSpace)
53     (f : preimage U →+ preimage V) :
54     Function.Injective f ↔ ∀ p, homDiagonal U V f p ≠ 0 := by
55   constructor
56   · intro hf p hp
57     have hz : f (preimageSeed U p) = 0 := by
58       apply Subtype.ext
59       funext q
60       rw [hom_coordinate_formula U V f]
61       by_cases hq : q = p
62       · subst q
63         simp [hp]
64       · classical
65         simp [preimageSeed, primeSeed, cut, hq]
66     have he : preimageSeed U p = 0 := hf (hz.trans (map_zero f).symm)
67     have he' := congrArg (fun x : preimage U => x.val p) he
68     simp at he'
69   · intro hc x y hxy
70     apply Subtype.ext
71     funext p
72     have he := congrArg (fun z : preimage V => z.val p) hxy
73     rw [hom_coordinate_formula U V f, hom_coordinate_formula U V f] at he
74     exact mul_left_cancel₀ (hc p) he
75 
76 /-- Surjectivity also forces every diagonal coefficient to be nonzero. -/
77 theorem hom_surjective_diagonal_nonzero (U V : Submodule ℚ TailSpace)
78     (f : preimage U →+ preimage V) (hf : Function.Surjective f) :
79     ∀ p, homDiagonal U V f p ≠ 0 := by
80   intro p hp
81   obtain ⟨x, hx⟩ := hf (preimageSeed V p)
82   have he := congrArg (fun z : preimage V => z.val p) hx
83   rw [hom_coordinate_formula U V f, hp, zero_mul, preimageSeed_apply] at he
84   exact zero_ne_one he
85 
86 /-- Nonzero coordinate scalars cannot annihilate the source's nonzero rational line. -/
87 theorem diagonalSlope_ne_zero (S T : Set Prime) (hS : S.Infinite) (c : Ambient)
88     (hc : DiagonalAdmissible (selectorLine S) (selectorLine T) c)
89     (hn : ∀ p, c p ≠ 0) : diagonalSlope S T c hc ≠ 0 := by
90   intro hz
91   have hs := diagonalSlope_spec S T c hc
92   rw [hz, zero_smul] at hs
93   have hi := congrArg (diagonalTail (inverseDiagonal c)) hs
94   rw [diagonalTail_inverse_left c hn, map_zero] at hi
95   exact indicator_tail_ne_zero hS hi
96 
97 /-- The inverse multiplier maps the target line back to the source line.
98 The nonzero slope and the inverse line equation are derived explicitly. -/
99 theorem inverseDiagonal_admissible (S T : Set Prime) (hS : S.Infinite) (c : Ambient)
100     (hc : DiagonalAdmissible (selectorLine S) (selectorLine T) c)
101     (hn : ∀ p, c p ≠ 0) :
102     DiagonalAdmissible (selectorLine T) (selectorLine S) (inverseDiagonal c) := by
103   let r := diagonalSlope S T c hc
104   have hr : r ≠ 0 := diagonalSlope_ne_zero S T hS c hc hn
105   have he : quotientMap (indicator S) =
106       r • diagonalTail (inverseDiagonal c) (quotientMap (indicator T)) := by
107     have h := congrArg (diagonalTail (inverseDiagonal c)) (diagonalSlope_spec S T c hc)
108     rw [diagonalTail_inverse_left c hn, map_smul] at h
109     exact h
110   apply (diagonalAdmissible_selector_iff T S _).mpr
111   apply (mem_selectorGroup_iff S _).mpr
112   refine ⟨r⁻¹, ?_⟩
113   rw [he, smul_smul, inv_mul_cancel₀ hr, one_smul]
114   rfl
115 
116 /-- Exact inverse on the original subgroups, not only on their completion. -/
117 def selectorEquivOfNonzeroDiagonal (S T : Set Prime) (hS : S.Infinite)
118     (f : selectorGroup S →+ selectorGroup T)
119     (hn : ∀ p, homDiagonal (selectorLine S) (selectorLine T) f p ≠ 0) :
120     selectorGroup S ≃+ selectorGroup T where
121   toFun := f
122   invFun := diagonalRestriction (selectorLine T) (selectorLine S)
123     (inverseDiagonal (homDiagonal (selectorLine S) (selectorLine T) f))
124     (inverseDiagonal_admissible S T hS _ (homDiagonal_admissible _ _ f) hn)
125   left_inv x := by
126     apply Subtype.ext
127     change diagonal (inverseDiagonal (homDiagonal (selectorLine S) (selectorLine T) f))
128       (f x).val = x.val
129     exact (congrArg (diagonal (inverseDiagonal
130       (homDiagonal (selectorLine S) (selectorLine T) f)))
131       (hom_eq_diagonal (selectorLine S) (selectorLine T) f x)).trans
132         (diagonal_inverse_left _ hn x.val)
133   right_inv y := by
134     apply Subtype.ext
135     exact (hom_eq_diagonal (selectorLine S) (selectorLine T) f _).trans
136       (diagonal_inverse_right _ hn y.val)
137   map_add' := map_add f
138 
139 @[simp] theorem selectorEquivOfNonzeroDiagonal_apply (S T : Set Prime) (hS : S.Infinite)
140     (f : selectorGroup S →+ selectorGroup T)
141     (hn : ∀ p, homDiagonal (selectorLine S) (selectorLine T) f p ≠ 0)
142     (x : selectorGroup S) : selectorEquivOfNonzeroDiagonal S T hS f hn x = f x := rfl
143 
144 /-- The inverse formula is the reciprocal diagonal at every prime, with no tail exceptions. -/
145 theorem selectorEquiv_inverse_coordinate (S T : Set Prime) (hS : S.Infinite)
146     (f : selectorGroup S →+ selectorGroup T)
147     (hn : ∀ p, homDiagonal (selectorLine S) (selectorLine T) f p ≠ 0)
148     (y : selectorGroup T) (p : Prime) :
149     ((selectorEquivOfNonzeroDiagonal S T hS f hn).symm y).val p =
150       (homDiagonal (selectorLine S) (selectorLine T) f p)⁻¹ * y.val p := rfl
151 
152 /-- The rank-one line argument is essential to this converse. -/
153 theorem selector_hom_bijective_iff (S T : Set Prime) (hS : S.Infinite)
154     (f : selectorGroup S →+ selectorGroup T) :
155     Function.Bijective f ↔ ∀ p, homDiagonal (selectorLine S) (selectorLine T) f p ≠ 0 := by
156   constructor
157   · intro hf
158     exact (hom_injective_iff_diagonal_nonzero _ _ f).mp hf.1
159   · intro hn
160     exact (selectorEquivOfNonzeroDiagonal S T hS f hn).bijective
161 
162 /-- In this rank-one family an injective supplied map is automatically an isomorphism. -/
163 theorem selector_hom_injective_iff_bijective (S T : Set Prime) (hS : S.Infinite)
164     (f : selectorGroup S →+ selectorGroup T) :
165     Function.Injective f ↔ Function.Bijective f := by
166   rw [selector_hom_bijective_iff S T hS]
167   exact hom_injective_iff_diagonal_nonzero _ _ f
168 
169 theorem selector_hom_surjective_iff_bijective (S T : Set Prime) (hS : S.Infinite)
170     (f : selectorGroup S →+ selectorGroup T) :
171     Function.Surjective f ↔ Function.Bijective f := by
172   constructor
173   · intro hf
174     exact (selector_hom_bijective_iff S T hS f).mpr
175       (hom_surjective_diagonal_nonzero _ _ f hf)
176   · exact fun hf => hf.2
177 
178 /-- Corollary 7.8, including the existence of an actual additive automorphism. -/
179 theorem selector_endomorphism_automorphism_iff (S : Set Prime) (hS : S.Infinite)
180     (f : AddMonoid.End (selectorGroup S)) :
181     (∃ e : selectorGroup S ≃+ selectorGroup S, e.toAddMonoidHom = f) ↔
182       ∀ p, homDiagonal (selectorLine S) (selectorLine S) f p ≠ 0 := by
183   constructor
184   · rintro ⟨e, rfl⟩
185     exact (hom_injective_iff_diagonal_nonzero _ _ _).mp e.injective
186   · intro hn
187     exact ⟨selectorEquivOfNonzeroDiagonal S S hS f hn, rfl⟩
188 
189 end RealizationBoundaries

Back to source controls