Module

HasCanonicalDivisor_of_isCurveOver.lean

Nyll.AlgebraicCurves.Divisors.HasCanonicalDivisor_of_isCurveOver

136 declarations indexed from sourceView source ↗

Module documentation

Algebra, divisors, and base change

Finite-type valuation-ring charts and separating coordinates produce canonical divisors for curve function fields.

Imports8

Imported by23

def

uniformizerSubring'

L46 ↗

AlgebraicCurve.Place.uniformizerSubring'

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L50 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.instSMulCommClass_subring

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L53 ↗

AlgebraicCurve.Place.kaehlerMap_subring_D_uniformizer

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L68 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.ValSubringKaehlerSpanTop

Documentation

At every place, the differential of the chosen valuation-ring uniformizer generates the module of Kähler differentials.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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''

L90 ↗

AlgebraicCurve.Place.uniformizerSubring''

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L94 ↗

AlgebraicCurve.Place.polynomialAlgebra

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L99 ↗

AlgebraicCurve.Place.polynomialAlgebra_algebraMap_X

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L105 ↗

AlgebraicCurve.Place.polynomialIsScalarTower

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L114 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L137 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L150 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L169 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L176 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringKaehlerSpanTop_of_polynomialFormallyUnramified

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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'''

L198 ↗

AlgebraicCurve.Place.uniformizerSubring'''

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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'''

L203 ↗

AlgebraicCurve.Place.irreducible_uniformizerSubring'''

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L208 ↗

AlgebraicCurve.Place.maximalIdeal_eq_span_uniformizer

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L213 ↗

AlgebraicCurve.Place.D_polynomialAlgebra_uniformizer

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L222 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L229 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L241 ↗

AlgebraicCurve.Place.subsingleton_residueKaehler_of_isSeparable

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L250 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L284 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L295 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L313 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.ValSubringKaehlerFinite

Documentation

The Kähler differentials of every valuation ring form a finite module.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L318 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringPolynomialFormallyUnramified_of_kaehlerFinite_of_isSeparable

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L341 ↗

AlgebraicCurve.Place.finite_kaehler_of_essFiniteType

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L347 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L362 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.ValSubringEssFiniteType

Documentation

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

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L366 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L373 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringKaehlerFinite_of_essFiniteType

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L379 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringEssFiniteType_of_finiteTypeModel

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L384 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringEssFiniteType_iff_finiteTypeModel

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L392 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringKaehlerFinite_of_finiteTypeModel

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L407 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.ValuationSubring.ofPrime_congr_s12

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L411 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L416 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L420 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L445 ↗

AlgebraicCurve.Place.modelInclusion

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L450 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.coe_modelInclusion

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L453 ↗

AlgebraicCurve.Place.modelAlgebra

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L458 ↗

AlgebraicCurve.Place.centerIdeal

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L463 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.centerIdeal_isPrime

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L467 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L476 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L482 ↗

AlgebraicCurve.Place.modelAlgebra_isScalarTower

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L492 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L512 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L521 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringEssFiniteType_of_dedekindModel

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L527 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringFiniteTypeModel_of_dedekindModel

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L550 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L564 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L571 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L595 ↗

AlgebraicCurve.Place.centerLocalizationSubalgebra

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L602 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.centerLocalizationSubalgebra_isLocalization

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L606 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.centerLocalizationSubalgebra_isDomain

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L610 ↗

AlgebraicCurve.Place.centerLocalizationSubalgebra_isDiscreteValuationRing

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L617 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.centerLocalizationSubalgebra_isFractionRing

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L621 ↗

AlgebraicCurve.Place.centerLocalizationSubalgebra_subset

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L631 ↗

AlgebraicCurve.Place.centerLocalizationValuationSubring

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L642 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.coe_centerLocalizationValuationSubring

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L646 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.centerLocalizationValuationSubring_isDiscreteValuationRing

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L651 ↗

AlgebraicCurve.Place.centerLocalizationValuationSubring_le

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L657 ↗

AlgebraicCurve.Place.centerLocalizationValuationSubring_eq

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L664 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.coe_centerLocalizationSubalgebra_eq

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L670 ↗

AlgebraicCurve.Place.mem_centerLocalizationSubalgebra_of_mem

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L677 ↗

AlgebraicCurve.Place.isLocalization_centerIdeal_of_isDedekindDomain

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L711 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.ValSubringDedekindFractionModel

Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L718 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringDedekindModel_of_dedekindFractionModel

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L740 ↗

AlgebraicCurve.Place.isIntegrallyClosed_toValuationSubring

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L744 ↗

AlgebraicCurve.Place.mem_valuationSubring_of_isIntegral

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L754 ↗

AlgebraicCurve.Place.modelAlgebra_isScalarTower_top

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L763 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L772 ↗

AlgebraicCurve.Place.integralClosure_subset_valuationSubring

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L787 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.IsAffineChart

Documentation

A finite-type Dedekind subalgebra with the given function field as fraction field.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L791 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.ValSubringTwoAffineCharts

Documentation

Two affine charts cover the places: every valuation ring contains at least one chart.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L798 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringDedekindFractionModel_of_twoAffineCharts

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L806 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringDedekindModel_of_twoAffineCharts

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L829 ↗

AlgebraicCurve.Place.toKSubalgebra

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L838 ↗

AlgebraicCurve.Place.coe_toKSubalgebra

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L843 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L866 ↗

Transcendental.isPrincipalIdealRing_adjoin_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L874 ↗

Transcendental.isDedekindDomain_adjoin_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L881 ↗

Transcendental.isIntegrallyClosed_adjoin_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L888 ↗

Transcendental.isNoetherianRing_adjoin_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L895 ↗

Algebra.FiniteType.adjoin_singleton_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L899 ↗

Transcendental.inv_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L911 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.transcendentalChart

Documentation

The integral closure of the algebra generated by the chosen function, restricted to the base field.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L914 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.coe_transcendentalChart

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L921 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.transcendentalChart_subset_valuationSubring_of_mem

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L928 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.transcendentalChart_subset_or_inv_subset

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L945 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.isScalarTower_integralClosure_subalgebra

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L950 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.finiteType_integralClosure_of_moduleFinite

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L959 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.isDedekindDomain_integralClosure_adjoin

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L965 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.isFractionRing_integralClosure_adjoin

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L970 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.moduleFinite_integralClosure_adjoin

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L979 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.finiteType_integralClosure_adjoin

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L985 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.isAffineChart_restrictScalars_integralClosure

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L992 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.isAffineChart_transcendentalChart

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1008 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.HasSeparatingTranscendental

Documentation

A transcendental function makes the field finite and separable over both its rational- function subfield and the subfield generated by its inverse.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1015 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringTwoAffineCharts_of_hasSeparatingTranscendental

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1024 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringDedekindModel_of_hasSeparatingTranscendental

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1042 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.IntermediateField.adjoin_simple_inv_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1049 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.IntermediateField.algebraMap_comp_equivOfEq_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1054 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.IntermediateField.finiteDimensional_of_eq_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1059 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.IntermediateField.isSeparable_of_eq_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1064 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.IntermediateField.finiteDimensional_adjoin_inv_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1068 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.IntermediateField.isSeparable_adjoin_inv_s12

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1085 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.dCoordGenerates_of_valSubringKaehlerSpanTop

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1123 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1135 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.isSeparable_residueField_forall_of_perfectField

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1147 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.valSubringKaehlerSpanTop_of_kaehlerFinite_of_isSeparable

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1155 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1169 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1193 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1201 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1209 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1218 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.hasSeparatingTranscendental_of_isCurveOver_of_perfectField

Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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

L1242 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1260 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1277 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1287 ↗

AlgebraicCurve.Place.ord_uniformizerSubring'_s12

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1293 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1298 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1319 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1379 ↗

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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1393 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

L1401 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.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.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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

hasCanonicalDivisor_of_generator_finiteSupport_s12

L1439 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.hasCanonicalDivisor_of_generator_finiteSupport_s12

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.Polynomial
section S12HCD
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem hasCanonicalDivisor_of_generator_finiteSupport_s12
    [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates]
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (hgen : Submodule.span F ({ω₀} : Set Ω[F⁄K]) = ⊤)
    (hfin : {v : Place K F | v.ordDifferential ω₀ ≠ 0}.Finite) :
    HasCanonicalDivisor (K := K) (F := F)

theorem

ordDifferential_D_eq_zero_of_span_eq_top_s12

L1459 ↗

AlgebraicCurve.Place.ordDifferential_D_eq_zero_of_span_eq_top_s12

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.Polynomial
section S12HCD
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.ordDifferential_D_eq_zero_of_span_eq_top_s12
  (hspan : ValSubringKaehlerSpanTop K F)
    [Nontrivial Ω[F⁄K]] (v : Place K F) [v.DCoordGenerates]
    (s : v.toValuationSubring)
    (hs : Submodule.span v.toValuationSubring
      ({KaehlerDifferential.D K v.toValuationSubring s} : Set Ω[v.toValuationSubring⁄K]) = ⊤) :
    v.ordDifferential (KaehlerDifferential.D K F (s : F)) = 0

theorem

mem_span_D_adjoin_s12

L1514 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.mem_span_D_adjoin_s12

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.Polynomial
section S12HCD
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve

Lean source · statement

theorem mem_span_D_adjoin_s12 (t : F) (ω : Ω[↥(Algebra.adjoin K ({t} : Set F))⁄K]) :
    ω ∈ Submodule.span ↥(Algebra.adjoin K ({t} : Set F))
      (Set.singleton (KaehlerDifferential.D K ↥(Algebra.adjoin K ({t} : Set F))
        ⟨t, Algebra.self_mem_adjoin_singleton K t⟩) : Set Ω[↥(Algebra.adjoin K ({t} :
          Set F))⁄K])

theorem

span_D_eq_top_of_isUnramifiedAt_s12

L1538 ↗

AlgebraicCurve.Place.span_D_eq_top_of_isUnramifiedAt_s12

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.Polynomial
section S12HCD
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
namespace Place
open scoped _root_.AlgebraicCurve.Place in

Lean source · full declaration

theorem _root_.AlgebraicCurve.Place.span_D_eq_top_of_isUnramifiedAt_s12 (v : Place K F)
  (T : Subalgebra K F)
    (hT : (T : Set F) ⊆ (v.toValuationSubring : Set F))
    {t : F} (hRT : Algebra.adjoin K ({t} : Set F) ≤ T)
    [IsDedekindDomain T] [IsFractionRing T F]
    (hunr : letI : Algebra ↥(Algebra.adjoin K ({t} : Set F)) T :=
      (Subalgebra.inclusion hRT).toRingHom.toAlgebra
      Algebra.IsUnramifiedAt ↥(Algebra.adjoin K ({t} : Set F)) (v.centerIdeal T hT)) :
    Submodule.span v.toValuationSubring
      (Set.singleton (KaehlerDifferential.D K v.toValuationSubring
        ⟨t, hT (hRT (Algebra.self_mem_adjoin_singleton K t))⟩) :
          Set Ω[v.toValuationSubring⁄K]) = ⊤ := by
  let iRT : Algebra ↥(Algebra.adjoin K ({t} : Set F)) T :=
    (Subalgebra.inclusion hRT).toRingHom.toAlgebra
  let iTO : Algebra T v.toValuationSubring := v.modelAlgebra T hT
  let iRO : Algebra ↥(Algebra.adjoin K ({t} : Set F)) v.toValuationSubring :=
    ((algebraMap T v.toValuationSubring).comp (algebraMap ↥(Algebra.adjoin K ({t} :
      Set F)) T)).toAlgebra
  have : IsScalarTower ↥(Algebra.adjoin K ({t} : Set F)) T v.toValuationSubring :=
    IsScalarTower.of_algebraMap_eq fun _ => rfl
  have : IsScalarTower K ↥(Algebra.adjoin K ({t} : Set F)) v.toValuationSubring :=
    IsScalarTower.of_algebraMap_eq fun a => Subtype.ext rfl
  have hloc := v.isLocalization_centerIdeal_of_isDedekindDomain T hT
  have : Algebra.FormallyUnramified ↥(Algebra.adjoin K ({t} : Set F))
      (Localization.AtPrime (v.centerIdeal T hT)) := hunr
  let e : Localization.AtPrime (v.centerIdeal T hT) ≃ₐ[T] v.toValuationSubring :=
    IsLocalization.algEquiv (v.centerIdeal T hT).primeCompl _ _
  have : Algebra.FormallyUnramified ↥(Algebra.adjoin K ({t} : Set F)) v.toValuationSubring :=
    Algebra.FormallyUnramified.of_equiv (e.restrictScalars ↥(Algebra.adjoin K ({t} : Set F)))
  have hsub : Subsingleton Ω[v.toValuationSubring⁄↥(Algebra.adjoin K ({t} : Set F))] :=
    Algebra.FormallyUnramified.subsingleton_kaehlerDifferential
  have hrange : LinearMap.range
      (KaehlerDifferential.mapBaseChange K ↥(Algebra.adjoin K ({t} :
        Set F)) v.toValuationSubring) = ⊤ := by
    rw [KaehlerDifferential.range_mapBaseChange]
    exact LinearMap.ker_eq_top.mpr (Subsingleton.elim _ _)
  have htO : algebraMap ↥(Algebra.adjoin K ({t} : Set F)) v.toValuationSubring
      ⟨t, Algebra.self_mem_adjoin_singleton K t⟩
        = ⟨t, hT (hRT (Algebra.self_mem_adjoin_singleton K t))⟩ := Subtype.ext rfl
  have hle : LinearMap.range
      (KaehlerDifferential.mapBaseChange K ↥(Algebra.adjoin K ({t} : Set F)) v.toValuationSubring)
      ≤ Submodule.span v.toValuationSubring
        (Set.singleton (KaehlerDifferential.D K v.toValuationSubring
          ⟨t, hT (hRT (Algebra.self_mem_adjoin_singleton K t))⟩) :
            Set Ω[v.toValuationSubring⁄K]) := by
    rintro _ ⟨x, rfl⟩
    induction x with
    | add x y hx hy => rw [map_add]; exact add_mem hx hy
    | tmul b ω =>
      rw [KaehlerDifferential.mapBaseChange_tmul]
      refine Submodule.smul_mem _ b ?_
      obtain ⟨r, hr⟩ := Submodule.mem_span_singleton.mp (mem_span_D_adjoin_s12 t ω)
      rw [← hr, LinearMap.map_smul_of_tower, KaehlerDifferential.map_D, htO]
      exact Submodule.smul_mem _ _ (Submodule.subset_span rfl)
  exact top_le_iff.mp (hrange ▸ hle)

theorem

eq_of_centerIdeal_eq_s12

L1598 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.Place.eq_of_centerIdeal_eq_s12

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.Polynomial
section S12HCD
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve.Place in

Lean source · statement

theorem Place.eq_of_centerIdeal_eq_s12 (T : Subalgebra K F) [IsDedekindDomain T]
  [IsFractionRing T F]
    {v₁ v₂ : Place K F} (h₁ : (T : Set F) ⊆ (v₁.toValuationSubring : Set F))
    (h₂ : (T : Set F) ⊆ (v₂.toValuationSubring : Set F))
    (hP : v₁.centerIdeal T h₁ = v₂.centerIdeal T h₂) : v₁ = v₂

theorem

adjoin_le_transcendentalChart_s12

L1614 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.adjoin_le_transcendentalChart_s12

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.Polynomial
section S12HCD
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem adjoin_le_transcendentalChart_s12 (t : F) :
    Algebra.adjoin K ({t} : Set F) ≤ transcendentalChart K t

theorem

finite_ordDifferential_D_ne_zero_s12

L1623 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.finite_ordDifferential_D_ne_zero_s12

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.Polynomial
section S12HCD
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra

Lean source · statement

theorem finite_ordDifferential_D_ne_zero_s12 (hspan : ValSubringKaehlerSpanTop K F)
    [IsCurveOver K F] [∀ v : Place K F, v.DCoordGenerates] [PerfectField K]
    {t : F} (htr : Transcendental K t) [FiniteDimensional K⟮t⟯ F] [Algebra.IsSeparable K⟮t⟯ F] :
    {v : Place K F | v.ordDifferential (KaehlerDifferential.D K F t) ≠ 0}.Finite

theorem

hasCanonicalDivisor_of_isCurveOver_s12

L1722 ↗

AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver.AlgebraicCurve.hasCanonicalDivisor_of_isCurveOver_s12

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasCanonicalDivisor_of_isCurveOver
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
open _root_.KaehlerDifferential
open _root_.IntermediateField
open _root_.IntermediateField.algebraAdjoinAdjoin
open _root_.Polynomial
section S12HCD
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance] FractionRing.liftAlgebra FractionRing.isScalarTower_liftAlgebra

Lean source · statement

theorem hasCanonicalDivisor_of_isCurveOver_s12
    [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F] :
    HasCanonicalDivisor (K := K) (F := F)

theorem