Finite extensions of complete discrete valuation rings

TheoremCompleteness passes to finite extensions of discrete valuation rings#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings, and let \(B\) be an \(A\)-algebra that is finitely generated as an \(A\)-module and whose structure map \(A \to B\) is injective. If \(A\) is complete and Hausdorff for the adic topology of its maximal ideal, then \(B\) is complete and Hausdorff for the adic topology of its maximal ideal.

theorem IsDiscreteValuationRing.isAdicComplete_of_finite_local_extension
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A] :
    IsAdicComplete (IsLocalRing.maximalIdeal B) B

Sources

generalizes integral_closure_isAdicComplete (atlas-lean v1) from the integral closure to any finite faithful extension of DVRs.

Used by 2

Used byFinitely many DVR points with trivial common kernel · The integral closure of a complete DVR is complete

TheoremMaximal ideals contract to the maximal ideal of a complete base#✓fully proved

Let \(A\) and \(B\) be commutative rings with \(B\) an \(A\)-algebra that is integral over \(A\), and let \(\mathfrak p\) be a maximal ideal of \(A\) such that \(A\) is \(\mathfrak p\)-adically complete. Then every maximal ideal \(Q\) of \(B\) has preimage \(\mathfrak p\) under the structure map \(A \to B\).

theorem Ideal.comap_eq_base_maximal_of_isAdicComplete_of_isIntegral
    : Q.comap (algebraMap A B) = p

Used by 1

Used byDomains integral over a complete local domain are local

TheoremDomains integral over a complete local domain are local#✓fully proved

Let \(A\) be an integral domain and \(\mathfrak p\) a maximal ideal of \(A\) such that \(A\) is \(\mathfrak p\)-adically complete. If \(B\) is an integral domain and an \(A\)-algebra that is integral over \(A\), then \(B\) is a local ring.

theorem isLocalRing_of_isIntegral_of_isAdicComplete_maximal
    (p : Ideal A) [p.IsMaximal] [IsAdicComplete p A]
    [IsDomain A] [IsDomain B] : IsLocalRing B

Uses 2 · Used by 1

Proof usesMaximal ideals contract to the maximal ideal of a complete base · Hensel lifting of monic coprime factorizations

Used byThe integral closure of a complete DVR is local

TheoremThe integral closure of a complete DVR is local#✓fully proved

Let \(A\) be a discrete valuation ring that is complete with respect to its maximal ideal, \(K\) its fraction field and \(L\) a finite separable extension of \(K\). Then the integral closure of \(A\) in \(L\) is a local ring.

theorem isLocalRing_of_isAdicComplete
    (A K L B : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L]
    [IsScalarTower A B L] [IsIntegralClosure B A L]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A] : IsLocalRing B

Uses 1 · Used by 3

Proof usesDomains integral over a complete local domain are local

Used byExactly one prime lies over the maximal ideal of a complete DVR · Integral closure of a complete DVR in a separable extension · The integral closure of a complete DVR is a DVR

TheoremThe integral closure of a complete DVR is a DVR#✓fully proved

Let \(A\) be a discrete valuation ring that is complete with respect to its maximal ideal, \(K\) its fraction field and \(L\) a finite separable extension of \(K\). Then the integral closure of \(A\) in \(L\) is a discrete valuation ring.

theorem isDiscreteValuationRing_of_isAdicComplete
    (A K L B : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L]
    [IsScalarTower A B L] [IsIntegralClosure B A L]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A] : IsDiscreteValuationRing B

Uses 1 · Used by 3

Proof usesThe integral closure of a complete DVR is local

Used byIntegral closure of a complete DVR in a separable extension · Valuation rings dominating a complete DVR are integral closures · The integral closure of a complete DVR is complete

TheoremThe integral closure of a complete DVR is complete#✓fully proved

Let \(A\) be a discrete valuation ring that is complete with respect to its maximal ideal, \(K\) its fraction field, \(L\) a finite separable extension of \(K\), and \(B\) the integral closure of \(A\) in \(L\). If \(B\) is local (as it always is here), then \(B\) is complete with respect to its maximal ideal.

theorem isAdicComplete_of_isAdicComplete
    {A K L B : Type*} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L]
    [IsScalarTower A B L] [IsIntegralClosure B A L]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [IsLocalRing B] :
    IsAdicComplete (IsLocalRing.maximalIdeal B) B

Sources

ATLAS integral_closure_isAdicComplete, obtained here from the general completeness theorem for finite local extensions.

Uses 2 · Used by 1

Proof usesCompleteness passes to finite extensions of discrete valuation rings · The integral closure of a complete DVR is a DVR

Used byIntegral closure of a complete DVR in a separable extension

TheoremExactly one prime lies over the maximal ideal of a complete DVR#✓fully proved

Let \(A\) be a discrete valuation ring that is complete with respect to its maximal ideal \(\mathfrak m\), \(K\) its fraction field, \(L\) a finite separable extension of \(K\), and \(B\) the integral closure of \(A\) in \(L\). Then there is exactly one prime ideal of \(B\) whose preimage under \(A \to B\) is \(\mathfrak m\).

theorem existsUnique_primesOver_maximalIdeal_of_isAdicComplete
    (A K L B : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Algebra A K] [IsFractionRing A K]
    [Field L] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L]
    [IsScalarTower A B L] [IsIntegralClosure B A L]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A] :
    ∃! Q : Ideal B, Q ∈ (IsLocalRing.maximalIdeal A).primesOver B

Uses 1 · Used by 1

Proof usesThe integral closure of a complete DVR is local

Used byValuation rings dominating a complete DVR are integral closures

TheoremValuation rings dominating a complete DVR are integral closures#✓fully proved

Let \(A\) be a discrete valuation ring that is complete with respect to its maximal ideal, \(K\) its fraction field, and \(L\) a finite separable extension of \(K\). Let \(v\) be a valuation on \(L\) with values in a linearly ordered commutative group with zero, with valuation ring \(\mathcal O_v = \{x \in L : v(x) \le 1\}\). Suppose \(\mathcal O_v\) is an \(A\)-algebra such that the composite \(A \to \mathcal O_v \subseteq L\) is the structure map \(A \to L\), and \(A \to \mathcal O_v\) is a local homomorphism. Then \(\mathcal O_v\) is the integral closure of \(A\) in \(L\).

theorem integer_isIntegralClosure_of_isAdicComplete
    (A K L Gamma : Type*) [CommRing A] [IsDomain A]
    [IsDiscreteValuationRing A] [Field K] [Algebra A K]
    [IsFractionRing A K] [Field L] [Algebra A L] [Algebra K L]
    [IsScalarTower A K L] [FiniteDimensional K L]
    [Algebra.IsSeparable K L] [LinearOrderedCommGroupWithZero Gamma]
    (v : Valuation L Gamma) [Algebra A ↥v.integer]
    [IsScalarTower A ↥v.integer L]
    [IsLocalHom (algebraMap A ↥v.integer)]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A] :
    IsIntegralClosure ↥v.integer A L

Uses 2 · Used by 1

Proof usesExactly one prime lies over the maximal ideal of a complete DVR · The integral closure of a complete DVR is a DVR

Used byValuation rings dominating a complete DVR are finite over it

TheoremValuation rings dominating a complete DVR are finite over it#✓fully proved

Let \(A\) be a discrete valuation ring that is complete with respect to its maximal ideal, \(K\) its fraction field, and \(L\) a finite separable extension of \(K\). Let \(v\) be a valuation on \(L\) with values in a linearly ordered commutative group with zero, with valuation ring \(\mathcal O_v = \{x \in L : v(x) \le 1\}\). Suppose \(\mathcal O_v\) is an \(A\)-algebra such that the composite \(A \to \mathcal O_v \subseteq L\) is the structure map \(A \to L\), and \(A \to \mathcal O_v\) is a local homomorphism. Then \(\mathcal O_v\) is a finitely generated \(A\)-module.

theorem module_finite_integer_of_isAdicComplete
    (A K L Gamma : Type*) [CommRing A] [IsDomain A]
    [IsDiscreteValuationRing A] [Field K] [Algebra A K]
    [IsFractionRing A K] [Field L] [Algebra A L] [Algebra K L]
    [IsScalarTower A K L] [FiniteDimensional K L]
    [Algebra.IsSeparable K L] [LinearOrderedCommGroupWithZero Gamma]
    (v : Valuation L Gamma) [Algebra A ↥v.integer]
    [IsScalarTower A ↥v.integer L]
    [IsLocalHom (algebraMap A ↥v.integer)]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A] :
    Module.Finite A ↥v.integer

Uses 1 · Used by 1

Proof usesValuation rings dominating a complete DVR are integral closures

Used byThe local degree is the product of ramification index and inertia degree

TheoremIntegral closure of a complete DVR in a separable extension#✓fully proved

The integral closure of a complete discrete valuation ring in a finite separable extension of its fraction field is finite over the base, is a discrete valuation ring, and is complete for its maximal ideal.

theorem integralClosure.finite_and_isDiscreteValuationRing_and_isAdicComplete_maximalIdeal
    (𝒪 : Type*) [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪]
    [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪]
    (L : Type*) [Field L] [Algebra 𝒪 L] [IsFractionRing 𝒪 L]
    (L' : Type*) [Field L'] [Algebra 𝒪 L'] [Algebra L L'] [IsScalarTower 𝒪 L L']
    [FiniteDimensional L L'] [Algebra.IsSeparable L L'] :
    Module.Finite 𝒪 (integralClosure 𝒪 L') ∧
    ∃ _ : IsDiscreteValuationRing (integralClosure 𝒪 L'),
      IsAdicComplete (IsLocalRing.maximalIdeal (integralClosure 𝒪 L'))
        (integralClosure 𝒪 L')

Uses 3

Proof usesThe integral closure of a complete DVR is complete · The integral closure of a complete DVR is a DVR · The integral closure of a complete DVR is local

TheoremFinite domains over adically complete local rings are local#✓fully proved

A finite algebra over an adically complete Noetherian local ring that is a domain is itself local.

theorem of_isDomain_of_module_finite_of_isAdicComplete
    {R : Type u} {S : Type v} [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    [CommRing S] [IsDomain S] [Algebra R S] [Module.Finite R S] : IsLocalRing S

Used by 1

Used byFinitely many DVR points with trivial common kernel

TheoremFinitely many DVR points with trivial common kernel#✓fully proved

A finite torsion-free local reduced algebra over an adically complete DVR with finite residue field and characteristic zero admits finitely many adically complete DVR points whose kernels intersect to ⊥, with a common denominator clearing all denominators.

IsLocalRing.exists_fin_points_dvr_iInf_ker_eq_bot · 15 lines

theorem exists_fin_points_dvr_iInf_ker_eq_bot
    {𝒪 : Type u} {P : Type v} [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪]
    [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] [Finite (IsLocalRing.ResidueField 𝒪)]
    [CharZero 𝒪]
    [CommRing P] [IsLocalRing P] [IsReduced P] [Algebra 𝒪 P] [Module.Finite 𝒪 P]
    [Module.IsTorsionFree 𝒪 P] :
    ∃ (n : ℕ) (A : Fin n → Type v) (_ : ∀ i, CommRing (A i)) (_ : ∀ i, IsDomain (A i))
      (_ : ∀ i, IsDiscreteValuationRing (A i))
      (_ : ∀ i, IsAdicComplete (IsLocalRing.maximalIdeal (A i)) (A i))
      (_ : ∀ i, Finite (IsLocalRing.ResidueField (A i))) (_ : ∀ i, CharZero (A i))
      (_ : ∀ i, Algebra 𝒪 (A i)) (_ : ∀ i, Module.Finite 𝒪 (A i))
      (_ : ∀ i, IsLocalHom (algebraMap 𝒪 (A i)))
      (χ : ∀ i, P →ₐ[𝒪] A i),
      (∀ i, IsLocalHom (χ i).toRingHom) ∧ ⨅ i, RingHom.ker (χ i).toRingHom = ⊥ ∧
        ∃ a : 𝒪, a ≠ 0 ∧ ∀ y : ∀ i, A i, ∃ x : P, ∀ i, χ i x = a • y i

Uses 2

Proof usesCompleteness passes to finite extensions of discrete valuation rings · Finite domains over adically complete local rings are local

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.