Preimages.lean

1 import RealizationBoundaries.Quotient
2 import Mathlib.Algebra.Module.Submodule.Basic
3 import Mathlib.Algebra.Module.Submodule.Map
4 
5 /-! # Rational preimages and exact integer-root certificates -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace RealizationBoundaries
9 
10 /-- The actual subgroup q⁻¹(W) of the unrestricted prime product. -/
11 def preimage (W : Submodule ℚ TailSpace) : AddSubgroup Ambient :=
12   W.toAddSubgroup.comap quotientMap
13 
14 @[simp] theorem mem_preimage (W : Submodule ℚ TailSpace) (x : Ambient) :
15     x ∈ preimage W ↔ quotientMap x ∈ W := Iff.rfl
16 
17 theorem finiteSupport_le_preimage (W : Submodule ℚ TailSpace) :
18     finiteSupport ≤ preimage W := by
19   intro x hx
20   change quotientMap x ∈ W
21   rw [(quotientMap_eq_zero_iff x).mpr hx]
22   exact W.zero_mem
23 
24 /-- Every ambient integer root of a member of H_W is already in H_W. -/
25 theorem nsmul_mem_preimage_iff (W : Submodule ℚ TailSpace) {m : ℕ}
26     (hm : 0 < m) (x : Ambient) : m • x ∈ preimage W ↔ x ∈ preimage W := by
27   change quotientMap (m • x) ∈ W ↔ quotientMap x ∈ W
28   rw [map_nsmul, ← Nat.cast_smul_eq_nsmul ℚ]
29   exact W.smul_mem_iff (by exact_mod_cast Nat.ne_of_gt hm)
30 
31 /-- Complete root condition in the actual infinite ambient product. -/
32 theorem ambient_root_iff (m : ℕ) (x : Ambient) :
33     (∃ y : Ambient, m • y = x) ↔ ∀ p : Prime, p.val ∣ m → x p = 0 := by
34   constructor
35   · rintro ⟨y, rfl⟩ p hp
36     simp [(coordinate_cast_eq_zero m p).mpr hp]
37   · intro hx
38     refine ⟨coordinateDivide m x, ?_⟩
39     funext p
40     rw [coordinate_nsmul]
41     change (m : Coordinate p) * ((m : Coordinate p)⁻¹ * x p) = x p
42     by_cases hp : p.val ∣ m
43     · simp [(coordinate_cast_eq_zero m p).mpr hp, hx p hp]
44     · exact mul_inv_cancel_left₀ ((coordinate_cast_eq_zero m p).not.mpr hp) (x p)
45 
46 /-- Monograph Theorem 4.2: root solvability in every rational preimage. -/
47 theorem preimage_root_iff (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
48     (x : preimage W) :
49     (∃ y : preimage W, m • y = x) ↔ ∀ p : Prime, p.val ∣ m → x.val p = 0 := by
50   constructor
51   · rintro ⟨y, hy⟩
52     apply (ambient_root_iff m x.val).mp
53     exact ⟨y.val, congrArg Subtype.val hy⟩
54   · intro hx
55     obtain ⟨y, hy⟩ := (ambient_root_iff m x.val).mpr hx
56     have hymem : y ∈ preimage W := (nsmul_mem_preimage_iff W hm y).mp (hy ▸ x.property)
57     exact ⟨⟨y, hymem⟩, Subtype.ext hy⟩
58 
59 /-- Purity is a proved property of the constructed subgroup, not a supplied hypothesis. -/
60 theorem preimage_pure (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
61     (x : preimage W) (h : ∃ y : Ambient, m • y = x.val) :
62     ∃ y : preimage W, m • y = x :=
63   (preimage_root_iff W hm x).mpr ((ambient_root_iff m x.val).mp h)
64 
65 /-- A single exceptional nonzero coordinate rules out every root. -/
66 theorem prime_obstruction (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
67     (x : preimage W) (p : Prime) (hp : p.val ∣ m) (hx : x.val p ≠ 0) :
68     ¬ ∃ y : preimage W, m • y = x := by
69   intro hy
70   exact hx ((preimage_root_iff W hm x).mp hy p hp)
71 
72 /-- Torsion remains precisely the original finite-support subgroup. -/
73 theorem preimage_torsion_iff (W : Submodule ℚ TailSpace) (x : preimage W) :
74     (∃ m : ℕ, 0 < m ∧ m • x = 0) ↔ x.val ∈ finiteSupport := by
75   constructor
76   · rintro ⟨m, hm, hx⟩
77     exact (torsion_iff_finiteSupport x.val).mp ⟨m, hm, congrArg Subtype.val hx⟩
78   · intro hx
79     obtain ⟨m, hm, hmx⟩ := exists_annihilator_of_finiteSupport x.val hx
80     exact ⟨m, hm, Subtype.ext hmx⟩
81 
82 /-- Every nonzero element is detected by a finite prime coordinate. -/
83 theorem nonzero_coordinate (W : Submodule ℚ TailSpace) (x : preimage W) (hx : x ≠ 0) :
84     ∃ p : Prime, x.val p ≠ 0 := by
85   by_contra h
86   push Not at h
87   apply hx
88   apply Subtype.ext
89   funext p
90   exact h p
91 
92 end RealizationBoundaries

Back to source controls