RadicalCounts.lean

1 import RealizationBoundaries.RootFibers
2 import Mathlib.Data.Nat.Factorization.Basic
3 import Mathlib.Data.Fintype.BigOperators
4 
5 /-! # Exact finite root counts
6 
7 The radical is the product of distinct prime divisors. All root-count statements
8 retain m > 0, so the convention for the product at zero cannot conceal an
9 infinite zero-multiplier fiber behind Nat.card's value zero.
10 -/
11 set_option autoImplicit false
12 noncomputable section
13 open scoped BigOperators
14 namespace RealizationBoundaries
15 
16 /-- Product of distinct prime divisors. Only positive multipliers enter root counts. -/
17 def primeRadical (m : ℕ) : ℕ := ∏ p ∈ m.primeFactors, p
18 
19 theorem primeRadical_pos (m : ℕ) : 0 < primeRadical m :=
20   Finset.prod_pos (fun _ hp => Nat.pos_of_mem_primeFactors hp)
21 
22 @[simp] theorem primeRadical_one : primeRadical 1 = 1 := by simp [primeRadical]
23 
24 @[simp] theorem primeRadical_prime {p : ℕ} (hp : p.Prime) : primeRadical p = p := by
25   simp [primeRadical, hp.primeFactors]
26 
27 /-- Repeated prime powers do not change the radical. -/
28 theorem primeRadical_pow (m : ℕ) {k : ℕ} (hk : k ≠ 0) :
29     primeRadical (m ^ k) = primeRadical m := by
30   simp only [primeRadical, Nat.primeFactors_pow m hk]
31 
32 theorem primeRadical_prime_pow {p k : ℕ} (hp : p.Prime) (hk : k ≠ 0) :
33     primeRadical (p ^ k) = p := by
34   rw [primeRadical_pow p hk, primeRadical_prime hp]
35 
36 theorem primeRadical_dvd (m : ℕ) : primeRadical m ∣ m := Nat.prod_primeFactors_dvd m
37 
38 theorem prime_dvd_radical_iff {m : ℕ} (hm : 0 < m) (p : Prime) :
39     p.val ∣ primeRadical m ↔ p.val ∣ m := by
40   constructor
41   · exact fun h => dvd_trans h (primeRadical_dvd m)
42   · intro h
43     exact Finset.dvd_prod_of_mem (fun n : ℕ => n)
44       (p.property.mem_primeFactors h (Nat.ne_of_gt hm))
45 
46 theorem primeRadical_dvd_of_dvd {m n : ℕ} (hn : 0 < n) (hmn : m ∣ n) :
47     primeRadical m ∣ primeRadical n :=
48   Finset.prod_dvd_prod_of_subset _ _ _ (Nat.primeFactors_mono hmn (Nat.ne_of_gt hn))
49 
50 /-- Relate the actual subtype of prime divisors to the printed radical. -/
51 theorem divisorPrime_prod {m : ℕ} (hm : 0 < m) [Fintype (DivisorPrime m)] :
52     (∏ p : DivisorPrime m, p.val.val) = primeRadical m := by
53   classical
54   apply Finset.prod_bij (fun (p : DivisorPrime m) _ => p.val.val)
55   · intro p _
56     exact p.val.property.mem_primeFactors p.property (Nat.ne_of_gt hm)
57   · intro p _ q _ h
58     exact Subtype.ext (Subtype.ext h)
59   · intro p hp
60     exact ⟨⟨⟨p, Nat.prime_of_mem_primeFactors hp⟩, Nat.dvd_of_mem_primeFactors hp⟩,
61       Finset.mem_univ _, rfl⟩
62   · intro p _
63     rfl
64 
65 /-- Cardinality of the finite divisor-coordinate product, with no counted roots assumed. -/
66 theorem divisorCoordinates_card {m : ℕ} (hm : 0 < m) :
67     Nat.card (DivisorCoordinates m) = primeRadical m := by
68   let : Finite (DivisorPrime m) := divisorPrime_finite hm
69   let := Fintype.ofFinite (DivisorPrime m)
70   change Nat.card ((p : DivisorPrime m) → Coordinate p.val) = _
71   rw [Nat.card_pi]
72   simp only [Nat.card_eq_fintype_card, ZMod.card]
73   exact divisorPrime_prod hm
74 
75 /-- The torsion kernel contains exactly one independent factor per distinct prime. -/
76 theorem rootKernel_card (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
77     Nat.card (rootKernel W m) = primeRadical m :=
78   (Nat.card_congr (rootKernelEquiv W hm).toEquiv).trans (divisorCoordinates_card hm)
79 
80 /-- A supplied actual root parameterizes all roots, including the m=1 singleton case. -/
81 theorem rootFiber_card_of_root (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
82     (x : preimage W) (y : RootFiber W m x) :
83     Nat.card (RootFiber W m x) = primeRadical m :=
84   (Nat.card_congr (rootFiberEquiv W hm x y)).trans (divisorCoordinates_card hm)
85 
86 theorem rootFiber_card_of_solvable (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
87     (x : preimage W) (h : ∃ y : preimage W, m • y = x) :
88     Nat.card (RootFiber W m x) = primeRadical m := by
89   obtain ⟨y, hy⟩ := h
90   exact rootFiber_card_of_root W hm x ⟨y, hy⟩
91 
92 theorem rootFiber_card_of_obstruction (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
93     (x : preimage W) (p : Prime) (hp : p.val ∣ m) (hx : x.val p ≠ 0) :
94     Nat.card (RootFiber W m x) = 0 := by
95   let := rootFiber_isEmpty W m x (prime_obstruction W hm x p hp hx)
96   exact Nat.card_of_isEmpty
97 
98 open scoped Classical in
99 /-- Exact case split: an empty fiber or a finite radical-sized fiber. -/
100 theorem rootFiber_card (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m)
101     (x : preimage W) :
102     Nat.card (RootFiber W m x) =
103       if ∀ p : Prime, p.val ∣ m → x.val p = 0 then primeRadical m else 0 := by
104   classical
105   split_ifs with h
106   · exact rootFiber_card_of_solvable W hm x ((preimage_root_iff W hm x).mpr h)
107   · let := rootFiber_isEmpty W m x (fun hy => h ((preimage_root_iff W hm x).mp hy))
108     exact Nat.card_of_isEmpty
109 
110 /-- Equality of actual multiple subgroups, not just matching quotient cardinalities. -/
111 theorem multiples_eq_radical (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
112     multiples W m = multiples W (primeRadical m) :=
113   multiples_eq_of_same_prime_divisors W hm (primeRadical_pos m)
114     (fun p => (prime_dvd_radical_iff hm p).symm)
115 
116 /-- The already-constructed quotient has the same exact cardinal as a nonempty root fiber. -/
117 theorem integerQuotient_card (W : Submodule ℚ TailSpace) {m : ℕ} (hm : 0 < m) :
118     Nat.card (preimage W ⧸ multiples W m) = primeRadical m :=
119   (Nat.card_congr (integerQuotientEquiv W hm).toEquiv).trans (divisorCoordinates_card hm)
120 
121 end RealizationBoundaries

Back to source controls