NYLL
Module

Exists_mem_D_eq_smul_D_of_isCurveOver.lean

Nyll.AlgebraicCurves.FunctionFields.Exists_mem_D_eq_smul_D_of_isCurveOver
128 declarations indexed from sourceView source ↗

Module documentation

Exists mem D eq smul D of is Curve Over

Imports4
Imported by3

Declarations

def

uniformizerSubring'

L39 ↗
AlgebraicCurve.Place.uniformizerSubring'
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Transport
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
def _root_.AlgebraicCurve.Place.uniformizerSubring' : v.toValuationSubring
instance

instSMulCommClass_subring

L43 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.instSMulCommClass_subring
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Transport
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
instance instSMulCommClass_subring : SMulCommClass K v.toValuationSubring F
theorem

kaehlerMap_subring_D_uniformizer

L46 ↗
AlgebraicCurve.Place.kaehlerMap_subring_D_uniformizer
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Transport
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.kaehlerMap_subring_D_uniformizer :
    KaehlerDifferential.map K K v.toValuationSubring F
      (KaehlerDifferential.D K v.toValuationSubring v.uniformizerSubring') = v.dCoord
def

ValSubringKaehlerSpanTop

L60 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.ValSubringKaehlerSpanTop
Documentation

The differential of a uniformizer spans the differential module of every valuation ring.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def ValSubringKaehlerSpanTop : Prop
def

uniformizerSubring''

L82 ↗
AlgebraicCurve.Place.uniformizerSubring''
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CotangentEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
def _root_.AlgebraicCurve.Place.uniformizerSubring'' : v.toValuationSubring
def

polynomialAlgebra

L86 ↗
AlgebraicCurve.Place.polynomialAlgebra
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CotangentEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
def _root_.AlgebraicCurve.Place.polynomialAlgebra : Algebra
  K[X] v.toValuationSubring
theorem

polynomialAlgebra_algebraMap_X

L91 ↗
AlgebraicCurve.Place.polynomialAlgebra_algebraMap_X
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CotangentEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.polynomialAlgebra_algebraMap_X :
    letI := v.polynomialAlgebra
    algebraMap K[X] v.toValuationSubring X = v.uniformizerSubring'' :=
  aeval_X _
theorem

polynomialIsScalarTower

L97 ↗
AlgebraicCurve.Place.polynomialIsScalarTower
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CotangentEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.polynomialIsScalarTower :
    letI := v.polynomialAlgebra
    IsScalarTower K K[X] v.toValuationSubring := by
  let := v.polynomialAlgebra
  refine IsScalarTower.of_algebraMap_eq fun a => ?_
  change _ = aeval v.uniformizerSubring'' (algebraMap K K[X] a)
  simp [Polynomial.algebraMap_eq, aeval_C]
theorem

range_mapBaseChange_le_span_D_uniformizer

L106 ↗
AlgebraicCurve.Place.range_mapBaseChange_le_span_D_uniformizer
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CotangentEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.range_mapBaseChange_le_span_D_uniformizer :
    letI := v.polynomialAlgebra
    letI := v.polynomialIsScalarTower
    LinearMap.range (KaehlerDifferential.mapBaseChange K K[X] v.toValuationSubring)
      ≤ Submodule.span v.toValuationSubring
          {KaehlerDifferential.D K v.toValuationSubring v.uniformizerSubring''} := by
  let := v.polynomialAlgebra
  let := v.polynomialIsScalarTower
  rintro _ ⟨t, rfl⟩
  induction t with
  | add x y hx hy => rw [map_add]; exact add_mem hx hy
  | tmul b ω =>
    rw [KaehlerDifferential.mapBaseChange_tmul,
      show ω = (KaehlerDifferential.polynomialEquiv K ω) • (KaehlerDifferential.D K K[X] X) from
        ((KaehlerDifferential.polynomialEquiv K).symm_apply_apply ω).symm.trans
          (KaehlerDifferential.polynomialEquiv_symm K _),
      LinearMap.map_smul, KaehlerDifferential.map_D,
      show algebraMap K[X] v.toValuationSubring X = v.uniformizerSubring'' from aeval_X _,
      ← algebraMap_smul (A := v.toValuationSubring)]
    exact Submodule.smul_mem _ b
      (Submodule.smul_mem _ _ (Submodule.mem_span_singleton_self _))
theorem

range_mapBaseChange_eq_top_of_subsingleton

L129 ↗
AlgebraicCurve.Place.range_mapBaseChange_eq_top_of_subsingleton
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CotangentEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.range_mapBaseChange_eq_top_of_subsingleton
    (hsub :
      letI := v.polynomialAlgebra
      Subsingleton Ω[v.toValuationSubring⁄K[X]]) :
    letI := v.polynomialAlgebra
    letI := v.polynomialIsScalarTower
    LinearMap.range (KaehlerDifferential.mapBaseChange K K[X] v.toValuationSubring) = ⊤ := by
  let := v.polynomialAlgebra
  let := v.polynomialIsScalarTower
  rw [KaehlerDifferential.range_mapBaseChange]
  exact LinearMap.ker_eq_top.mpr (Subsingleton.elim _ _)
theorem

span_D_uniformizer_eq_top_of_subsingleton

L142 ↗
AlgebraicCurve.Place.span_D_uniformizer_eq_top_of_subsingleton
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CotangentEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.span_D_uniformizer_eq_top_of_subsingleton
    (hsub :
      letI := v.polynomialAlgebra
      Subsingleton Ω[v.toValuationSubring⁄K[X]]) :
    Submodule.span v.toValuationSubring
      {KaehlerDifferential.D K v.toValuationSubring v.uniformizerSubring''} = ⊤ := by
  refine top_le_iff.mp ?_
  rw [← v.range_mapBaseChange_eq_top_of_subsingleton hsub]
  exact v.range_mapBaseChange_le_span_D_uniformizer
def

ValSubringPolynomialFormallyUnramified

L161 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.ValSubringPolynomialFormallyUnramified
Documentation

Each valuation ring has vanishing relative differentials over the polynomial algebra defined by its uniformizer.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def ValSubringPolynomialFormallyUnramified : Prop
theorem

valSubringKaehlerSpanTop_of_polynomialFormallyUnramified

L168 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringKaehlerSpanTop_of_polynomialFormallyUnramified
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringKaehlerSpanTop_of_polynomialFormallyUnramified
    (hfu : ValSubringPolynomialFormallyUnramified K F) :
    ValSubringKaehlerSpanTop K F
def

uniformizerSubring'''

L190 ↗
AlgebraicCurve.Place.uniformizerSubring'''
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ResidueEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
def _root_.AlgebraicCurve.Place.uniformizerSubring''' : v.toValuationSubring
theorem

irreducible_uniformizerSubring'''

L195 ↗
AlgebraicCurve.Place.irreducible_uniformizerSubring'''
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ResidueEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.irreducible_uniformizerSubring''' : Irreducible
  v.uniformizerSubring'''
theorem

maximalIdeal_eq_span_uniformizer

L200 ↗
AlgebraicCurve.Place.maximalIdeal_eq_span_uniformizer
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ResidueEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.maximalIdeal_eq_span_uniformizer :
    IsLocalRing.maximalIdeal v.toValuationSubring = Ideal.span {v.uniformizerSubring'''}
theorem

D_polynomialAlgebra_uniformizer

L205 ↗
AlgebraicCurve.Place.D_polynomialAlgebra_uniformizer
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ResidueEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.D_polynomialAlgebra_uniformizer :
    letI := v.polynomialAlgebra
    KaehlerDifferential.D K[X] v.toValuationSubring v.uniformizerSubring''' = 0 := by
  let := v.polynomialAlgebra
  rw [show v.uniformizerSubring''' = algebraMap K[X] v.toValuationSubring X from
    (v.polynomialAlgebra_algebraMap_X).symm]
  exact (KaehlerDifferential.D K[X] v.toValuationSubring).map_algebraMap X
theorem

ker_algebraMap_residueField_eq_span

L214 ↗
AlgebraicCurve.Place.ker_algebraMap_residueField_eq_span
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ResidueEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ker_algebraMap_residueField_eq_span :
    RingHom.ker (algebraMap v.toValuationSubring v.ResidueField)
      = Ideal.span {v.uniformizerSubring'''}
theorem

formallyUnramified_polynomial_residueField_of_isSeparable

L221 ↗
AlgebraicCurve.Place.formallyUnramified_polynomial_residueField_of_isSeparable
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ResidueEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem
  _root_.AlgebraicCurve.Place.formallyUnramified_polynomial_residueField_of_isSeparable
    [Algebra.IsSeparable K (IsLocalRing.ResidueField v.toValuationSubring)] :
    letI := v.polynomialAlgebra
    Algebra.FormallyUnramified K[X] (IsLocalRing.ResidueField v.toValuationSubring) := by
  let := v.polynomialAlgebra
  let := v.polynomialIsScalarTower
  have : Algebra.FormallyUnramified K (IsLocalRing.ResidueField v.toValuationSubring) :=
    Algebra.FormallyUnramified.of_isSeparable K _
  exact Algebra.FormallyUnramified.of_restrictScalars K K[X] _
theorem

subsingleton_residueKaehler_of_isSeparable

L233 ↗
AlgebraicCurve.Place.subsingleton_residueKaehler_of_isSeparable
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ResidueEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.subsingleton_residueKaehler_of_isSeparable
    [Algebra.IsSeparable K (IsLocalRing.ResidueField v.toValuationSubring)] :
    letI := v.polynomialAlgebra
    Subsingleton Ω[(IsLocalRing.ResidueField v.toValuationSubring)⁄K[X]] := by
  let := v.polynomialAlgebra
  have := v.formallyUnramified_polynomial_residueField_of_isSeparable
  exact Algebra.FormallyUnramified.subsingleton_kaehlerDifferential
theorem

subsingleton_residueTensor_polynomialKaehler_of_isSeparable

L242 ↗
AlgebraicCurve.Place.subsingleton_residueTensor_polynomialKaehler_of_isSeparable
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ResidueEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem
  _root_.AlgebraicCurve.Place.subsingleton_residueTensor_polynomialKaehler_of_isSeparable
    [Algebra.IsSeparable K (IsLocalRing.ResidueField v.toValuationSubring)] :
    letI := v.polynomialAlgebra
    Subsingleton (v.ResidueField ⊗[v.toValuationSubring] Ω[v.toValuationSubring⁄K[X]]) := by
  let := v.polynomialAlgebra
  let := v.polynomialIsScalarTower
  have := v.subsingleton_residueKaehler_of_isSeparable
  refine subsingleton_of_forall_eq 0 fun t => ?_
  obtain ⟨c, rfl⟩ :=
    ((KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange K[X]
      v.toValuationSubring v.ResidueField
      Ideal.Quotient.mk_surjective) t).mp (Subsingleton.elim _ _)
  obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ c
  simp only [KaehlerDifferential.kerCotangentToTensor_toCotangent]
  rw [v.ker_algebraMap_residueField_eq_span] at hx
  induction hx using Submodule.span_induction with
  | mem y hy =>
    rcases hy with rfl
    rw [v.D_polynomialAlgebra_uniformizer, TensorProduct.tmul_zero]
  | zero => simp
  | add y z _ _ hy hz =>
    rw [map_add, TensorProduct.tmul_add, hy, hz, add_zero]
  | smul a y hy IH =>
    have hres : (algebraMap v.toValuationSubring v.ResidueField y) = 0 := by
      rw [IsLocalRing.ResidueField.algebraMap_eq, IsLocalRing.residue_eq_zero_iff,
        v.maximalIdeal_eq_span_uniformizer]
      exact hy
    rw [smul_eq_mul, Derivation.leibniz, TensorProduct.tmul_add,
      TensorProduct.tmul_smul, IH, smul_zero, zero_add,
      ← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, hres,
      TensorProduct.zero_tmul]
theorem

finite_polynomialKaehler_of_finite_kaehler

L276 ↗
AlgebraicCurve.Place.finite_polynomialKaehler_of_finite_kaehler
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ResidueEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.finite_polynomialKaehler_of_finite_kaehler
    [Module.Finite v.toValuationSubring Ω[v.toValuationSubring⁄K]] :
    letI := v.polynomialAlgebra
    Module.Finite v.toValuationSubring Ω[v.toValuationSubring⁄K[X]] := by
  let := v.polynomialAlgebra
  let := v.polynomialIsScalarTower
  exact Module.Finite.of_surjective
    (KaehlerDifferential.map K K[X] v.toValuationSubring v.toValuationSubring)
    (KaehlerDifferential.map_surjective K K[X] v.toValuationSubring)
theorem

subsingleton_polynomialKaehler_of_isSeparable_of_finite

L287 ↗
AlgebraicCurve.Place.subsingleton_polynomialKaehler_of_isSeparable_of_finite
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ResidueEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.subsingleton_polynomialKaehler_of_isSeparable_of_finite
    [Algebra.IsSeparable K (IsLocalRing.ResidueField v.toValuationSubring)]
    [Module.Finite v.toValuationSubring Ω[v.toValuationSubring⁄K]] :
    letI := v.polynomialAlgebra
    Subsingleton Ω[v.toValuationSubring⁄K[X]] := by
  let := v.polynomialAlgebra
  have := v.finite_polynomialKaehler_of_finite_kaehler
  have := v.subsingleton_residueTensor_polynomialKaehler_of_isSeparable
  exact (IsLocalRing.subsingleton_tensorProduct (R := v.toValuationSubring)).mp ‹_›
def

ValSubringKaehlerFinite

L305 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.ValSubringKaehlerFinite
Documentation

Every valuation ring has a finite module of differentials over the constant field.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def ValSubringKaehlerFinite : Prop
theorem

valSubringPolynomialFormallyUnramified_of_kaehlerFinite_of_isSeparable

L310 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringPolynomialFormallyUnramified_of_kaehlerFinite_of_isSeparable
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringPolynomialFormallyUnramified_of_kaehlerFinite_of_isSeparable
    [∀ v : Place K F, Algebra.IsSeparable K (IsLocalRing.ResidueField v.toValuationSubring)]
    (hfin : ValSubringKaehlerFinite K F) :
    ValSubringPolynomialFormallyUnramified K F
theorem

finite_kaehler_of_essFiniteType

L333 ↗
AlgebraicCurve.Place.finite_kaehler_of_essFiniteType
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section EftEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.finite_kaehler_of_essFiniteType [Algebra.EssFiniteType
  K v.toValuationSubring] :
    Module.Finite v.toValuationSubring Ω[v.toValuationSubring⁄K]
theorem

essFiniteType_of_exists_finiteType_isLocalization

L339 ↗
AlgebraicCurve.Place.essFiniteType_of_exists_finiteType_isLocalization
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section EftEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.essFiniteType_of_exists_finiteType_isLocalization
    (h : ∃ (S₀ : Subalgebra K v.toValuationSubring) (M : Submonoid S₀),
      Algebra.FiniteType K S₀ ∧ IsLocalization M v.toValuationSubring) :
    Algebra.EssFiniteType K v.toValuationSubring
def

ValSubringEssFiniteType

L354 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.ValSubringEssFiniteType
Documentation

Every valuation ring is essentially of finite type over the constant field.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def ValSubringEssFiniteType : Prop
def

ValSubringFiniteTypeModel

L358 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.ValSubringFiniteTypeModel
Documentation

Each valuation ring is a localization of a finitely generated subalgebra.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def ValSubringFiniteTypeModel : Prop
theorem

valSubringKaehlerFinite_of_essFiniteType

L365 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringKaehlerFinite_of_essFiniteType
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringKaehlerFinite_of_essFiniteType
    (heft : ValSubringEssFiniteType K F) :
    ValSubringKaehlerFinite K F
theorem

valSubringEssFiniteType_of_finiteTypeModel

L371 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringEssFiniteType_of_finiteTypeModel
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringEssFiniteType_of_finiteTypeModel
    (hmodel : ValSubringFiniteTypeModel K F) :
    ValSubringEssFiniteType K F
theorem

valSubringEssFiniteType_iff_finiteTypeModel

L376 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringEssFiniteType_iff_finiteTypeModel
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringEssFiniteType_iff_finiteTypeModel :
    ValSubringEssFiniteType K F ↔ ValSubringFiniteTypeModel K F
theorem

valSubringKaehlerFinite_of_finiteTypeModel

L384 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringKaehlerFinite_of_finiteTypeModel
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringKaehlerFinite_of_finiteTypeModel
    (hmodel : ValSubringFiniteTypeModel K F) :
    ValSubringKaehlerFinite K F
theorem

ofPrime_congr_s12

L399 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.ValuationSubring.ofPrime_congr_s12
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
Lean source · statement
theorem ofPrime_congr_s12 {R : ValuationSubring F} {P Q : Ideal R}
    [P.IsPrime] [Q.IsPrime] (h : P = Q) : R.ofPrime P = R.ofPrime Q
theorem

eq_top_of_idealOfLE_eq_bot_s12

L403 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.ValuationSubring.eq_top_of_idealOfLE_eq_bot_s12
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
Lean source · statement
theorem eq_top_of_idealOfLE_eq_bot_s12 {R S : ValuationSubring F} (h : R ≤ S)
    (hbot : idealOfLE R S h = ⊥) : S = ⊤
theorem

idealOfLE_ne_bot_of_ne_top_s12

L408 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.ValuationSubring.idealOfLE_ne_bot_of_ne_top_s12
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
Lean source · statement
theorem idealOfLE_ne_bot_of_ne_top_s12 {R S : ValuationSubring F} (h : R ≤ S)
    (hS : S ≠ ⊤) : idealOfLE R S h ≠ ⊥
theorem

eq_of_isDiscreteValuationRing_of_le_s12

L412 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.ValuationSubring.eq_of_isDiscreteValuationRing_of_le_s12
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
Lean source · statement
theorem eq_of_isDiscreteValuationRing_of_le_s12 {R S : ValuationSubring F}
    [IsDiscreteValuationRing R] (h : R ≤ S) (hS : S ≠ ⊤) : R = S
def

modelInclusion

L437 ↗
AlgebraicCurve.Place.modelInclusion
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterIdeal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
variable (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
Lean source · statement
def _root_.AlgebraicCurve.Place.modelInclusion : A →+*
  v.toValuationSubring
theorem

coe_modelInclusion

L442 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.coe_modelInclusion
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterIdeal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
variable (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem coe_modelInclusion (a : A) :
    ((v.modelInclusion A hA a : v.toValuationSubring) : F) = (a : F)
def

modelAlgebra

L445 ↗
AlgebraicCurve.Place.modelAlgebra
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterIdeal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
variable (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
Lean source · statement
def _root_.AlgebraicCurve.Place.modelAlgebra : Algebra A
  v.toValuationSubring
def

centerIdeal

L450 ↗
AlgebraicCurve.Place.centerIdeal
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterIdeal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
variable (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
def _root_.AlgebraicCurve.Place.centerIdeal : Ideal A
instance

centerIdeal_isPrime

L455 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.centerIdeal_isPrime
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterIdeal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
variable (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
instance centerIdeal_isPrime : (v.centerIdeal A hA).IsPrime
theorem

isUnit_modelInclusion_of_not_mem_centerIdeal

L459 ↗
AlgebraicCurve.Place.isUnit_modelInclusion_of_not_mem_centerIdeal
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterIdeal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
variable (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isUnit_modelInclusion_of_not_mem_centerIdeal {s : A}
    (hs : s ∉ v.centerIdeal A hA) :
    IsUnit (v.modelInclusion A hA s)
theorem

isUnit_modelInclusion_of_mem_primeCompl

L468 ↗
AlgebraicCurve.Place.isUnit_modelInclusion_of_mem_primeCompl
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterIdeal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
variable (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isUnit_modelInclusion_of_mem_primeCompl (s :
  (v.centerIdeal A hA).primeCompl) :
    IsUnit (v.modelInclusion A hA (s : A))
theorem

modelAlgebra_isScalarTower

L474 ↗
AlgebraicCurve.Place.modelAlgebra_isScalarTower
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterIdeal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
variable (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.modelAlgebra_isScalarTower :
    letI := v.modelAlgebra A hA
    IsScalarTower K A v.toValuationSubring := by
  let := v.modelAlgebra A hA
  refine IsScalarTower.of_algebraMap_eq fun c => ?_
  apply Subtype.ext
  simp only [coe_modelInclusion, RingHom.algebraMap_toAlgebra]
  rfl
theorem

essFiniteType_of_finiteType_isLocalization_centerIdeal

L484 ↗
AlgebraicCurve.Place.essFiniteType_of_finiteType_isLocalization_centerIdeal
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterIdeal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
variable (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.essFiniteType_of_finiteType_isLocalization_centerIdeal
    [Algebra.FiniteType K A]
    (hloc : letI := v.modelAlgebra A hA
            IsLocalization.AtPrime v.toValuationSubring (v.centerIdeal A hA)) :
    Algebra.EssFiniteType K v.toValuationSubring := by
  let := v.modelAlgebra A hA
  have := v.modelAlgebra_isScalarTower A hA
  have : Algebra.EssFiniteType A v.toValuationSubring :=
    Algebra.EssFiniteType.of_isLocalization _ (v.centerIdeal A hA).primeCompl
  exact Algebra.EssFiniteType.comp K A v.toValuationSubring
def

ValSubringDedekindModel

L504 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.ValSubringDedekindModel
Documentation

Each valuation ring is a localization at its centre in a finite-type subalgebra of the function field.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def ValSubringDedekindModel : Prop
theorem

valSubringEssFiniteType_of_dedekindModel

L513 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringEssFiniteType_of_dedekindModel
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringEssFiniteType_of_dedekindModel
    (hmodel : ValSubringDedekindModel K F) :
    ValSubringEssFiniteType K F
theorem

valSubringFiniteTypeModel_of_dedekindModel

L519 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringFiniteTypeModel_of_dedekindModel
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringFiniteTypeModel_of_dedekindModel
    (hmodel : ValSubringDedekindModel K F) :
    ValSubringFiniteTypeModel K F
theorem

inv_mem_of_not_mem_centerIdeal

L542 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.inv_mem_of_not_mem_centerIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterNonzero
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
Lean source · statement
theorem inv_mem_of_not_mem_centerIdeal {a : A} (ha : a ∉ v.centerIdeal A hA) :
    ((a : F))⁻¹ ∈ v.toValuationSubring
theorem

div_mem_of_not_mem_centerIdeal

L556 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.div_mem_of_not_mem_centerIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterNonzero
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
Lean source · statement
theorem div_mem_of_not_mem_centerIdeal (r : A) {a : A}
    (ha : a ∉ v.centerIdeal A hA) :
    (r : F) / (a : F) ∈ v.toValuationSubring
theorem

centerIdeal_ne_bot_of_isFractionRing

L563 ↗
AlgebraicCurve.Place.centerIdeal_ne_bot_of_isFractionRing
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section CenterNonzero
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
Lean source · statement
theorem _root_.AlgebraicCurve.Place.centerIdeal_ne_bot_of_isFractionRing [IsFractionRing A
  F] :
    v.centerIdeal A hA ≠ ⊥
def

centerLocalizationSubalgebra

L587 ↗
AlgebraicCurve.Place.centerLocalizationSubalgebra
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
Lean source · statement
def _root_.AlgebraicCurve.Place.centerLocalizationSubalgebra
  [IsFractionRing A F] :
    Subalgebra A F
instance

centerLocalizationSubalgebra_isLocalization

L594 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.centerLocalizationSubalgebra_isLocalization
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
Lean source · statement
instance centerLocalizationSubalgebra_isLocalization [IsFractionRing A F] :
    IsLocalization.AtPrime (v.centerLocalizationSubalgebra A hA) (v.centerIdeal A hA)
instance

centerLocalizationSubalgebra_isDomain

L598 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.centerLocalizationSubalgebra_isDomain
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
Lean source · statement
instance centerLocalizationSubalgebra_isDomain [IsFractionRing A F] :
    IsDomain (v.centerLocalizationSubalgebra A hA)
theorem

centerLocalizationSubalgebra_isDiscreteValuationRing

L602 ↗
AlgebraicCurve.Place.centerLocalizationSubalgebra_isDiscreteValuationRing
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.centerLocalizationSubalgebra_isDiscreteValuationRing
    [IsDedekindDomain A] [IsFractionRing A F] :
    IsDiscreteValuationRing (v.centerLocalizationSubalgebra A hA)
instance

centerLocalizationSubalgebra_isFractionRing

L609 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.centerLocalizationSubalgebra_isFractionRing
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
instance centerLocalizationSubalgebra_isFractionRing [IsFractionRing A F] :
    IsFractionRing (v.centerLocalizationSubalgebra A hA) F
theorem

centerLocalizationSubalgebra_subset

L613 ↗
AlgebraicCurve.Place.centerLocalizationSubalgebra_subset
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.centerLocalizationSubalgebra_subset [IsFractionRing A
  F] :
    ((v.centerLocalizationSubalgebra A hA : Subalgebra A F) : Set F)
      ⊆ (v.toValuationSubring : Set F)
def

centerLocalizationValuationSubring

L623 ↗
AlgebraicCurve.Place.centerLocalizationValuationSubring
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
def _root_.AlgebraicCurve.Place.centerLocalizationValuationSubring
    [IsDedekindDomain A] [IsFractionRing A F] : ValuationSubring F where
  toSubring := (v.centerLocalizationSubalgebra A hA).toSubring
  mem_or_inv_mem' x := by
    have := v.centerLocalizationSubalgebra_isDiscreteValuationRing A hA
    rcases ValuationRing.isInteger_or_isInteger (v.centerLocalizationSubalgebra A hA) x with
      ⟨a, ha⟩ | ⟨a, ha⟩
    · exact Or.inl (ha ▸ a.2)
    · exact Or.inr (ha ▸ a.2)
theorem

coe_centerLocalizationValuationSubring

L634 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.coe_centerLocalizationValuationSubring
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem coe_centerLocalizationValuationSubring [IsDedekindDomain A] [IsFractionRing A F] :
    ((v.centerLocalizationValuationSubring A hA : ValuationSubring F) : Set F)
      = ((v.centerLocalizationSubalgebra A hA : Subalgebra A F) : Set F)
instance

centerLocalizationValuationSubring_isDiscreteValuationRing

L638 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.centerLocalizationValuationSubring_isDiscreteValuationRing
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
instance centerLocalizationValuationSubring_isDiscreteValuationRing
    [IsDedekindDomain A] [IsFractionRing A F] :
    IsDiscreteValuationRing (v.centerLocalizationValuationSubring A hA)
theorem

centerLocalizationValuationSubring_le

L643 ↗
AlgebraicCurve.Place.centerLocalizationValuationSubring_le
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.centerLocalizationValuationSubring_le
  [IsDedekindDomain A] [IsFractionRing A F] :
    v.centerLocalizationValuationSubring A hA ≤ v.toValuationSubring
theorem

centerLocalizationValuationSubring_eq

L649 ↗
AlgebraicCurve.Place.centerLocalizationValuationSubring_eq
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.centerLocalizationValuationSubring_eq
  [IsDedekindDomain A] [IsFractionRing A F] :
    v.centerLocalizationValuationSubring A hA = v.toValuationSubring
theorem

coe_centerLocalizationSubalgebra_eq

L656 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.coe_centerLocalizationSubalgebra_eq
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem coe_centerLocalizationSubalgebra_eq [IsDedekindDomain A] [IsFractionRing A F] :
    ((v.centerLocalizationSubalgebra A hA : Subalgebra A F) : Set F)
      = (v.toValuationSubring : Set F)
theorem

mem_centerLocalizationSubalgebra_of_mem

L662 ↗
AlgebraicCurve.Place.mem_centerLocalizationSubalgebra_of_mem
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_centerLocalizationSubalgebra_of_mem
  [IsDedekindDomain A] [IsFractionRing A F]
    (x : F) (hx : x ∈ v.toValuationSubring) :
    x ∈ (v.centerLocalizationSubalgebra A hA : Subalgebra A F)
theorem

isLocalization_centerIdeal_of_isDedekindDomain

L669 ↗
AlgebraicCurve.Place.isLocalization_centerIdeal_of_isDedekindDomain
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section LocalizationSubalgebra
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
  (A : Subalgebra K F) (hA : (A : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.isLocalization_centerIdeal_of_isDedekindDomain
    [IsDedekindDomain A] [IsFractionRing A F] :
    letI := v.modelAlgebra A hA
    IsLocalization.AtPrime v.toValuationSubring (v.centerIdeal A hA) := by
  let := v.modelAlgebra A hA
  refine (isLocalization_iff _ _).mpr ⟨?_, ?_, ?_⟩
  · exact v.isUnit_modelInclusion_of_mem_primeCompl A hA
  · intro x
    have hxP : (x : F) ∈ (v.centerLocalizationSubalgebra A hA : Subalgebra A F) :=
      v.mem_centerLocalizationSubalgebra_of_mem A hA (x : F) x.2
    obtain ⟨a, s, hs, hxeq⟩ := hxP
    refine ⟨⟨a, ⟨s, hs⟩⟩, Subtype.ext ?_⟩
    change (x : F) * ((s : A) : F) = ((a : A) : F)
    have halg_s : algebraMap A F s = ((s : A) : F) := rfl
    have halg_a : algebraMap A F a = ((a : A) : F) := rfl
    have hs0 : algebraMap A F s ≠ 0 := by
      intro hF
      have hsne : s ≠ 0 := fun h => (h ▸ hs) (Ideal.zero_mem _)
      exact hsne (Subtype.ext (p := (· ∈ A)) (halg_s ▸ hF))
    rw [← halg_s, ← halg_a, hxeq, mul_assoc, inv_mul_cancel₀ hs0, mul_one]
  · intro a₁ a₂ h
    have hF : (a₁ : F) = (a₂ : F) :=
      congrArg (Subtype.val : v.toValuationSubring → F) h
    exact ⟨1, by rw [show a₁ = a₂ from Subtype.ext hF]⟩
def

ValSubringDedekindFractionModel

L703 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.ValSubringDedekindFractionModel
Documentation

Every valuation ring contains a finite-type Dedekind subalgebra with the given fraction field.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def ValSubringDedekindFractionModel : Prop
theorem

valSubringDedekindModel_of_dedekindFractionModel

L710 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringDedekindModel_of_dedekindFractionModel
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringDedekindModel_of_dedekindFractionModel
    (hfrac : ValSubringDedekindFractionModel K F) :
    ValSubringDedekindModel K F
theorem

isIntegrallyClosed_toValuationSubring

L732 ↗
AlgebraicCurve.Place.isIntegrallyClosed_toValuationSubring
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section IntegrallyClosed
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isIntegrallyClosed_toValuationSubring :
    IsIntegrallyClosed v.toValuationSubring
theorem

mem_valuationSubring_of_isIntegral

L736 ↗
AlgebraicCurve.Place.mem_valuationSubring_of_isIntegral
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section IntegrallyClosed
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_valuationSubring_of_isIntegral {x : F}
    (hx : IsIntegral v.toValuationSubring x) :
    x ∈ v.toValuationSubring
theorem

modelAlgebra_isScalarTower_top

L746 ↗
AlgebraicCurve.Place.modelAlgebra_isScalarTower_top
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section IntegrallyClosed
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (B : Subalgebra K F) (hB : (B : Set F) ⊆ (v.toValuationSubring : Set F))
include hB in
Lean source · full declaration
theorem _root_.AlgebraicCurve.Place.modelAlgebra_isScalarTower_top :
    letI := v.modelAlgebra B hB
    IsScalarTower B v.toValuationSubring F := by
  let := v.modelAlgebra B hB
  refine IsScalarTower.of_algebraMap_eq fun b => ?_
  rfl
theorem

mem_valuationSubring_of_isIntegral_subalgebra

L755 ↗
AlgebraicCurve.Place.mem_valuationSubring_of_isIntegral_subalgebra
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section IntegrallyClosed
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (B : Subalgebra K F) (hB : (B : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
include hB in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_valuationSubring_of_isIntegral_subalgebra {x : F}
    (hx : IsIntegral B x) :
    x ∈ v.toValuationSubring
theorem

integralClosure_subset_valuationSubring

L764 ↗
AlgebraicCurve.Place.integralClosure_subset_valuationSubring
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section IntegrallyClosed
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (B : Subalgebra K F) (hB : (B : Set F) ⊆ (v.toValuationSubring : Set F))
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
include hB in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.integralClosure_subset_valuationSubring :
    ((integralClosure B F : Subalgebra B F) : Set F)
      ⊆ (v.toValuationSubring : Set F)
def

IsAffineChart

L779 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.IsAffineChart
Documentation

A finite-type Dedekind subalgebra whose fraction field is the given function field.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section TwoCharts
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def IsAffineChart (A : Subalgebra K F) : Prop
def

ValSubringTwoAffineCharts

L783 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.ValSubringTwoAffineCharts
Documentation

Two affine charts such that each valuation ring contains at least one of them.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section TwoCharts
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def ValSubringTwoAffineCharts : Prop
theorem

valSubringDedekindFractionModel_of_twoAffineCharts

L790 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringDedekindFractionModel_of_twoAffineCharts
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section TwoCharts
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringDedekindFractionModel_of_twoAffineCharts
    (h : ValSubringTwoAffineCharts K F) :
    ValSubringDedekindFractionModel K F
theorem

valSubringDedekindModel_of_twoAffineCharts

L798 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringDedekindModel_of_twoAffineCharts
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section TwoCharts
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringDedekindModel_of_twoAffineCharts
    (h : ValSubringTwoAffineCharts K F) :
    ValSubringDedekindModel K F
def

toKSubalgebra

L821 ↗
AlgebraicCurve.Place.toKSubalgebra
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open scoped _root_.AlgebraicCurve.Place in
Lean source · full declaration
def _root_.AlgebraicCurve.Place.toKSubalgebra (v : Place K F) :
  Subalgebra K F where
  __ := v.toValuationSubring.toSubring
  algebraMap_mem' c := v.algebraMap_mem' c
theorem

coe_toKSubalgebra

L830 ↗
AlgebraicCurve.Place.coe_toKSubalgebra
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
namespace Place
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.coe_toKSubalgebra (v : Place K F) :
    (v.toKSubalgebra : Set F) = (v.toValuationSubring : Set F)
theorem

gate_adjoin_subset_valuationSubring_of_mem

L835 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.gate_adjoin_subset_valuationSubring_of_mem
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section Gates
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
theorem gate_adjoin_subset_valuationSubring_of_mem (v : Place K F) {t : F}
    (ht : t ∈ v.toValuationSubring) :
    ((Algebra.adjoin K {t} : Subalgebra K F) : Set F)
      ⊆ (v.toValuationSubring : Set F)
theorem

isPrincipalIdealRing_adjoin_s12

L858 ↗
Transcendental.isPrincipalIdealRing_adjoin_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section AdjoinRingProperties
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem _root_.Transcendental.isPrincipalIdealRing_adjoin_s12 {t : F} (ht : Transcendental
  K t) :
    IsPrincipalIdealRing ↥(Algebra.adjoin K ({t} : Set F))
theorem

isDedekindDomain_adjoin_s12

L866 ↗
Transcendental.isDedekindDomain_adjoin_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section AdjoinRingProperties
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem _root_.Transcendental.isDedekindDomain_adjoin_s12 {t : F} (ht : Transcendental K
  t) :
    IsDedekindDomain ↥(Algebra.adjoin K ({t} : Set F))
theorem

isIntegrallyClosed_adjoin_s12

L873 ↗
Transcendental.isIntegrallyClosed_adjoin_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section AdjoinRingProperties
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem _root_.Transcendental.isIntegrallyClosed_adjoin_s12 {t : F} (ht : Transcendental K
  t) :
    IsIntegrallyClosed ↥(Algebra.adjoin K ({t} : Set F))
theorem

isNoetherianRing_adjoin_s12

L880 ↗
Transcendental.isNoetherianRing_adjoin_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section AdjoinRingProperties
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem _root_.Transcendental.isNoetherianRing_adjoin_s12 {t : F} (ht : Transcendental K
  t) :
    IsNoetherianRing ↥(Algebra.adjoin K ({t} : Set F))
theorem

adjoin_singleton_s12

L887 ↗
Algebra.FiniteType.adjoin_singleton_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section AdjoinRingProperties
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem _root_.Algebra.FiniteType.adjoin_singleton_s12 (t : F) :
    Algebra.FiniteType K ↥(Algebra.adjoin K ({t} : Set F))
theorem

inv_s12

L891 ↗
Transcendental.inv_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section AdjoinRingProperties
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem _root_.Transcendental.inv_s12 {t : F} (ht : Transcendental K t) :
    Transcendental K t⁻¹
def

transcendentalChart

L902 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.transcendentalChart
Documentation

The integral closure of the algebra generated by the chosen element.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section TranscendentalChart
variable (K : Type*) {F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
def transcendentalChart (t : F) : Subalgebra K F
theorem

coe_transcendentalChart

L905 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.coe_transcendentalChart
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section TranscendentalChart
variable (K : Type*) {F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem coe_transcendentalChart (t : F) :
    (transcendentalChart K t : Set F)
      = ((integralClosure (Algebra.adjoin K ({t} : Set F)) F : Subalgebra _ F) : Set F)
theorem

transcendentalChart_subset_valuationSubring_of_mem

L912 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.transcendentalChart_subset_valuationSubring_of_mem
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section TranscendentalChart
variable (K : Type*) {F : Type*} [Field K] [Field F] [Algebra K F]
variable {K}
Lean source · statement
theorem transcendentalChart_subset_valuationSubring_of_mem (v : Place K F)
    {t : F} (ht : t ∈ v.toValuationSubring) :
    (transcendentalChart K t : Set F) ⊆ (v.toValuationSubring : Set F)
theorem

transcendentalChart_subset_or_inv_subset

L919 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.transcendentalChart_subset_or_inv_subset
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section TranscendentalChart
variable (K : Type*) {F : Type*} [Field K] [Field F] [Algebra K F]
variable {K}
Lean source · statement
theorem transcendentalChart_subset_or_inv_subset (v : Place K F) (t : F) :
    (transcendentalChart K t : Set F) ⊆ (v.toValuationSubring : Set F)
      ∨ (transcendentalChart K t⁻¹ : Set F) ⊆ (v.toValuationSubring : Set F)
theorem

isScalarTower_integralClosure_subalgebra

L936 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.isScalarTower_integralClosure_subalgebra
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section IsAffineChartEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section
variable (B : Subalgebra K F)
Lean source · statement
theorem isScalarTower_integralClosure_subalgebra :
    IsScalarTower K B ↥(integralClosure B F)
theorem

finiteType_integralClosure_of_moduleFinite

L941 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.finiteType_integralClosure_of_moduleFinite
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section IsAffineChartEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section
variable (B : Subalgebra K F)
Lean source · statement
theorem finiteType_integralClosure_of_moduleFinite (hft : Algebra.FiniteType K B)
    (hfin : Module.Finite B ↥(integralClosure B F)) :
    Algebra.FiniteType K ↥(integralClosure B F)
theorem

isDedekindDomain_integralClosure_adjoin

L950 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.isDedekindDomain_integralClosure_adjoin
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section IsAffineChartEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isDedekindDomain_integralClosure_adjoin {t : F} (ht : Transcendental K t)
    [FiniteDimensional K⟮t⟯ F] [Algebra.IsSeparable K⟮t⟯ F] :
    IsDedekindDomain ↥(integralClosure (Algebra.adjoin K ({t} : Set F)) F)
theorem

isFractionRing_integralClosure_adjoin

L956 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.isFractionRing_integralClosure_adjoin
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section IsAffineChartEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isFractionRing_integralClosure_adjoin (t : F) [FiniteDimensional K⟮t⟯ F] :
    IsFractionRing ↥(integralClosure (Algebra.adjoin K ({t} : Set F)) F) F
theorem

moduleFinite_integralClosure_adjoin

L961 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.moduleFinite_integralClosure_adjoin
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section IsAffineChartEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem moduleFinite_integralClosure_adjoin {t : F} (ht : Transcendental K t)
    [FiniteDimensional K⟮t⟯ F] [Algebra.IsSeparable K⟮t⟯ F] :
    Module.Finite ↥(Algebra.adjoin K ({t} : Set F))
      ↥(integralClosure (Algebra.adjoin K ({t} : Set F)) F)
theorem

finiteType_integralClosure_adjoin

L970 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.finiteType_integralClosure_adjoin
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section IsAffineChartEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finiteType_integralClosure_adjoin {t : F} (ht : Transcendental K t)
    [FiniteDimensional K⟮t⟯ F] [Algebra.IsSeparable K⟮t⟯ F] :
    Algebra.FiniteType K ↥(integralClosure (Algebra.adjoin K ({t} : Set F)) F)
theorem

isAffineChart_restrictScalars_integralClosure

L976 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.isAffineChart_restrictScalars_integralClosure
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section IsAffineChartEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isAffineChart_restrictScalars_integralClosure (B : Subalgebra K F)
    (hft : Algebra.FiniteType K ↥(integralClosure B F))
    (hded : IsDedekindDomain ↥(integralClosure B F))
    (hfrac : IsFractionRing ↥(integralClosure B F) F) :
    IsAffineChart K F ((integralClosure B F).restrictScalars K)
theorem

isAffineChart_transcendentalChart

L983 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.isAffineChart_transcendentalChart
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section IsAffineChartEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isAffineChart_transcendentalChart {t : F} (ht : Transcendental K t)
    [FiniteDimensional K⟮t⟯ F] [Algebra.IsSeparable K⟮t⟯ F] :
    IsAffineChart K F (transcendentalChart K t)
def

HasSeparatingTranscendental

L998 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.HasSeparatingTranscendental
Documentation

A transcendental element giving finite separable extensions for itself and its inverse.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section SeparatingTranscendental
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def HasSeparatingTranscendental : Prop
theorem

valSubringTwoAffineCharts_of_hasSeparatingTranscendental

L1005 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringTwoAffineCharts_of_hasSeparatingTranscendental
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section SeparatingTranscendental
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringTwoAffineCharts_of_hasSeparatingTranscendental
    (h : HasSeparatingTranscendental K F) :
    ValSubringTwoAffineCharts K F
theorem

valSubringDedekindModel_of_hasSeparatingTranscendental

L1014 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringDedekindModel_of_hasSeparatingTranscendental
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section SeparatingTranscendental
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
Lean source · statement
theorem valSubringDedekindModel_of_hasSeparatingTranscendental
    (h : HasSeparatingTranscendental K F) :
    ValSubringDedekindModel K F
theorem

adjoin_simple_inv_s12

L1032 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.IntermediateField.adjoin_simple_inv_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
namespace IntermediateField
open _root_.IntermediateField
open _root_.IntermediateField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem adjoin_simple_inv_s12 (t : F) : K⟮t⁻¹⟯ = K⟮t⟯
theorem

algebraMap_comp_equivOfEq_s12

L1039 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.IntermediateField.algebraMap_comp_equivOfEq_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
namespace IntermediateField
open _root_.IntermediateField
open _root_.IntermediateField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem algebraMap_comp_equivOfEq_s12 {S T : IntermediateField K F} (h : S = T) :
    (algebraMap T F).comp ((IntermediateField.equivOfEq h).toRingEquiv : S →+* T)
      = ((RingEquiv.refl F : F ≃+* F) : F →+* F).comp (algebraMap S F)
theorem

finiteDimensional_of_eq_s12

L1044 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.IntermediateField.finiteDimensional_of_eq_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
namespace IntermediateField
open _root_.IntermediateField
open _root_.IntermediateField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finiteDimensional_of_eq_s12 {S T : IntermediateField K F} (h : S = T)
    [FiniteDimensional ↥S F] : FiniteDimensional ↥T F
theorem

isSeparable_of_eq_s12

L1049 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.IntermediateField.isSeparable_of_eq_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
namespace IntermediateField
open _root_.IntermediateField
open _root_.IntermediateField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isSeparable_of_eq_s12 {S T : IntermediateField K F} (h : S = T)
    [Algebra.IsSeparable ↥S F] : Algebra.IsSeparable ↥T F
theorem

finiteDimensional_adjoin_inv_s12

L1054 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.IntermediateField.finiteDimensional_adjoin_inv_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
namespace IntermediateField
open _root_.IntermediateField
open _root_.IntermediateField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem finiteDimensional_adjoin_inv_s12 (t : F) [FiniteDimensional K⟮t⟯ F] :
    FiniteDimensional K⟮t⁻¹⟯ F
theorem

isSeparable_adjoin_inv_s12

L1058 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.IntermediateField.isSeparable_adjoin_inv_s12
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
namespace IntermediateField
open _root_.IntermediateField
open _root_.IntermediateField
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isSeparable_adjoin_inv_s12 (t : F) [Algebra.IsSeparable K⟮t⟯ F] :
    Algebra.IsSeparable K⟮t⁻¹⟯ F
theorem

dCoordGenerates_of_valSubringKaehlerSpanTop

L1075 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.dCoordGenerates_of_valSubringKaehlerSpanTop
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section AbstractEngine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.dCoordGenerates_of_valSubringKaehlerSpanTop
    (hspan : ValSubringKaehlerSpanTop K F) (v : Place K F) :
    v.DCoordGenerates
theorem

isSeparable_residueField_of_perfectField_of_finiteResidue

L1113 ↗
AlgebraicCurve.Place.isSeparable_residueField_of_perfectField_of_finiteResidue
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section PerPlaceSupply
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem
  _root_.AlgebraicCurve.Place.isSeparable_residueField_of_perfectField_of_finiteResidue
    [PerfectField K] (v : Place K F) [v.FiniteResidue] :
    Algebra.IsSeparable K (IsLocalRing.ResidueField v.toValuationSubring)
theorem

isSeparable_residueField_forall_of_perfectField

L1125 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.isSeparable_residueField_forall_of_perfectField
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section PerPlaceSupply
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
Lean source · statement
theorem isSeparable_residueField_forall_of_perfectField
    [PerfectField K] [∀ v : Place K F, v.FiniteResidue] :
    ∀ v : Place K F,
      Algebra.IsSeparable K (IsLocalRing.ResidueField v.toValuationSubring)
theorem

valSubringKaehlerSpanTop_of_kaehlerFinite_of_isSeparable

L1137 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringKaehlerSpanTop_of_kaehlerFinite_of_isSeparable
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section IsSeparableEngines
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem valSubringKaehlerSpanTop_of_kaehlerFinite_of_isSeparable
    [∀ v : Place K F, Algebra.IsSeparable K (IsLocalRing.ResidueField v.toValuationSubring)]
    (hfin : ValSubringKaehlerFinite K F) :
    ValSubringKaehlerSpanTop K F
theorem

dCoordGenerates_of_valSubringKaehlerFinite_of_isSeparable

L1145 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.dCoordGenerates_of_valSubringKaehlerFinite_of_isSeparable
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section IsSeparableEngines
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.dCoordGenerates_of_valSubringKaehlerFinite_of_isSeparable
    [∀ v : Place K F, Algebra.IsSeparable K (IsLocalRing.ResidueField v.toValuationSubring)]
    (hfin : ValSubringKaehlerFinite K F) (v : Place K F) :
    v.DCoordGenerates
theorem

dCoordGenerates_of_valSubringKaehlerFinite_of_perfectField

L1159 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.dCoordGenerates_of_valSubringKaehlerFinite_of_perfectField
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section PerfectFieldEngines
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.dCoordGenerates_of_valSubringKaehlerFinite_of_perfectField
    [PerfectField K] [∀ v : Place K F, v.FiniteResidue]
    (hfin : ValSubringKaehlerFinite K F) (v : Place K F) :
    v.DCoordGenerates
theorem

dCoordGenerates_of_valSubringFiniteTypeModel_of_perfectField

L1183 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.dCoordGenerates_of_valSubringFiniteTypeModel_of_perfectField
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12ChainWires
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.dCoordGenerates_of_valSubringFiniteTypeModel_of_perfectField
    [PerfectField K] [∀ v : Place K F, v.FiniteResidue]
    (hmodel : ValSubringFiniteTypeModel K F) (v : Place K F) :
    v.DCoordGenerates
theorem

dCoordGenerates_of_valSubringDedekindModel_of_perfectField

L1191 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.dCoordGenerates_of_valSubringDedekindModel_of_perfectField
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12ChainWires
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.dCoordGenerates_of_valSubringDedekindModel_of_perfectField
    [PerfectField K] [∀ v : Place K F, v.FiniteResidue]
    (hmodel : ValSubringDedekindModel K F) (v : Place K F) :
    v.DCoordGenerates
theorem

dCoordGenerates_of_hasSeparatingTranscendental_of_perfectField

L1199 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.Place.dCoordGenerates_of_hasSeparatingTranscendental_of_perfectField
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12ChainWires
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.dCoordGenerates_of_hasSeparatingTranscendental_of_perfectField
    [PerfectField K] [∀ v : Place K F, v.FiniteResidue]
    (hsep : HasSeparatingTranscendental K F) (v : Place K F) :
    v.DCoordGenerates
theorem

hasSeparatingTranscendental_of_isCurveOver_of_perfectField

L1208 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.hasSeparatingTranscendental_of_isCurveOver_of_perfectField
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12ChainWires
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.IntermediateField
  _root_.AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.IntermediateField in
Lean source · statement
theorem hasSeparatingTranscendental_of_isCurveOver_of_perfectField
    [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F] :
    HasSeparatingTranscendental K F
theorem

valSubringKaehlerSpanTop_of_isCurveOver_of_perfectField_s12

L1232 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.valSubringKaehlerSpanTop_of_isCurveOver_of_perfectField_s12
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12WellDefined
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem valSubringKaehlerSpanTop_of_isCurveOver_of_perfectField_s12
    [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F] :
    ValSubringKaehlerSpanTop K F
theorem

ord_nonneg_of_mem_s12

L1250 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem_s12
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12WellDefined
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem_s12 {f : F} (hf : f ∈
  v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg_s12

L1267 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg_s12
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12WellDefined
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_of_ord_nonneg_s12 {f : F} (hf : f ≠ 0) (h : 0 ≤
  v.ord f) :
    f ∈ v.toValuationSubring
theorem

ord_uniformizerSubring'_s12

L1277 ↗
AlgebraicCurve.Place.ord_uniformizerSubring'_s12
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12WellDefined
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_uniformizerSubring'_s12 : v.ord
  (uniformizerSubring' v : F) = 1
theorem

dCoord_eq_D_uniformizerSubring'_s12

L1283 ↗
AlgebraicCurve.Place.dCoord_eq_D_uniformizerSubring'_s12
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12WellDefined
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.dCoord_eq_D_uniformizerSubring'_s12 :
    v.dCoord = KaehlerDifferential.D K F (uniformizerSubring' v : F)
theorem

exists_mem_D_eq_smul_dCoord_s12

L1288 ↗
AlgebraicCurve.Place.exists_mem_D_eq_smul_dCoord_s12
Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12WellDefined
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_mem_D_eq_smul_dCoord_s12 (hspan :
  ValSubringKaehlerSpanTop K F)
    {x : F} (hx : x ∈ v.toValuationSubring) :
    ∃ c : F, c ∈ v.toValuationSubring ∧ KaehlerDifferential.D K F x = c • v.dCoord
theorem

exists_unit_D_eq_smul_dCoord_s12

L1308 ↗
AlgebraicCurve.Place.exists_unit_D_eq_smul_dCoord_s12
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12WellDefined
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_unit_D_eq_smul_dCoord_s12 (hspan :
  ValSubringKaehlerSpanTop K F)
    [Nontrivial Ω[F⁄K]] [v.DCoordGenerates] {ϖ : F} (hϖ : v.ord ϖ = 1) :
    ∃ w : F, w ≠ 0 ∧ v.ord w = 0 ∧ KaehlerDifferential.D K F ϖ = w • v.dCoord
theorem

exists_ord_eq_zero_D_eq_smul_D_s12

L1368 ↗
AlgebraicCurve.Place.exists_ord_eq_zero_D_eq_smul_D_s12
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12WellDefined
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_ord_eq_zero_D_eq_smul_D_s12 (hspan :
  ValSubringKaehlerSpanTop K F)
    [Nontrivial Ω[F⁄K]] [v.DCoordGenerates]
    (π π' : F) (hπ : v.ord π = 1) (hπ' : v.ord π' = 1) :
    ∃ u : F, v.ord u = 0 ∧ KaehlerDifferential.D K F π' = u • KaehlerDifferential.D K F π
theorem

exists_ord_eq_zero_D_eq_smul_D_of_isCurveOver_s12

L1382 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.exists_ord_eq_zero_D_eq_smul_D_of_isCurveOver_s12
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12WellDefined
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_ord_eq_zero_D_eq_smul_D_of_isCurveOver_s12
    [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
    (v : Place K F) (π π' : F) (hπ : v.ord π = 1) (hπ' : v.ord π' = 1) :
    ∃ u : F, v.ord u = 0 ∧ KaehlerDifferential.D K F π' = u • KaehlerDifferential.D K F π
theorem

exists_mem_D_eq_smul_D_of_isCurveOver_s12

L1390 ↗
AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve.AlgebraicCurve.exists_mem_D_eq_smul_D_of_isCurveOver_s12
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section S12WellDefined
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_mem_D_eq_smul_D_of_isCurveOver_s12
    [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
    (v : Place K F) {π : F} (hπ : v.ord π = 1) {x : F} (hx : x ∈ v.toValuationSubring) :
    ∃ c : F, c ∈ v.toValuationSubring ∧ KaehlerDifferential.D K F x = c • KaehlerDifferential.D K
      F π
theorem

exists_mem_D_eq_smul_D_of_isCurveOver

L1413 ↗
AlgebraicCurve.exists_mem_D_eq_smul_D_of_isCurveOver
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ExistsMemDSmulDCurve
open IsDedekindDomain
open IsDedekindDomain Polynomial
open IsDedekindDomain Polynomial IsLocalRing
open scoped TensorProduct
open IsDedekindDomain Polynomial IsLocalRing
open IsDedekindDomain Polynomial IsLocalRing
open IsLocalRing
open IsLocalRing
open _root_.IsLocalRing
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.IntermediateField
open _root_.IntermediateField
noncomputable section
Lean source · statement
theorem _root_.AlgebraicCurve.exists_mem_D_eq_smul_D_of_isCurveOver
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    [PerfectField K] [Algebra.EssFiniteType K F] [AlgebraicCurve.IsCurveOver K F]
    (v : AlgebraicCurve.Place K F) {π : F} (hπ : v.ord π = 1) {x : F} (hx : x ∈
      v.toValuationSubring) :
    ∃ c : F, c ∈ v.toValuationSubring ∧ KaehlerDifferential.D K F x = c • KaehlerDifferential.D K
      F π

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