TailSignature.lean

1 import RealizationBoundaries.PairedPrimes
2 import RealizationBoundaries.Sections
3 
4 /-!
5 # The intrinsic tail-divisibility signature
6 
7 All statements concern elements of the actual infinite product preimages. The
8 exceptional set retains numerator primes, denominator primes and finite support.
9 -/
10 set_option autoImplicit false
11 set_option backward.isDefEq.respectTransparency false
12 noncomputable section
13 namespace RealizationBoundaries
14 
15 /-- A root predicate on the actual group, with no chosen coordinate presentation. -/
16 def HasPrimeRoot {H : Type*} [AddGroup H] (x : H) (p : Prime) : Prop :=
17   ∃ y : H, p.val • y = x
18 
19 /-- Every additive homomorphism preserves root solvability. -/
20 theorem hasPrimeRoot_map {H K : Type*} [AddGroup H] [AddGroup K]
21     (f : H →+ K) (x : H) (p : Prime) (hx : HasPrimeRoot x p) :
22     HasPrimeRoot (f x) p := by
23   obtain ⟨y, hy⟩ := hx
24   exact ⟨f y, by rw [← map_nsmul, hy]⟩
25 
26 /-- An actual additive equivalence preserves and reflects prime-root solvability. -/
27 theorem hasPrimeRoot_equiv {H K : Type*} [AddGroup H] [AddGroup K]
28     (e : H ≃+ K) (x : H) (p : Prime) :
29     HasPrimeRoot (e x) p ↔ HasPrimeRoot x p := by
30   constructor
31   · intro h
32     simpa using hasPrimeRoot_map e.symm.toAddMonoidHom (e x) p h
33   · exact hasPrimeRoot_map e.toAddMonoidHom x p
34 
35 /-- For a rational preimage, the intrinsic root test is precisely one coordinate test. -/
36 theorem preimage_prime_root_iff (W : Submodule ℚ TailSpace) (x : preimage W)
37     (p : Prime) : HasPrimeRoot x p ↔ x.val p = 0 := by
38   refine (preimage_root_iff W p.property.pos x).trans ?_
39   constructor
40   · intro h
41     exact h p (dvd_refl _)
42   · intro h q hq
43     have hqp : q = p := Subtype.ext ((p.property.dvd_iff_eq q.property.ne_one).mp hq).symm
44     subst q
45     exact h
46 
47 /-- The exceptional primes are not merely denominator primes: numerator primes and
48 all coordinates of the finite perturbation must also be retained. -/
49 def tailExceptions (r : ℚ) (d : finiteSupport) : Set Prime :=
50   exceptional r.num.natAbs ∪ exceptional r.den ∪ support d.val
51 
52 /-- A nonzero rational coordinate makes the entire exceptional set finite. -/
53 theorem tailExceptions_finite {r : ℚ} (hr : r ≠ 0) (d : finiteSupport) :
54     (tailExceptions r d).Finite := by
55   have hn : 0 < r.num.natAbs := by
56     apply Nat.pos_of_ne_zero
57     simpa using hr
58   exact ((exceptional_finite hn).union (exceptional_finite r.den_pos)).union d.property
59 
60 /-- Reduction of a nonzero rational remains nonzero away from both numerator and denominator. -/
61 theorem rational_cast_ne_zero {r : ℚ} (p : Prime)
62     (hn : ¬ p.val ∣ r.num.natAbs) (hd : ¬ p.val ∣ r.den) :
63     (r : Coordinate p) ≠ 0 := by
64   rw [Rat.cast_def]
65   apply div_ne_zero
66   · intro h
67     exact hn (Int.natCast_dvd.mp ((ZMod.intCast_zmod_eq_zero_iff_dvd r.num p.val).mp h))
68   · exact (coordinate_cast_eq_zero _ p).not.mpr hd
69 
70 /-- The nonzero-coordinate signature of a normal form outside its explicit exceptions. -/
71 theorem normalForm_coordinate_ne_zero_iff (S : Set Prime) (r : ℚ)
72     (d : finiteSupport) (p : Prime) (hp : p ∉ tailExceptions r d) :
73     (rationalSection S r + d.val) p ≠ 0 ↔ p ∈ S := by
74   classical
75   have hn : ¬ p.val ∣ r.num.natAbs := fun h => hp (Or.inl (Or.inl h))
76   have hd : ¬ p.val ∣ r.den := fun h => hp (Or.inl (Or.inr h))
77   have hz : d.val p = 0 := by
78     by_contra h
79     exact hp (Or.inr h)
80   have hc := rational_cast_ne_zero p hn hd
81   by_cases hs : p ∈ S <;> simp [Pi.add_apply, rationalSection, hs, hz, hc]
82 
83 /-- Finite perturbation of the selected support, with a concrete containing exceptional set. -/
84 theorem normalForm_support_disagreement_subset (S : Set Prime) (r : ℚ)
85     (d : finiteSupport) :
86     {p | ¬ ((rationalSection S r + d.val) p ≠ 0 ↔ p ∈ S)} ⊆ tailExceptions r d := by
87   intro p hp
88   by_contra he
89   exact hp (normalForm_coordinate_ne_zero_iff S r d p he)
90 
91 /-- The normal form of a nontorsion element has nonzero rational coordinate. -/
92 theorem normalForm_rational_ne_zero (S : Set Prime) (x : selectorGroup S)
93     (hx : x.val ∉ finiteSupport) (r : ℚ) (d : finiteSupport)
94     (h : x.val = rationalSection S r + d.val) : r ≠ 0 := by
95   intro hr
96   subst r
97   apply hx
98   rw [h, rationalSection_zero, zero_add]
99   exact d.property
100 
101 /-- Monograph Theorem 7.1: every nontorsion element carries the selector's tail signature. -/
102 theorem selector_tail_signature (S : Set Prime) (x : selectorGroup S)
103     (hx : x.val ∉ finiteSupport) :
104     ∃ E : Set Prime, E.Finite ∧ ∀ p ∉ E, (HasPrimeRoot x p ↔ p ∉ S) := by
105   obtain ⟨r, d, h⟩ := normalForm_exists S x
106   have hr := normalForm_rational_ne_zero S x hx r d h
107   refine ⟨tailExceptions r d, tailExceptions_finite hr d, ?_⟩
108   intro p hp
109   rw [preimage_prime_root_iff (selectorLine S) x p, h]
110   simpa only [not_not] using (normalForm_coordinate_ne_zero_iff S r d p hp).not
111 
112 /-- Infinite selected support means that the marked element has infinite order. -/
113 theorem markedElement_not_finiteSupport {S : Set Prime} (hS : S.Infinite) :
114     (markedElement S).val ∉ finiteSupport := by
115   change ¬ (support (indicator S)).Finite
116   rw [support_indicator]
117   exact hS
118 
119 /-- An additive homomorphism cannot turn a torsion source element into a nontorsion target. -/
120 theorem nontorsion_source_of_image (U V : Submodule ℚ TailSpace)
121     (f : preimage U →+ preimage V) (x : preimage U)
122     (hx : (f x).val ∉ finiteSupport) : x.val ∉ finiteSupport := by
123   intro ht
124   obtain ⟨m, hm, he⟩ := (preimage_torsion_iff U x).mpr ht
125   apply hx
126   apply (preimage_torsion_iff V (f x)).mp
127   exact ⟨m, hm, by rw [← map_nsmul, he, map_zero]⟩
128 
129 end RealizationBoundaries

Back to source controls