Non-vacuity of the hypotheses of `main_dvr`

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.Main7import Mathlib.RingTheory.PowerSeries.PiTopology8import Mathlib.RingTheory.AdicCompletion.Completeness9import Mathlib.FieldTheory.Finite.GaloisField10import Mathlib.Data.Finsupp.Encodable11import Mathlib.Topology.Connected.Separation12import Mathlib.Topology.Instances.ZMod13import Mathlib.Topology.Separation.Lemmas14 15/-!16# Non-vacuity of the hypotheses of `main_dvr`17 18The hypotheses of `SurfaceBlowup.main_dvr` are satisfiable in equal characteristic: for a finite19field `k` with the discrete topology, the power series ring `k⟦X⟧` with Mathlib's coefficientwise20(pi) topology is a complete discrete valuation ring with finite residue field `k`, a compact21Hausdorff second-countable topological ring whose topology is the `(X)`-adic one. Equipping it with22the Borel σ-algebra, `main_dvr` applies and gives the type densities of polynomials over `𝔽_q⟦X⟧`.23 24## Main results25 26* `SurfaceBlowup.Tests.isAdic_maximalIdeal_powerSeries`: the pi topology on `k⟦X⟧` is `(X)`-adic.27* `SurfaceBlowup.Tests.main_dvr_powerSeries`: `main_dvr` for `k⟦X⟧`, with `q = |k|`.28* `SurfaceBlowup.Tests.main_dvr_zmod`, `SurfaceBlowup.Tests.main_dvr_galoisField`: the explicit29  cases `𝔽_p⟦X⟧` (`q = p`) and `𝔽_{p^m}⟦X⟧` (`q = p^m`).30 31Provenance: port of the independent certificate `Monolith/NonVacuityExample.lean` (monolith_gen).32-/33 34open PowerSeries IsLocalRing Topology Filter35open scoped PowerSeries.WithPiTopology36 37namespace SurfaceBlowup.Tests38 39section FiniteField40 41variable (k : Type) [Field k] [TopologicalSpace k] [DiscreteTopology k]42 43/-- `k⟦X⟧` is complete for its maximal ideal `(X)`. -/44instance : IsAdicComplete (maximalIdeal k⟦X⟧) k⟦X⟧ := by45  rw [PowerSeries.maximalIdeal_eq_span_X]; infer_instance46 47/-- The residue field of `k⟦X⟧` is `k`, hence finite when `k` is. -/48instance [Finite k] : Finite (ResidueField k⟦X⟧) :=49  .of_equiv k (residueFieldOfPowerSeries (k := k)).symm.toEquiv50 51/-- Tychonoff: `k⟦X⟧ = k^ℕ` is compact for finite discrete `k`. -/52instance [Finite k] : CompactSpace k⟦X⟧ := inferInstanceAs (CompactSpace ((Unit →₀ ℕ) → k))53 54/-- A countable product of finite discrete spaces is second countable. -/55instance [Finite k] : SecondCountableTopology k⟦X⟧ :=56  inferInstanceAs (SecondCountableTopology ((Unit →₀ ℕ) → k))57 58/-- The Borel σ-algebra on `k⟦X⟧`. -/59instance : MeasurableSpace k⟦X⟧ := borel _60 61/-- The Borel σ-algebra makes `k⟦X⟧` a Borel space. -/62instance : BorelSpace k⟦X⟧ := ⟨rfl⟩63 64omit [TopologicalSpace k] [DiscreteTopology k] in65private theorem mem_span_X_pow_iff (n : ℕ) (φ : k⟦X⟧) :66    φ ∈ Ideal.span {(X : k⟦X⟧)} ^ n ↔ ∀ m < n, coeff m φ = 0 := by67  rw [Ideal.span_singleton_pow, Ideal.mem_span_singleton, X_pow_dvd_iff]68 69/-- The pi topology on `k⟦X⟧` is the `(X)`-adic topology. -/70theorem isAdic_maximalIdeal_powerSeries : IsAdic (maximalIdeal k⟦X⟧) := by71  rw [PowerSeries.maximalIdeal_eq_span_X, isAdic_iff]72  refine ⟨fun n ↦ ?_, fun s hs ↦ ?_⟩73  · have : ((Ideal.span {(X : k⟦X⟧)} ^ n : Ideal k⟦X⟧) : Set k⟦X⟧) =74        ⋂ m ∈ Finset.range n, coeff (R := k) m ⁻¹' {0} := by75      ext φ; simp [mem_span_X_pow_iff]76    rw [this]77    exact isOpen_biInter_finset fun m _ ↦78      (WithPiTopology.continuous_coeff k m).isOpen_preimage _ (isOpen_discrete _)79  · have hs' : s ∈ Filter.pi fun _ : Unit →₀ ℕ ↦ 𝓝 (0 : k) := by80      rw [← nhds_pi]; exact hs81    obtain ⟨I, hI, t, ht, hIt⟩ := Filter.mem_pi.mp hs'82    refine ⟨hI.toFinset.sup (fun d ↦ d ()) + 1, fun φ hφ ↦ hIt (Set.mem_pi.mpr fun d hd ↦ ?_)⟩83    have h0 : (0 : k) ∈ t d := mem_pure.mp (nhds_discrete k ▸ ht d)84    have hcoef : coeff (d ()) φ = 0 := (mem_span_X_pow_iff k _ φ).mp hφ _85      (Nat.lt_succ_of_le (Finset.le_sup (f := fun d : Unit →₀ ℕ ↦ d ()) (hI.mem_toFinset.mpr hd)))86    have hφd : φ d = coeff (d ()) φ := by rw [coeff_def rfl]; rfl87    change φ d ∈ t d88    rwa [hφd, hcoef]89 90/-- `main_dvr` instantiated at `O = k⟦X⟧` for a finite field `k` with the discrete topology: the91type densities of monic polynomials and primitive binary forms over `k⟦X⟧` are the universal92expressions evaluated at `q = |k|`. -/93theorem main_dvr_powerSeries [Finite k] (n : ℕ) (σ : FactorType) :Theorem 1.194    monicDensity k⟦X⟧ n σ = densityValue (monicExpr n σ) (Nat.card k) ∧95      projectiveDensity k⟦X⟧ n σ = densityValue (projectiveExpr n σ) (Nat.card k) := by96  rw [← Nat.card_congr (residueFieldOfPowerSeries (k := k)).toEquiv]97  exact main_dvr k⟦X⟧ (isAdic_maximalIdeal_powerSeries k) n σ98 99end FiniteField100 101section Concrete102 103/-- The discrete topology on `GaloisField p m`. -/104instance (p m : ℕ) [Fact p.Prime] : TopologicalSpace (GaloisField p m) := ⊥105 106/-- The topology `⊥` on `GaloisField p m` is discrete. -/107instance (p m : ℕ) [Fact p.Prime] : DiscreteTopology (GaloisField p m) := ⟨rfl⟩108 109/-- Densities over `𝔽_p⟦X⟧`: the universal expressions evaluated at `q = p`. -/110theorem main_dvr_zmod (p : ℕ) [hp : Fact p.Prime] (n : ℕ) (σ : FactorType) :111    monicDensity (ZMod p)⟦X⟧ n σ = densityValue (monicExpr n σ) p ∧112      projectiveDensity (ZMod p)⟦X⟧ n σ = densityValue (projectiveExpr n σ) p := by113  simpa using main_dvr_powerSeries (ZMod p) n σ114 115/-- Densities over `𝔽_{p^m}⟦X⟧` (`GaloisField p m`, `m ≠ 0`): the universal expressions evaluated116at `q = p^m`. -/117theorem main_dvr_galoisField (p : ℕ) [Fact p.Prime] (m : ℕ) (hm : m ≠ 0) (n : ℕ)118    (σ : FactorType) :119    monicDensity (GaloisField p m)⟦X⟧ n σ = densityValue (monicExpr n σ) (p ^ m) ∧120      projectiveDensity (GaloisField p m)⟦X⟧ n σ = densityValue (projectiveExpr n σ) (p ^ m) := by121  simpa [GaloisField.card p m hm] using main_dvr_powerSeries (GaloisField p m) n σ122 123end Concrete124 125end SurfaceBlowup.Tests126 127#print axioms SurfaceBlowup.Tests.main_dvr_zmod128#print axioms SurfaceBlowup.Tests.main_dvr_galoisField