Module

CurveOver.lean

Nyll.AlgebraicCurves.FunctionFields.CurveOver

10 declarations indexed from sourceView source ↗

Module documentation

Function fields of curves over a base field. The curve condition records principal divisors, finite residues and rank-one differentials.

Imports3

Nyll.AlgebraicCurves.Divisors.ClassGroup
Mathlib.RingTheory.Kaehler.Basic
Mathlib.FieldTheory.IsAlgClosed.Basic

Imported by373

class

IsCurveOver

L31 ↗

AlgebraicCurve.IsCurveOver

Documentation

The field extension has principal divisors, finite residues and rank-one differentials.

Source context 4 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]

Lean source · full declaration

class IsCurveOver : Prop extends HasPrincipalDivisors K F where
  /-- Every place has a residue field finite over the base field. -/
  finiteResidue : ∀ v : Place K F, Module.Finite K v.ResidueField
  /-- The module of relative differentials is free of rank one over the function field. -/
  kaehler_free_rank_one : Module.Free F Ω[F⁄K] ∧ Module.finrank F Ω[F⁄K] = 1

theorem

hasPrincipalDivisors

L41 ↗

AlgebraicCurve.IsCurveOver.hasPrincipalDivisors

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace IsCurveOver
variable {K F}

Lean source · statement

theorem hasPrincipalDivisors [h : IsCurveOver K F] : HasPrincipalDivisors K F

theorem

finite_residueField

L44 ↗

AlgebraicCurve.IsCurveOver.finite_residueField

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace IsCurveOver
variable {K F}

Lean source · statement

theorem finite_residueField [IsCurveOver K F] (v : Place K F) :
    Module.Finite K v.ResidueField

instance

instFiniteResidue

L48 ↗

AlgebraicCurve.IsCurveOver.instFiniteResidue

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace IsCurveOver
variable {K F}

Lean source · statement

instance instFiniteResidue [IsCurveOver K F] (v : Place K F) : v.FiniteResidue

instance

instFreeKaehler

L51 ↗

AlgebraicCurve.IsCurveOver.instFreeKaehler

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace IsCurveOver
variable {K F}

Lean source · statement

instance instFreeKaehler [h : IsCurveOver K F] : Module.Free F Ω[F⁄K]

theorem

finrank_kaehler

L54 ↗

AlgebraicCurve.IsCurveOver.finrank_kaehler

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace IsCurveOver
variable {K F}

Lean source · statement

theorem finrank_kaehler [h : IsCurveOver K F] : Module.finrank F Ω[F⁄K] = 1

instance

instNontrivialKaehler

L57 ↗

AlgebraicCurve.IsCurveOver.instNontrivialKaehler

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace IsCurveOver
variable {K F}

Lean source · statement

instance instNontrivialKaehler [IsCurveOver K F] : Nontrivial Ω[F⁄K]

theorem

deg_eq_one_of_isAlgClosed_of_finite

L66 ↗

AlgebraicCurve.Place.deg_eq_one_of_isAlgClosed_of_finite

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Place
variable {K F}

Lean source · statement

theorem deg_eq_one_of_isAlgClosed_of_finite [IsAlgClosed K] (v : Place K F)
    [Module.Finite K v.ResidueField] : v.deg = 1

theorem

deg_eq_one_of_isAlgClosed

L81 ↗

AlgebraicCurve.IsCurveOver.deg_eq_one_of_isAlgClosed

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace IsCurveOver
variable {K F}

Lean source · statement

theorem deg_eq_one_of_isAlgClosed [IsAlgClosed K] [IsCurveOver K F] (v : Place K F) :
    v.deg = 1

theorem

forall_deg_eq_one_of_isAlgClosed

L86 ↗

AlgebraicCurve.IsCurveOver.forall_deg_eq_one_of_isAlgClosed

Source context 6 commands

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

noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace IsCurveOver
variable {K F}

Lean source · statement

theorem forall_deg_eq_one_of_isAlgClosed [IsAlgClosed K] [IsCurveOver K F] :
    ∀ w : Place K F, w.deg = 1

Module documentation

Declarations