NYLL
Module

RationalFunctionField_ell_sub_ell_eq_genus_zero.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ell_sub_ell_eq_genus_zero
16 declarations indexed from sourceView source ↗

Module documentation

Rational Function Field ell sub ell eq genus zero

Imports7
Imported by1

Declarations

theorem

ord_nonneg_iff_mem

L44 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.Place.ord_nonneg_iff_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
section principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem Place.ord_nonneg_iff_mem (v : Place K F) {f : F} (hf : f ≠ 0) :
    0 ≤ v.ord f ↔ f ∈ v.toValuationSubring
theorem

lSpace_add_map_mulLeft

L51 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.lSpace_add_map_mulLeft
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
section principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem lSpace_add_map_mulLeft {D P : Divisor K F} {f : F} (hf : f ≠ 0)
    (hP : ∀ v : Place K F, P v = v.ord f) :
    (LSpace (D + P)).map (LinearMap.mulLeft K f) = LSpace D
theorem

ell_add_of_forall_eq_ord

L82 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.ell_add_of_forall_eq_ord
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
section principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ell_add_of_forall_eq_ord {D P : Divisor K F} {f : F} (hf : f ≠ 0)
    (hP : ∀ v : Place K F, P v = v.ord f) : ell (D + P) = ell D
def

polyIncl

L96 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.polyIncl
Documentation

The base-field linear inclusion of polynomials into the rational function field.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
Lean source · statement
def polyIncl : K[X] →ₗ[K] RatFunc K
theorem

polyIncl_apply

L99 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.polyIncl_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
Lean source · statement
theorem polyIncl_apply (q : K[X]) : polyIncl K q = algebraMap K[X] (RatFunc K) q
theorem

polyIncl_injective

L102 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.polyIncl_injective
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
Lean source · statement
theorem polyIncl_injective : Function.Injective (polyIncl K)
theorem

placeInfty_ne_ofHeightOneSpectrum'

L107 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.placeInfty_ne_ofHeightOneSpectrum'
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem placeInfty_ne_ofHeightOneSpectrum' (w : HeightOneSpectrum K[X]) :
    placeInfty K ≠ Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w
theorem

smul_single_placeInfty_apply_ofHeightOneSpectrum

L116 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.smul_single_placeInfty_apply_ofHeightOneSpectrum
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem smul_single_placeInfty_apply_ofHeightOneSpectrum (n : ℤ) (w : HeightOneSpectrum K[X]) :
    (n • Finsupp.single (placeInfty K) (1 : ℤ)) (Place.ofHeightOneSpectrum w) = 0
theorem

smul_single_placeInfty_apply_placeInfty

L123 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.smul_single_placeInfty_apply_placeInfty
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem smul_single_placeInfty_apply_placeInfty (n : ℤ) :
    (n • Finsupp.single (placeInfty K) (1 : ℤ)) (placeInfty K) = n
theorem

algebraMap_mem_lSpace_smul_single_placeInfty_iff

L127 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.algebraMap_mem_lSpace_smul_single_placeInfty_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem algebraMap_mem_lSpace_smul_single_placeInfty_iff (n : ℤ) {q : K[X]} (hq : q ≠ 0) :
    algebraMap K[X] (RatFunc K) q ∈ LSpace (n • Finsupp.single (placeInfty K) (1 : ℤ)) ↔
      (q.natDegree : ℤ) ≤ n
theorem

exists_eq_algebraMap_of_forall_ord_nonneg

L144 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.exists_eq_algebraMap_of_forall_ord_nonneg
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem exists_eq_algebraMap_of_forall_ord_nonneg {g : RatFunc K} (hg : g ≠ 0)
    (h : ∀ w : HeightOneSpectrum K[X], 0 ≤ (Place.ofHeightOneSpectrum (K := K) w).ord g) :
    ∃ q : K[X], algebraMap K[X] (RatFunc K) q = g
theorem

lSpace_smul_single_placeInfty

L153 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.lSpace_smul_single_placeInfty
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem lSpace_smul_single_placeInfty (n : ℤ) :
    LSpace (n • Finsupp.single (placeInfty K) (1 : ℤ)) =
      (Polynomial.degreeLT K (n + 1).toNat).map (polyIncl K)
theorem

ell_smul_single_placeInfty

L181 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.ell_smul_single_placeInfty
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem ell_smul_single_placeInfty (n : ℤ) :
    ell (n • Finsupp.single (placeInfty K) (1 : ℤ)) = (n + 1).toNat
theorem

ell_eq_max

L189 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.ell_eq_max
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem ell_eq_max (D : Divisor K (RatFunc K)) :
    (ell D : ℤ) = max (Divisor.degree D + 1) 0
theorem

ell_sub_ell_eq_genus_zero

L200 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero.RRSol.RationalFunctionField.ell_sub_ell_eq_genus_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
namespace RRSol
namespace RationalFunctionField
variable (K : Type u) [Field K]
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem ell_sub_ell_eq_genus_zero (D : Divisor K (RatFunc K)) :
    (ell D : ℤ) - ell ((-2 : ℤ) • Finsupp.single (placeInfty K) (1 : ℤ) - D) =
      Divisor.degree D + 1 - ((0 : ℕ) : ℤ)
theorem

ell_sub_ell_eq_genus_zero

L213 ↗
AlgebraicCurve.RationalFunctionField.ell_sub_ell_eq_genus_zero
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_ell_sub_ell_eq_genus_zero
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
open Polynomial IsDedekindDomain WithZero AlgebraicCurve AlgebraicCurve.RationalFunctionField
universe u v
Lean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.ell_sub_ell_eq_genus_zero
    (K : Type u) [Field K] [DecidableEq (RatFunc K)] (D : Divisor K (RatFunc K)) :
    (ell D : ℤ) - ell ((-2 : ℤ) • Finsupp.single (placeInfty K) (1 : ℤ) - D) =
      Divisor.degree D + 1 - ((0 : ℕ) : ℤ)

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