ReleaseSmithDVR.lean

1 import KomorebiVerification.PaperII.SmithDyadic
2 import Mathlib.RingTheory.DiscreteValuationRing.Basic
3 import Mathlib.RingTheory.Ideal.Norm.AbsNorm
4 
5 /-! Actual DVR quotient fibres, derived from ideal powers and their cardinalities. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace Komorebi.PaperII.SmithDVR
9 open IsLocalRing
10 universe u
11 variable {O : Type u} [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]
12 
13 def powerIdeal (pi : O) (L : Nat) : Ideal O := Ideal.span {pi ^ L}
14 abbrev QuotientAt (pi : O) (L : Nat) := O ⧸ powerIdeal pi L
15 
16 theorem powerIdeal_eq (pi : O) (hpi : Irreducible pi) (L : Nat) :
17     powerIdeal pi L = maximalIdeal O ^ L := by
18   rw [hpi.maximalIdeal_eq, Ideal.span_singleton_pow]
19   rfl
20 
21 /-- Cardinality follows from the ideal-power theorem, not a supplied coordinate certificate. -/
22 theorem quotientAt_card (pi : O) (hpi : Irreducible pi) (L : Nat) :
23     Nat.card (QuotientAt pi L) = Nat.card (ResidueField O) ^ L := by
24   have hp : maximalIdeal O ≠ ⊥ := by
25     rw [hpi.maximalIdeal_eq]
26     exact fun h => hpi.ne_zero (Ideal.span_singleton_eq_bot.mp h)
27   change Nat.card (O ⧸ powerIdeal pi L) = _
28   rw [powerIdeal_eq pi hpi]
29   exact cardQuot_pow_of_prime hp
30 
31 theorem quotientAt_finite [Finite (ResidueField O)]
32     (pi : O) (hpi : Irreducible pi) (L : Nat) : Finite (QuotientAt pi L) := by
33   apply Nat.finite_of_card_ne_zero
34   rw [quotientAt_card pi hpi]
35   exact pow_ne_zero _ (Nat.ne_of_gt Nat.card_pos)
36 
37 /-- Multiplication by the uniformizer power on the actual residue quotient. -/
38 def multiplyPower (pi : O) (s L : Nat) : QuotientAt pi L →ₗ[O] QuotientAt pi L where
39   toFun x := pi ^ s • x
40   map_add' x y := smul_add _ _ _
41   map_smul' c x := by
42     simp only [smul_smul, RingHom.id_apply]
43     rw [mul_comm]
44 
45 omit [IsDomain O] [IsDiscreteValuationRing O] in
46 @[simp] theorem multiplyPower_mk (pi : O) (s L : Nat) (x : O) :
47     multiplyPower pi s L ((powerIdeal pi L).mkQ x) =
48       (powerIdeal pi L).mkQ (pi ^ s * x) := rfl
49 
50 def baseMultiply (pi : O) (s L : Nat) : O →ₗ[O] QuotientAt pi L :=
51   (multiplyPower pi s L).comp (powerIdeal pi L).mkQ
52 
53 omit [IsDiscreteValuationRing O] in
54 theorem baseMultiply_ker (pi : O) (hpi : pi ≠ 0) (s L : Nat) (hs : s ≤ L) :
55     (baseMultiply pi s L).ker = powerIdeal pi (L - s) := by
56   ext x
57   change (powerIdeal pi L).mkQ (pi ^ s * x) = 0 ↔ x ∈ powerIdeal pi (L - s)
58   rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
59   change pi ^ s * x ∈ Ideal.span {pi ^ L} ↔ x ∈ Ideal.span {pi ^ (L - s)}
60   rw [Ideal.mem_span_singleton, Ideal.mem_span_singleton]
61   rw [show pi ^ L = pi ^ s * pi ^ (L - s) by rw [← pow_add, Nat.add_sub_of_le hs]]
62   exact mul_dvd_mul_iff_left (pow_ne_zero _ hpi)
63 
64 omit [IsDomain O] [IsDiscreteValuationRing O] in
65 theorem baseMultiply_range (pi : O) (s L : Nat) :
66     (baseMultiply pi s L).range = (multiplyPower pi s L).range := by
67   rw [baseMultiply, LinearMap.range_comp, Submodule.range_mkQ, Submodule.map_top]
68 
69 theorem multiplyPower_range_card (pi : O) (hpi : Irreducible pi)
70     (s L : Nat) (hs : s ≤ L) :
71     Nat.card (multiplyPower pi s L).range = Nat.card (ResidueField O) ^ (L - s) := by
72   rw [← baseMultiply_range]
73   rw [← Nat.card_congr (baseMultiply pi s L).quotKerEquivRange.toEquiv]
74   rw [baseMultiply_ker pi hpi.ne_zero s L hs]
75   exact quotientAt_card pi hpi (L - s)
76 
77 omit [IsDomain O] [IsDiscreteValuationRing O] in
78 theorem multiplyPower_zero (pi : O) (s L : Nat) (hs : L ≤ s) :
79     multiplyPower pi s L = 0 := by
80   apply LinearMap.ext
81   intro x
82   obtain ⟨a, rfl⟩ := (powerIdeal pi L).mkQ_surjective x
83   rw [multiplyPower_mk, LinearMap.zero_apply, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
84   apply Ideal.mem_span_singleton.mpr
85   exact dvd_mul_of_dvd_left (pow_dvd_pow pi hs) a
86 
87 /-- The true scalar kernel has the expected finite residue-field cardinality. -/
88 theorem multiplyPower_ker_card [Finite (ResidueField O)]
89     (pi : O) (hpi : Irreducible pi) (s L : Nat) :
90     Nat.card (multiplyPower pi s L).ker = Nat.card (ResidueField O) ^ min s L := by
91   rcases le_total s L with hs | hs
92   · rw [min_eq_left hs]
93     have hcard := Submodule.card_eq_card_quotient_mul_card (multiplyPower pi s L).ker
94     rw [Nat.card_congr (multiplyPower pi s L).quotKerEquivRange.toEquiv,
95       quotientAt_card pi hpi, multiplyPower_range_card pi hpi s L hs] at hcard
96     apply Nat.eq_of_mul_eq_mul_right (pow_pos (Nat.card_pos (α := ResidueField O)) (L - s))
97     rw [← hcard, ← pow_add, Nat.add_sub_of_le hs]
98   · rw [min_eq_right hs, multiplyPower_zero pi s L hs, LinearMap.ker_zero]
99     rw [Nat.card_congr (Submodule.topEquiv : (⊤ : Submodule O (QuotientAt pi L)) ≃ₗ[O]
100       QuotientAt pi L).toEquiv]
101     exact quotientAt_card pi hpi L
102 
103 abbrev ScalarFiber (pi : O) (s L : Nat) (b : O) :=
104   {x : QuotientAt pi L // multiplyPower pi s L x = (powerIdeal pi L).mkQ b}
105 
106 omit [IsDomain O] [IsDiscreteValuationRing O] in
107 /-- Exact scalar solvability, with divisibility of the actual integral target. -/
108 theorem scalarFiber_nonempty_iff (pi : O) (s L : Nat) (b : O) :
109     Nonempty (ScalarFiber pi s L b) ↔ pi ^ min s L ∣ b := by
110   constructor
111   · rintro ⟨⟨x, hx⟩⟩
112     obtain ⟨a, rfl⟩ := (powerIdeal pi L).mkQ_surjective x
113     rw [multiplyPower_mk] at hx
114     have hd : pi ^ L ∣ pi ^ s * a - b :=
115       Ideal.mem_span_singleton.mp ((Submodule.Quotient.eq _).mp hx)
116     have hsa : pi ^ min s L ∣ pi ^ s * a :=
117       dvd_mul_of_dvd_left (pow_dvd_pow pi (min_le_left s L)) a
118     have hdiff : pi ^ min s L ∣ pi ^ s * a - b :=
119       dvd_trans (pow_dvd_pow pi (min_le_right s L)) hd
120     simpa using dvd_sub hsa hdiff
121   · intro hb
122     rcases le_total s L with hs | hs
123     · rw [min_eq_left hs] at hb
124       obtain ⟨a, ha⟩ := hb
125       exact ⟨⟨(powerIdeal pi L).mkQ a, by rw [multiplyPower_mk, ← ha]⟩⟩
126     · rw [min_eq_right hs] at hb
127       have hb0 : (powerIdeal pi L).mkQ b = 0 :=
128         (Submodule.Quotient.mk_eq_zero _).mpr (Ideal.mem_span_singleton.mpr hb)
129       exact ⟨⟨0, by simp [hb0]⟩⟩
130 
131 /-- Inhabited actual scalar fibres have the kernel cardinality. -/
132 theorem scalarFiber_card [Finite (ResidueField O)]
133     (pi : O) (hpi : Irreducible pi) (s L : Nat) (b : O)
134     (hb : pi ^ min s L ∣ b) :
135     Nat.card (ScalarFiber pi s L b) = Nat.card (ResidueField O) ^ min s L := by
136   obtain ⟨⟨x, hx⟩⟩ := (scalarFiber_nonempty_iff pi s L b).mpr hb
137   let f := (multiplyPower pi s L).toAddMonoidHom
138   have he : ScalarFiber pi s L b ≃ f.ker := by
139     refine {
140       toFun := fun z => ⟨z.val - x, ?_⟩
141       invFun := fun k => ⟨k.val + x, ?_⟩
142       left_inv := fun z => Subtype.ext (sub_add_cancel z.val x)
143       right_inv := fun k => Subtype.ext (add_sub_cancel_right k.val x) }
144     · change (multiplyPower pi s L) (z.val - x) = 0
145       rw [map_sub, z.property, hx, sub_self]
146     · rw [map_add, show (multiplyPower pi s L) k.val = 0 from k.property, zero_add, hx]
147   rw [Nat.card_congr he]
148   exact multiplyPower_ker_card pi hpi s L
149 
150 end Komorebi.PaperII.SmithDVR
151 #print axioms Komorebi.PaperII.SmithDVR.quotientAt_card
152 #print axioms Komorebi.PaperII.SmithDVR.scalarFiber_nonempty_iff
153 #print axioms Komorebi.PaperII.SmithDVR.scalarFiber_card

Back to source controls