Counting.lean

1 import Mathlib.RingTheory.Ideal.Norm.AbsNorm
2 import Mathlib.RingTheory.DiscreteValuationRing.Basic
3 import Mathlib.Data.Fintype.Pi
4 import Mathlib.Tactic
5 
6 /-!
7 Actual finite ideal-quotient coordinates, not counts defined to equal a power.
8 The result works for any nonzero prime ideal of a Dedekind domain with finite
9 residue ring. In a DVR it applies to the maximal ideal. The additional passage
10 from continuous maps out of a formal power-series ring to parameter tuples is
11 kept separate from this finite ideal-chart counting theorem.
12 -/
13 set_option autoImplicit false
14 namespace PaperX.Counting
15 
16 variable {O : Type*} [CommRing O] [IsDedekindDomain O]
17 variable (P : Ideal O) [P.IsPrime] (hP : P ≠ ⊥) [Finite (O ⧸ P)]
18 
19 /-- The actual image of P^w inside O/P^m. -/
20 def Coordinate (m w : ℕ) := ↥(Submodule.map (P ^ m).mkQ (P ^ w))
21 
22 noncomputable def residueCard : ℕ := Nat.card (O ⧸ P)
23 
24 include hP
25 
26 omit [Finite (O ⧸ P)] in
27 theorem quotient_count (m : ℕ) : Nat.card (O ⧸ P ^ m) = residueCard P ^ m := by
28   exact cardQuot_pow_of_prime hP
29 
30 /-- The dimension-one ideal chart, including the invisible range m <= w. -/
31 theorem coordinate_count (m w : ℕ) :
32     Nat.card (Coordinate P m w) = residueCard P ^ (m - w) := by
33   by_cases hwm : w ≤ m
34   · have h := Submodule.card_quotient_mul_card_quotient
35       (P ^ w) (P ^ m) (Ideal.pow_le_pow_right hwm)
36     change Nat.card (Coordinate P m w) * Nat.card (O ⧸ P ^ w) =
37       Nat.card (O ⧸ P ^ m) at h
38     rw [quotient_count P hP w, quotient_count P hP m] at h
39     have hp : residueCard P ^ w ≠ 0 := by
40       exact pow_ne_zero w (show residueCard P ≠ 0 from Nat.card_pos.ne')
41     apply Nat.mul_right_cancel (m := residueCard P ^ w)
42     · exact Nat.pos_of_ne_zero hp
43     · rw [h, ← pow_add, Nat.sub_add_cancel hwm]
44   · have hle : P ^ w ≤ P ^ m := Ideal.pow_le_pow_right (by omega)
45     have hz : Submodule.map (P ^ m).mkQ (P ^ w) = ⊥ := by
46       apply le_antisymm _ bot_le
47       rw [Submodule.map_le_iff_le_comap, Submodule.comap_bot, Submodule.ker_mkQ]
48       exact hle
49     simp [Coordinate, hz, Nat.sub_eq_zero_of_le (by omega : m ≤ w)]
50 
51 /-- A weighted chart is a tuple of independently constrained quotient elements. -/
52 def WeightedChart {d : ℕ} (w : Fin d → ℕ) (m : ℕ) :=
53   (i : Fin d) → Coordinate P m (w i)
54 
55 /-- Exact weighted smooth-chart cardinality, for actual ideal quotients. -/
56 theorem weighted_chart_count {d : ℕ} (w : Fin d → ℕ) (m : ℕ) :
57     Nat.card (WeightedChart P w m) = residueCard P ^ (∑ i, (m - w i)) := by
58   change Nat.card ((i : Fin d) → Coordinate P m (w i)) = _
59   rw [Nat.card_pi]
60   simp_rw [coordinate_count P hP]
61   exact (Finset.prod_pow_eq_pow_sum Finset.univ (fun i => m - w i) (residueCard P))
62 
63 /-- Smooth d-dimensional positive-depth coordinates are the all-weight-one chart. -/
64 theorem smooth_chart_count (d m : ℕ) :
65     Nat.card (WeightedChart P (fun _ : Fin d => 1) m) =
66       residueCard P ^ (d * (m - 1)) := by
67   rw [weighted_chart_count P hP]
68   simp
69 
70 /-- Written with max as in the manuscript; Nat subtraction is already truncated. -/
71 theorem weighted_chart_count_max {d : ℕ} (w : Fin d → ℕ) (m : ℕ) :
72     Nat.card (WeightedChart P w m) =
73       residueCard P ^ (∑ i, max (m - w i) 0) := by
74   simpa using weighted_chart_count P hP w m
75 
76 /-- Any independently established chart equivalence transfers this cardinality. -/
77 theorem count_via_chart {X : Type*} {d : ℕ} (w : Fin d → ℕ) (m : ℕ)
78     (e : X ≃ WeightedChart P w m) :
79     Nat.card X = residueCard P ^ (∑ i, (m - w i)) := by
80   rw [Nat.card_congr e]
81   exact weighted_chart_count P hP w m
82 
83 end PaperX.Counting

Back to source controls