Module

Basic.lean

Nyll.AlgebraicCurves.Models.Basic

9 declarations indexed from sourceView source ↗

Module documentation

Geometric models of function fields of curves. A model identifies closed points with places and stalks with their valuation subrings.

Imports5

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.Proper
Mathlib.AlgebraicGeometry.FunctionField
Mathlib.AlgebraicGeometry.AlgClosed.Basic
Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by203

def

baseToFunctionField

L33 ↗

AlgebraicCurve.baseToFunctionField

Documentation

The base-field homomorphism into the function field induced by the structure morphism.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
universe u v
namespace AlgebraicCurve

Lean source · statement

def baseToFunctionField {K : Type u} [Field K] {C : Scheme.{u}} [IsIntegral C]
    (c : C ⟶ Spec (CommRingCat.of K)) : K →+* C.functionField

structure

CurveModel

L39 ↗

AlgebraicCurve.CurveModel

Documentation

A proper smooth integral curve model of a field extension, with its place correspondence.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
universe u v
namespace AlgebraicCurve

Lean source · full declaration

structure CurveModel (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] where
  /-- The underlying scheme of the curve model. -/
  C : Scheme.{u}
  /-- The structure morphism to the spectrum of the base field. -/
  toBase : C ⟶ Spec (CommRingCat.of K)
  /-- The underlying scheme is integral. -/
  [isIntegral : IsIntegral C]
  /-- The structure morphism is proper. -/
  [isProper : IsProper toBase]
  /-- The structure morphism is smooth of relative dimension one. -/
  [smooth : SmoothOfRelativeDimension 1 toBase]
  /-- The specified ring equivalence with the model function field. -/
  ffEquiv : L ≃+* C.functionField
  /-- The function-field equivalence respects the specified base-field homomorphisms. -/
  ffEquiv_algebraMap : ∀ a : K, ffEquiv (algebraMap K L a) = baseToFunctionField toBase a
  /-- The place associated with each closed point of the model. -/
  placeOfPoint : closedPoints C → Place K L
  /-- Closed points correspond bijectively to places. -/
  placeOfPoint_bijective : Function.Bijective placeOfPoint
  /-- The stalk image transported to the given field is the corresponding valuation subring. -/
  range_stalk_eq : ∀ x : closedPoints C,
    ((ffEquiv.symm : C.functionField ≃+* L).toRingHom.comp
        (algebraMap (C.presheaf.stalk x.1) C.functionField)).range =
      (placeOfPoint x).toValuationSubring.toSubring
  /-- Every finite subset of the model lies in an affine open. -/
  finset_subset_affineOpen : ∀ F : Finset C, ∃ U : C.Opens, IsAffineOpen U ∧ ∀ x ∈ F, x ∈ U

abbrev

functionFieldAlgebra

L73 ↗

AlgebraicCurve.CurveModel.functionFieldAlgebra

Documentation

The base-field algebra structure on the model function field.

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
universe u v
namespace AlgebraicCurve
attribute [instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

abbrev functionFieldAlgebra (M : CurveModel K L) : Algebra K M.C.functionField

def

ffAlgEquiv

L77 ↗

AlgebraicCurve.CurveModel.ffAlgEquiv

Documentation

The specified function-field equivalence regarded as a base-field algebra equivalence.

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
universe u v
namespace AlgebraicCurve
attribute [instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · full declaration

def ffAlgEquiv (M : CurveModel K L) :
    letI := M.functionFieldAlgebra
    L ≃ₐ[K] M.C.functionField :=
  letI := M.functionFieldAlgebra
  AlgEquiv.ofRingEquiv (f := M.ffEquiv) M.ffEquiv_algebraMap

theorem

ffAlgEquiv_apply

L83 ↗

AlgebraicCurve.CurveModel.ffAlgEquiv_apply

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
universe u v
namespace AlgebraicCurve
attribute [instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem ffAlgEquiv_apply (M : CurveModel K L) (f : L) : M.ffAlgEquiv f = M.ffEquiv f

def

placeEquiv

L86 ↗

AlgebraicCurve.CurveModel.placeEquiv

Documentation

The equivalence between closed points of the model and places of the given field.

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
universe u v
namespace AlgebraicCurve
attribute [instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

def placeEquiv (M : CurveModel K L) : closedPoints M.C ≃ Place K L

theorem

placeEquiv_apply

L89 ↗

AlgebraicCurve.CurveModel.placeEquiv_apply

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
universe u v
namespace AlgebraicCurve
attribute [instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem placeEquiv_apply (M : CurveModel K L) (x : closedPoints M.C) :
    M.placeEquiv x = M.placeOfPoint x

def

pointEquivPlace

L93 ↗

AlgebraicCurve.CurveModel.pointEquivPlace

Documentation

Identify base-field points with places over an algebraically closed base field.

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
universe u v
namespace AlgebraicCurve
attribute [instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

def pointEquivPlace [IsAlgClosed K] (M : CurveModel K L) :
    {p : Spec (CommRingCat.of K) ⟶ M.C // p ≫ M.toBase = 𝟙 _} ≃ Place K L

theorem

pointEquivPlace_apply

L97 ↗

AlgebraicCurve.CurveModel.pointEquivPlace_apply

Source context 7 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
universe u v
namespace AlgebraicCurve
attribute [instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smooth
namespace CurveModel
variable {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]

Lean source · statement

theorem pointEquivPlace_apply [IsAlgClosed K] (M : CurveModel K L)
    (p : {p : Spec (CommRingCat.of K) ⟶ M.C // p ≫ M.toBase = 𝟙 _}) :
    M.pointEquivPlace p = M.placeOfPoint (pointEquivClosedPoint M.toBase p)

Module documentation

Declarations