The primitive locus, state measures, and integral closures

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.Algebra.AlgebraType7import SurfaceBlowup.Unramified.Extension8import Mathlib.Algebra.GroupWithZero.Submonoid.CancelMulZero9import Mathlib.Algebra.Module.StablyFree.Basic10import Mathlib.NumberTheory.Padics.RingHoms11 12/-!13# The primitive locus, state measures, and integral closures14 15Mass computations for the coefficient measure (the primitive locus of `O^(n+1)`, total masses of16state measures, the Haar property of the unramified coefficient measure), lifting lemmas for17generators of residue cells, and the structure of the integral closure of a complete DVR with18finite residue field in a finite extension of its fraction field (complete, local, a DVR),19with the `p`-adic specializations.20 21## Main results22 23* `primitive_locus_mass`: the primitive vectors of `O^(n+1)` have mass `1 - q^(-(n+1))`.24* `state_measure_total_mass`: an atlas with `N` charts has total state mass `N q^(-n)`.25* `unramified_coefficient_measure_haar`: the unramified coefficient measure is a Haar probability26  measure with the expected cylinder masses.27* `integral_closure_is_local`, `integral_closure_is_dvr`, `integral_closure_own_adic_complete`.28* `polynomial_type_degree`: a polynomial type is valid and has the polynomial's degree.29 30Provenance: `Thm_SurfaceBlowupV2_*`: `primitive_locus_mass`, `scaled_normalization_identity`,31`state_measure_total_mass`, `units_lift_from_local_quotient`,32`residue_ideal_has_fixed_generator_lift`, `unramified_coefficient_measure_haar`,33`integral_closure_{adic_complete, finite_reduction, is_local, is_dvr, own_adic_complete}`,34`irreducible_factor_invariant_degree`, `polynomial_type_degree`,35`padicIntegers_{isDVR, maximal_adic_complete, residueField_finite}`,36`quotient_ring_length_intrinsic`.37-/38 39open MeasureTheory40open scoped BigOperators ENNReal41 42namespace SurfaceBlowup43 44/-- The primitive vectors of `O^(n+1)` (some coordinate a unit) have coefficient measure45`1 - q^(-(n+1))`. -/46theorem primitive_locus_mass (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]47    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]48    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]49    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]50    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) :51    coefficientMeasure O (n+1) {a | primitive O a} =52      1-(Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^(n+1) := by53  have h1 := coefficient_cylinder_mass O htop (n+1) 1 054  have h0 := coefficient_cylinder_mass O htop (n+1) 0 055  simp only [pow_zero, mul_zero, Ideal.one_eq_top, Submodule.mem_top, implies_true,56    Set.ofPred_true, Pi.zero_apply, sub_zero, mul_one, pow_one] at h1 h057  have hS : {a : Fin (n+1) → O | primitive O a} =58      {b : Fin (n+1) → O | ∀ i, b i ∈ IsLocalRing.maximalIdeal O}ᶜ := by59    ext a60    simp [primitive, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff]61  have hopen : IsOpen ((IsLocalRing.maximalIdeal O : Ideal O) : Set O) := by62    simpa using (isAdic_iff.mp htop).1 163  have hm : MeasurableSet {b : Fin (n+1) → O | ∀ i, b i ∈ IsLocalRing.maximalIdeal O} := by64    have : {b : Fin (n+1) → O | ∀ i, b i ∈ IsLocalRing.maximalIdeal O} =65        Set.univ.pi fun _ ↦ ((IsLocalRing.maximalIdeal O : Ideal O) : Set O) := by66      ext; simp67    rw [this]68    exact MeasurableSet.univ_pi fun _ ↦ hopen.measurableSet69  rw [hS]70  have hne : (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (n+1) ≠ ⊤ :=71    ENNReal.pow_ne_top <| ENNReal.inv_ne_top.mpr <|72      Nat.cast_ne_zero.2 (Nat.card_pos (α := IsLocalRing.ResidueField O)).ne'73  have hadd := measure_add_measure_compl (μ := coefficientMeasure O (n+1)) hm74  rw [h1, h0, add_comm] at hadd75  exact ENNReal.eq_sub_of_add_eq hne hadd76 77/-- The normalization identity `(1 + π v)(f + π ∑ zᵢ bᵢ) = f + π E⁻¹(s + remainder s)` for a78division chart. -/79theorem scaled_normalization_identity (O R : Type) [CommRing O] [CommRing R] [Algebra O R] (n : ℕ)Lemma 3.180    (pi : O) (f : R) (b : Fin n → R) (E : R ≃ₗ[O] ((Fin n → O) × R))81    (hE : ∀ s, E.symm s = divisionMap f b s) (s : (Fin n → O) × R) :82    (1 + pi • s.2) * (f + pi • coordinateLift b s.1) =83      f + pi • E.symm (adicPerturb (coordinateRemainder pi b E) s) := by84  simp only [adicPerturb, coordinateRemainder, map_add, map_smul, LinearEquiv.symm_apply_apply]85  rw [hE, divisionMap]86  simp only [Algebra.smul_def]87  ring88 89/-- An atlas whose chart maps are measurable has total state mass `#charts · q^(-n)`. -/90theorem state_measure_total_mass (O R : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]91    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]92    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]93    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]94    (htop : IsAdic (IsLocalRing.maximalIdeal O)) [CommRing R] [Algebra O R]95    [MeasurableSpace (Ideal R)] (pi : O) (n : ℕ) (X : Set (Ideal R))96    (A : IdealAtlas O R pi n X)97    (hA : ∀ i, Measurable (coordinateIdeal pi (A.chart i).f (A.chart i).b)) :98    stateMeasure O R pi n (Nat.card (IsLocalRing.ResidueField O)) A Set.univ =99      (Fintype.card A.ι : ℝ≥0∞) * (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹^n := by100  unfold stateMeasure101  rw [Measure.smul_apply, Measure.finsetSum_apply]102  have h : ∀ i : A.ι, chartMeasure O R pi n (A.chart i) Set.univ = 1 := fun i =>103    chart_measure_total_mass O R htop pi n (A.chart i) (hA i)104  simp only [h, Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one, smul_eq_mul]105  rw [mul_comm]106 107/-- Units of `R/I` lift to units of `R` when `I` lies in the maximal ideal of the local ring `R`. -/108theorem units_lift_from_local_quotient (R : Type) [CommRing R] [IsLocalRing R] (I : Ideal R)109    (hI : I ≤ IsLocalRing.maximalIdeal R) (v : (R ⧸ I)ˣ) :110    ∃ u : Rˣ, Ideal.Quotient.mk I (u : R) = (v : R ⧸ I) := by111  obtain ⟨a, ha⟩ := Ideal.Quotient.mk_surjective (v : R ⧸ I)112  obtain ⟨b, hb⟩ := Ideal.Quotient.mk_surjective ((v⁻¹ : (R ⧸ I)ˣ) : R ⧸ I)113  have hab : a * b - 1 ∈ I := by114    rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, ha, hb, map_one]115    simp116  have hunit : IsUnit a := by117    by_contra h118    have ham : a ∈ IsLocalRing.maximalIdeal R := (IsLocalRing.mem_maximalIdeal a).2 h119    have h1 : a * b - (a * b - 1) ∈ IsLocalRing.maximalIdeal R :=120      Ideal.sub_mem _ (Ideal.mul_mem_right b _ ham) (hI hab)121    simp at h1122  exact ⟨hunit.unit, by simpa using ha⟩123 124/-- Every ideal in the residue cell of a regular `f` has a generator of the form `f + π h`. -/125theorem residue_ideal_has_fixed_generator_lift (R : Type) [CommRing R] [IsLocalRing R] (pi f : R)126    (hp : pi ∈ IsLocalRing.maximalIdeal R)127    (hf : Function.Injective128      (fun x : R ⧸ Ideal.span {pi} => x * Ideal.Quotient.mk (Ideal.span {pi}) f))129    (J : Ideal R) (hJ : J ∈ residueIdealCell pi f) :130    ∃ h : R, J = Ideal.span {f + pi*h} := by131  obtain ⟨⟨g, rfl⟩, hmap⟩ := hJ132  rw [Ideal.map_span, Set.image_singleton] at hmap133  obtain ⟨v, hv⟩ := regular_principal_generators_associated _ _ _ hf hmap.symm134  have hle : Ideal.span {pi} ≤ IsLocalRing.maximalIdeal R :=135    (Ideal.span_singleton_le_iff_mem _).2 hp136  obtain ⟨u, hu⟩ := units_lift_from_local_quotient R _ hle v137  have hmem : g - (u : R) * f ∈ Ideal.span {pi} := by138    rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_mul, hu, ← hv, sub_self]139  obtain ⟨k, hk⟩ := Ideal.mem_span_singleton'.1 hmem140  refine ⟨(↑u⁻¹ : R) * k, ?_⟩141  have : f + pi * ((↑u⁻¹ : R) * k) = (↑u⁻¹ : R) * g := by142    have hg : g = (u : R) * f + k * pi := by rw [hk]; ring143    rw [hg, mul_add, ← mul_assoc (↑u⁻¹ : R), Units.inv_mul, one_mul]; ring144  rw [this, eq_comm]145  exact Ideal.span_singleton_mul_left_unit (Units.isUnit _) _146 147/-- The unramified coefficient measure on `O[X]/(Φ)` is an additive Haar probability measure,148and the ball `x + (base ideal)^L` has mass `q^(-δL)`. -/149theorem unramified_coefficient_measure_haar (O : Type) [CommRing O] [IsDomain O]150    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]151    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] (Φ : Polynomial O) (hm : Φ.Monic)152    [TopologicalSpace (AdjoinRoot Φ)]153    (hτ : ‹TopologicalSpace (AdjoinRoot Φ)› = unramifiedTopology O Φ hm)154    [MeasurableSpace (AdjoinRoot Φ)]155    (hmeas : ‹MeasurableSpace (AdjoinRoot Φ)› = unramifiedMeasurableSpace O Φ hm)156    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]157    [Finite (IsLocalRing.ResidueField O)] (htop : IsAdic (IsLocalRing.maximalIdeal O)) :158    Measure.IsAddHaarMeasure (unramifiedCoefficientMeasure O Φ hm) ∧159      IsProbabilityMeasure (unramifiedCoefficientMeasure O Φ hm) ∧ ∀ (L : ℕ) (x : AdjoinRoot Φ),160      unramifiedCoefficientMeasure O Φ hm {y | y - x ∈ (baseIdeal O Φ) ^ L} =161      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (Φ.natDegree * L) := by162  obtain ⟨hTR, hC, hT2, hSC, hB, hce, hces, hme, hmes⟩ :=163    power_coordinates_transport O Φ hm hτ hmeas164  set e := powerCoordinates O Φ hm165  have hprob := coefficient_measure_probability O htop Φ.natDegree166  have hμ : Measure.IsAddHaarMeasure (coefficientMeasure O Φ.natDegree) := by167    unfold coefficientMeasure168    apply Measure.IsAddHaarMeasure.smul169    · exact ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)170    · exact ENNReal.inv_ne_top.mpr171        (Measure.IsOpenPosMeasure.open_pos _ isOpen_univ Set.univ_nonempty)172  refine ⟨Measure.isAddHaarMeasure_map_of_isFiniteMeasure (coefficientMeasure O Φ.natDegree)173      e.symm.toLinearMap.toAddMonoidHom hces e.symm.surjective,174    Measure.isProbabilityMeasure_map hmes.aemeasurable, fun L x ↦ ?_⟩175  let E : AdjoinRoot Φ ≃ᵐ (Fin Φ.natDegree → O) :=176    { toEquiv := e.toEquiv, measurable_toFun := hme, measurable_invFun := hmes }177  rw [show unramifiedCoefficientMeasure O Φ hm =178    Measure.map E.symm (coefficientMeasure O Φ.natDegree) from rfl, MeasurableEquiv.map_apply]179  have hset : E.symm ⁻¹' {y | y - x ∈ (baseIdeal O Φ) ^ L} =180      {b | ∀ i, b i - e x i ∈ (IsLocalRing.maximalIdeal O) ^ L} := by181    ext v182    simp only [Set.mem_preimage, Set.mem_ofPred_eq]183    rw [base_ideal_coordinates O Φ hm L]184    have key : ∀ z i, (AdjoinRoot.powerBasis' hm).basis.repr z i = e z i := fun z i => rfl185    have hEv : E.symm v = e.symm v := rfl186    simp only [map_sub, Finsupp.coe_sub, Pi.sub_apply, key, hEv, LinearEquiv.apply_symm_apply]187    rfl188  rw [hset]189  exact coefficient_cylinder_mass O htop Φ.natDegree L (e x)190 191/-- The integral closure of a complete DVR in a finite extension (assumed `O`-finite) is192`𝔪_O`-adically complete. -/193private theorem integral_closure_adic_complete (O K L : Type) [CommRing O] [IsDomain O]194    [IsDiscreteValuationRing O] [Field K] [Algebra O K] [IsFractionRing O K] [Field L] [Algebra K L]195    [Algebra O L] [IsScalarTower O K L] [FiniteDimensional K L]196    [Module.Finite O (integralClosure O L)] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]197    [Finite (IsLocalRing.ResidueField O)] :198    IsAdicComplete (IsLocalRing.maximalIdeal O) (integralClosure O L) := by199  obtain ⟨h1, h2, -⟩ := integral_closure_finite_free O K L200  exact finite_free_adic_complete O (integralClosure O L) _201 202/-- The integral closure has finite reduction modulo `𝔪_O`. -/203private theorem integral_closure_finite_reduction (O K L : Type) [CommRing O] [IsDomain O]204    [IsDiscreteValuationRing O] [Field K] [Algebra O K] [IsFractionRing O K] [Field L] [Algebra K L]205    [Algebra O L] [IsScalarTower O K L] [FiniteDimensional K L]206    [Module.Finite O (integralClosure O L)] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]207    [Finite (IsLocalRing.ResidueField O)] :208    Finite (integralClosure O L ⧸209      (IsLocalRing.maximalIdeal O).map (algebraMap O (integralClosure O L))) := by210  obtain ⟨h1, h2, -⟩ := integral_closure_finite_free O K L211  have : Finite (O ⧸ IsLocalRing.maximalIdeal O) := ‹Finite (IsLocalRing.ResidueField O)›212  have hfin := finite_free_residue_quotient O (integralClosure O L)213    (IsLocalRing.maximalIdeal O)214  rw [Ideal.smul_top_eq_map] at hfin215  exact Finite.of_equiv _ (Submodule.Quotient.restrictScalarsEquiv O _).toEquiv216 217/-- The integral closure of a complete DVR with finite residue field in a finite extension218(assumed `O`-finite) is a local ring. -/219theorem integral_closure_is_local (O K L : Type) [CommRing O] [IsDomain O]220    [IsDiscreteValuationRing O] [Field K] [Algebra O K] [IsFractionRing O K] [Field L] [Algebra K L]221    [Algebra O L] [IsScalarTower O K L] [FiniteDimensional K L]222    [Module.Finite O (integralClosure O L)] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]223    [Finite (IsLocalRing.ResidueField O)] :224    IsLocalRing (integralClosure O L) := by225  have h1 := integral_closure_adic_complete O K L226  have h2 := integral_closure_finite_reduction O K L227  have : IsAdicComplete ((IsLocalRing.maximalIdeal O).map228      (algebraMap O (integralClosure O L))) (integralClosure O L) :=229    (IsAdicComplete.map_algebraMap_iff _ _).mpr h1230  exact complete_domain_finite_quotient_local (integralClosure O L)231    ((IsLocalRing.maximalIdeal O).map (algebraMap O (integralClosure O L)))232 233/-- The integral closure of a complete DVR with finite residue field in a finite extension234(assumed `O`-finite) is a DVR. -/235theorem integral_closure_is_dvr (O K L : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Standard facts236    [Field K] [Algebra O K] [IsFractionRing O K] [Field L] [Algebra K L] [Algebra O L]237    [IsScalarTower O K L] [FiniteDimensional K L] [Module.Finite O (integralClosure O L)]238    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] :239    IsDiscreteValuationRing (integralClosure O L) := by240  have := integral_closure_is_local O K L241  have hD := integral_closure_is_dedekind O K L242  have hN : IsNoetherianRing (integralClosure O L) := inferInstance243  exact ((IsDiscreteValuationRing.TFAE (R := integralClosure O L)244    (integral_closure_not_field O K L)).out 0 2).mpr hD245 246/-- The integral closure is complete for its own maximal ideal. -/247theorem integral_closure_own_adic_complete (O K L : Type) [CommRing O] [IsDomain O]248    [IsDiscreteValuationRing O] [Field K] [Algebra O K] [IsFractionRing O K] [Field L] [Algebra K L]249    [Algebra O L] [IsScalarTower O K L] [FiniteDimensional K L]250    [Module.Finite O (integralClosure O L)] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]251    [Finite (IsLocalRing.ResidueField O)] (hlocal : IsLocalRing (integralClosure O L)) :252    letI : IsLocalRing (integralClosure O L) := hlocal253    IsAdicComplete (IsLocalRing.maximalIdeal (integralClosure O L)) (integralClosure O L) := by254  have : IsLocalRing (integralClosure O L) := hlocal255  have : IsDiscreteValuationRing (integralClosure O L) :=256    integral_closure_is_dvr O K L257  have hc := integral_closure_adic_complete O K L258  have hinj : Function.Injective (algebraMap O (integralClosure O L)) := by259    intro a b h260    have h2 : algebraMap O L a = algebraMap O L b := by261      simpa using congrArg (fun x : integralClosure O L => (x : L)) h262    simp only [IsScalarTower.algebraMap_apply O K L] at h2263    exact IsFractionRing.injective O K ((algebraMap K L).injective h2)264  have : Algebra.IsIntegral O (integralClosure O L) := integralClosure.AlgebraIsIntegral265  have : FaithfulSMul O (integralClosure O L) := (faithfulSMul_iff_algebraMap_injective _ _).2 hinj266  have h512 := dvr_extension_maximalIdeal_map_eq_pow O (integralClosure O L) hinj267  have hI : (IsLocalRing.maximalIdeal O).map (algebraMap O (integralClosure O L)) ≤268      IsLocalRing.maximalIdeal (integralClosure O L) := by269    rw [Ideal.map_le_iff_le_comap]270    intro x hx271    simp only [Ideal.mem_comap]272    by_contra hn273    have hu : IsUnit (algebraMap O (integralClosure O L) x) := by274      simpa [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] using hn275    exact (IsLocalRing.mem_maximalIdeal x).1 hx ((isUnit_map_iff _ x).1 hu)276  have h1 := (IsAdicComplete.map_algebraMap_iff (S := integralClosure O L)277    (I := IsLocalRing.maximalIdeal O) (M := integralClosure O L)).2 hc278  exact (adic_complete_iff_of_pow_le (integralClosure O L) (integralClosure O L) _ _279    _ (le_of_eq h512.symm) hI).1 h1280 281/-- For a monic irreducible `g` with `O`-finite integral closure, the factor invariants `(f, e)`282are positive with `f e = deg g`. -/283private theorem irreducible_factor_invariant_degree (O : Type) [CommRing O] [IsDomain O]284    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]285    [Finite (IsLocalRing.ResidueField O)] (g : Polynomial (BaseField O)) (hg : g.Monic)286    (hirr : Irreducible g) (hfin : Module.Finite O (integralClosure O (AdjoinRoot g))) :287    0 < (factorInvariant O g).1 ∧ 0 < (factorInvariant O g).2 ∧288      (factorInvariant O g).1 * (factorInvariant O g).2 = g.natDegree := by289  have : Fact (Irreducible g) := ⟨hirr⟩290  have : Module.Finite (BaseField O) (AdjoinRoot g) := hg.finite_adjoinRoot291  have hloc := integral_closure_is_local O (BaseField O) (AdjoinRoot g)292  have h := integral_closure_invariants_degree O (BaseField O) (AdjoinRoot g) hloc293  have hdeg : Module.finrank (BaseField O) (AdjoinRoot g) = g.natDegree :=294    finrank_quotient_span_eq_natDegree295  unfold factorInvariant296  rw [dif_pos hloc]297  exact ⟨h.1, h.2.1, h.2.2.trans hdeg⟩298 299/-- A polynomial type of `F` is a valid factor type of degree `deg F`. -/300theorem polynomial_type_degree (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]301    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]302    (F : Polynomial (BaseField O)) (σ : FactorType) (hF : HasPolynomialTypeF O F σ) :303    ValidType σ ∧ typeDegree σ=F.natDegree := by304  obtain ⟨gs, hgs, -, rfl, rfl, hfin⟩ := hF305  constructor306  · intro z hz307    rw [Multiset.mem_coe, List.mem_map] at hz308    obtain ⟨g, hg, rfl⟩ := hz309    have := irreducible_factor_invariant_degree O g (hgs g hg).1 (hgs g hg).2 (hfin g hg)310    exact ⟨this.1, this.2.1⟩311  · induction gs with312    | nil => simp [typeDegree]313    | cons g gs ih =>314      have hg := hgs g (by simp)315      have ht : ∀ h ∈ gs, h.Monic ∧ Irreducible h := fun h hh => hgs h (by simp [hh])316      have hm : gs.prod.Monic := by317        simpa using Polynomial.monic_multiset_prod_of_monic (gs : Multiset _) id318          (fun h hh => (ht h (by simpa using hh)).1)319      have := irreducible_factor_invariant_degree O g hg.1 hg.2 (hfin g (by simp))320      have ih' := ih ht (fun h hh => hfin h (by simp [hh]))321      simp only [typeDegree, List.map_cons, ← Multiset.cons_coe, Multiset.map_cons,322        Multiset.sum_cons, List.prod_cons] at ih' ⊢323      rw [Polynomial.Monic.natDegree_mul hg.1 hm, ih', this.2.2]324 325/-- The ring of integers of a finite extension of `ℚ_[p]` is a DVR. -/326theorem padicIntegers_isDVR (p : ℕ) [Fact p.Prime] (K : Type) [Field K] [Algebra ℚ_[p] K]327    [Algebra ℤ_[p] K] [IsScalarTower ℤ_[p] ℚ_[p] K] [FiniteDimensional ℚ_[p] K] :328    IsDiscreteValuationRing (padicIntegers p K) := by329  have : Algebra.IsSeparable ℚ_[p] K :=330    Algebra.IsAlgebraic.isSeparable_of_perfectField331  have : Finite (IsLocalRing.ResidueField ℤ_[p]) :=332    Finite.of_equiv (ZMod p) (PadicInt.residueField (p := p)).toEquiv.symm333  have : Module.Finite ℤ_[p] (integralClosure ℤ_[p] K) :=334    IsIntegralClosure.finite ℤ_[p] ℚ_[p] K (integralClosure ℤ_[p] K)335  exact integral_closure_is_dvr ℤ_[p] ℚ_[p] K336 337/-- The ring of integers of a finite extension of `ℚ_[p]` is complete for its maximal ideal. -/338theorem padicIntegers_maximal_adic_complete (p : ℕ) [Fact p.Prime] (K : Type) [Field K]339    [Algebra ℚ_[p] K] [Algebra ℤ_[p] K] [IsScalarTower ℤ_[p] ℚ_[p] K] [FiniteDimensional ℚ_[p] K]340    (hdvr : IsDiscreteValuationRing (padicIntegers p K)) :341    letI := hdvr342    IsAdicComplete (IsLocalRing.maximalIdeal (padicIntegers p K)) (padicIntegers p K) := by343  have := hdvr344  have : Finite (IsLocalRing.ResidueField ℤ_[p]) :=345    Finite.of_equiv (ZMod p) PadicInt.residueField.toEquiv.symm346  have : Module.Finite ℤ_[p] (integralClosure ℤ_[p] K) :=347    IsIntegralClosure.finite ℤ_[p] ℚ_[p] K (integralClosure ℤ_[p] K)348  exact integral_closure_own_adic_complete ℤ_[p] ℚ_[p] K inferInstance349 350/-- The ring of integers of a finite extension of `ℚ_[p]` has finite residue field. -/351theorem padicIntegers_residueField_finite (p : ℕ) [Fact p.Prime] (K : Type) [Field K]352    [Algebra ℚ_[p] K] [Algebra ℤ_[p] K] [IsScalarTower ℤ_[p] ℚ_[p] K] [FiniteDimensional ℚ_[p] K]353    (hdvr : IsDiscreteValuationRing (padicIntegers p K)) :354    letI := hdvr; Finite (IsLocalRing.ResidueField (padicIntegers p K)) := by355  have := hdvr356  have : Finite (IsLocalRing.ResidueField ℤ_[p]) :=357    Finite.of_equiv _ PadicInt.residueField.symm.toEquiv358  have : Module.Finite ℤ_[p] (integralClosure ℤ_[p] K) :=359    IsIntegralClosure.finite ℤ_[p] ℚ_[p] K (integralClosure ℤ_[p] K)360  have h1 : Finite (integralClosure ℤ_[p] K ⧸361      (IsLocalRing.maximalIdeal ℤ_[p]).map (algebraMap ℤ_[p] (integralClosure ℤ_[p] K))) :=362    integral_closure_finite_reduction ℤ_[p] ℚ_[p] K363  have h2 := (integral_local_extension_unique_prime ℤ_[p] (padicIntegers p K)).1364  have hle : (IsLocalRing.maximalIdeal ℤ_[p]).map (algebraMap ℤ_[p] (padicIntegers p K)) ≤365      IsLocalRing.maximalIdeal (padicIntegers p K) := by366    rw [Ideal.map_le_iff_le_comap, h2]367  exact Finite.of_surjective (Ideal.Quotient.factor hle) (Ideal.Quotient.factor_surjective hle)368 369/-- The length of a quotient ring over itself depends only on its ring isomorphism class. -/370theorem quotient_ring_length_intrinsic (S S' : Type) [CommRing S] [CommRing S'] (I : Ideal S)371    (J : Ideal S') (e : (S ⧸ I) ≃+* (S' ⧸ J)) :372    Module.length S (S ⧸ I) = Module.length S' (S' ⧸ J) := by373  rw [Module.length_eq_of_surjective (R := S ⧸ I) (M := S ⧸ I) Ideal.Quotient.mk_surjective,374    Module.length_eq_of_surjective (R := S' ⧸ J) (M := S' ⧸ J) Ideal.Quotient.mk_surjective]375  have : RingHomSurjective (e : (S ⧸ I) →+* (S' ⧸ J)) := ⟨e.surjective⟩376  let f : (S ⧸ I) →ₛₗ[(e : (S ⧸ I) →+* (S' ⧸ J))] (S' ⧸ J) :=377    ⟨(e : (S ⧸ I) →+* (S' ⧸ J)).toAddMonoidHom, by intro c x; simp⟩378  rw [Module.length, Module.length, WithBot.unbot_inj,379    Order.krullDim_eq_of_orderIso (Submodule.orderIsoMapComapOfBijective f e.bijective)]380 381end SurfaceBlowup