Module

IsDiscreteValuationRing_exists_finite_locallyPrincipalOverring.lean

Nyll.AlgebraicCurves.Valuations.IsDiscreteValuationRing_exists_finite_locallyPrincipalOverring

3 declarations indexed from sourceView source ↗

Module documentation

Is Discrete Valuation Ring exists finite locally Principal Overring

Imports11

Batteries.Tactic.Init
Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.DedekindDomain.PID
Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
Mathlib.RingTheory.Algebraic.Integral
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Mathlib.Tactic.Set
Mathlib.Tactic.Push
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.Ring

Imported by2

theorem

isPrincipalIdealRing_integralClosure

L46 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_exists_finite_locallyPrincipalOverring.R1AF8H3.isPrincipalIdealRing_integralClosure

Documentation

The integral closure of a DVR in a finite separable extension is a principal ideal ring.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_exists_finite_locallyPrincipalOverring
open IsLocalRing Polynomial
namespace R1AF8H3
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
  (K₀ : Type*) [Field K₀] [Algebra C K₀] [IsFractionRing C K₀]
  {κ : Type*} [Field κ] [Algebra K₀ κ] [Algebra C κ] [IsScalarTower C K₀ κ] [FiniteDimensional K₀ κ]
  [Algebra.IsSeparable K₀ κ]
  {A : Type*} [CommRing A] [Algebra C A] [Algebra A κ] [IsScalarTower C A κ]
include K₀ in

Lean source · statement

theorem isPrincipalIdealRing_integralClosure : IsPrincipalIdealRing (integralClosure C κ)

theorem

exists_subalgebra_finite_locallyPrincipal

L68 ↗

AlgebraicCurves.Valuations.Proofs.IsDiscreteValuationRing_exists_finite_locallyPrincipalOverring.R1AF8H3.exists_subalgebra_finite_locallyPrincipal

Documentation

A finite subalgebra containing the integral closure is principal after localization at each maximal ideal.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_exists_finite_locallyPrincipalOverring
open IsLocalRing Polynomial
namespace R1AF8H3
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
  (K₀ : Type*) [Field K₀] [Algebra C K₀] [IsFractionRing C K₀]
  {κ : Type*} [Field κ] [Algebra K₀ κ] [Algebra C κ] [IsScalarTower C K₀ κ] [FiniteDimensional K₀ κ]
  [Algebra.IsSeparable K₀ κ]
  {A : Type*} [CommRing A] [Algebra C A] [Algebra A κ] [IsScalarTower C A κ]
include K₀ in

Lean source · statement

theorem exists_subalgebra_finite_locallyPrincipal :
    ∃ D₁ : Subalgebra A κ, Module.Finite A D₁ ∧ (∀ x : κ, IsIntegral C x → x ∈ D₁) ∧
      ∀ 𝔫 : Ideal D₁, 𝔫.IsMaximal → ∃ t ∈ 𝔫, ∀ x ∈ 𝔫, ∃ s ∉ 𝔫, ∃ y : D₁, s * x = t * y

theorem

exists_finite_locallyPrincipalOverring

L237 ↗

IsDiscreteValuationRing.exists_finite_locallyPrincipalOverring

Documentation

There is a finite overring containing the integral closure that is locally principal at maximal ideals.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace IsDiscreteValuationRing_exists_finite_locallyPrincipalOverring
open IsLocalRing Polynomial

Lean source · statement

theorem _root_.IsDiscreteValuationRing.exists_finite_locallyPrincipalOverring
    {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
    (K₀ : Type*) [Field K₀] [Algebra C K₀] [IsFractionRing C K₀]
    {κ : Type*} [Field κ] [Algebra K₀ κ] [Algebra C κ] [IsScalarTower C K₀ κ] [FiniteDimensional K₀
      κ]
    [Algebra.IsSeparable K₀ κ]
    {A : Type*} [CommRing A] [Algebra C A] [Algebra A κ] [IsScalarTower C A κ] :
    ∃ D₁ : Subalgebra A κ, Module.Finite A D₁ ∧ (∀ x : κ, IsIntegral C x → x ∈ D₁) ∧
      ∀ 𝔫 : Ideal D₁, 𝔫.IsMaximal → ∃ t ∈ 𝔫, ∀ x ∈ 𝔫, ∃ s ∉ 𝔫, ∃ y : D₁, s * x = t * y

Module documentation

Is Discrete Valuation Ring exists finite locally Principal Overring

Declarations

isPrincipalIdealRing_integralClosure

exists_subalgebra_finite_locallyPrincipal

exists_finite_locallyPrincipalOverring