NYLL
Module

Place_exists_toValuationSubring_eq_comap_ringHom_of_isSeparable.lean

Nyll.AlgebraicCurves.Places.Place_exists_toValuationSubring_eq_comap_ringHom_of_isSeparable
14 declarations indexed from sourceView source ↗

Module documentation

Place exists to Valuation Subring eq comap ring Hom 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 by10

Declarations

theorem

isDedekindDomain_Kx

L47 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.isDedekindDomain_Kx
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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 [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] [FiniteDimensional
  (IntermediateField.adjoin K ({x} : Set F)) F] in
include hx in
Lean source · statement
theorem isDedekindDomain_Kx : IsDedekindDomain (Kx)
theorem

isDedekindDomain_integralClosure

L59 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.isDedekindDomain_integralClosure
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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 :
    IsDedekindDomain (integralClosure (Kx) F)
theorem

isFractionRing_integralClosure

L65 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.isFractionRing_integralClosure
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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 [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] in
Lean source · statement
theorem isFractionRing_integralClosure :
    IsFractionRing (integralClosure (Kx) F) F
theorem

Kx_le_A

L72 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.Kx_le_A
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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 [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] [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)

L80 ↗
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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)

L83 ↗
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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

L89 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.integralClosure_Kx_le_A
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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 [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] [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

L104 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.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.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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 [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] [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

L118 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.idealOfA_ne_bot
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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 [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] in
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

L142 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.place_of_idealOfA_le
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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 [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] [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

L158 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.exists_place_of_mem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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]
  [Algebra.IsSeparable (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 :
    ∃ v : Place K F, v.toValuationSubring = A
theorem

exists_of_valuationSubring

L180 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.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.PlaceValuationComapSeparable
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_toValuationSubring_eq_comap_ringHom

L225 ↗
AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable.AlgebraicCurve.Place.exists_toValuationSubring_eq_comap_ringHom
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
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_toValuationSubring_eq_comap_ringHom {K F F' : Type*}
  [Field K] [Field F] [Field F'] [Algebra K F] (x : F) [FiniteDimensional
  (IntermediateField.adjoin K ({x} : Set F)) F] [Algebra.IsSeparable (IntermediateField.adjoin K
  ({x} : Set F)) F] (φ : F →+* F') (w : ValuationSubring F') (hwK : ∀ a : K, φ (algebraMap K F a)
  ∈ w) (hwx : ∃ y : F, φ y ∉ w) : ∃ v : AlgebraicCurve.Place K F, v.toValuationSubring = w.comap φ
theorem

exists_toValuationSubring_eq_comap_ringHom_of_isSeparable

L239 ↗
AlgebraicCurve.Place.exists_toValuationSubring_eq_comap_ringHom_of_isSeparable
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceValuationComapSeparable
open _root_.AlgebraicCurve
open _root_.IsDedekindDomain
open scoped IntermediateField.algebraAdjoinAdjoin
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_toValuationSubring_eq_comap_ringHom_of_isSeparable {K F
  F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] (x : F) [FiniteDimensional
  (IntermediateField.adjoin K ({x} : Set F)) F] [Algebra.IsSeparable (IntermediateField.adjoin K
  ({x} : Set F)) F] (φ : F →+* F') (w : ValuationSubring F') (hwK : ∀ a : K, φ (algebraMap K F a)
  ∈ w) (hwx : ∃ y : F, φ y ∉ w) : ∃ v : AlgebraicCurve.Place K F, v.toValuationSubring = w.comap φ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.