NYLL
Module

ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
33 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring is Discrete Valuation Ring of forall algebra Map mem of is Separable

Imports12
  • Mathlib.Algebra.Module.Torsion.Free
  • Mathlib.RingTheory.Valuation.ValuationSubring
  • Mathlib.RingTheory.Valuation.LocalSubring
  • Mathlib.RingTheory.RamificationInertia.Inertia
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.Localization.Integral
  • Mathlib.RingTheory.Ideal.GoingUp
  • Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
  • Mathlib.RingTheory.DedekindDomain.IntegralClosure
  • Mathlib.RingTheory.DedekindDomain.AdicValuation
  • Mathlib.RingTheory.DedekindDomain.Dvr
  • Mathlib.RingTheory.DiscreteValuationRing.Basic
Imported by1

Declarations

theorem

isUnit_iff_inv_mem

L43 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.isUnit_iff_inv_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section general
variable {L : Type*} [Field L]
Lean source · statement
theorem isUnit_iff_inv_mem (V : ValuationSubring L) (x : V) (hx0 : (x : L) ≠ 0) :
    IsUnit x ↔ (x : L)⁻¹ ∈ V
theorem

mem_maximalIdeal_iff_inv_not_mem

L54 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.mem_maximalIdeal_iff_inv_not_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section general
variable {L : Type*} [Field L]
Lean source · statement
theorem mem_maximalIdeal_iff_inv_not_mem (V : ValuationSubring L) (x : V) (hx0 : (x : L) ≠ 0) :
    x ∈ maximalIdeal V ↔ (x : L)⁻¹ ∉ V
theorem

mem_nonunits_iff_eq_zero_or_inv_not_mem

L58 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.mem_nonunits_iff_eq_zero_or_inv_not_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section general
variable {L : Type*} [Field L]
Lean source · statement
theorem mem_nonunits_iff_eq_zero_or_inv_not_mem (V : ValuationSubring L) (x : L) :
    x ∈ V.nonunits ↔ x = 0 ∨ x⁻¹ ∉ V
theorem

inertiaDeg_maximalIdeal_eq_one_of_isLocalization

L74 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.inertiaDeg_maximalIdeal_eq_one_of_isLocalization
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section general
variable {L : Type*} [Field L]
Lean source · statement
theorem inertiaDeg_maximalIdeal_eq_one_of_isLocalization {R : Type*} [CommRing R]
    (p : Ideal R) [p.IsMaximal] (Rₚ : Type*) [CommRing Rₚ] [Algebra R Rₚ]
    [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] :
    (maximalIdeal Rₚ).inertiaDeg R = 1
structure

Over

L96 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.Over
Documentation

Compatibility of a valuation ring with a local base ring and its maximal ideal.

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
Lean source · full declaration
structure Over (C : Type*) [CommRing C] [IsLocalRing C] {F : Type*} [Field F] [Algebra C F]
    (B : ValuationSubring F) : Prop where
  /-- The valuation ring contains the image of the local base ring. -/
  mem : ∀ c : C, algebraMap C F c ∈ B
  /-- The preimage of the valuation-ring nonunits is the maximal ideal of the base ring. -/
  nonunit_iff : ∀ c : C, algebraMap C F c ∈ B.nonunits ↔ c ∈ maximalIdeal C
abbrev

overAlgebra

L110 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.overAlgebra
Documentation

The algebra structure on the valuation subring induced by the base-ring map landing in it.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
abbrev overAlgebra (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) : Algebra C B
theorem

coe_algebraMap_overAlgebra

L113 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.coe_algebraMap_overAlgebra
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · full declaration
theorem coe_algebraMap_overAlgebra (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B)
    (c : C) :
    letI := overAlgebra B h
    ((algebraMap C B c : B) : F) = algebraMap C F c := rfl
theorem

isScalarTower_overAlgebra

L118 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.isScalarTower_overAlgebra
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · full declaration
theorem isScalarTower_overAlgebra (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    letI := overAlgebra B h
    IsScalarTower C B F := by
  let := overAlgebra B h
  exact IsScalarTower.of_algebraMap_eq fun a => rfl
theorem

algebraMap_injective

L125 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.algebraMap_injective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
include K in
Lean source · statement
theorem algebraMap_injective : Function.Injective (algebraMap C F)
theorem

algebraMap_overAlgebra_injective

L130 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.algebraMap_overAlgebra_injective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
include K in
Lean source · full declaration
theorem algebraMap_overAlgebra_injective (B : ValuationSubring F)
    (h : ∀ c : C, algebraMap C F c ∈ B) :
    letI := overAlgebra B h
    Function.Injective (algebraMap C B) := by
  let := overAlgebra B h
  intro a b hab
  have := congrArg (fun z : B => (z : F)) hab
  exact algebraMap_injective K this
theorem

comap_maximalIdeal_overAlgebra

L139 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.comap_maximalIdeal_overAlgebra
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · full declaration
theorem comap_maximalIdeal_overAlgebra (B : ValuationSubring F) (h : Over C B) :
    letI := overAlgebra B h.mem
    (maximalIdeal B).comap (algebraMap C B) = maximalIdeal C := by
  let := overAlgebra B h.mem
  ext c
  rw [Ideal.mem_comap, ← h.nonunit_iff, ← ValuationSubring.coe_mem_nonunits_iff]
  rfl
theorem

liesOver_overAlgebra

L147 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.liesOver_overAlgebra
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · full declaration
theorem liesOver_overAlgebra (B : ValuationSubring F) (h : Over C B) :
    letI := overAlgebra B h.mem
    (maximalIdeal B).LiesOver (maximalIdeal C) := by
  let := overAlgebra B h.mem
  exact ⟨(comap_maximalIdeal_overAlgebra B h).symm⟩
theorem

mem_of_mem_integralClosure

L153 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.mem_of_mem_integralClosure
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem mem_of_mem_integralClosure (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B)
    {y : F} (hy : y ∈ integralClosure C F) : y ∈ B
theorem

ne_top_of_over

L162 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.ne_top_of_over
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
include K in
Lean source · statement
theorem ne_top_of_over (B : ValuationSubring F) (h : Over C B) : B ≠ ⊤
theorem

maximalIdeal_ne_bot

L174 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.maximalIdeal_ne_bot
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
theorem maximalIdeal_ne_bot : maximalIdeal C ≠ ⊥
theorem

coe_algebraMap_integralClosure

L177 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.coe_algebraMap_integralClosure
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem coe_algebraMap_integralClosure (c : C) :
    ((algebraMap C (integralClosure C F) c : integralClosure C F) : F) = algebraMap C F c
theorem

algebraMap_integralClosure_injective

L181 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.algebraMap_integralClosure_injective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
include K in
Lean source · statement
theorem algebraMap_integralClosure_injective :
    Function.Injective (algebraMap C (integralClosure C F))
theorem

isTorsionFree_integralClosure

L188 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.isTorsionFree_integralClosure
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDiscreteValuationRing C] in
include K in
Lean source · statement
theorem isTorsionFree_integralClosure : Module.IsTorsionFree C (integralClosure C F)
theorem

liesOver_maximalIdeal

L196 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.liesOver_maximalIdeal
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
include K in
Lean source · statement
theorem liesOver_maximalIdeal (v : HeightOneSpectrum (integralClosure C F)) :
    v.asIdeal.LiesOver (maximalIdeal C)
def

toOver

L205 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.toOver
Documentation

The inclusion of the integral closure into a valuation ring containing the base ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
def toOver (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    integralClosure C F →+* B
theorem

coe_toOver

L209 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.coe_toOver
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem coe_toOver (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B)
    (s : integralClosure C F) : ((toOver B h s : B) : F) = (s : F)
def

center

L213 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.center
Documentation

The center of the valuation on the integral closure of the local base ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
def center (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    Ideal (integralClosure C F)
theorem

mem_center_iff

L217 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.mem_center_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
omit [IsDomain C] [IsDiscreteValuationRing C] in
Lean source · statement
theorem mem_center_iff (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B)
    (s : integralClosure C F) :
    s ∈ center B h ↔ (s : F) ∈ B.nonunits
instance

center_isPrime

L223 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.center_isPrime
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
instance center_isPrime (B : ValuationSubring F) (h : ∀ c : C, algebraMap C F c ∈ B) :
    (center B h).IsPrime
theorem

center_ne_bot

L228 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.center_ne_bot
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
include K in
Lean source · statement
theorem center_ne_bot (B : ValuationSubring F) (h : Over C B) : center B h.mem ≠ ⊥
def

vOf

L239 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.vOf
Documentation

The height-one prime obtained from the center of a valuation lying over the local base ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
Lean source · statement
def vOf (B : ValuationSubring F) (h : Over C B) :
    HeightOneSpectrum (integralClosure C F)
theorem

isFractionRing_integralClosure

L249 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.isFractionRing_integralClosure
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
section finite
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
omit [IsDiscreteValuationRing C] [Algebra.IsSeparable K F] in
include K in
Lean source · statement
theorem isFractionRing_integralClosure : IsFractionRing (integralClosure C F) F
theorem

isDedekindDomain_integralClosure

L252 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.isDedekindDomain_integralClosure
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
section finite
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
include K in
Lean source · statement
theorem isDedekindDomain_integralClosure : IsDedekindDomain (integralClosure C F)
theorem

finite_integralClosure

L255 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.finite_integralClosure
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
section finite
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
include K in
Lean source · statement
theorem finite_integralClosure : Module.Finite C (integralClosure C F)
def

W

L259 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.W
Documentation

The valuation ring at a height-one prime of the Dedekind integral closure.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
section finite
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
Lean source · statement
def W (v : HeightOneSpectrum (integralClosure C F)) : ValuationSubring F
theorem

W_def

L264 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.W_def
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section dict
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
section finite
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
Lean source · full declaration
theorem W_def (v : HeightOneSpectrum (integralClosure C F)) :
    letI := isFractionRing_integralClosure K (F := F) (C := C)
    letI := isDedekindDomain_integralClosure K (F := F) (C := C)
    W K v = HeightOneSpectrum.valuationSubringAtPrime F v := rfl
theorem

main

L287 ↗
AlgebraicCurves.Valuations.Proofs.ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable.EmbCountDvr.main
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
namespace EmbCountDvr
open IsLocalRing IsDedekindDomain
section main
variable {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
variable (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
variable {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
variable [FiniteDimensional K F] [Algebra.IsSeparable K F]
include K in
Lean source · statement
theorem main (B : ValuationSubring F) (h : Over C B) : IsDiscreteValuationRing ↥B
theorem

isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable

L314 ↗
ValuationSubring.isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs
namespace ValuationSubring_isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
open IsLocalRing in
Lean source · statement
theorem _root_.ValuationSubring.isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable
    {C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
    (K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
    {F : Type*} [Field F] [Algebra K F] [Algebra C F] [IsScalarTower C K F]
    [FiniteDimensional K F] [Algebra.IsSeparable K F]
    (B : ValuationSubring F) (hCB : ∀ c : C, algebraMap C F c ∈ B)
    (hCBmax : ∀ c : C, algebraMap C F c ∈ B.nonunits ↔ c ∈ maximalIdeal C) :
    IsDiscreteValuationRing ↥B

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