EndomorphismScalars.lean

1 import RealizationBoundaries.DiagonalRealization
2 
3 /-!
4 # Rational quotient scalars and the full endomorphism ring
5 
6 The eventual rational value is derived from membership in the actual rational
7 line. Its ring laws and surjectivity are proved. Exceptional primes, including
8 denominator primes, are retained by the finite-defect formulation.
9 -/
10 set_option autoImplicit false
11 set_option backward.isDefEq.respectTransparency false
12 noncomputable section
13 namespace RealizationBoundaries
14 
15 /-- The scalar on the target rational line, chosen only after admissibility is proved. -/
16 def diagonalSlope (S T : Set Prime) (c : Ambient)
17     (hc : DiagonalAdmissible (selectorLine S) (selectorLine T) c) : ℚ :=
18   Classical.choose ((mem_selectorGroup_iff T _).mp
19     ((diagonalAdmissible_selector_iff S T c).mp hc))
20 
21 theorem diagonalSlope_spec (S T : Set Prime) (c : Ambient)
22     (hc : DiagonalAdmissible (selectorLine S) (selectorLine T) c) :
23     diagonalTail c (quotientMap (indicator S)) =
24       diagonalSlope S T c hc • quotientMap (indicator T) :=
25   (Classical.choose_spec ((mem_selectorGroup_iff T _).mp
26     ((diagonalAdmissible_selector_iff S T c).mp hc))).symm
27 
28 /-- Infinite target support is needed to identify the rational scalar uniquely. -/
29 theorem diagonalSlope_unique (S T : Set Prime) (hT : T.Infinite) (c : Ambient)
30     (hc : DiagonalAdmissible (selectorLine S) (selectorLine T) c) (r : ℚ)
31     (hr : diagonalTail c (quotientMap (indicator S)) = r • quotientMap (indicator T)) :
32     diagonalSlope S T c hc = r := by
33   apply smul_left_injective ℚ (indicator_tail_ne_zero hT)
34   exact (diagonalSlope_spec S T c hc).symm.trans hr
35 
36 /-- The same scalar governs every element of the quotient line. -/
37 theorem diagonalSlope_on_line (S T : Set Prime) (c : Ambient)
38     (hc : DiagonalAdmissible (selectorLine S) (selectorLine T) c) (r : ℚ) :
39     diagonalTail c (r • quotientMap (indicator S)) =
40       (r * diagonalSlope S T c hc) • quotientMap (indicator T) := by
41   rw [map_smul, diagonalSlope_spec, smul_smul]
42 
43 /-- On a selected coordinate, the finite defect is the difference from rational reduction. -/
44 theorem diagonal_section_defect_support (S : Set Prime) (c : Ambient) (r : ℚ) :
45     support (diagonal c (indicator S) - rationalSection S r) =
46       {p | p ∈ S ∧ c p ≠ (r : Coordinate p)} := by
47   classical
48   ext p
49   by_cases hp : p ∈ S <;> simp [support, rationalSection, indicator, hp, sub_eq_zero]
50 
51 /-- The printed eventual-rational condition, with all exceptions explicitly finite. -/
52 theorem diagonalEndRing_mem_iff (S : Set Prime) (c : Ambient) :
53     c ∈ diagonalEndRing (selectorLine S) ↔
54       ∃ r : ℚ, {p | p ∈ S ∧ c p ≠ (r : Coordinate p)}.Finite := by
55   change DiagonalAdmissible (selectorLine S) (selectorLine S) c ↔ _
56   rw [diagonalAdmissible_iff_finite_defect]
57   simp only [mem_finiteSupport, diagonal_section_defect_support]
58 
59 /-- Each finite-defect scalar equals the unique rational quotient scalar. -/
60 theorem diagonalSlope_eq_of_finite_defect (S T : Set Prime) (hT : T.Infinite)
61     (c : Ambient) (hc : DiagonalAdmissible (selectorLine S) (selectorLine T) c)
62     (r : ℚ) (hr : diagonal c (indicator S) - rationalSection T r ∈ finiteSupport) :
63     diagonalSlope S T c hc = r := by
64   apply diagonalSlope_unique S T hT c hc r
65   have hq := (quotientMap_eq_iff _ _).mpr hr
66   rw [quotientMap_rationalSection] at hq
67   exact hq
68 
69 /-- The unique rational value is a ring homomorphism on the admissible diagonal ring. -/
70 def quotientScalar (S : Set Prime) (hS : S.Infinite) :
71     diagonalEndRing (selectorLine S) →+* ℚ where
72   toFun c := diagonalSlope S S c.val c.property
73   map_zero' := by
74     apply diagonalSlope_unique S S hS 0 _ 0
75     have hz : diagonal 0 (indicator S) = 0 := by funext p; simp
76     rw [diagonalTail_quotient, hz, map_zero, zero_smul]
77   map_one' := by
78     apply diagonalSlope_unique S S hS 1 _ 1
79     simp
80   map_add' c d := by
81     apply smul_left_injective ℚ (indicator_tail_ne_zero hS)
82     calc
83       _ = diagonalTail (c + d).val (quotientMap (indicator S)) :=
84         (diagonalSlope_spec S S (c + d).val (c + d).property).symm
85       _ = diagonalTail c.val (quotientMap (indicator S)) +
86           diagonalTail d.val (quotientMap (indicator S)) :=
87         diagonalTail_add c.val d.val _
88       _ = _ := by
89         rw [diagonalSlope_spec S S c.val c.property,
90           diagonalSlope_spec S S d.val d.property]
91         exact (add_smul _ _ _).symm
92   map_mul' c d := by
93     apply smul_left_injective ℚ (indicator_tail_ne_zero hS)
94     calc
95       _ = diagonalTail (c * d).val (quotientMap (indicator S)) :=
96         (diagonalSlope_spec S S (c * d).val (c * d).property).symm
97       _ = diagonalTail c.val (diagonalTail d.val (quotientMap (indicator S))) :=
98         diagonalTail_mul c.val d.val _
99       _ = _ := by
100         rw [diagonalSlope_spec S S d.val d.property, map_smul,
101           diagonalSlope_spec S S c.val c.property, smul_smul, mul_comm]
102 
103 @[simp] theorem quotientScalar_spec (S : Set Prime) (hS : S.Infinite)
104     (c : diagonalEndRing (selectorLine S)) :
105     diagonalTail c.val (quotientMap (indicator S)) =
106       quotientScalar S hS c • quotientMap (indicator S) :=
107   diagonalSlope_spec S S c.val c.property
108 
109 @[simp] theorem diagonal_section_indicator (S : Set Prime) (r : ℚ) :
110     diagonal (rationalSection S r) (indicator S) = rationalSection S r := by
111   classical
112   funext p
113   by_cases hp : p ∈ S <;> simp [rationalSection, indicator, hp]
114 
115 /-- A rational section is an admissible multiplier, even at denominator primes. -/
116 def rationalDiagonal (S : Set Prime) (r : ℚ) : diagonalEndRing (selectorLine S) :=
117   ⟨rationalSection S r, (diagonalAdmissible_selector_iff S S _).mpr
118     (by rw [diagonal_section_indicator]; exact rationalSection_mem S r)⟩
119 
120 @[simp] theorem quotientScalar_rationalDiagonal (S : Set Prime) (hS : S.Infinite) (r : ℚ) :
121     quotientScalar S hS (rationalDiagonal S r) = r := by
122   refine diagonalSlope_unique S S hS (rationalDiagonal S r).val
123     (rationalDiagonal S r).property r ?_
124   change quotientMap (diagonal (rationalSection S r) (indicator S)) = _
125   rw [diagonal_section_indicator, quotientMap_rationalSection]
126 
127 /-- Surjectivity does not require a homomorphic section of the nonsplit group extension. -/
128 theorem quotientScalar_surjective (S : Set Prime) (hS : S.Infinite) :
129     Function.Surjective (quotientScalar S hS) :=
130   fun r => ⟨rationalDiagonal S r, quotientScalar_rationalDiagonal S hS r⟩
131 
132 /-- The kernel consists exactly of families with finitely many nonzero selected entries. -/
133 theorem quotientScalar_eq_zero_iff (S : Set Prime) (hS : S.Infinite)
134     (c : diagonalEndRing (selectorLine S)) :
135     quotientScalar S hS c = 0 ↔ {p | p ∈ S ∧ c.val p ≠ 0}.Finite := by
136   constructor
137   · intro hz
138     have hq := quotientScalar_spec S hS c
139     rw [hz, zero_smul] at hq
140     have hf := (quotientMap_eq_zero_iff _).mp hq
141     have he := diagonal_section_defect_support S c.val 0
142     simp only [rationalSection_zero, sub_zero, Rat.cast_zero] at he
143     change (support (diagonal c.val (indicator S))).Finite at hf
144     rwa [he] at hf
145   · intro hf
146     apply diagonalSlope_eq_of_finite_defect S S hS c.val c.property 0
147     change (support (diagonal c.val (indicator S) - rationalSection S 0)).Finite
148     simpa only [diagonal_section_defect_support, Rat.cast_zero] using hf
149 
150 /-- The original endomorphism ring carries this surjective rational quotient character. -/
151 def endomorphismQuotientScalar (S : Set Prime) (hS : S.Infinite) :
152     AddMonoid.End (selectorGroup S) →+* ℚ :=
153   (quotientScalar S hS).comp (homDiagonalRing (selectorLine S))
154 
155 theorem endomorphismQuotientScalar_surjective (S : Set Prime) (hS : S.Infinite) :
156     Function.Surjective (endomorphismQuotientScalar S hS) := by
157   intro r
158   obtain ⟨c, hc⟩ := quotientScalar_surjective S hS r
159   obtain ⟨f, hf⟩ := (endomorphismRingEquiv (selectorLine S)).surjective c
160   refine ⟨f, ?_⟩
161   change quotientScalar S hS (homDiagonalRing (selectorLine S) f) = r
162   have he : homDiagonalRing (selectorLine S) f = c := hf
163   rw [he, hc]
164 
165 end RealizationBoundaries

Back to source controls