The étale convention agrees with the published densities

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.Etale.Defs7import SurfaceBlowup.Main8 9/-!10# The étale convention agrees with the published densities11 12The two conventions for the type of a polynomial (finite integral closures versus étale algebras)13agree off a Haar-null set (paper, Remark 1.3). Formally: the non-étale binary forms are null, the14published densities equal the étale-convention densities, and hence Theorem 1.1 holds verbatim15under the étale convention.16 17## Main results18 19* `SurfaceBlowup.binary_nonEtale_null`20* `SurfaceBlowup.monicDensity_eq_etale`, `SurfaceBlowup.projectiveDensity_eq_etale`21* `SurfaceBlowup.main_dvr_etale`22-/23 24open MeasureTheory Polynomial25open scoped ENNReal26 27namespace SurfaceBlowup28 29section EtaleBridge30 31variable (O : Type) [CommRing O] [IsDomain O]32 33omit [IsDomain O] in34/-- The coefficient of `X^n` in `F_a(X,1)` is `a_n`. -/35theorem affinePolynomial_coeff_last {n : ℕ} (a : Fin (n + 1) → O) :36    (affinePolynomial O a).coeff n = algebraMap O (BaseField O) (a (Fin.last n)) := by37  simp only [affinePolynomial, Polynomial.finsetSum_coeff, Polynomial.coeff_C_mul_X_pow]38  rw [Finset.sum_eq_single (Fin.last n)]39  · simp40  · exact fun i _ hi => if_neg fun h => hi (Fin.ext (by simp [h]))41  · simp42 43omit [IsDomain O] in44/-- If `a_n ≠ 0` then `F_a(X,1)` is nonzero of degree exactly `n`. -/45theorem affinePolynomial_natDegree_of_last {n : ℕ} (a : Fin (n + 1) → O)46    (ha : a (Fin.last n) ≠ 0) :47    affinePolynomial O a ≠ 0 ∧ (affinePolynomial O a).natDegree = n := by48  have hc : (affinePolynomial O a).coeff n ≠ 0 := by49    rw [affinePolynomial_coeff_last]50    exact fun h => ha (IsFractionRing.injective O (BaseField O) (by rw [h, map_zero]))51  refine ⟨fun h => hc (by rw [h, Polynomial.coeff_zero]), ?_⟩52  apply Polynomial.natDegree_eq_of_le_of_coeff_ne_zero _ hc53  exact Polynomial.natDegree_sum_le_of_forall_le _ _ fun i _ =>54    (Polynomial.natDegree_C_mul_X_pow_le _ _).trans (Nat.lt_succ_iff.1 i.2)55 56omit [IsDomain O] in57/-- Appending the coefficient `1` turns `F_a(X,1)` into the monic polynomial with coefficients `a`.58-/59theorem affinePolynomial_snoc_one {n : ℕ} (a : Fin n → O) :60    affinePolynomial O (Fin.snoc (α := fun _ => O) a 1) = monicPolynomial O a := by61  simp [affinePolynomial, monicPolynomial, Fin.sum_univ_castSucc, add_comm]62 63/-- Off `{a_n = 0} ∪ {disc = 0}` the binary form `F_a` is étale. -/64theorem isEtaleForm_of_good {n : ℕ} (a : Fin (n + 1) → O) (ha : a (Fin.last n) ≠ 0)65    (hd : MvPolynomial.eval a (MvPolynomial.map (Int.castRingHom O) (discAffine n)) ≠ 0) :66    IsEtaleForm O a := by67  obtain ⟨h0, hdeg⟩ := affinePolynomial_natDegree_of_last O a ha68  refine ⟨h0, by omega, separable_of_resultant _ n hdeg h0 ?_⟩69  rw [affine_resultant_eq]70  exact fun h => hd (IsFractionRing.injective O (BaseField O) (by rw [h, map_zero]))71 72variable [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]73  [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]74  [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]75 76/-- The locus `{a_n = 0} ∪ {disc = 0}` is Haar-null. -/77theorem affine_degenerate_null (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) :78    coefficientMeasure O (n+1) ({a : Fin (n+1) → O | a (Fin.last n) = 0} ∪79      {a | MvPolynomial.eval a (MvPolynomial.map (Int.castRingHom O) (discAffine n)) = 0}) =80      0 := by81  refine measure_union_null (coordinate_hyperplane_null O htop (n+1) (Fin.last n)).2 ?_82  obtain ⟨a₀, h₀⟩ := exists_separable_monic O n83  refine coefficientMeasure_zero_null O htop (n+1) _ (Fin.snoc (α := fun _ => O) a₀ 1) ?_84  have hdeg := monic_polynomial_degree O n a₀85  have := resultant_ne_zero_of_separable (monicPolynomial O a₀) n hdeg.2 hdeg.1.ne_zero h₀86  rw [← affinePolynomial_snoc_one, affine_resultant_eq] at this87  exact fun h => this (by rw [h, map_zero])88 89end EtaleBridge90 91/-- The non-étale binary forms are Haar-null. -/92theorem binary_nonEtale_null (O : Type) [CommRing O] [IsDomain O]Remark 1.393    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]94    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]95    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]96    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) :97    coefficientMeasure O (n+1) {a | ¬ IsEtaleForm O a} = 0 := by98  refine measure_mono_null (fun a ha => ?_) (affine_degenerate_null O htop n)99  by_contra hne100  simp only [Set.mem_union, Set.mem_ofPred_eq, not_or] at hne101  exact ha (isEtaleForm_of_good O a hne.1 hne.2)102 103/-- The published monic density equals the étale-convention density (Remark 1.3). -/104theorem monicDensity_eq_etale (O : Type) [CommRing O] [IsDomain O]Remark 1.3105    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]106    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]107    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]108    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (σ : FactorType) :109    monicDensity O n σ = etaleMonicDensity O n σ :=110  measure_congr <| (measure_eq_zero_iff_ae_notMem.1 (monic_inseparable_null O htop n)).mono111    fun _ ha => propext ⟨fun h => ⟨not_not.1 ha, h⟩, fun h => h.2⟩112 113/-- The published projective density equals the étale-convention density (Remark 1.3). -/114theorem projectiveDensity_eq_etale (O : Type) [CommRing O] [IsDomain O]Remark 1.3115    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]116    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]117    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]118    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (σ : FactorType) :119    projectiveDensity O n σ = etaleProjectiveDensity O n σ :=120  congrArg (· / _) <| measure_congr <|121    (measure_eq_zero_iff_ae_notMem.1 (binary_nonEtale_null O htop n)).mono fun _ ha =>122      propext <| and_congr_right fun _ =>123        ⟨fun h => ⟨not_not.1 ha, h⟩, fun h => h.2⟩124 125/-- Theorem 1.1 under the étale convention: the monic and projective laws, with the events126restricted to étale algebras, are the universal rational functions. -/127theorem main_dvr_etale (O : Type) [CommRing O] [IsDomain O]Theorem 1.1Remark 1.3128    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]129    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]130    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]131    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (σ : FactorType) :132    etaleMonicDensity O n σ =133        densityValue (monicExpr n σ) (Nat.card (IsLocalRing.ResidueField O)) ∧134    etaleProjectiveDensity O n σ =135        densityValue (projectiveExpr n σ) (Nat.card (IsLocalRing.ResidueField O)) := by136  rw [← monicDensity_eq_etale O htop, ← projectiveDensity_eq_etale O htop]137  exact main_dvr O htop n σ138 139end SurfaceBlowup