Module

Place_exists_of_valuationSubring_of_isSeparable.lean

Nyll.AlgebraicCurves.Places.Place_exists_of_valuationSubring_of_isSeparable

13 declarations indexed from sourceView source ↗

Module documentation

Place exists of valuation Subring of is Separable

Imports7

Nyll.AlgebraicCurves.Divisors.ClassGroup
Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.DedekindDomain.Dvr
Mathlib.RingTheory.DiscreteValuationRing.TFAE
Mathlib.RingTheory.Localization.Integral
Mathlib.RingTheory.Valuation.LocalSubring
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

Imported by3

theorem

isDedekindDomain_Kx

L45 ↗

AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable.isDedekindDomain_Kx

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)
omit [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] in
include hx in

Lean source · statement

theorem isDedekindDomain_Kx : IsDedekindDomain (Kx)

theorem

isDedekindDomain_integralClosure

L56 ↗

AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable.isDedekindDomain_integralClosure

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)
include hx in

Lean source · statement

theorem isDedekindDomain_integralClosure [Algebra.IsSeparable (Kxfield) F] :
    IsDedekindDomain (integralClosure (Kx) F)

theorem

isFractionRing_integralClosure

L61 ↗

AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable.isFractionRing_integralClosure

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)

Lean source · statement

theorem isFractionRing_integralClosure :
    IsFractionRing (integralClosure (Kx) F) F

theorem

Kx_le_A

L66 ↗

AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable.Kx_le_A

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)
omit [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] in
include hxA hAK in

Lean source · statement

theorem Kx_le_A : (Kx).toSubring ≤ A.toSubring

instance

(anonymous instance)

L74 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)

Lean source · statement

instance : IsFractionRing (A : ValuationSubring F).toSubring F

instance

(anonymous instance)

L77 ↗

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)

Lean source · statement

instance : IsFractionRing (A : ValuationSubring F) F

theorem

integralClosure_Kx_le_A

L82 ↗

AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable.integralClosure_Kx_le_A

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)
omit [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] in
include hxA hAK in

Lean source · statement

theorem integralClosure_Kx_le_A :
    (integralClosure (Kx) F).toSubring ≤ A.toSubring

theorem

inv_mem_of_notMem_maximalIdeal

L95 ↗

AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable.inv_mem_of_notMem_maximalIdeal

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)
omit [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] in
include hxA hAK in

Lean source · statement

theorem inv_mem_of_notMem_maximalIdeal {b : integralClosure (Kx) F}
    (hb : Subring.inclusion (integralClosure_Kx_le_A x A hAK hxA) b
        ∉ IsLocalRing.maximalIdeal A) :
    ((b : F))⁻¹ ∈ A

theorem

idealOfA_ne_bot

L107 ↗

AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable.idealOfA_ne_bot

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)
include hxA hAK hA in

Lean source · statement

theorem idealOfA_ne_bot :
    (IsLocalRing.maximalIdeal A).comap
        (Subring.inclusion (integralClosure_Kx_le_A x A hAK hxA)) ≠ ⊥

theorem

place_of_idealOfA_le

L129 ↗

AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable.place_of_idealOfA_le

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)
omit [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] in
include hxA hAK in

Lean source · statement

theorem place_of_idealOfA_le (P : HeightOneSpectrum (integralClosure (Kx) F))
    [IsDedekindDomain (integralClosure (Kx) F)] [IsFractionRing (integralClosure (Kx) F) F]
    (hP : P.asIdeal = (IsLocalRing.maximalIdeal A).comap
        (Subring.inclusion (integralClosure_Kx_le_A x A hAK hxA))) :
    (Place.ofHeightOneSpectrum (K := K) (F := F) P).toValuationSubring ≤ A

theorem

exists_place_of_mem

L144 ↗

AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable.exists_place_of_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Crux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
variable (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤)
variable (hx : Transcendental K x) (hxA : x ∈ A)
include hx hxA hAK hA in

Lean source · statement

theorem exists_place_of_mem [Algebra.IsSeparable (Kxfield) F] :
    ∃ v : Place K F, v.toValuationSubring = A

theorem

exists_of_valuationSubring'

L166 ↗

AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable.AlgebraicCurve.Place.exists_of_valuationSubring'

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
section Roots
open scoped _root_.AlgebraicCurve _root_.AlgebraicCurve.Place in

Lean source · statement

theorem AlgebraicCurve.Place.exists_of_valuationSubring' {K F : Type*} [Field K] [Field F]
  [Algebra K F] (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
  [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] (A : ValuationSubring F) (hAK
  : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤) : ∃ v : AlgebraicCurve.Place K F,
  v.toValuationSubring = A

theorem

exists_of_valuationSubring_of_isSeparable

L212 ↗

AlgebraicCurve.Place.exists_of_valuationSubring_of_isSeparable

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_valuationSubring_of_isSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin

Lean source · statement

theorem _root_.AlgebraicCurve.Place.exists_of_valuationSubring_of_isSeparable
    {K F : Type*} [Field K] [Field F] [Algebra K F] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F]
    (A : ValuationSubring F) (hAK : ∀ a : K, algebraMap K F a ∈ A) (hA : A ≠ ⊤) :
    ∃ v : AlgebraicCurve.Place K F, v.toValuationSubring = A

Module documentation

Place exists of valuation Subring of is Separable

Declarations