NYLL
Module

InstIsCurveOverRatFunc.lean

Nyll.AlgebraicCurves.FunctionFields.InstIsCurveOverRatFunc
14 declarations indexed from sourceView source ↗

Module documentation

InstIsCurveOverRatFunc

Rational function fields have finite residue fields at their places and a free module of Kähler differentials of rank one.

Imports7
Imported by6

Declarations

instance

instHasPrincipalDivisorsRatFuncLaneB

L41 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.instHasPrincipalDivisorsRatFuncLaneB
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
instance instHasPrincipalDivisorsRatFuncLaneB (K : Type*) [Field K] :
  HasPrincipalDivisors K (RatFunc K)
theorem

finiteResidue_of_deg_pos

L65 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.Place.finiteResidue_of_deg_pos
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section DegPos
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem finiteResidue_of_deg_pos (h : 0 < v.deg) : v.FiniteResidue
instance

instFiniteResidueOfHeightOneSpectrum

L74 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.instFiniteResidueOfHeightOneSpectrum
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
Lean source · statement
instance instFiniteResidueOfHeightOneSpectrum (w : HeightOneSpectrum K[X]) :
    (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).FiniteResidue
instance

instFiniteResiduePlaceInfty

L81 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.instFiniteResiduePlaceInfty
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
Lean source · statement
instance instFiniteResiduePlaceInfty [DecidableEq (RatFunc K)] :
    (placeInfty K).FiniteResidue
instance

instFiniteResidue

L86 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.instFiniteResidue
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K} in
Lean source · statement
instance instFiniteResidue (v : Place K (RatFunc K)) : v.FiniteResidue
def

KaehlerRankOne

L121 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.KaehlerRankOne
Documentation

The module of Kähler differentials is free of rank one over the extension field.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
section
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
Lean source · statement
def KaehlerRankOne : Prop
theorem

of_finiteResidue_of_kaehlerRankOne

L129 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.IsCurveOver.of_finiteResidue_of_kaehlerRankOne
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
section
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
open scoped _root_.AlgebraicCurve.IsCurveOver in
Lean source · full declaration
theorem IsCurveOver.of_finiteResidue_of_kaehlerRankOne
    [HasPrincipalDivisors K F] [∀ v : Place K F, v.FiniteResidue]
    (hΩ : KaehlerRankOne K F) : IsCurveOver K F where
  finiteResidue v := Place.FiniteResidue.finite (v := v)
  kaehler_free_rank_one := hΩ
theorem

isCurveOver_of_kaehlerRankOne

L141 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.isCurveOver_of_kaehlerRankOne
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
section
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable {K F}
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
Lean source · statement
theorem isCurveOver_of_kaehlerRankOne (hΩ : KaehlerRankOne K (RatFunc K)) :
    IsCurveOver K (RatFunc K)
def

kaehlerPolynomialBasis

L169 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.kaehlerPolynomialBasis
Documentation

The single differential basis for a polynomial ring, transported from its standard module.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
section
section
noncomputable section
open _root_.IntermediateField
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.TensorProduct
open _root_.Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K : Type*) [Field K]
Lean source · statement
def kaehlerPolynomialBasis : Basis Unit K[X] Ω[K[X]⁄K]
instance

instFormallyEtalePolynomialRatFunc

L172 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.instFormallyEtalePolynomialRatFunc
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
section
section
noncomputable section
open _root_.IntermediateField
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.TensorProduct
open _root_.Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K : Type*) [Field K]
Lean source · statement
instance instFormallyEtalePolynomialRatFunc : Algebra.FormallyEtale K[X] (RatFunc K)
def

kaehlerRatFuncBasis

L176 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.kaehlerRatFuncBasis
Documentation

The polynomial differential basis transported to the rational function field.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
section
section
noncomputable section
open _root_.IntermediateField
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.TensorProduct
open _root_.Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K : Type*) [Field K]
Lean source · statement
def kaehlerRatFuncBasis : Basis Unit (RatFunc K) Ω[(RatFunc K)⁄K]
theorem

kaehlerRankOne_ratFunc

L180 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.kaehlerRankOne_ratFunc
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
section
section
noncomputable section
open _root_.IntermediateField
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.TensorProduct
open _root_.Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K : Type*) [Field K]
Lean source · statement
theorem kaehlerRankOne_ratFunc : KaehlerRankOne K (RatFunc K)
instance

instIsCurveOverRatFunc

L184 ↗
AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc.AlgebraicCurve.instIsCurveOverRatFunc
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
section
section
noncomputable section
open _root_.IntermediateField
open _root_.AlgebraicCurve
open _root_.Polynomial
open _root_.TensorProduct
open _root_.Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K : Type*) [Field K]
Lean source · statement
instance instIsCurveOverRatFunc : IsCurveOver K (RatFunc K)
theorem

instIsCurveOverRatFunc

L202 ↗
AlgebraicCurve.instIsCurveOverRatFunc
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.InstIsCurveOverRatFunc
attribute [-instance] AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
section
section
section
Lean source · statement
theorem _root_.AlgebraicCurve.instIsCurveOverRatFunc (K : Type*) [Field K] :
  AlgebraicCurve.IsCurveOver K (RatFunc K)

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