Module

ChartAlgebra.lean

Nyll.AlgebraicCurves.Models.ChartAlgebra

47 declarations indexed from sourceView source ↗

Module documentation

Chart Algebra

Imports11

Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.DedekindDomain.AdicValuation
Mathlib.RingTheory.Localization.Integral
Mathlib.RingTheory.Valuation.Integral
Mathlib.RingTheory.Polynomial.ScaleRoots
Mathlib.Algebra.Polynomial.Lifts
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.RingTheory.Adjoin.Polynomial.Basic
Mathlib.RingTheory.Algebraic.Basic
Mathlib.FieldTheory.Perfect
Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by4

def

aevalAdjoin

L42 ↗

AlgebraicCurve.CurveModel.aevalAdjoin

Documentation

Evaluation into the subalgebra generated by the chosen element.

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

def aevalAdjoin (s : L) : K[X] →ₐ[K] Algebra.adjoin K ({s} : Set L)

theorem

aevalAdjoin_surjective

L46 ↗

AlgebraicCurve.CurveModel.aevalAdjoin_surjective

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem aevalAdjoin_surjective (s : L) : Function.Surjective (aevalAdjoin K s)

instance

isPrincipalIdealRing_adjoin_singleton

L52 ↗

AlgebraicCurve.CurveModel.isPrincipalIdealRing_adjoin_singleton

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

instance isPrincipalIdealRing_adjoin_singleton (s : L) :
    IsPrincipalIdealRing (Algebra.adjoin K ({s} : Set L))

instance

isDedekindDomain_adjoin_singleton

L56 ↗

AlgebraicCurve.CurveModel.isDedekindDomain_adjoin_singleton

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

instance isDedekindDomain_adjoin_singleton (s : L) :
    IsDedekindDomain (Algebra.adjoin K ({s} : Set L))

def

chartRing

L61 ↗

AlgebraicCurve.CurveModel.chartRing

Documentation

The integral closure of the coordinate subalgebra in the given function field.

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · full declaration

def chartRing (S : Set L) : Subalgebra K L where
  carrier := {x | IsIntegral (Algebra.adjoin K S) x}
  mul_mem' ha hb := ha.mul hb
  one_mem' := isIntegral_one
  add_mem' ha hb := ha.add hb
  zero_mem' := isIntegral_zero
  algebraMap_mem' a := by
    have : IsIntegral (Algebra.adjoin K S)
        (algebraMap (Algebra.adjoin K S) L (algebraMap K (Algebra.adjoin K S) a)) :=
      isIntegral_algebraMap
    simpa [← IsScalarTower.algebraMap_apply] using this

theorem

mem_chartRing_iff

L73 ↗

AlgebraicCurve.CurveModel.mem_chartRing_iff

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem mem_chartRing_iff {S : Set L} {x : L} :
    x ∈ chartRing K S ↔ IsIntegral (Algebra.adjoin K S) x

theorem

adjoin_le_chartRing

L76 ↗

AlgebraicCurve.CurveModel.adjoin_le_chartRing

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem adjoin_le_chartRing (S : Set L) : Algebra.adjoin K S ≤ chartRing K S

theorem

subset_chartRing

L83 ↗

AlgebraicCurve.CurveModel.subset_chartRing

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem subset_chartRing (S : Set L) : S ⊆ (chartRing K S : Set L)

theorem

chartRing_mono

L86 ↗

AlgebraicCurve.CurveModel.chartRing_mono

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem chartRing_mono {S S' : Set L} (h : S ⊆ S') : chartRing K S ≤ chartRing K S'

abbrev

chartIncl

L94 ↗

AlgebraicCurve.CurveModel.chartIncl

Documentation

The inclusion of chart rings induced by inclusion of the generating sets.

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

abbrev chartIncl {S S' : Set L} (h : S ⊆ S') : chartRing K S →ₐ[K] chartRing K S'

theorem

coe_chartIncl

L97 ↗

AlgebraicCurve.CurveModel.coe_chartIncl

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem coe_chartIncl {S S' : Set L} (h : S ⊆ S') (x : chartRing K S) :
    (chartIncl K h x : L) = x

theorem

chartIncl_injective

L101 ↗

AlgebraicCurve.CurveModel.chartIncl_injective

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

theorem chartIncl_injective {S S' : Set L} (h : S ⊆ S') :
    Function.Injective (chartIncl K h)

instance

algebraAdjoin

L105 ↗

AlgebraicCurve.CurveModel.algebraAdjoin

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

instance algebraAdjoin (S : Set L) : Algebra (Algebra.adjoin K S) (chartRing K S)

instance

isScalarTower_adjoin

L108 ↗

AlgebraicCurve.CurveModel.isScalarTower_adjoin

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

instance isScalarTower_adjoin (S : Set L) :
    IsScalarTower (Algebra.adjoin K S) (chartRing K S) L

instance

isScalarTower_base_adjoin

L112 ↗

AlgebraicCurve.CurveModel.isScalarTower_base_adjoin

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · statement

instance isScalarTower_base_adjoin (S : Set L) :
    IsScalarTower K (Algebra.adjoin K S) (chartRing K S)

instance

isIntegralClosure

L116 ↗

AlgebraicCurve.CurveModel.isIntegralClosure

Source context 6 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]

Lean source · full declaration

instance isIntegralClosure (S : Set L) : IsIntegralClosure (chartRing K S) (Algebra.adjoin K S) L
  where
  algebraMap_injective := Subtype.val_injective
  isIntegral_iff {x} := ⟨fun hx => ⟨⟨x, hx⟩, rfl⟩, by rintro ⟨y, rfl⟩; exact y.2⟩

instance

charZero_adjoin_simple

L125 ↗

AlgebraicCurve.CurveModel.charZero_adjoin_simple

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

instance charZero_adjoin_simple : CharZero K⟮s⟯

instance

isSeparable_adjoin_simple

L128 ↗

AlgebraicCurve.CurveModel.isSeparable_adjoin_simple

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

instance isSeparable_adjoin_simple : Algebra.IsSeparable K⟮s⟯ L

instance

isDedekindDomain_chartRing

L132 ↗

AlgebraicCurve.CurveModel.isDedekindDomain_chartRing

Source context 9 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional K⟮s⟯ L] [CharZero K]
open scoped IntermediateField.algebraAdjoinAdjoin in

Lean source · statement

instance isDedekindDomain_chartRing : IsDedekindDomain (chartRing K ({s} : Set L))

instance

finite_chartRing

L136 ↗

AlgebraicCurve.CurveModel.finite_chartRing

Source context 9 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional K⟮s⟯ L] [CharZero K]
open scoped IntermediateField.algebraAdjoinAdjoin in

Lean source · statement

instance finite_chartRing :
    Module.Finite (Algebra.adjoin K ({s} : Set L)) (chartRing K ({s} : Set L))

instance

isFractionRing_chartRing

L141 ↗

AlgebraicCurve.CurveModel.isFractionRing_chartRing

Source context 9 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional K⟮s⟯ L] [CharZero K]
open scoped IntermediateField.algebraAdjoinAdjoin in

Lean source · statement

instance isFractionRing_chartRing : IsFractionRing (chartRing K ({s} : Set L)) L

instance

finiteType_chartRing

L144 ↗

AlgebraicCurve.CurveModel.finiteType_chartRing

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

instance finiteType_chartRing : Algebra.FiniteType K (chartRing K ({s} : Set L))

instance

isNoetherianRing_chartRing

L149 ↗

AlgebraicCurve.CurveModel.isNoetherianRing_chartRing

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section OneGenerator
variable (s : L) [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

instance isNoetherianRing_chartRing : IsNoetherianRing (chartRing K ({s} : Set L))

theorem

adjoin_le_valuationSubring

L158 ↗

AlgebraicCurve.CurveModel.adjoin_le_valuationSubring

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}

Lean source · statement

theorem adjoin_le_valuationSubring (O : ValuationSubring L)
    (hK : ∀ a : K, algebraMap K L a ∈ O) {S : Set L} (hS : S ⊆ O) {y : L}
    (hy : y ∈ Algebra.adjoin K S) : y ∈ O

def

toSubalgebraOfBase

L168 ↗

ValuationSubring.toSubalgebraOfBase

Documentation

A valuation subring containing the base field, viewed as a subalgebra.

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}

Lean source · statement

def _root_.ValuationSubring.toSubalgebraOfBase (O : ValuationSubring L)
    (hK : ∀ a : K, algebraMap K L a ∈ O) : Subalgebra K L

theorem

mem_toSubalgebraOfBase_iff

L172 ↗

ValuationSubring.mem_toSubalgebraOfBase_iff

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}

Lean source · statement

theorem _root_.ValuationSubring.mem_toSubalgebraOfBase_iff (O : ValuationSubring L)
    (hK : ∀ a : K, algebraMap K L a ∈ O) {x : L} : x ∈ O.toSubalgebraOfBase hK ↔ x ∈ O

theorem

integers_toSubalgebraOfBase

L176 ↗

ValuationSubring.integers_toSubalgebraOfBase

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}

Lean source · full declaration

theorem _root_.ValuationSubring.integers_toSubalgebraOfBase (O : ValuationSubring L)
    (hK : ∀ a : K, algebraMap K L a ∈ O) : O.valuation.Integers (O.toSubalgebraOfBase hK) where
  hom_inj := Subtype.val_injective
  map_le_one a := (O.valuation_le_one_iff _).mpr a.2
  exists_of_le_one r hr := ⟨⟨r, O.mem_of_valuation_le_one r hr⟩, rfl⟩

theorem

chartRing_le_valuationSubring

L182 ↗

AlgebraicCurve.CurveModel.chartRing_le_valuationSubring

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}

Lean source · statement

theorem chartRing_le_valuationSubring (O : ValuationSubring L)
    (hK : ∀ a : K, algebraMap K L a ∈ O) {S : Set L} (hS : S ⊆ O) {x : L}
    (hx : x ∈ chartRing K S) : x ∈ O

def

centre

L198 ↗

AlgebraicCurve.CurveModel.centre

Documentation

The ideal of chart elements with valuation strictly less than one.

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)

Lean source · full declaration

def centre (O : ValuationSubring L) (hK : ∀ a : K, algebraMap K L a ∈ O) (hs : s ∈ O) :
    Ideal (chartRing K ({s} : Set L)) where
  carrier := {a | O.valuation a < 1}
  add_mem' {a b} ha hb := lt_of_le_of_lt (O.valuation.map_add a b) (max_lt ha hb)
  zero_mem' := by simp
  smul_mem' c a ha := by
    have hc : O.valuation c ≤ 1 := (O.valuation_le_one_iff _).mpr
      (chartRing_le_valuationSubring O hK (Set.singleton_subset_iff.mpr hs) c.2)
    change O.valuation ((c : L) * a) < 1
    rw [map_mul]
    exact mul_lt_of_le_one_of_lt hc ha

theorem

mem_centre_iff

L210 ↗

AlgebraicCurve.CurveModel.mem_centre_iff

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)

Lean source · statement

theorem mem_centre_iff (O : ValuationSubring L) (hK : ∀ a : K, algebraMap K L a ∈ O)
    (hs : s ∈ O) (a : chartRing K ({s} : Set L)) :
    a ∈ centre K s O hK hs ↔ O.valuation a < 1

theorem

valuation_coe_le_one

L214 ↗

AlgebraicCurve.CurveModel.valuation_coe_le_one

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)

Lean source · statement

theorem valuation_coe_le_one (O : ValuationSubring L) (hK : ∀ a : K, algebraMap K L a ∈ O)
    (hs : s ∈ O) (a : chartRing K ({s} : Set L)) : O.valuation a ≤ 1

theorem

valuation_eq_one_of_not_mem_centre

L219 ↗

AlgebraicCurve.CurveModel.valuation_eq_one_of_not_mem_centre

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)

Lean source · statement

theorem valuation_eq_one_of_not_mem_centre (O : ValuationSubring L)
    (hK : ∀ a : K, algebraMap K L a ∈ O) (hs : s ∈ O) {a : chartRing K ({s} : Set L)}
    (ha : a ∉ centre K s O hK hs) : O.valuation a = 1

instance

centre_isPrime

L224 ↗

AlgebraicCurve.CurveModel.centre_isPrime

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)

Lean source · full declaration

instance centre_isPrime (O : ValuationSubring L) (hK : ∀ a : K, algebraMap K L a ∈ O)
    (hs : s ∈ O) : (centre K s O hK hs).IsPrime where
  ne_top' := by
    rw [Ne, Ideal.eq_top_iff_one, mem_centre_iff]
    simp
  mem_or_mem' {a b} hab := by
    by_contra h
    push Not at h
    rw [mem_centre_iff, Subalgebra.coe_mul, map_mul,
      valuation_eq_one_of_not_mem_centre K s O hK hs h.1,
      valuation_eq_one_of_not_mem_centre K s O hK hs h.2, mul_one] at hab
    exact lt_irrefl _ hab

def

chartPlaces

L238 ↗

AlgebraicCurve.CurveModel.chartPlaces

Documentation

The places whose valuation subring contains the chosen coordinate.

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)

Lean source · statement

def chartPlaces (s : L) : Set (Place K L)

theorem

mem_chartPlaces_iff

L240 ↗

AlgebraicCurve.CurveModel.mem_chartPlaces_iff

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)

Lean source · statement

theorem mem_chartPlaces_iff {s : L} {v : Place K L} :
    v ∈ chartPlaces K s ↔ s ∈ v.toValuationSubring

theorem

mem_chartPlaces_or_mem_chartPlaces_inv

L243 ↗

AlgebraicCurve.CurveModel.mem_chartPlaces_or_mem_chartPlaces_inv

Source context 10 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)

Lean source · statement

theorem mem_chartPlaces_or_mem_chartPlaces_inv (v : Place K L) (t : L) :
    v ∈ chartPlaces K t ∨ v ∈ chartPlaces K t⁻¹

theorem

centre_ne_bot

L250 ↗

AlgebraicCurve.CurveModel.centre_ne_bot

Source context 12 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)
variable [FiniteDimensional K⟮s⟯ L] [CharZero K]
omit [CharZero K] in

Lean source · statement

theorem centre_ne_bot (O : ValuationSubring L) (hK : ∀ a : K, algebraMap K L a ∈ O)
    (hs : s ∈ O) (hO : O ≠ ⊤) : centre K s O hK hs ≠ ⊥

def

primeOfValuationSubring

L264 ↗

AlgebraicCurve.CurveModel.primeOfValuationSubring

Documentation

The height-one prime given by the centre of a nontrivial valuation subring.

Source context 11 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)
variable [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

def primeOfValuationSubring (O : ValuationSubring L) (hK : ∀ a : K, algebraMap K L a ∈ O)
    (hs : s ∈ O) (hO : O ≠ ⊤) : HeightOneSpectrum (chartRing K ({s} : Set L))

theorem

valuationSubringAtPrime_le

L268 ↗

AlgebraicCurve.CurveModel.valuationSubringAtPrime_le

Source context 11 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)
variable [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

theorem valuationSubringAtPrime_le (O : ValuationSubring L)
    (hK : ∀ a : K, algebraMap K L a ∈ O) (hs : s ∈ O) (hO : O ≠ ⊤) :
    HeightOneSpectrum.valuationSubringAtPrime L (primeOfValuationSubring K s O hK hs hO) ≤ O

theorem

valuationSubringAtPrime_primeOfValuationSubring

L280 ↗

AlgebraicCurve.CurveModel.valuationSubringAtPrime_primeOfValuationSubring

Source context 11 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)
variable [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

theorem valuationSubringAtPrime_primeOfValuationSubring (O : ValuationSubring L)
    (hK : ∀ a : K, algebraMap K L a ∈ O) (hs : s ∈ O) (hO : O ≠ ⊤) :
    HeightOneSpectrum.valuationSubringAtPrime L (primeOfValuationSubring K s O hK hs hO) = O

theorem

exists_ofHeightOneSpectrum_eq

L285 ↗

AlgebraicCurve.CurveModel.exists_ofHeightOneSpectrum_eq

Source context 11 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)
variable [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

theorem exists_ofHeightOneSpectrum_eq (v : Place K L) (hs : s ∈ v.toValuationSubring) :
    ∃ 𝔭 : HeightOneSpectrum (chartRing K ({s} : Set L)),
      Place.ofHeightOneSpectrum (K := K) 𝔭 = v

theorem

mem_ofHeightOneSpectrum

L294 ↗

AlgebraicCurve.CurveModel.mem_ofHeightOneSpectrum

Source context 11 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)
variable [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

theorem mem_ofHeightOneSpectrum (𝔭 : HeightOneSpectrum (chartRing K ({s} : Set L))) :
    s ∈ (Place.ofHeightOneSpectrum (K := K) (F := L) 𝔭).toValuationSubring

theorem

ofHeightOneSpectrum_injective

L300 ↗

AlgebraicCurve.CurveModel.ofHeightOneSpectrum_injective

Source context 11 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)
variable [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

theorem ofHeightOneSpectrum_injective :
    Function.Injective
      (Place.ofHeightOneSpectrum (K := K) (F := L) (R := chartRing K ({s} : Set L)))

def

primeEquivChartPlaces

L313 ↗

AlgebraicCurve.CurveModel.primeEquivChartPlaces

Documentation

The correspondence between height-one chart primes and coordinate-containing places.

Source context 11 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)
variable [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

def primeEquivChartPlaces : HeightOneSpectrum (chartRing K ({s} : Set L)) ≃ chartPlaces K s

theorem

coe_primeEquivChartPlaces

L321 ↗

AlgebraicCurve.CurveModel.coe_primeEquivChartPlaces

Source context 11 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section Valuation
variable {K}
variable (K)
variable (s : L)
variable [FiniteDimensional K⟮s⟯ L] [CharZero K]

Lean source · statement

theorem coe_primeEquivChartPlaces (𝔭 : HeightOneSpectrum (chartRing K ({s} : Set L))) :
    (primeEquivChartPlaces K s 𝔭 : Place K L) = Place.ofHeightOneSpectrum (K := K) 𝔭

theorem

exists_pow_mul_mem_adjoin

L331 ↗

AlgebraicCurve.CurveModel.exists_pow_mul_mem_adjoin

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section InvertGenerator
variable {K}

Lean source · statement

theorem exists_pow_mul_mem_adjoin {S : Set L} {s : L} (hs : s ∈ S) (hs0 : s ≠ 0) {x : L}
    (hx : x ∈ Algebra.adjoin K (insert s⁻¹ S)) : ∃ n : ℕ, s ^ n * x ∈ Algebra.adjoin K S

theorem

exists_pow_mul_mem_chartRing

L355 ↗

AlgebraicCurve.CurveModel.exists_pow_mul_mem_chartRing

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain IntermediateField
universe u
namespace AlgebraicCurve
namespace CurveModel
variable (K : Type u) [Field K] {L : Type u} [Field L] [Algebra K L]
section InvertGenerator
variable {K}

Lean source · statement

theorem exists_pow_mul_mem_chartRing {S : Set L} {s : L} (hs : s ∈ S) (hs0 : s ≠ 0) {x : L}
    (hx : x ∈ chartRing K (insert s⁻¹ S)) : ∃ n : ℕ, s ^ n * x ∈ chartRing K S

Module documentation

Chart Algebra

Declarations