RootConsequences.lean

1 import RealizationBoundaries.CyclicFiniteTargets
2 import RealizationBoundaries.Countability
3 
4 /-! # Normalized roots and boundary cases
5 
6 A solvable equation has a unique root with zero divisor coordinates, but in
7 general has many roots. The multiplier-zero fiber is infinite, not an empty
8 finite product. These are proved distinctions rather than comments in an API.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace RealizationBoundaries
13 
14 /-- Coordinate division solves the equation exactly when the obstruction coordinates vanish. -/
15 theorem coordinateDivide_root (m : ℕ) (x : Ambient)
16     (h : ∀ p : Prime, p.val ∣ m → x p = 0) : m • coordinateDivide m x = x := by
17   funext p
18   rw [coordinate_nsmul]
19   change (m : Coordinate p) * ((m : Coordinate p)⁻¹ * x p) = x p
20   by_cases hp : p.val ∣ m
21   · simp [(coordinate_cast_eq_zero m p).mpr hp, h p hp]
22   · exact mul_inv_cancel_left₀ ((coordinate_cast_eq_zero m p).not.mpr hp) (x p)
23 
24 /-- No root is chosen by classical existence here: every coordinate is specified. -/
25 def normalizedRoot (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
26     (x : preimage W) (h : ∀ p : Prime, p.val ∣ m → x.val p = 0) : RootFiber W m x :=
27   ⟨⟨coordinateDivide m x.val,
28     (nsmul_mem_preimage_iff W hm _).mp ((coordinateDivide_root m x.val h).symm ▸ x.property)⟩,
29     Subtype.ext (coordinateDivide_root m x.val h)⟩
30 
31 @[simp] theorem normalizedRoot_coordinate (W : Submodule ℚ TailSpace) {m : ℕ}
32     (hm : 0 < m) (x : preimage W) (h : ∀ p : Prime, p.val ∣ m → x.val p = 0)
33     (p : Prime) : (normalizedRoot W hm x h).val.val p = (m : Coordinate p)⁻¹ * x.val p := rfl
34 
35 theorem normalizedRoot_exceptional_zero (W : Submodule ℚ TailSpace) {m : ℕ}
36     (hm : 0 < m) (x : preimage W) (h : ∀ p : Prime, p.val ∣ m → x.val p = 0)
37     (p : Prime) (hp : p.val ∣ m) : (normalizedRoot W hm x h).val.val p = 0 := by
38   simp [normalizedRoot_coordinate, (coordinate_cast_eq_zero m p).mpr hp]
39 
40 /-- Zero values at all free divisor coordinates select exactly one root. -/
41 theorem normalizedRoot_unique (W : Submodule ℚ TailSpace) {m : ℕ}
42     (hm : 0 < m) (x : preimage W) (h : ∀ p : Prime, p.val ∣ m → x.val p = 0)
43     (y : RootFiber W m x) (hy : ∀ p : Prime, p.val ∣ m → y.val.val p = 0) :
44     y = normalizedRoot W hm x h := by
45   apply Subtype.ext
46   apply Subtype.ext
47   funext p
48   by_cases hp : p.val ∣ m
49   · rw [hy p hp, normalizedRoot_exceptional_zero W hm x h p hp]
50   · have hk : y.val - (normalizedRoot W hm x h).val ∈ rootKernel W m :=
51       (rootFiber_coset_iff W m x (normalizedRoot W hm x h) y.val).mp y.property
52     exact sub_eq_zero.mp (rootKernel_coordinate_zero W m ⟨_, hk⟩ p hp)
53 
54 /-- The positive multiplier with radical one is exactly one. -/
55 theorem primeRadical_eq_one_iff {m : ℕ} (hm : 0 < m) : primeRadical m = 1 ↔ m = 1 := by
56   constructor
57   · intro h
58     by_contra hm1
59     obtain ⟨p, hp, hpm⟩ := Nat.exists_prime_and_dvd hm1
60     have hd : p ∣ primeRadical m := (prime_dvd_radical_iff hm ⟨p,hp⟩).mpr hpm
61     rw [h] at hd
62     exact hp.ne_one (Nat.eq_one_of_dvd_one hd)
63   · rintro rfl
64     exact primeRadical_one
65 
66 /-- Uniqueness of the entire fiber is different from uniqueness of the normalized root. -/
67 theorem unique_root_iff_one (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
68     (x : preimage W) (h : ∃ y : preimage W, m • y = x) :
69     (∃! y : preimage W, m • y = x) ↔ m = 1 := by
70   have hc := rootFiber_card_of_solvable W hm x h
71   constructor
72   · rintro ⟨y, hy, hu⟩
73     have hs : Subsingleton (RootFiber W m x) := ⟨by
74       intro z w
75       apply Subtype.ext
76       exact (hu z.val z.property).trans (hu w.val w.property).symm⟩
77     have hn : Nonempty (RootFiber W m x) := ⟨⟨y,hy⟩⟩
78     have hcard : Nat.card (RootFiber W m x) = 1 := Nat.card_eq_one_iff_unique.mpr ⟨hs, hn⟩
79     exact (primeRadical_eq_one_iff hm).mp (hc.symm.trans hcard)
80   · rintro rfl
81     exact ⟨x, one_nsmul x, fun y hy => by simpa using hy⟩
82 
83 /-- A solvable positive prime-power equation has p roots, not p^k roots. -/
84 theorem prime_power_root_count (W : Submodule ℚ TailSpace) {p k : ℕ}
85     (hp : p.Prime) (hk : k ≠ 0) (x : preimage W)
86     (h : ∃ y : preimage W, (p ^ k) • y = x) :
87     Nat.card (RootFiber W (p ^ k) x) = p := by
88   rw [rootFiber_card_of_solvable W (pow_pos hp.pos k) x h, primeRadical_prime_pow hp hk]
89 
90 /-- Zero multiplication at zero has the whole original group as its root fiber. -/
91 def zeroRootFiberEquiv (W : Submodule ℚ TailSpace) : RootFiber W 0 0 ≃ preimage W where
92   toFun x := x.val
93   invFun x := ⟨x, zero_nsmul x⟩
94   left_inv _ := rfl
95   right_inv _ := rfl
96 
97 theorem zeroRootFiber_infinite (W : Submodule ℚ TailSpace) : Infinite (RootFiber W 0 0) :=
98   Infinite.of_injective (zeroRootFiberEquiv W).symm (zeroRootFiberEquiv W).symm.injective
99 
100 /-- Nat.card = 0 at multiplier zero must not be read as a proof of emptiness. -/
101 theorem zeroRootFiber_card (W : Submodule ℚ TailSpace) : Nat.card (RootFiber W 0 0) = 0 := by
102   let := zeroRootFiber_infinite W
103   exact Nat.card_eq_zero_of_infinite
104 
105 theorem zeroRootFiber_nonempty (W : Submodule ℚ TailSpace) : Nonempty (RootFiber W 0 0) :=
106   ⟨⟨0, zero_nsmul 0⟩⟩
107 
108 /-- Zero multiplication at a nonzero target has no root. -/
109 theorem zeroRootFiber_isEmpty_of_ne_zero (W : Submodule ℚ TailSpace) (x : preimage W)
110     (hx : x ≠ 0) : IsEmpty (RootFiber W 0 x) := by
111   apply rootFiber_isEmpty
112   rintro ⟨y, hy⟩
113   exact hx (by simpa using hy.symm)
114 
115 end RealizationBoundaries

Back to source controls