The étale monic density in algebra language

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 Mathlib.RingTheory.Etale.StandardEtale7import SurfaceBlowup.Etale.Main8 9/-!10# The étale monic density in algebra language11 12The étale-convention monic density, with the event phrased through algebras: the `K`-algebra13`K[X]/(f_a)` is étale (`Algebra.Etale`) and the `O`-algebra `O[X]/(f_a)` has algebra type `σ`14(`HasAlgebraType`: its generic fibre is a product of fields with the invariants `σ`).15 16## Main results17 18* `SurfaceBlowup.etale_adjoinRoot_of_separable`19* `SurfaceBlowup.etaleMonicDensity_eq_algebraType`20-/21 22open MeasureTheory Polynomial23open scoped ENNReal24 25namespace SurfaceBlowup26 27/-- For a monic separable polynomial `f` over a field `K`, the algebra `K[X]/(f)` is étale. -/28theorem etale_adjoinRoot_of_separable {K : Type} [Field K] (f : K[X]) (hm : f.Monic)29    (hs : f.Separable) : Algebra.Etale K (AdjoinRoot f) := by30  obtain ⟨u, v, huv⟩ := hs31  let P : StandardEtalePair K := ⟨f, hm, 1, ⟨v, u, 0, by rw [pow_zero, ← huv]; ring⟩⟩32  have hu : IsUnit (AdjoinRoot.mk f (1 : K[X])) := by rw [map_one]; exact isUnit_one33  exact Algebra.Etale.of_equiv (P.equivAwayAdjoinRoot.trans34    ((IsLocalization.atUnit (AdjoinRoot f) (Localization.Away (AdjoinRoot.mk f 1)) _35      hu).symm.restrictScalars K))36 37/-- The étale monic density, with the event "the algebra `K[X]/(f_a)` is étale and `O[X]/(f_a)`38has algebra type `σ`". -/39theorem etaleMonicDensity_eq_algebraType (O : Type) [CommRing O] [IsDomain O]Remark 1.340    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]41    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]42    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]43    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (σ : FactorType) :44    etaleMonicDensity O n σ = coefficientMeasure O n45      {a | Algebra.Etale (BaseField O) (AdjoinRoot (monicPolynomial O a)) ∧46        HasAlgebraType O (AdjoinRoot (monicPolyO a)) σ} := by47  refine measure_congr <| (measure_eq_zero_iff_ae_notMem.1 (monic_inseparable_null O htop n)).mono48    fun a ha => ?_49  have hs : (monicPolynomial O a).Separable := not_not.1 ha50  have hm := (monic_poly_reconstruct O n a).151  have ht : HasAlgebraType O (AdjoinRoot (monicPolyO a)) σ ↔52      HasPolynomialType O (monicPolynomial O a) σ := by53    rw [← polynomial_type_iff_algebra_type O _ hm, monicPolyO_map_fraction]54    exact hasPolynomialTypeF_iff_of_separable O hs55  refine propext ⟨fun h => ⟨etale_adjoinRoot_of_separable _56    (monic_polynomial_degree O n a).1 hs, ht.2 h.2⟩, fun h => ⟨hs, ht.1 h.2⟩⟩57 58end SurfaceBlowup