Sections.lean

1 import RealizationBoundaries.Extensions
2 import Mathlib.Data.Rat.Cast.Defs
3 import Mathlib.LinearAlgebra.Span.Basic
4 
5 /-! # Actual rational sections in the unrestricted prime product -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace RealizationBoundaries
9 
10 /-- The indicator of a chosen set of prime coordinates. -/
11 def indicator (S : Set Prime) : Ambient := by
12   classical
13   exact fun p => if p ∈ S then 1 else 0
14 
15 @[simp] theorem indicator_apply_mem {S : Set Prime} {p : Prime} (hp : p ∈ S) :
16     indicator S p = 1 := by
17   classical
18   simp [indicator, hp]
19 
20 @[simp] theorem indicator_apply_not_mem {S : Set Prime} {p : Prime} (hp : p ∉ S) :
21     indicator S p = 0 := by
22   classical
23   simp [indicator, hp]
24 
25 theorem support_indicator (S : Set Prime) : support (indicator S) = S := by
26   classical
27   ext p
28   simp [support, indicator]
29 
30 theorem indicator_tail_ne_zero {S : Set Prime} (hS : S.Infinite) :
31     quotientMap (indicator S) ≠ 0 := by
32   intro h
33   have hf := (quotientMap_eq_zero_iff _).mp h
34   change (support (indicator S)).Finite at hf
35   rw [support_indicator] at hf
36   exact hS hf
37 
38 /-- This is the monograph's reduced-rational section, including its zero branch
39 at denominator primes. The Rat cast into ZMod is num/den, with inverse zero = zero. -/
40 def rationalSection (S : Set Prime) (r : ℚ) : Ambient := by
41   classical
42   exact fun p => if p ∈ S then (r : Coordinate p) else 0
43 
44 @[simp] theorem rationalSection_zero (S : Set Prime) : rationalSection S 0 = 0 := by
45   classical
46   funext p
47   simp [rationalSection]
48 
49 @[simp] theorem rationalSection_one (S : Set Prime) : rationalSection S 1 = indicator S := by
50   classical
51   funext p
52   simp [rationalSection, indicator]
53 
54 @[simp] theorem rationalSection_neg (S : Set Prime) (r : ℚ) :
55     rationalSection S (-r) = -rationalSection S r := by
56   classical
57   funext p
58   by_cases hp : p ∈ S <;> simp [rationalSection, hp]
59 
60 /-- The arbitrary-prime zero-denominator branch is explicitly part of the formal statement. -/
61 theorem rationalSection_denominator_zero (S : Set Prime) (r : ℚ) (p : Prime)
62     (hp : p.val ∣ r.den) : rationalSection S r p = 0 := by
63   classical
64   simp [rationalSection, Rat.cast_def, (coordinate_cast_eq_zero r.den p).mpr hp]
65 
66 theorem rationalSection_denominator_defect (S : Set Prime) (r : ℚ) :
67     r.den • rationalSection S r - r.num • indicator S ∈ finiteSupport := by
68   classical
69   apply (exceptional_finite r.den_pos).subset
70   intro p hp
71   by_contra hn
72   have hd : (r.den : Coordinate p) ≠ 0 := (coordinate_cast_eq_zero r.den p).not.mpr hn
73   apply hp
74   by_cases hs : p ∈ S
75   · change r.den • rationalSection S r p - r.num • indicator S p = 0
76     rw [nsmul_eq_mul, zsmul_eq_mul]
77     simp only [rationalSection, hs, ite_true, indicator_apply_mem hs, mul_one, Rat.cast_def]
78     rw [mul_div_cancel₀ _ hd, sub_self]
79   · simp [Pi.sub_apply, rationalSection, indicator, hs]
80 
81 /-- The concrete section lands over the intended rational multiple of the tail. -/
82 theorem quotientMap_rationalSection (S : Set Prime) (r : ℚ) :
83     quotientMap (rationalSection S r) = r • quotientMap (indicator S) := by
84   have hd := (quotientMap_eq_zero_iff _).mpr (rationalSection_denominator_defect S r)
85   rw [map_sub, map_nsmul, map_zsmul, sub_eq_zero] at hd
86   apply tail_nsmul_injective r.den_pos
87   change r.den • quotientMap (rationalSection S r) =
88     r.den • (r • quotientMap (indicator S))
89   rw [hd, ← Nat.cast_smul_eq_nsmul ℚ, ← Int.cast_smul_eq_zsmul ℚ, smul_smul]
90   congr 1
91   exact (Rat.den_mul_eq_num r).symm
92 
93 /-- The actual rational line, and its original group of admissible ambient points. -/
94 def selectorLine (S : Set Prime) : Submodule ℚ TailSpace :=
95   Submodule.span ℚ {quotientMap (indicator S)}
96 
97 def selectorGroup (S : Set Prime) : AddSubgroup Ambient := preimage (selectorLine S)
98 
99 theorem mem_selectorGroup_iff (S : Set Prime) (x : Ambient) :
100     x ∈ selectorGroup S ↔ ∃ r : ℚ, r • quotientMap (indicator S) = quotientMap x := by
101   change quotientMap x ∈ Submodule.span ℚ {quotientMap (indicator S)} ↔ _
102   exact Submodule.mem_span_singleton
103 
104 theorem rationalSection_mem (S : Set Prime) (r : ℚ) :
105     rationalSection S r ∈ selectorGroup S :=
106   (mem_selectorGroup_iff _ _).mpr ⟨r, (quotientMap_rationalSection S r).symm⟩
107 
108 /-- Every point of the actual preimage has a reduced-rational, finite-support normal form. -/
109 theorem normalForm_exists (S : Set Prime) (x : selectorGroup S) :
110     ∃ r : ℚ, ∃ d : finiteSupport, x.val = rationalSection S r + d.val := by
111   obtain ⟨r, hr⟩ := (mem_selectorGroup_iff S x.val).mp x.property
112   have hd : x.val - rationalSection S r ∈ finiteSupport := by
113     apply (quotientMap_eq_iff _ _).mp
114     rw [quotientMap_rationalSection, hr]
115   exact ⟨r, ⟨x.val - rationalSection S r, hd⟩, by simp⟩
116 
117 /-- Infinite support is the precise hypothesis needed for a unique rational coordinate. -/
118 theorem normalForm_unique {S : Set Prime} (hS : S.Infinite)
119     (r t : ℚ) (d e : finiteSupport)
120     (h : rationalSection S r + d.val = rationalSection S t + e.val) : r = t ∧ d = e := by
121   have hq := congrArg quotientMap h
122   simp only [map_add, quotientMap_rationalSection,
123     (quotientMap_eq_zero_iff _).mpr d.property,
124     (quotientMap_eq_zero_iff _).mpr e.property, add_zero] at hq
125   have hrt : r = t := (smul_left_injective ℚ (indicator_tail_ne_zero hS)) hq
126   subst t
127   exact ⟨rfl, Subtype.ext (add_left_cancel h)⟩
128 
129 end RealizationBoundaries

Back to source controls