Counting over finite fields

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Surfaces.PowerSeries7 8/-!9# Counting over finite fields10 11Elementary counts: the number of monic irreducible polynomials of degree `δ` over a finite field12is the point-count polynomial at `#k`; the cardinality of a finite field is a prime power; and a13module of length `ℓ` over a local ring with finite residue field `k` has `|k|^ℓ` elements.14 15## Main results16 17* `SurfaceBlowup.finite_field_irreducible_count`18* `SurfaceBlowup.finite_field_card_primePower`19* `SurfaceBlowup.finite_length_module_card`20 21Provenance: `Thm_SurfaceBlowupV2_{finite_field_irreducible_count, finite_field_card_primePower,22finite_length_module_card}` (moved from `Unramified/LocalDescent.lean` and23`Blowup/CurveOrders.lean`).24-/25 26namespace SurfaceBlowup27 28/-- The number of monic irreducible polynomials of degree `δ > 0` over a finite field `k` is the29value of the point-count polynomial `pointCount δ` at `#k`. -/30theorem finite_field_irreducible_count (k : Type) [Field k] [Finite k] (δ : ℕ) (hδ : 0 < δ) :(6.2)31    ((Nat.card {g : Polynomial k // g.Monic ∧ Irreducible g32      ∧ g.natDegree = δ} : ℕ) : ℚ) = (pointCount δ).eval (Nat.card k) := by33  rw [pointCount_eval, ← irreducible_count_moebius k δ hδ]34  have : (δ : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr hδ.ne'35  field_simp36 37/-- The cardinality of a finite field is a prime power. -/38theorem finite_field_card_primePower (K : Type) [Field K] [Finite K] :39    PrimePower (Nat.card K) := by40  have : Fintype K := Fintype.ofFinite K41  obtain ⟨p, -, n, hp, hcard⟩ := FiniteField.card' K42  exact ⟨p, n, hp, n.pos, by rw [Nat.card_eq_fintype_card, hcard]⟩43 44/-- A module of length `ℓ` over a local ring with finite residue field `k` has `|k|^ℓ`45elements. -/46theorem finite_length_module_card (O : Type) [CommRing O] [IsLocalRing O]47    [Finite (IsLocalRing.ResidueField O)] (M : Type) [AddCommGroup M] [Module O M] (ℓ : ℕ)48    (hℓ : Module.length O M = ℓ) :49    Nat.card M = (Nat.card (IsLocalRing.ResidueField O))^ℓ := by50  induction ℓ generalizing M with51  | zero =>52    have : Subsingleton M := Module.length_eq_zero_iff.mp (by simpa using hℓ)53    simp54  | succ n ih =>55    have hfin : IsFiniteLength O M := Module.length_ne_top_iff.mp56        (by rw [hℓ]; exact ENat.natCast_ne_top _)57    have hA : IsArtinian O M := (isFiniteLength_iff_isNoetherian_isArtinian.mp hfin).258    have hnt : Nontrivial M := Module.length_pos_iff.mp (by rw [hℓ]; exact_mod_cast Nat.succ_pos n)59    have : IsAtomic (Submodule O M) := isAtomic_of_orderBot_wellFounded_lt wellFounded_lt60    obtain ⟨N, hN, -⟩ := (eq_bot_or_exists_atom_le (⊤ : Submodule O M)).resolve_left top_ne_bot61    have hS : IsSimpleModule O N := isSimpleModule_iff_isAtom.mpr hN62    obtain ⟨I, hI, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp hS63    have hIm : I = IsLocalRing.maximalIdeal O := IsLocalRing.eq_maximalIdeal hI64    subst hIm65    have hcardN : Nat.card N = Nat.card (IsLocalRing.ResidueField O) := Nat.card_congr e.toEquiv66    have hlen := Module.length_eq_add_of_exact N.subtype N.mkQ N.injective_subtype67      N.mkQ_surjective (LinearMap.exact_subtype_mkQ N)68    rw [Module.length_eq_one O N, hℓ] at hlen69    have hQ : Module.length O (M ⧸ N) = n := by70      have : ((n : ℕ∞) + 1) = 1 + Module.length O (M ⧸ N) := by exact_mod_cast hlen71      have h2 : ((n : ℕ∞) + 1) = Module.length O (M ⧸ N) + 1 := by rw [this, add_comm]72      exact (ENat.add_left_injective_of_ne_top ENat.one_ne_top h2).symm73    have := ih (M ⧸ N) hQ74    rw [AddSubgroup.card_eq_card_quotient_mul_card_addSubgroup N.toAddSubgroup]75    change Nat.card (M ⧸ N) * Nat.card N = _76    rw [this, hcardN, pow_succ]77 78end SurfaceBlowup