Finite separable extensions of a discrete valuation ring, with a chosen place

Let R be a discrete valuation ring with fraction field K. A TauCeti.FiniteDVRExtension R K records a finite separable extension K' of K together with a chosen place of K' above the closed point of R: the integral closure C of R in K', a maximal ideal 𝔪' of C lying over the maximal ideal of R, and a ring R' presented as the localization of C at 𝔪'.

The choice is genuine data. The integral closure C is in general semilocal rather than local, so C is not itself a discrete valuation ring, and the valuation of R extends to K' in as many ways as C has maximal ideals; the package fixes one such extension. Accordingly R' is not required to be Localization.AtPrime 𝔪' on the nose: it is any ring carrying IsLocalization.AtPrime, so that a package can be assembled from whichever model of the local ring is already at hand.

The package carries only what is not forced: the two type-valued carriers, the algebra maps that relate them, the chosen ideal, and the Ideal.LiesOver witness pinning it above the closed point of R. That R' is a discrete valuation ring with fraction field K' dominating R is proved here rather than assumed. Domination in particular makes algebraMap R R' an IsLocalHom, which is what lets Mathlib's residue-field machinery view the residue field of R' as an extension of that of R.

Main definitions

• TauCeti.FiniteDVRExtension: the package described above.
• TauCeti.FiniteDVRExtension.integralClosure: the integral closure of R in the extension field, the ring the chosen place is an ideal of.
• TauCeti.FiniteDVRExtension.of: the package attached to a maximal ideal of that integral closure lying over the maximal ideal of R, with Localization.AtPrime as its local ring.

Main results

• TauCeti.FiniteDVRExtension.isDiscreteValuationRing_localRing: the chosen local ring is a discrete valuation ring.
• TauCeti.FiniteDVRExtension.isFractionRing_localRing: its fraction field is the extension field.
• TauCeti.FiniteDVRExtension.under_prime: the chosen place lies over the closed point of R.
• TauCeti.FiniteDVRExtension.isLocalHom_algebraMap and TauCeti.FiniteDVRExtension.under_maximalIdeal_localRing: the chosen local ring dominates R.
• TauCeti.FiniteDVRExtension.exists_algEquiv_extensionField: every finite separable extension of K is, as a K-algebra, the extension field of such a package, for some place above the closed point of R; to fix a specified place, use TauCeti.FiniteDVRExtension.of.

References

The mathematics is standard; Q. Liu, Algebraic Geometry and Arithmetic Curves, covers reduction of curves over a discrete valuation ring.

structure TauCeti.FiniteDVRExtension (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] : Type (u + 1)

A finite separable extension of the fraction field K of a discrete valuation ring R, together with a chosen place of that extension above the closed point of R.

The place is recorded as a maximal ideal prime of the integral closure of R in the extension field, lying over the maximal ideal of R, together with a ring localRing presented as the localization there. See TauCeti.FiniteDVRExtension.of for the construction from such an ideal and TauCeti.FiniteDVRExtension.exists_algEquiv_extensionField for the fact that one always exists.

• extensionField : Type u

  The extension field K' of K.

• extensionFieldInst : Field self.extensionField
• extensionAlgebra : Algebra K self.extensionField
• extensionFinite : FiniteDimensional K self.extensionField
• extensionSeparable : Algebra.IsSeparable K self.extensionField
• extensionBaseAlgebra : Algebra R self.extensionField
• extensionTower : IsScalarTower R K self.extensionField
• prime : Ideal ↥(_root_.integralClosure R self.extensionField)

  The chosen place of K', as a maximal ideal of the integral closure of R in K'.

• prime_isMaximal : self.prime.IsMaximal
• prime_liesOver : self.prime.LiesOver (IsLocalRing.maximalIdeal R)
• localRing : Type u

  The local ring R' of the chosen place.

• localRingInst : CommRing self.localRing
• localRingClosureAlgebra : Algebra (↥(_root_.integralClosure R self.extensionField)) self.localRing
• localRingIsLocalization : IsLocalization.AtPrime self.localRing self.prime
• localRingAlgebra : Algebra R self.localRing
• localRingTower : IsScalarTower R (↥(_root_.integralClosure R self.extensionField)) self.localRing
• fractionAlgebra : Algebra self.localRing self.extensionField
• fractionTower : IsScalarTower (↥(_root_.integralClosure R self.extensionField)) self.localRing self.extensionField

@[reducible, inline]

abbrev TauCeti.FiniteDVRExtension.integralClosure {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : Type u

The integral closure of R in the extension field: the ring the chosen place is an ideal of.

Equations

• E.integralClosure = ↥(integralClosure R E.extensionField)

instance TauCeti.FiniteDVRExtension.isFractionRing_integralClosure {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : IsFractionRing E.integralClosure E.extensionField

instance TauCeti.FiniteDVRExtension.isDedekindDomain_integralClosure {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : IsDedekindDomain E.integralClosure

instance TauCeti.FiniteDVRExtension.isNoetherian_integralClosure {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : IsNoetherian R E.integralClosure

The integral closure C of R in K' is a Noetherian R-module: it is a finite R-module, because K' is a finite separable extension of the fraction field of the Noetherian integrally closed domain R.

instance TauCeti.FiniteDVRExtension.faithfulSMul_extensionField {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : FaithfulSMul R E.extensionField

instance TauCeti.FiniteDVRExtension.faithfulSMul_integralClosure {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : FaithfulSMul R E.integralClosure

@[simp]

theorem TauCeti.FiniteDVRExtension.under_prime {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : Ideal.under R E.prime = IsLocalRing.maximalIdeal R

The chosen place lies above the closed point of R, spelled as a contraction of ideals.

theorem TauCeti.FiniteDVRExtension.prime_ne_bot {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : E.prime ≠ ⊥

The chosen place is a nonzero prime: it lies over the maximal ideal of R, which is nonzero because a discrete valuation ring is not a field.

instance TauCeti.FiniteDVRExtension.isDomain_localRing {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : IsDomain E.localRing

instance TauCeti.FiniteDVRExtension.isFractionRing_localRing {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : IsFractionRing E.localRing E.extensionField

The extension field is the fraction field of the chosen localized ring.

instance TauCeti.FiniteDVRExtension.isDiscreteValuationRing_localRing {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : IsDiscreteValuationRing E.localRing

The local ring of the chosen place is a discrete valuation ring: it is the localization of the Dedekind domain C at the nonzero prime 𝔪'.

instance TauCeti.FiniteDVRExtension.isScalarTower_localRing {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : IsScalarTower R E.localRing E.extensionField

instance TauCeti.FiniteDVRExtension.faithfulSMul_localRing {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : FaithfulSMul R E.localRing

@[simp]

theorem TauCeti.FiniteDVRExtension.under_maximalIdeal_integralClosure {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : Ideal.under E.integralClosure (IsLocalRing.maximalIdeal E.localRing) = E.prime

The maximal ideal of the local ring of the chosen place contracts to the chosen place.

instance TauCeti.FiniteDVRExtension.isLocalHom_algebraMap {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : IsLocalHom (algebraMap R E.localRing)

The local ring of the chosen place dominates R.

@[simp]

theorem TauCeti.FiniteDVRExtension.under_maximalIdeal_localRing {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : Ideal.under R (IsLocalRing.maximalIdeal E.localRing) = IsLocalRing.maximalIdeal R

Domination spelled as a contraction of ideals: the closed point of Spec R' lies over the closed point of Spec R.

noncomputable def TauCeti.FiniteDVRExtension.of (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : FiniteDVRExtension R K

The finite extension of the discrete valuation ring R cut out by a maximal ideal P of the integral closure C of R in a finite separable extension L of K, provided P lies above the maximal ideal of R. Its local ring is Localization.AtPrime P.

The map from that local ring to L is Mathlib's canonical comparison IsLocalization.localizationAlgebraOfSubmonoidLe between the localizations of C at the two submonoids P.primeCompl ≤ nonZeroDivisors C, the second localization being L itself because L is the fraction field of C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FiniteDVRExtension.of_extensionField (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : (of R K L P).extensionField = L

@[simp]

theorem TauCeti.FiniteDVRExtension.of_prime (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : (of R K L P).prime ≍ P

@[simp]

theorem TauCeti.FiniteDVRExtension.of_localRing (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : (of R K L P).localRing = Localization.AtPrime P

@[simp]

theorem TauCeti.FiniteDVRExtension.of_extensionFieldInst (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : (of R K L P).extensionFieldInst ≍ inferInstance

@[simp]

theorem TauCeti.FiniteDVRExtension.of_localRingInst (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : (of R K L P).localRingInst ≍ inferInstance

@[simp]

theorem TauCeti.FiniteDVRExtension.of_extensionAlgebra (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : (of R K L P).extensionAlgebra ≍ inferInstance

@[simp]

theorem TauCeti.FiniteDVRExtension.of_extensionBaseAlgebra (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : (of R K L P).extensionBaseAlgebra ≍ inferInstance

@[simp]

theorem TauCeti.FiniteDVRExtension.of_localRingClosureAlgebra (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : (of R K L P).localRingClosureAlgebra ≍ inferInstance

@[simp]

theorem TauCeti.FiniteDVRExtension.of_localRingAlgebra (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : (of R K L P).localRingAlgebra ≍ inferInstance

@[simp]

theorem TauCeti.FiniteDVRExtension.of_fractionAlgebra (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : (of R K L P).fractionAlgebra ≍ IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.AtPrime P) L P.primeCompl (nonZeroDivisors ↥(_root_.integralClosure R L)) ⋯

theorem TauCeti.FiniteDVRExtension.exists_algEquiv_comap_prime_eq (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] (P : Ideal ↥(_root_.integralClosure R L)) [P.IsPrime] [P.LiesOver (IsLocalRing.maximalIdeal R)] : ∃ (e : (of R K L P).extensionField ≃ₐ[K] L), Ideal.comap (AlgHom.restrictScalars R ↑e.symm).mapIntegralClosure (of R K L P).prime = P

The algebra-level refinement of TauCeti.FiniteDVRExtension.of_extensionField and TauCeti.FiniteDVRExtension.of_prime: the extension field of the package cut out by P is L itself as a K-algebra, not merely as a type, and along that identification the chosen prime of the package pulls back to P.

theorem TauCeti.FiniteDVRExtension.exists_algEquiv_extensionField (R K : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [Algebra R L] [IsScalarTower R K L] : ∃ (E : FiniteDVRExtension R K), Nonempty (E.extensionField ≃ₐ[K] L)

Every finite separable extension L of K underlies a FiniteDVRExtension R K: the integral closure of R in L is integral over R, so going up produces a maximal ideal above the maximal ideal of R, and any such ideal cuts out a package whose extension field is L as a K-algebra.

instance TauCeti.FiniteDVRExtension.instNonempty {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] : Nonempty (FiniteDVRExtension R K)

The trivial extension exists: K itself is a finite separable extension of K, and R is already local, so FiniteDVRExtension R K is never empty.