Singular.lean

1 import PaperX.Counting
2 import Mathlib.Algebra.Order.Floor.Div
3 
4 /-!
5 Exact solutions to x^e = 0 in a DVR quotient. The count is derived by an
6 explicit equivalence with an ideal image; it is not stipulated as a model.
7 The exponent e is required to be positive.
8 -/
9 set_option autoImplicit false
10 namespace PaperX.Singular
11 open IsLocalRing IsDiscreteValuationRing
12 
13 variable {O : Type*} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
14 
15 /-- Membership in a maximal-ideal power is measured by the actual DVR valuation. -/
16 theorem mem_power_iff (x : O) (m : ℕ) :
17     x ∈ maximalIdeal O ^ m ↔ (m : ℕ∞) ≤ addVal O x := by
18   obtain ⟨p, hp⟩ := exists_irreducible O
19   rw [hp.maximalIdeal_eq, Ideal.span_singleton_pow, Ideal.mem_span_singleton,
20     ← addVal_le_iff_dvd, hp.addVal_pow]
21 
22 /-- The ceiling threshold is at most m for every positive exponent. -/
23 theorem ceil_threshold_le (m e : ℕ) (he : 0 < e) : m ⌈/⌉ e ≤ m := by
24   apply (ceilDiv_le_iff_le_mul he).mpr
25   nlinarith
26 
27 /-- The exact valuation threshold, including the zero representative. -/
28 theorem power_mem_iff (x : O) (m e : ℕ) (he : 0 < e) :
29     x ^ e ∈ maximalIdeal O ^ m ↔ x ∈ maximalIdeal O ^ (m ⌈/⌉ e) := by
30   by_cases hx : x = 0
31   · simp [hx, Nat.ne_of_gt he]
32   · obtain ⟨p, hp⟩ := exists_irreducible O
33     obtain ⟨n, u, hu⟩ := eq_unit_mul_pow_irreducible hx hp
34     rw [mem_power_iff, mem_power_iff, addVal_pow, hu, addVal_def' u hp n]
35     simp only [nsmul_eq_mul, ← Nat.cast_mul, ENat.natCast_le_natCast]
36     exact (ceilDiv_le_iff_le_mul he).symm
37 
38 /-- Actual roots in the quotient ring. -/
39 def Roots (m e : ℕ) := {x : O ⧸ maximalIdeal O ^ m // x ^ e = 0}
40 
41 /-- For quotient representatives, the root condition equals an ideal-image condition. -/
42 theorem root_iff_coordinate (m e : ℕ) (he : 0 < e)
43     (x : O ⧸ maximalIdeal O ^ m) :
44     x ^ e = 0 ↔ x ∈ Submodule.map (maximalIdeal O ^ m).mkQ
45       (maximalIdeal O ^ (m ⌈/⌉ e)) := by
46   obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective x
47   rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem, power_mem_iff a m e he]
48   change a ∈ maximalIdeal O ^ (m ⌈/⌉ e) ↔
49     a ∈ Submodule.comap (maximalIdeal O ^ m).mkQ
50       (Submodule.map (maximalIdeal O ^ m).mkQ (maximalIdeal O ^ (m ⌈/⌉ e)))
51   rw [Submodule.comap_map_eq, Submodule.ker_mkQ,
52     sup_eq_left.mpr (Ideal.pow_le_pow_right (ceil_threshold_le m e he))]
53 
54 /-- The identity on the ambient quotient restricts to this exact equivalence. -/
55 noncomputable def rootsEquivCoordinate (m e : ℕ) (he : 0 < e) :
56     Roots (O := O) m e ≃ PaperX.Counting.Coordinate (maximalIdeal O) m (m ⌈/⌉ e) :=
57   Equiv.subtypeEquivRight (root_iff_coordinate m e he)
58 
59 /-- Exact singular-power count over every DVR with finite residue field. -/
60 theorem singular_root_count [Finite (O ⧸ maximalIdeal O)] (m e : ℕ) (he : 0 < e) :
61     Nat.card (Roots (O := O) m e) =
62       Nat.card (O ⧸ maximalIdeal O) ^ (m - (m ⌈/⌉ e)) := by
63   rw [Nat.card_congr (rootsEquivCoordinate (O := O) m e he)]
64   exact PaperX.Counting.coordinate_count (maximalIdeal O) (not_a_field O) m (m ⌈/⌉ e)
65 
66 omit [IsDiscreteValuationRing O] in
67 /-- The increasing finite counts do not imply several roots in the complete DVR. -/
68 theorem only_zero_integral_root (x : O) (e : ℕ) (he : 0 < e) : x ^ e = 0 ↔ x = 0 := by
69   exact pow_eq_zero_iff (Nat.ne_of_gt he)
70 
71 /-- If an integral value is a root at every precision, it is zero. -/
72 theorem compatible_integral_root_zero (x : O) (e : ℕ) (he : 0 < e)
73     (h : ∀ m, Ideal.Quotient.mk (maximalIdeal O ^ m) x ^ e = 0) : x = 0 := by
74   have hz : x ^ e = 0 := by
75     apply (IsHausdorff.eq_iff_smodEq (I := maximalIdeal O)).mpr
76     intro m
77     simpa only [SModEq.zero, Ideal.smul_eq_mul, Ideal.mul_top] using
78       (Ideal.Quotient.eq_zero_iff_mem.mp (by simpa only [map_pow] using h m))
79   exact (only_zero_integral_root x e he).mp hz
80 
81 /-- An entire compatible root tower is the zero tower. No completeness assumption
82 is needed: a root at depth e*m already reduces to zero at depth m. -/
83 theorem compatible_root_family_zero (e : ℕ) (he : 0 < e)
84     (x : (m : ℕ) → O ⧸ maximalIdeal O ^ m)
85     (hcompat : ∀ {m n : ℕ} (h : m ≤ n),
86       Ideal.Quotient.factorPow (maximalIdeal O) h (x n) = x m)
87     (hroot : ∀ m, x m ^ e = 0) : ∀ m, x m = 0 := by
88   intro m
89   have hm : m ≤ e*m := by nlinarith
90   obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (x (e*m))
91   have hmem : y ^ e ∈ maximalIdeal O ^ (e*m) := by
92     apply Ideal.Quotient.eq_zero_iff_mem.mp
93     simpa only [map_pow, hy] using hroot (e*m)
94   have hdepth := (power_mem_iff y (e*m) e he).mp hmem
95   have hceil : (e*m) ⌈/⌉ e = m := smul_ceilDiv he m
96   rw [hceil] at hdepth
97   rw [← hcompat hm, ← hy]
98   change Ideal.Quotient.mk (maximalIdeal O ^ m) y = 0
99   exact Ideal.Quotient.eq_zero_iff_mem.mpr hdepth
100 
101 end PaperX.Singular

Back to source controls