Algebra types and integral closures over a discrete valuation ring

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.Formula.LawAlgebra7import Mathlib.RingTheory.Henselian8 9/-!10# Algebra types and integral closures over a discrete valuation ring11 12For a domain `O` with fraction field `K = BaseField O`, an `O`-algebra `B` *has algebra type* `σ`13when its generic fibre `K ⊗_O B` is a finite product of finite field extensions `Lᵢ/K` with finite14`O`-integral closures, `σ` being the multiset of the invariants `(e, f)` of these closures. This15file sets up that notion and the order defect `δ_O(B)`, and proves the closure-finiteness and16base-change facts used to compute types: transfer of closure finiteness along finite extensions of17`O` and finite separable extensions of fields, types of squarefree monic polynomials, invariance18of algebra types under isomorphism and products, and the structure of integral closures in finite19extensions of `K` (finite free of the right rank, Dedekind, not a field).20 21## Main definitions22 23* `SurfaceBlowup.fieldInvariant`, `SurfaceBlowup.HasAlgebraType`24* `SurfaceBlowup.GenericClosure`, `SurfaceBlowup.orderImage`, `SurfaceBlowup.orderDefect`25 26## Main results27 28* `SurfaceBlowup.closure_finite_descent`, `SurfaceBlowup.closure_finite_ascent`,29  `SurfaceBlowup.closure_finite_ascent_root`, `SurfaceBlowup.closure_finite_of_separable`30* `SurfaceBlowup.HasPolynomialTypeF.to_original`,31  `SurfaceBlowup.hasPolynomialTypeF_iff_of_separable`32* `SurfaceBlowup.squarefree_monic_has_polynomial_type`, `SurfaceBlowup.polynomial_type_dvd`33* `SurfaceBlowup.algebra_type_pi`, `SurfaceBlowup.integral_closure_finite_free`,34  `SurfaceBlowup.integral_closure_is_dedekind`, `SurfaceBlowup.unramified_generic_fibre_witness`35 36Provenance: Def_SurfaceBlowupV2_{AlgebraType, OrderDefect}; Thm_Gen_{ClosureTransfer, Ascent,37SepHelpers, TypeDvd}; Thm_SurfaceBlowupV2_{adjoinRoot_base_change, algebra_type_{algEquiv,38of_generic_fibre_equiv, pi}, integral_closure_{algEquiv, finite_free, invariants_degree,39is_dedekind, not_field}, pi_field_maximal_ideals, unramified_{fraction_base_change,40generic_fibre_witness}}.41-/42 43noncomputable section44 45namespace SurfaceBlowup46 47open scoped TensorProduct48open Polynomial IsLocalRing49 50/-! ### Definitions -/51 52section Definitions53 54variable (O : Type) [CommRing O] [IsDomain O]55 56/-- The invariants (e,f) of the maximal ideal of the integral closure of O in an O-algebra L (a57field in the applications), with the junk value (0,0) when that closure is not local. -/58noncomputable def fieldInvariant (L : Type) [CommRing L] [Algebra O L] : ℕ × ℕ := byReduced-algebra type convention59  classical60  let B := integralClosure O L61  exact if h : IsLocalRing B then62    letI : IsLocalRing B := h63    ((maximalIdeal B).ramificationIdx O, (maximalIdeal B).inertiaDeg O)64  else (0,0)65 66/-- `HasAlgebraType O B σ`: the generic fibre K ⊗_O B (K = FractionRing O) is isomorphic as a67K-algebra to a finite product of finite field extensions L_i of K whose O-integral closures are68finite O-modules, and σ is the multiset of their invariants. -/69def HasAlgebraType (B : Type) [CommRing B] [Algebra O B] (σ : FactorType) : Prop :=Reduced-algebra type convention70  ∃ (ι : Type) (_ : Fintype ι) (L : ι → Type) (_ : ∀ i, Field (L i))71    (_ : ∀ i, Algebra (BaseField O) (L i)) (_ : ∀ i, Algebra O (L i))72    (_ : ∀ i, IsScalarTower O (BaseField O) (L i)) (_ : ∀ i, FiniteDimensional (BaseField O) (L i))73    (_ : (BaseField O ⊗[O] B) ≃ₐ[BaseField O] (∀ i, L i)),74    σ = ∑ i, ({fieldInvariant O (L i)} : FactorType) ∧75      ∀ i, Module.Finite O (integralClosure O (L i))76 77/-- The integral closure of O in the generic fibre K ⊗_O B (K = BaseField O), as a type: a `def`78copy of the coerced subalgebra, so that the module quotient defining `orderDefect` can be formed. -/79def GenericClosure (B : Type) [CommRing B] [Algebra O B] : Type :=80  ↥(integralClosure O (BaseField O ⊗[O] B))81 82/-- The ring structure of `GenericClosure O B`, inherited from the subalgebra. -/83instance (B : Type) [CommRing B] [Algebra O B] : CommRing (GenericClosure O B) :=84  inferInstanceAs (CommRing ↥(integralClosure O (BaseField O ⊗[O] B)))85 86/-- The `O`-algebra structure of `GenericClosure O B`, inherited from the subalgebra. -/87instance (B : Type) [CommRing B] [Algebra O B] : Algebra O (GenericClosure O B) :=88  inferInstanceAs (Algebra O ↥(integralClosure O (BaseField O ⊗[O] B)))89 90/-- The inclusion of the closure into the generic fibre (the subalgebra's `val`). -/91def genericClosureVal (B : Type) [CommRing B] [Algebra O B] :92    GenericClosure O B →ₐ[O] BaseField O ⊗[O] B :=93  (integralClosure O (BaseField O ⊗[O] B)).val94 95/-- The O-submodule of the closure formed by the elements 1 ⊗ b, b ∈ B (the image of the order B96in its generic fibre): the preimage of the range of includeRight under the inclusion. -/97def orderImage (B : Type) [CommRing B] [Algebra O B] : Submodule O (GenericClosure O B) :=98  Submodule.comap (genericClosureVal O B).toLinearMap99    (LinearMap.range (Algebra.TensorProduct.includeRight : B →ₐ[O] BaseField O ⊗[O] B).toLinearMap)100 101/-- δ_O(B): the O-length (an ℕ∞) of the integral closure of O in K ⊗_O B modulo the image of B.102It is finite when K ⊗_O B is a product of fields and B is finite free; ⊤ is a legitimate value. -/103noncomputable def orderDefect (B : Type) [CommRing B] [Algebra O B] : ℕ∞ :=104  Module.length O (GenericClosure O B ⧸ orderImage O B)105 106end Definitions107 108/-! ### Transfer of closure finiteness -/109 110/-- Over a finite (hence integral) extension `O → Oδ`, the integral closures of `O` and of `Oδ` in111`L` coincide. -/112def integralClosureTowerEquiv (O Oδ L : Type) [CommRing O] [CommRing Oδ] [Algebra O Oδ]113    [Module.Finite O Oδ] [CommRing L] [Algebra O L] [Algebra Oδ L] [IsScalarTower O Oδ L] :114    integralClosure O L ≃ₐ[O] integralClosure Oδ L := by115  have : Algebra.IsIntegral O Oδ := Algebra.IsIntegral.of_finite O Oδ116  exact117  { toFun := fun x ↦ ⟨x.1, x.2.tower_top⟩118    invFun := fun x ↦ ⟨x.1, isIntegral_trans _ x.2⟩119    left_inv := fun _ ↦ rfl120    right_inv := fun _ ↦ rfl121    map_mul' := fun _ _ ↦ rfl122    map_add' := fun _ _ ↦ rfl123    commutes' := fun _ ↦ rfl }124 125/-- `O` embeds into any `O`-subring `S` of a field `L` over `K = Frac O`. -/126theorem algebraMap_injective_of_tower (O : Type) [CommRing O] [IsDomain O] (S L : Type)127    [CommRing S] [Field L] [Algebra O S] [Algebra S L] [Algebra (BaseField O) L] [Algebra O L]128    [IsScalarTower O S L] [IsScalarTower O (BaseField O) L] :129    Function.Injective (algebraMap O S) := by130  refine Function.Injective.of_comp (f := algebraMap S L) ?_131  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq,132    IsScalarTower.algebraMap_eq O (BaseField O) L, RingHom.coe_comp]133  exact (algebraMap (BaseField O) L).injective.comp (IsFractionRing.injective O (BaseField O))134 135/-- Closure finiteness descends along a finite extension `O → Oδ`: the two integral closures136coincide, and finite over `Oδ` finite over `O` is finite over `O`. -/137theorem closure_finite_descent (O Oδ L : Type) [CommRing O] [CommRing Oδ] [Algebra O Oδ]138    [Module.Finite O Oδ] [CommRing L] [Algebra O L] [Algebra Oδ L] [IsScalarTower O Oδ L]139    (h : Module.Finite Oδ (integralClosure Oδ L)) : Module.Finite O (integralClosure O L) :=140  have : Module.Finite O (integralClosure Oδ L) := .trans Oδ _141  .equiv (integralClosureTowerEquiv O Oδ L).symm.toLinearEquiv142 143/-- Closure finiteness ascends along a finite extension `O → Oδ` acting on the same ring. -/144theorem closure_finite_ascent (O Oδ L : Type) [CommRing O] [CommRing Oδ] [Algebra O Oδ]145    [Module.Finite O Oδ] [CommRing L] [Algebra O L] [Algebra Oδ L] [IsScalarTower O Oδ L]146    (h : Module.Finite O (integralClosure O L)) : Module.Finite Oδ (integralClosure Oδ L) :=147  have := Module.Finite.equiv (integralClosureTowerEquiv O Oδ L).toLinearEquiv148  .of_restrictScalars_finite O Oδ _149 150private theorem faithfulSMul_of_isFractionRing (O K L : Type) [CommRing O] [IsDomain O] [Field K]151    [Algebra O K] [IsFractionRing O K] [Field L] [Algebra K L] [Algebra O L]152    [IsScalarTower O K L] : FaithfulSMul O L := by153  rw [faithfulSMul_iff_algebraMap_injective, IsScalarTower.algebraMap_eq O K L]154  exact (algebraMap K L).injective.comp (IsFractionRing.injective O K)155 156/-- The integral closure of a DVR `O` in a finite extension `L` of `K = Frac O`, assumed finite157over `O`, is a Dedekind domain. -/158theorem integral_closure_is_dedekind (O K L : Type) [CommRing O] [IsDomain O]159    [IsDiscreteValuationRing O] [Field K] [Algebra O K] [IsFractionRing O K] [Field L] [Algebra K L]160    [Algebra O L] [IsScalarTower O K L] [FiniteDimensional K L]161    [Module.Finite O (integralClosure O L)] :162    IsDedekindDomain (integralClosure O L) := by163  have := faithfulSMul_of_isFractionRing O K L164  have hN : IsNoetherianRing (integralClosure O L) :=165    isNoetherian_of_tower O (isNoetherian_of_isNoetherianRing_of_finite O (integralClosure O L))166  have : IsFractionRing (integralClosure O L) L :=167    IsIntegralClosure.isFractionRing_of_finite_extension O K L (integralClosure O L)168  have : Algebra.IsIntegral O (integralClosure O L) := IsIntegralClosure.isIntegral_algebra O L169  exact { hN, Ring.DimensionLEOne.of_isIntegral O (integralClosure O L),170    (isIntegrallyClosed_iff L).mpr fun {x} hx ↦171      ⟨IsIntegralClosure.mk' (integralClosure O L) x (isIntegral_trans (R := O) _ hx),172        IsIntegralClosure.algebraMap_mk' _ _ _⟩ with : IsDedekindDomain (integralClosure O L) }173 174/-- Finiteness of the integral closure is stable under a finite separable extension on top: if175the closure `C` of `O` in `L` is finite over `O` and `M/L` is finite separable, the closure of `O`176in `M` is finite over `O` (it sits inside the closure of the Dedekind domain `C` in `M`). -/177private theorem closure_finite_of_separable_tower (O K L M : Type) [CommRing O] [IsDomain O]178    [IsDiscreteValuationRing O] [Field K] [Algebra O K] [IsFractionRing O K] [Field L]179    [Algebra K L] [Algebra O L] [IsScalarTower O K L] [FiniteDimensional K L] [Field M]180    [Algebra L M] [Algebra O M] [IsScalarTower O L M] [FiniteDimensional L M]181    [Algebra.IsSeparable L M] (hL : Module.Finite O (integralClosure O L)) :182    Module.Finite O (integralClosure O M) := by183  have := integral_closure_is_dedekind O K L184  have : IsFractionRing (integralClosure O L) L :=185    IsIntegralClosure.isFractionRing_of_finite_extension O K L (integralClosure O L)186  have := IsIntegralClosure.finite (integralClosure O L) L M187    (integralClosure (integralClosure O L) M)188  have : IsScalarTower O (integralClosure O L) M := .of_algebraMap_eq fun x ↦ by189    rw [IsScalarTower.algebraMap_apply O L M,190      IsScalarTower.algebraMap_apply (integralClosure O L) L M]191    rfl192  have := Module.Finite.trans (R := O) (integralClosure O L)193    (integralClosure (integralClosure O L) M)194  have : IsNoetherian O (integralClosure (integralClosure O L) M) :=195    isNoetherian_of_isNoetherianRing_of_finite _ _196  let f : integralClosure O M →ₗ[O] integralClosure (integralClosure O L) M :=197    { toFun := fun x ↦ ⟨x.1, x.2.tower_top⟩198      map_add' := fun _ _ ↦ rfl199      map_smul' := fun _ _ ↦ rfl }200  exact .of_injective f fun x y h ↦ Subtype.ext (show x.1 = y.1 from congrArg (fun z ↦ z.1) h)201 202/-! ### Base change of root fields -/203 204/-- Base change of `R[X]/(g)` along `R → A`: `A ⊗_R R[X]/(g) ≃ A[X]/(g)`, compatibly with `mk`. -/205private theorem adjoinRoot_tensor (R A : Type) [CommRing R] [CommRing A] [Algebra R A] (g : R[X]) :206    ∃ e : A ⊗[R] AdjoinRoot g ≃ₐ[A] AdjoinRoot (g.map (algebraMap R A)), ∀ P : R[X],207      e (1 ⊗ₜ AdjoinRoot.mk g P) = AdjoinRoot.mk _ (P.map (algebraMap R A)) := by208  have hmap : ∀ P : R[X], (polyEquivTensor' R A).symm (1 ⊗ₜ P) = P.map (algebraMap R A) :=209    fun P ↦ by simp [polyEquivTensor_symm_apply_tmul_eq_smul]210  have hI : Ideal.span {g.map (algebraMap R A)} =211      ((Ideal.span {g}).map (Algebra.TensorProduct.includeRight (A := A) (R := R))).map212        ((polyEquivTensor' R A).symm : A ⊗[R] R[X] →+* A[X]) := by213    rw [Ideal.map_span, Ideal.map_span, Set.image_singleton, Set.image_singleton, ← hmap]214    rfl215  refine ⟨(Algebra.TensorProduct.tensorQuotientEquiv A R[X] A (Ideal.span {g})).trans216    (Ideal.quotientEquivAlg _ _ (polyEquivTensor' R A).symm hI), fun P ↦ ?_⟩217  change Ideal.Quotient.mk _ ((polyEquivTensor' R A).symm (1 ⊗ₜ P)) = _218  rw [hmap]219  rfl220 221/-- Base change of `O[X]/(F)` to the fraction field `K` of `O` is `K[X]/(F)`, compatibly with222`mk`. -/223theorem adjoinRoot_base_change (O : Type) [CommRing O] [IsDomain O] (F : Polynomial O) :224    ∃ e : TensorProduct O (BaseField O) (AdjoinRoot F) ≃ₐ[BaseField O]225      AdjoinRoot (F.map (algebraMap O (BaseField O))), ∀ P : Polynomial O,226      e (TensorProduct.tmul O (1 : BaseField O) (AdjoinRoot.mk F P)) =227        AdjoinRoot.mk (F.map (algebraMap O (BaseField O))) (P.map (algebraMap O (BaseField O))) :=228  adjoinRoot_tensor O (BaseField O) F229 230section Fields231 232variable (K K' : Type) [Field K] [Field K'] [Algebra K K']233 234/-- A nonzero `q` with `K'[X]/(q)` reduced is squarefree. -/235theorem squarefree_of_isReduced_adjoinRoot (q : K'[X]) (hq : q ≠ 0)236    (hred : IsReduced (AdjoinRoot q)) : Squarefree q := by237  rintro g ⟨h, rfl⟩238  have hgh : g * h ≠ 0 := by rintro h0; apply hq; rw [mul_assoc, h0, mul_zero]239  have h0 := (show IsNilpotent (AdjoinRoot.mk (g * g * h) (g * h)) from240    ⟨2, by rw [← map_pow, AdjoinRoot.mk_eq_zero]; exact ⟨h, by ring⟩⟩).eq_zero241  rw [AdjoinRoot.mk_eq_zero, mul_assoc] at h0242  exact isUnit_of_dvd_one ((mul_dvd_mul_iff_right hgh).1 (by simpa using h0))243 244/-- Along a finite separable extension `K'/K`, the image of an irreducible polynomial stays245squarefree (`K' ⊗_K K[X]/(g)` is formally unramified over the field `K[X]/(g)`, hence reduced). -/246theorem squarefree_map_of_isSeparable [FiniteDimensional K K'] [Algebra.IsSeparable K K']247    (g : K[X]) [Fact (Irreducible g)] : Squarefree (g.map (algebraMap K K')) := by248  have : Algebra.FormallyUnramified K K' := .of_isSeparable K K'249  have hred : IsReduced (TensorProduct K (AdjoinRoot g) K') :=250    Algebra.FormallyUnramified.isReduced_of_field (AdjoinRoot g) _251  obtain ⟨e, -⟩ := adjoinRoot_tensor K K' g252  let c := (Algebra.TensorProduct.comm K K' (AdjoinRoot g)).toRingEquiv253  exact squarefree_of_isReduced_adjoinRoot K' _ (map_ne_zero (Fact.out : Irreducible g).ne_zero)254    (isReduced_of_injective (c.toRingHom.comp e.symm.toRingEquiv.toRingHom)255      (c.injective.comp e.symm.injective))256 257/-- The root-field map `K[X]/(g) → K'[X]/(h)` for `h ∣ g` over `K'`. -/258private def rootHom (g : K[X]) (h : K'[X]) (hdvd : h ∣ g.map (algebraMap K K')) :259    AdjoinRoot g →ₐ[K] AdjoinRoot h :=260  AdjoinRoot.liftAlgHom g (Algebra.ofId K (AdjoinRoot h)) (AdjoinRoot.root h) (by261    change g.eval₂ (algebraMap K (AdjoinRoot h)) _ = 0262    rwa [IsScalarTower.algebraMap_eq K K' (AdjoinRoot h), ← eval₂_map, ← aeval_def,263      AdjoinRoot.aeval_eq, AdjoinRoot.mk_eq_zero])264 265/-- `K'[X]/(h)` is separable over `K[X]/(g)` when `K'/K` is separable: it is generated over266`K[X]/(g)` by the separable elements of `K'`. -/267private theorem rootHom_isSeparable [Algebra.IsSeparable K K'] (g : K[X]) [Fact (Irreducible g)]268    (h : K'[X]) [Fact (Irreducible h)] (hdvd : h ∣ g.map (algebraMap K K')) :269    letI := (rootHom K K' g h hdvd).toRingHom.toAlgebra270    Algebra.IsSeparable (AdjoinRoot g) (AdjoinRoot h) := by271  let := (rootHom K K' g h hdvd).toRingHom.toAlgebra272  have : IsScalarTower K (AdjoinRoot g) (AdjoinRoot h) :=273    .of_algebraMap_eq fun x ↦ ((rootHom K K' g h hdvd).commutes x).symm274  rw [← separableClosure.eq_top_iff, eq_top_iff]275  rintro x -276  induction x using AdjoinRoot.induction_on with277  | ih p =>278    induction p using Polynomial.induction_on with279    | C a =>280      rw [AdjoinRoot.mk_C]281      exact mem_separableClosure_iff.2 <| ((Algebra.IsSeparable.isSeparable K a).map282        (IsScalarTower.toAlgHom K K' (AdjoinRoot h)) (RingHom.injective _)).tower_top _283    | add p q hp hq => rw [map_add]; exact add_mem hp hq284    | monomial n a ih =>285      rw [pow_succ, ← mul_assoc, map_mul, AdjoinRoot.mk_X]286      refine mul_mem ih ?_287      rw [show AdjoinRoot.root h = rootHom K K' g h hdvd (AdjoinRoot.root g) from288        (AdjoinRoot.liftAlgHom_root _ _ _ _).symm]289      exact IntermediateField.algebraMap_mem _ _290 291end Fields292 293/-- The ascent step: let `O → Oδ` be finite, `K = Frac O`, and `Kδ/K` finite separable (with294compatible structures). If `g` is monic irreducible over `K` with finite `O`-closure of295`K[X]/(g)`, and `h` is an irreducible factor of `g` over `Kδ`, then the `Oδ`-closure of296`Kδ[X]/(h)` is finite over `Oδ`. -/297theorem closure_finite_ascent_root (O Oδ K Kδ : Type) [CommRing O] [IsDomain O]298    [IsDiscreteValuationRing O] [CommRing Oδ] [Algebra O Oδ] [Module.Finite O Oδ]299    [Field K] [Algebra O K] [IsFractionRing O K] [Field Kδ] [Algebra K Kδ] [Algebra O Kδ]300    [Algebra Oδ Kδ] [IsScalarTower O K Kδ] [IsScalarTower O Oδ Kδ] [FiniteDimensional K Kδ]301    [Algebra.IsSeparable K Kδ] (g : K[X]) (hgm : g.Monic) (hgi : Irreducible g)302    (hfin : Module.Finite O (integralClosure O (AdjoinRoot g)))303    (h : Kδ[X]) (hhi : Irreducible h) (hdvd : h ∣ g.map (algebraMap K Kδ)) :304    Module.Finite Oδ (integralClosure Oδ (AdjoinRoot h)) := by305  have : Fact (Irreducible g) := ⟨hgi⟩306  have : Fact (Irreducible h) := ⟨hhi⟩307  have : FiniteDimensional K (AdjoinRoot g) := hgm.finite_adjoinRoot308  have : FiniteDimensional Kδ (AdjoinRoot h) := (AdjoinRoot.powerBasis hhi.ne_zero).finite309  have : FiniteDimensional K (AdjoinRoot h) := Module.Finite.trans Kδ _310  let := (rootHom K Kδ g h hdvd).toRingHom.toAlgebra311  have : IsScalarTower K (AdjoinRoot g) (AdjoinRoot h) :=312    .of_algebraMap_eq fun x ↦ ((rootHom K Kδ g h hdvd).commutes x).symm313  have : FiniteDimensional (AdjoinRoot g) (AdjoinRoot h) := .of_restrictScalars_finite K _ _314  have := rootHom_isSeparable K Kδ g h hdvd315  have : IsScalarTower O (AdjoinRoot g) (AdjoinRoot h) := .of_algebraMap_eq fun c ↦ by316    rw [IsScalarTower.algebraMap_apply O K (AdjoinRoot h),317      IsScalarTower.algebraMap_apply O K (AdjoinRoot g),318      IsScalarTower.algebraMap_apply K (AdjoinRoot g) (AdjoinRoot h)]319  exact closure_finite_ascent O Oδ (AdjoinRoot h)320    (closure_finite_of_separable_tower O K (AdjoinRoot g) (AdjoinRoot h) hfin)321 322/-- `K[X]/(g)` is separable over `K` when `g` is irreducible and separable. -/323private theorem adjoinRoot_isSeparable {K : Type} [Field K] (g : K[X]) [Fact (Irreducible g)]324    (hs : g.Separable) : Algebra.IsSeparable K (AdjoinRoot g) := by325  have hx : IsSeparable K (AdjoinRoot.root g) :=326    hs.of_dvd (minpoly.dvd K _ (by rw [AdjoinRoot.aeval_eq, AdjoinRoot.mk_self]))327  have := (IntermediateField.isSeparable_adjoin_simple_iff_isSeparable K (AdjoinRoot g)).2 hx328  refine ⟨fun y ↦ IntermediateField.isSeparable_of_mem_isSeparable K (AdjoinRoot g)329    (L := IntermediateField.adjoin K {AdjoinRoot.root g}) ?_⟩330  have : y ∈ Algebra.adjoin K {AdjoinRoot.root g} := by rw [AdjoinRoot.adjoinRoot_eq_top]; trivial331  exact IntermediateField.algebra_adjoin_le_adjoin K _ this332 333/-- For `g` irreducible and separable over `Frac O`, the integral closure of `O` in `K[X]/(g)` is334a finite `O`-module. -/335theorem closure_finite_of_separable (O : Type) [CommRing O] [IsDomain O]336    [IsDiscreteValuationRing O] (g : (FractionRing O)[X]) (hirr : Irreducible g)337    (hs : g.Separable) : Module.Finite O (integralClosure O (AdjoinRoot g)) := by338  have : Fact (Irreducible g) := ⟨hirr⟩339  have : Module.Finite (FractionRing O) (AdjoinRoot g) :=340    (AdjoinRoot.powerBasis hirr.ne_zero).finite341  have := adjoinRoot_isSeparable g hs342  exact IsIntegralClosure.finite O (FractionRing O) (AdjoinRoot g) _343 344/-- A route-F polynomial type is a polynomial type (forget the closure-finiteness witnesses). -/345theorem HasPolynomialTypeF.to_original {O : Type} [CommRing O] [IsDomain O]346    {F : (BaseField O)[X]} {σ : FactorType} (h : HasPolynomialTypeF O F σ) :347    HasPolynomialType O F σ :=348  let ⟨gs, h1, h2, hF, hσ, _⟩ := h; ⟨gs, h1, h2, hF, hσ⟩349 350/-- For separable `F` the route-F and original polynomial types agree: every factor is351separable, so its closure is finite by `closure_finite_of_separable`. -/352theorem hasPolynomialTypeF_iff_of_separable (O : Type) [CommRing O] [IsDomain O]353    [IsDiscreteValuationRing O] {F : (BaseField O)[X]} {σ : FactorType} (hs : F.Separable) :354    HasPolynomialTypeF O F σ ↔ HasPolynomialType O F σ :=355  ⟨HasPolynomialTypeF.to_original, fun ⟨gs, h1, h2, hF, hσ⟩ => ⟨gs, h1, h2, hF, hσ, fun g hg =>356    closure_finite_of_separable O g (h1 g hg).2 (hs.of_dvd (hF ▸ List.dvd_prod hg))⟩⟩357 358/-! ### Polynomial types -/359 360section TypeDvd361 362open UniqueFactorizationMonoid363 364open scoped Classical in365/-- A squarefree monic polynomial whose irreducible factors have finite closures has a type. -/366theorem squarefree_monic_has_polynomial_type (O : Type) [CommRing O] [IsDomain O]367    (F : Polynomial (BaseField O)) (hF : F.Monic) (hsq : Squarefree F)368    (hfin : ∀ g ∈ normalizedFactors F, Module.Finite O (integralClosure O (AdjoinRoot g))) :369    ∃ σ : FactorType, HasPolynomialTypeF O F σ := by370  have h0 : F ≠ 0 := hF.ne_zero371  have hmon : ∀ g ∈ normalizedFactors F, g.Monic := fun g hg ↦ by372    rw [← normalize_normalized_factor g hg]373    exact monic_normalize (irreducible_of_normalized_factor g hg).ne_zero374  have hprod : (normalizedFactors F).toList.prod = F := by375    rw [Multiset.prod_toList]376    exact eq_of_monic_of_associated (by simpa using monic_multiset_prod_of_monic _ id hmon) hF377      (prod_normalizedFactors h0)378  refine ⟨_, (normalizedFactors F).toList, fun g hg ↦ ?_, ?_, hprod.symm, rfl,379    fun g hg ↦ hfin g (Multiset.mem_toList.1 hg)⟩380  · rw [Multiset.mem_toList] at hg381    exact ⟨hmon g hg, irreducible_of_normalized_factor g hg⟩382  · change List.Nodup _383    rw [← Multiset.coe_nodup, Multiset.coe_toList]384    exact (squarefree_iff_nodup_normalizedFactors h0).1 hsq385 386/-- A monic divisor of a polynomial with a type has a type. -/387theorem polynomial_type_dvd (O : Type) [CommRing O] [IsDomain O]388    (F G : Polynomial (BaseField O)) (σ : FactorType)389    (hF : HasPolynomialTypeF O F σ) (hG : G.Monic) (hdvd : G ∣ F) :390    ∃ τ : FactorType, HasPolynomialTypeF O G τ := by391  classical392  obtain ⟨gs, hgs, hpw, rfl, -, hfin⟩ := hF393  have hNF : normalizedFactors gs.prod = (gs : Multiset _) := by394    rw [← Multiset.prod_coe, normalizedFactors_prod_eq _ fun g hg ↦ (hgs g hg).2]395    exact (Multiset.map_congr rfl fun g hg ↦ (hgs g hg).1.normalize_eq_self).trans396      (Multiset.map_id _)397  have hF0 : gs.prod ≠ 0 := fun h0 ↦ (hgs 0 (List.prod_eq_zero_iff.1 h0)).2.ne_zero rfl398  have hle : normalizedFactors G ≤ (gs : Multiset _) :=399    hNF ▸ (dvd_iff_normalizedFactors_le_normalizedFactors hG.ne_zero hF0).1 hdvd400  exact squarefree_monic_has_polynomial_type O G hG401    ((squarefree_iff_nodup_normalizedFactors hG.ne_zero).2402      (Multiset.nodup_of_le hle (Multiset.coe_nodup.2 hpw)))403    fun g hg ↦ hfin g (Multiset.mem_coe.1 (Multiset.mem_of_le hle hg))404 405end TypeDvd406 407/-! ### Algebra types -/408 409/-- Algebra types are invariant under `O`-algebra isomorphism. -/410theorem algebra_type_algEquiv (O : Type) [CommRing O] [IsDomain O] (B B' : Type) [CommRing B]411    [CommRing B'] [Algebra O B] [Algebra O B'] (e : B ≃ₐ[O] B') (σ : FactorType)412    (h : HasAlgebraType O B σ) : HasAlgebraType O B' σ := by413  obtain ⟨ι, hι, L, hF, hA, hA2, hT, hD, e₀, hσ⟩ := h414  exact ⟨ι, hι, L, hF, hA, hA2, hT, hD,415    (Algebra.TensorProduct.congr AlgEquiv.refl e).symm.trans e₀, hσ⟩416 417/-- Algebra types only depend on the generic fibre: an isomorphism `K ⊗_O A ≃ K ⊗_O B` transports418the type of `B` to `A`. -/419theorem algebra_type_of_generic_fibre_equiv (O : Type) [CommRing O] [IsDomain O] (A B : Type)420    [CommRing A] [Algebra O A] [CommRing B] [Algebra O B]421    (e : TensorProduct O (BaseField O) A ≃ₐ[BaseField O] TensorProduct O (BaseField O) B)422    (σ : FactorType) (h : HasAlgebraType O B σ) : HasAlgebraType O A σ := by423  obtain ⟨ι, i1, L, i2, i3, i4, i5, i6, g, hg⟩ := h424  exact ⟨ι, i1, L, i2, i3, i4, i5, i6, e.trans g, hg⟩425 426/-- The type of a finite product of algebras is the sum of their types. -/427theorem algebra_type_pi (O : Type) [CommRing O] [IsDomain O] (n : ℕ) (B : Fin n → Type)428    [∀ j, CommRing (B j)] [∀ j, Algebra O (B j)] (σ : Fin n → FactorType)429    (h : ∀ j, HasAlgebraType O (B j) (σ j)) : HasAlgebraType O (∀ j, B j) (∑ j, σ j) := by430  choose ι hι L hF hKL hOL hST hFD e hσ using h431  let K := BaseField O432  let Lp : (Σ j, ι j) → Type := fun p ↦ L p.1 p.2433  let c : (∀ p : (Σ j, ι j), Lp p) ≃ₐ[K] ∀ j, ∀ i, L j i :=434    { toEquiv := Equiv.piCurry (fun j i ↦ L j i)435      map_mul' := fun _ _ ↦ rfl436      map_add' := fun _ _ ↦ rfl437      commutes' := fun _ ↦ rfl }438  refine ⟨Σ j, ι j, inferInstance, Lp, fun p ↦ hF p.1 p.2, fun p ↦ hKL p.1 p.2,439    fun p ↦ hOL p.1 p.2, fun p ↦ hST p.1 p.2, fun p ↦ hFD p.1 p.2,440    ((Algebra.TensorProduct.piRight O K K B).trans (AlgEquiv.piCongrRight e)).trans c.symm,441    ?_, fun p ↦ (hσ p.1).2 p.2⟩442  rw [Fintype.sum_sigma]443  exact Finset.sum_congr rfl fun j _ ↦ (hσ j).1444 445/-! ### Integral closures in finite extensions -/446 447/-- An `O`-algebra isomorphism `L ≃ L'` restricts to the integral closures of `O`. -/448theorem integral_closure_algEquiv (O L L' : Type) [CommRing O] [CommRing L] [CommRing L']449    [Algebra O L] [Algebra O L'] (e : L ≃ₐ[O] L') :450    ∃ φ : integralClosure O L ≃ₐ[O] integralClosure O L',451      ∀ x : integralClosure O L, (φ x : L') = e x :=452  ⟨(e.subalgebraMap (integralClosure O L)).trans453    (Subalgebra.equivOfEq _ _ (integralClosure_map_algEquiv e)), fun _ ↦ rfl⟩454 455/-- If the integral closure of a DVR `O` in a finite extension `L/K` is finite over `O`, it is456free of rank `[L : K]`. -/457theorem integral_closure_finite_free (O K L : Type) [CommRing O] [IsDomain O]Standard facts458    [IsDiscreteValuationRing O] [Field K] [Algebra O K] [IsFractionRing O K] [Field L]459    [Algebra K L] [Algebra O L] [IsScalarTower O K L] [FiniteDimensional K L]460    [hfin : Module.Finite O (integralClosure O L)] :461    Module.Finite O (integralClosure O L) ∧ Module.Free O (integralClosure O L) ∧462      Module.finrank O (integralClosure O L) = Module.finrank K L := by463  have := faithfulSMul_of_isFractionRing O K L464  have : Module.IsTorsionFree O L := .trans_faithfulSMul O K L465  have : Module.IsTorsionFree O (integralClosure O L) := IsIntegralClosure.isTorsionFree O L466  have : IsNoetherian O (integralClosure O L) := isNoetherian_of_isNoetherianRing_of_finite _ _467  refine ⟨hfin, inferInstance, ?_⟩468  have : IsLocalization (Algebra.algebraMapSubmonoid (integralClosure O L) (nonZeroDivisors O)) L :=469    IsIntegralClosure.isLocalization O K L (integralClosure O L)470  rw [Module.finrank_eq_card_chooseBasisIndex, Module.finrank_eq_card_basis471    (Module.Basis.localizationLocalization K (nonZeroDivisors O) L472      (Module.Free.chooseBasis O (integralClosure O L)))]473 474/-- Over a complete DVR with finite residue field, if the (finite) integral closure of `O` in475`L` is local, its ramification index and inertia degree are positive with `e · f = [L : K]`. -/476theorem integral_closure_invariants_degree (O K L : Type) [CommRing O] [IsDomain O]477    [IsDiscreteValuationRing O] [Field K] [Algebra O K] [IsFractionRing O K] [Field L] [Algebra K L]478    [Algebra O L] [IsScalarTower O K L] [FiniteDimensional K L]479    [Module.Finite O (integralClosure O L)] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]480    [Finite (IsLocalRing.ResidueField O)] (hlocal : IsLocalRing (integralClosure O L)) :481    letI : IsLocalRing (integralClosure O L) := hlocal;482      0 < (IsLocalRing.maximalIdeal (integralClosure O L)).ramificationIdx O ∧483      0 < (IsLocalRing.maximalIdeal (integralClosure O L)).inertiaDeg O ∧484      (IsLocalRing.maximalIdeal (integralClosure O L)).ramificationIdx O *485        (IsLocalRing.maximalIdeal (integralClosure O L)).inertiaDeg O = Module.finrank K L := by486  obtain ⟨-, _, hrank⟩ := integral_closure_finite_free O K L487  refine ⟨Ideal.ramificationIdx_pos _ _, Ideal.inertiaDeg_pos _ _, ?_⟩488  rw [finite_flat_local_ramification_degree O (integralClosure O L), hrank]489 490/-- The integral closure of a DVR `O` in a finite extension of `K = Frac O`, assumed finite over491`O`, is not a field. -/492theorem integral_closure_not_field (O K L : Type) [CommRing O] [IsDomain O]493    [IsDiscreteValuationRing O] [Field K] [Algebra O K] [IsFractionRing O K] [Field L]494    [Algebra K L] [Algebra O L] [IsScalarTower O K L] [FiniteDimensional K L]495    [Module.Finite O (integralClosure O L)] : ¬ IsField (integralClosure O L) := fun h ↦ by496  have := faithfulSMul_of_isFractionRing O K L497  exact IsDiscreteValuationRing.not_isField O (isField_of_isIntegral_of_isField498    (fun a b hab ↦ FaithfulSMul.algebraMap_injective O L (congrArg Subtype.val hab)) h)499 500/-- The maximal ideals of a finite product of fields `∏ Lᵢ` are exactly the kernels of the501projections, and distinct projections have distinct kernels. -/502theorem pi_field_maximal_ideals (ι : Type) [Finite ι] (L : ι → Type) [∀ i, Field (L i)]503    (m : Ideal (∀ i, L i)) :504    (m.IsMaximal ↔ ∃ i, m = RingHom.ker (Pi.evalRingHom L i)) ∧ ∀ i j : ι,505      RingHom.ker (Pi.evalRingHom L i) = RingHom.ker (Pi.evalRingHom L j) → i = j := by506  have := Fintype.ofFinite ι507  classical508  have hmax : ∀ i, (RingHom.ker (Pi.evalRingHom L i)).IsMaximal := fun i ↦509    RingHom.ker_isMaximal_of_surjective _ (Function.surjective_eval i)510  refine ⟨⟨fun hm ↦ ?_, fun ⟨i, hi⟩ ↦ hi ▸ hmax i⟩, fun i j h ↦ ?_⟩511  · obtain ⟨i, hi⟩ : ∃ i, (Pi.single i (1 : L i) : ∀ i, L i) ∉ m := by512      by_contra! hc513      apply hm.ne_top514      rw [Ideal.eq_top_iff_one, show (1 : ∀ i, L i) = ∑ i, Pi.single i (1 : L i) by515        ext k; simp [Finset.sum_apply]]516      exact Ideal.sum_mem _ fun i _ ↦ hc i517    refine ⟨i, ((hmax i).eq_of_le hm.ne_top fun x (hx : x i = 0) ↦ ?_).symm⟩518    have hxe : x = ∑ j ∈ Finset.univ.erase i, x * (Pi.single j (1 : L j) : ∀ i, L i) := by519      ext k520      rw [← Finset.mul_sum, Pi.mul_apply, Finset.sum_apply]521      by_cases hk : k = i522      · subst hk; simp [hx]523      · rw [Finset.sum_eq_single k]524        · simp525        · intro b _ hb; simp [hb]526        · simp [hk]527    rw [hxe]528    refine Ideal.sum_mem _ fun j hj ↦ Ideal.mul_mem_left _ _ ?_529    have h0 : (Pi.single i (1 : L i) : ∀ i, L i) * Pi.single j (1 : L j) = 0 := by530      ext k; by_cases hk : k = i531      · subst hk; simp [Ne.symm (Finset.ne_of_mem_erase hj)]532      · simp [hk]533    exact (hm.isPrime.mem_or_mem (h0 ▸ m.zero_mem)).resolve_left hi534  · by_contra hij535    have : (Pi.single j (1 : L j) : ∀ i, L i) ∈ RingHom.ker (Pi.evalRingHom L i) := by536      simp [RingHom.mem_ker, Ne.symm hij]537    simp [h, RingHom.mem_ker] at this538 539/-! ### Unramified base change -/540 541/-- For a finite free extension of DVRs `O → Oδ` of rank `δ` in which a uniformizer stays542irreducible, `K ⊗_O Oδ` is a field of degree `δ` over `K` and a fraction field of `Oδ`. -/543theorem unramified_fraction_base_change (O Oδ : Type) [CommRing O] [IsDomain O]544    [IsDiscreteValuationRing O] [CommRing Oδ] [IsDomain Oδ] [IsDiscreteValuationRing Oδ]545    [Algebra O Oδ] [Module.Finite O Oδ] [Module.Free O Oδ] (δ : ℕ) (hrank : Module.finrank O Oδ = δ)546    (pi : O) (hpi : Irreducible pi) (hpiδ : Irreducible (algebraMap O Oδ pi)) :547    IsField (TensorProduct O (BaseField O) Oδ) ∧ Module.finrank (BaseField O)548      (TensorProduct O (BaseField O) Oδ) = δ549      ∧ (letI : Algebra Oδ (TensorProduct O (BaseField O) Oδ) := Algebra.TensorProduct.rightAlgebra;550        IsFractionRing Oδ (TensorProduct O (BaseField O) Oδ)) := by551  have hinj : Function.Injective (algebraMap O Oδ) := by552    rw [injective_iff_map_eq_zero]553    intro x hx554    by_contra hx0555    obtain ⟨k, u, rfl⟩ := IsDiscreteValuationRing.eq_unit_mul_pow_irreducible hx0 hpi556    rw [map_mul, map_pow] at hx557    rcases mul_eq_zero.mp hx with h | h558    · exact (Units.map (algebraMap O Oδ : O →* Oδ) u).ne_zero h559    · exact hpiδ.ne_zero (pow_eq_zero_iff'.mp h).1560  let : Algebra Oδ (TensorProduct O (BaseField O) Oδ) := Algebra.TensorProduct.rightAlgebra561  have hle : Algebra.algebraMapSubmonoid Oδ (nonZeroDivisors O) ≤ nonZeroDivisors Oδ := by562    rintro _ ⟨a, ha, rfl⟩563    exact mem_nonZeroDivisors_of_ne_zero564      ((map_ne_zero_iff _ hinj).mpr (nonZeroDivisors.ne_zero ha))565  have : IsDomain (TensorProduct O (BaseField O) Oδ) :=566    IsLocalization.isDomain_of_le_nonZeroDivisors (TensorProduct O (BaseField O) Oδ) hle567  have hfield : IsField (TensorProduct O (BaseField O) Oδ) :=568    isField_of_isIntegral_of_isField' (R := BaseField O) (Field.toIsField _)569  refine ⟨hfield, by rw [Module.finrank_baseChange, hrank], ?_⟩570  let := hfield.toField571  have : FaithfulSMul Oδ (TensorProduct O (BaseField O) Oδ) :=572    (faithfulSMul_iff_algebraMap_injective _ _).mpr (IsLocalization.injective _ hle)573  refine IsFractionRing.of_field _ _ fun z ↦ ?_574  obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalization.mk'_surjective575    (Algebra.algebraMapSubmonoid Oδ (nonZeroDivisors O)) z576  refine ⟨x, s, (eq_div_iff ?_).2 (IsLocalization.mk'_spec _ x s)⟩577  exact (map_ne_zero_iff _ (IsLocalization.injective _ hle)).mpr (nonZeroDivisors.ne_zero (hle s.2))578 579/-- In the unramified situation of `unramified_fraction_base_change`, a presentation of the580`Oδ`-generic fibre of an `Oδ`-algebra `B` as a product of fields `Lᵢ` induces compatible581`K`- and `O`-structures on the `Lᵢ` and a presentation of the `O`-generic fibre of `B`. -/582theorem unramified_generic_fibre_witness (O Oδ : Type) [CommRing O] [IsDomain O]583    [IsDiscreteValuationRing O] [CommRing Oδ] [IsDomain Oδ] [IsDiscreteValuationRing Oδ]584    [Algebra O Oδ] [Module.Finite O Oδ] [Module.Free O Oδ] (δ : ℕ) (hrank : Module.finrank O Oδ = δ)585    (pi : O) (hpi : Irreducible pi) (hpiδ : Irreducible (algebraMap O Oδ pi))586    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)] (B : Type)587    [CommRing B] [Algebra O B] [Algebra Oδ B] [IsScalarTower O Oδ B] (ι : Type)588    (L : ι → Type) [∀ i, Field (L i)] [∀ i, Algebra (BaseField Oδ) (L i)] [∀ i, Algebra Oδ (L i)]589    [∀ i, IsScalarTower Oδ (BaseField Oδ) (L i)] [∀ i, FiniteDimensional (BaseField Oδ) (L i)]590    (e : TensorProduct Oδ (BaseField Oδ) B ≃ₐ[BaseField Oδ] (∀ i, L i)) :591    ∃ (_ : ∀ i, Algebra (BaseField O) (L i)) (_ : ∀ i, Algebra O (L i))592      (_ : ∀ i, IsScalarTower O (BaseField O) (L i)) (_ : ∀ i, IsScalarTower O Oδ (L i))593      (_ : ∀ i, FiniteDimensional (BaseField O) (L i))594      (_ : TensorProduct O (BaseField O) B ≃ₐ[BaseField O] (∀ i, L i)), True := by595  obtain ⟨-, -, hfr⟩ := unramified_fraction_base_change O Oδ δ hrank pi hpi hpiδ596  let K := BaseField O597  let Kδ := BaseField Oδ598  let rA : Algebra Oδ (K ⊗[O] Oδ) := Algebra.TensorProduct.rightAlgebra599  have : IsFractionRing Oδ (K ⊗[O] Oδ) := hfr600  let χ : K ⊗[O] Oδ ≃ₐ[Oδ] Kδ := IsLocalization.algEquiv (nonZeroDivisors Oδ) (K ⊗[O] Oδ) Kδ601  let χ' : Oδ ⊗[O] K ≃ₐ[Oδ] Kδ :=602    AlgEquiv.ofRingEquiv (f := (Algebra.TensorProduct.comm O Oδ K).toRingEquiv.trans χ.toRingEquiv)603      fun d ↦ χ.commutes d604  let φ : K →+* Kδ := χ.toRingHom.comp Algebra.TensorProduct.includeLeftRingHom605  let aKKδ : Algebra K Kδ := φ.toAlgebra606  have : Module.Finite K Kδ := .equiv607    { χ.toRingEquiv with608      map_smul' := fun k x ↦ by609        change χ (k • x) = φ k * χ x610        rw [Algebra.smul_def (R := K) k x, map_mul]611        rfl : K ⊗[O] Oδ ≃ₗ[K] Kδ }612  let E : K ⊗[O] B ≃+* (∀ i, L i) :=613    (Algebra.TensorProduct.comm O K B).toRingEquiv.trans <|614    (Algebra.TensorProduct.cancelBaseChange O Oδ Oδ B K).symm.toRingEquiv.trans <|615    (Algebra.TensorProduct.congr (AlgEquiv.refl (R := Oδ) (A₁ := B)) χ').toRingEquiv.trans <|616    (Algebra.TensorProduct.comm Oδ B Kδ).toRingEquiv.trans e.toRingEquiv617  let aK : ∀ i, Algebra K (L i) := fun i ↦ ((algebraMap Kδ (L i)).comp φ).toAlgebra618  let aO : ∀ i, Algebra O (L i) := fun i ↦619    ((algebraMap Oδ (L i)).comp (algebraMap O Oδ)).toAlgebra620  have : ∀ i, IsScalarTower K Kδ (L i) := fun i ↦ .of_algebraMap_eq' rfl621  have t2 : ∀ i, IsScalarTower O Oδ (L i) := fun i ↦ .of_algebraMap_eq' rfl622  have t3 : ∀ i, IsScalarTower O K (L i) := fun i ↦ .of_algebraMap_eq fun c ↦ by623    change algebraMap Oδ (L i) (algebraMap O Oδ c) =624      algebraMap Kδ (L i) (χ (algebraMap O K c ⊗ₜ[O] 1))625    have h1 : algebraMap O K c ⊗ₜ[O] (1 : Oδ) = algebraMap Oδ (K ⊗[O] Oδ) (algebraMap O Oδ c) := by626      change _ = (1 : K) ⊗ₜ[O] algebraMap O Oδ c627      rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, TensorProduct.smul_tmul]628    rw [h1, χ.commutes]629    exact IsScalarTower.algebraMap_apply Oδ Kδ (L i) _630  refine ⟨aK, aO, t3, t2, fun i ↦ Module.Finite.trans Kδ (L i),631    AlgEquiv.ofRingEquiv (f := E) fun x ↦ ?_, trivial⟩632  funext i633  change e (Algebra.TensorProduct.comm Oδ B Kδ634    (Algebra.TensorProduct.congr (AlgEquiv.refl (R := Oδ) (A₁ := B)) χ'635      ((Algebra.TensorProduct.cancelBaseChange O Oδ Oδ B K).symm ((1 : B) ⊗ₜ[O] x)))) i =636    algebraMap Kδ (L i) (χ (x ⊗ₜ[O] 1))637  rw [Algebra.TensorProduct.cancelBaseChange_symm_tmul]638  simp only [Algebra.TensorProduct.congr_apply, Algebra.TensorProduct.map_tmul,639    AlgEquiv.coe_toAlgHom, Algebra.TensorProduct.comm_tmul]640  change e (algebraMap Kδ (Kδ ⊗[Oδ] B) (χ (x ⊗ₜ[O] 1))) i = _641  rw [e.commutes]642  rfl643 644end SurfaceBlowup