Module

Exists_mem_riemannRochSpace_ord_sub_eq_one_hasValue_of_ringEquiv_ratFunc.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_ord_sub_eq_one_hasValue_of_ringEquiv_ratFunc

68 declarations indexed from sourceView source ↗

Module documentation

Exists mem riemann Roch Space ord sub eq one has Value of ring Equiv rat Func

Imports11

Nyll.AlgebraicCurves.Cohomology.Adelic.Repartitions
Mathlib.FieldTheory.RatFunc.IntermediateField
Mathlib.LinearAlgebra.Lagrange
Mathlib.RingTheory.Polynomial.DegreeLT
Nyll.AlgebraicCurves.Places.Rational.Basic
Nyll.AlgebraicCurves.Places.Rational.Infinity
Nyll.AlgebraicCurves.Places.Value
Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_placeOfPoint_algebraMap
Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_ord_placeInfty
Nyll.AlgebraicCurves.Places.Rational.Classification
Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_deg_placeInfty

Imported by1

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.All

theorem

hasValue_of_ord_sub_algebraMap_pos

L54 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.Place.hasValue_of_ord_sub_algebraMap_pos

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem hasValue_of_ord_sub_algebraMap_pos (v : Place K F) {g : F} {γ : K}
    (h : 0 < v.ord (g - algebraMap K F γ)) : v.HasValue g γ

theorem

congrResidueAlgEquiv_residue

L85 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.Place.congrResidueAlgEquiv_residue

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section CongrTransport
variable {F' : Type*} [Field F'] [Algebra K F']
variable (e : F ≃+* F') (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem congrResidueAlgEquiv_residue (v : Place K F) (x : v.toValuationSubring) :
    congrResidueAlgEquiv e he v (IsLocalRing.residue _ x)
      = IsLocalRing.residue _ (comapSymmRingEquiv e v.toValuationSubring x)

theorem

hasValue_congrRingEquiv_iff

L92 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.Place.hasValue_congrRingEquiv_iff

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section CongrTransport
variable {F' : Type*} [Field F'] [Algebra K F']
variable (e : F ≃+* F') (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem hasValue_congrRingEquiv_iff (v : Place K F) (g : F) (c : K) :
    (congrRingEquiv e he v).HasValue (e g) c ↔ v.HasValue g c

theorem

mem_riemannRochSpace_mapDomain_congrEquiv_iff

L112 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.Place.mem_riemannRochSpace_mapDomain_congrEquiv_iff

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section CongrTransport
variable {F' : Type*} [Field F'] [Algebra K F']
variable (e : F ≃+* F') (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem mem_riemannRochSpace_mapDomain_congrEquiv_iff (D : Divisor K F) (f : F) :
    e f ∈ riemannRochSpace (Finsupp.mapDomain (congrEquiv e he) D) ↔ f ∈ riemannRochSpace D

theorem

algebraMap_comm_trans

L128 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.Place.algebraMap_comm_trans

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section CongrTransport
variable {F' : Type*} [Field F'] [Algebra K F']
variable (e : F ≃+* F') (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem algebraMap_comm_trans {F'' : Type*} [Field F''] [Algebra K F''] (e' : F' ≃+* F'')
    (he' : ∀ a : K, e' (algebraMap K F' a) = algebraMap K F'' a) (a : K) :
    (e.trans e') (algebraMap K F a) = algebraMap K F'' a

theorem

congrEquiv_trans_apply

L133 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.Place.congrEquiv_trans_apply

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section CongrTransport
variable {F' : Type*} [Field F'] [Algebra K F']
variable (e : F ≃+* F') (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he

Lean source · statement

theorem congrEquiv_trans_apply {F'' : Type*} [Field F''] [Algebra K F''] (e' : F' ≃+* F'')
    (he' : ∀ a : K, e' (algebraMap K F' a) = algebraMap K F'' a) (v : Place K F) :
    congrEquiv (e.trans e') (algebraMap_comm_trans e he e' he') v
      = congrEquiv e' he' (congrEquiv e he v)

def

divisorPoints

L162 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.divisorPoints

Documentation

The finite points whose places lie in the support of the rational-function divisor.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points

Lean source · statement

def divisorPoints (E : Divisor k (RatFunc k)) : Finset k

theorem

mem_divisorPoints

L168 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.mem_divisorPoints

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}

Lean source · statement

theorem mem_divisorPoints {E : Divisor k (RatFunc k)} {a : k} :
    a ∈ divisorPoints k E ↔ E (placeOfPoint k a) ≠ 0

def

divisorPolynomial

L175 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.divisorPolynomial

Documentation

The product of linear factors at finite points, with the nonnegative multiplicities of the divisor.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

def divisorPolynomial (E : Divisor k (RatFunc k)) : k[X]

theorem

divisorPolynomial_ne_zero

L178 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.divisorPolynomial_ne_zero

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem divisorPolynomial_ne_zero (E : Divisor k (RatFunc k)) : divisorPolynomial k E ≠ 0

theorem

algebraMap_divisorPolynomial_ne_zero

L182 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.algebraMap_divisorPolynomial_ne_zero

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem algebraMap_divisorPolynomial_ne_zero (E : Divisor k (RatFunc k)) :
    algebraMap k[X] (RatFunc k) (divisorPolynomial k E) ≠ 0

theorem

rootMultiplicity_divisorPolynomial

L186 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.rootMultiplicity_divisorPolynomial

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem rootMultiplicity_divisorPolynomial (E : Divisor k (RatFunc k)) (b : k) :
    rootMultiplicity b (divisorPolynomial k E) = (E (placeOfPoint k b)).toNat

theorem

natDegree_divisorPolynomial

L216 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.natDegree_divisorPolynomial

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem natDegree_divisorPolynomial (E : Divisor k (RatFunc k)) :
    (divisorPolynomial k E).natDegree = ∑ a ∈ divisorPoints k E, (E (placeOfPoint k a)).toNat

theorem

eval_divisorPolynomial_ne_zero

L221 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.eval_divisorPolynomial_ne_zero

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem eval_divisorPolynomial_ne_zero {E : Divisor k (RatFunc k)} {b : k} (hb : E (placeOfPoint k
  b) = 0) :
    (divisorPolynomial k E).eval b ≠ 0

theorem

ord_placeOfPoint_divisorPolynomial

L232 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_divisorPolynomial

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem ord_placeOfPoint_divisorPolynomial (E : Divisor k (RatFunc k)) (b : k) :
    (placeOfPoint k b).ord (algebraMap k[X] (RatFunc k) (divisorPolynomial k E))
      = (E (placeOfPoint k b)).toNat

theorem

ord_placeInfty_divisorPolynomial

L238 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.ord_placeInfty_divisorPolynomial

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem ord_placeInfty_divisorPolynomial [DecidableEq (RatFunc k)] (E : Divisor k (RatFunc k)) :
    (placeInfty k).ord (algebraMap k[X] (RatFunc k) (divisorPolynomial k E))
      = -((divisorPolynomial k E).natDegree : ℤ)

theorem

ord_placeOfPoint_div_divisorPolynomial

L243 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_div_divisorPolynomial

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem ord_placeOfPoint_div_divisorPolynomial (E : Divisor k (RatFunc k)) {P : k[X]} (hP : P ≠ 0)
  (b : k) :
    (placeOfPoint k b).ord (algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k)
      (divisorPolynomial k E))
      = (rootMultiplicity b P : ℤ) - (E (placeOfPoint k b)).toNat

theorem

ord_placeInfty_div_divisorPolynomial

L255 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.ord_placeInfty_div_divisorPolynomial

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem ord_placeInfty_div_divisorPolynomial [DecidableEq (RatFunc k)] (E : Divisor k (RatFunc k))
  {P : k[X]} (hP : P ≠ 0) :
    (placeInfty k).ord (algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k)
      (divisorPolynomial k E))
      = ((divisorPolynomial k E).natDegree : ℤ) - P.natDegree

theorem

support_subset_insert

L269 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.support_subset_insert

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in
open scoped Classical in

Lean source · statement

theorem support_subset_insert [IsAlgClosed k] [DecidableEq (RatFunc k)] (E : Divisor k (RatFunc
  k)) :
    E.support ⊆ insert (placeInfty k) ((divisorPoints k E).image (placeOfPoint k))

theorem

degree_eq_sum_divisorPoints

L278 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.degree_eq_sum_divisorPoints

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem degree_eq_sum_divisorPoints [IsAlgClosed k] [DecidableEq (RatFunc k)] (E : Divisor k
  (RatFunc k)) :
    E.degree = (∑ a ∈ divisorPoints k E, E (placeOfPoint k a)) + E (placeInfty k)

theorem

degree_eq_natDegree_add

L295 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.degree_eq_natDegree_add

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem degree_eq_natDegree_add [IsAlgClosed k] [DecidableEq (RatFunc k)] {E : Divisor k (RatFunc
  k)}
    (hE : 0 ≤ E) :
    E.degree = (divisorPolynomial k E).natDegree + E (placeInfty k)

theorem

degree_nonneg

L303 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.degree_nonneg

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
variable (k : Type*) [Field k]
section Points
variable {k}
variable (k) in

Lean source · statement

theorem degree_nonneg [IsAlgClosed k] {E : Divisor k (RatFunc k)}
    (hE : 0 ≤ E) : 0 ≤ E.degree

theorem

ord_placeOfPoint_div

L330 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_div

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]

Lean source · statement

theorem ord_placeOfPoint_div (b : k) {P Q : k[X]} (hP : P ≠ 0) (hQ : Q ≠ 0) :
    (placeOfPoint k b).ord (algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k) Q)
      = (rootMultiplicity b P : ℤ) - rootMultiplicity b Q

theorem

exists_eq_algebraMap_of_forall_ord_nonneg

L342 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.exists_eq_algebraMap_of_forall_ord_nonneg

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]

Lean source · statement

theorem exists_eq_algebraMap_of_forall_ord_nonneg [IsAlgClosed k] {f : RatFunc k}
    (hf : ∀ a : k, 0 ≤ (placeOfPoint k a).ord f) :
    ∃ P : k[X], f = algebraMap k[X] (RatFunc k) P

theorem

div_divisorPolynomial_mem_riemannRochSpace

L376 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.div_divisorPolynomial_mem_riemannRochSpace

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [DecidableEq (RatFunc k)] in

Lean source · statement

theorem div_divisorPolynomial_mem_riemannRochSpace {E : Divisor k (RatFunc k)} (hE : 0 ≤ E) {P :
  k[X]}
    (hP : (P.natDegree : ℤ) ≤ E.degree) :
    algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k) (divisorPolynomial k E)
      ∈ riemannRochSpace E

theorem

exists_eq_div_divisorPolynomial_of_mem

L396 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.exists_eq_div_divisorPolynomial_of_mem

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [DecidableEq (RatFunc k)] in

Lean source · statement

theorem exists_eq_div_divisorPolynomial_of_mem {E : Divisor k (RatFunc k)} (hE : 0 ≤ E) {f :
  RatFunc k}
    (hf : f ∈ riemannRochSpace E) :
    ∃ P : k[X], (P.natDegree : ℤ) ≤ E.degree ∧
      f = algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k) (divisorPolynomial k E)

theorem

mem_riemannRochSpace_iff_exists_polynomial

L427 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.mem_riemannRochSpace_iff_exists_polynomial

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [DecidableEq (RatFunc k)] in

Lean source · statement

theorem mem_riemannRochSpace_iff_exists_polynomial {E : Divisor k (RatFunc k)} (hE : 0 ≤ E) {f :
  RatFunc k} :
    f ∈ riemannRochSpace E ↔ ∃ P : k[X], (P.natDegree : ℤ) ≤ E.degree ∧
      f = algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k) (divisorPolynomial k E)

def

divDivisorPolynomial

L438 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.divDivisorPolynomial

Documentation

The linear map sending a polynomial to its image in the rational function field divided by the divisor polynomial.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [IsAlgClosed k] [DecidableEq (RatFunc k)] in

Lean source · statement

def divDivisorPolynomial (E : Divisor k (RatFunc k)) : k[X] →ₗ[k] RatFunc k

theorem

divDivisorPolynomial_apply

L444 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.divDivisorPolynomial_apply

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [IsAlgClosed k] [DecidableEq (RatFunc k)] in

Lean source · statement

theorem divDivisorPolynomial_apply (E : Divisor k (RatFunc k)) (P : k[X]) :
    divDivisorPolynomial E P
      = algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k) (divisorPolynomial k E)

theorem

divDivisorPolynomial_injective

L450 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.divDivisorPolynomial_injective

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [IsAlgClosed k] [DecidableEq (RatFunc k)] in

Lean source · statement

theorem divDivisorPolynomial_injective (E : Divisor k (RatFunc k)) :
    Function.Injective (divDivisorPolynomial E)

theorem

mem_degreeLT_succ_iff

L458 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.mem_degreeLT_succ_iff

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [IsAlgClosed k] [DecidableEq (RatFunc k)] in

Lean source · statement

theorem mem_degreeLT_succ_iff {P : k[X]} {d : ℕ} : P ∈ degreeLT k (d + 1) ↔ P.natDegree ≤ d

def

riemannRochSpaceEquiv

L466 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.riemannRochSpaceEquiv

Documentation

Dividing by the divisor polynomial identifies bounded-degree polynomials with the Riemann–Roch space of an effective divisor.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]

Lean source · statement

def riemannRochSpaceEquiv {E : Divisor k (RatFunc k)} (hE : 0 ≤ E) :
    degreeLT k (E.degree.toNat + 1) ≃ₗ[k] riemannRochSpace E

theorem

riemannRochSpaceEquiv_apply

L487 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.riemannRochSpaceEquiv_apply

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [DecidableEq (RatFunc k)] in

Lean source · statement

theorem riemannRochSpaceEquiv_apply {E : Divisor k (RatFunc k)} (hE : 0 ≤ E)
    (P : degreeLT k (E.degree.toNat + 1)) :
    (riemannRochSpaceEquiv hE P : RatFunc k)
      = algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k) (divisorPolynomial k E)

theorem

finrank_degreeLT

L496 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.finrank_degreeLT

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [IsAlgClosed k] [DecidableEq (RatFunc k)] in

Lean source · statement

theorem finrank_degreeLT (n : ℕ) : Module.finrank k (degreeLT k n) = n

theorem

finrank_riemannRochSpace

L500 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.finrank_riemannRochSpace

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [DecidableEq (RatFunc k)] in

Lean source · statement

theorem finrank_riemannRochSpace {E : Divisor k (RatFunc k)} (hE : 0 ≤ E) :
    Module.finrank k (riemannRochSpace E) = E.degree.toNat + 1

theorem

finiteDimensional_riemannRochSpace

L506 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.finiteDimensional_riemannRochSpace

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section RiemannRoch
variable {k : Type*} [Field k]
variable [IsAlgClosed k] [DecidableEq (RatFunc k)]
omit [DecidableEq (RatFunc k)] in

Lean source · statement

theorem finiteDimensional_riemannRochSpace {E : Divisor k (RatFunc k)} (hE : 0 ≤ E) :
    FiniteDimensional k (riemannRochSpace E)

theorem

hasValue_placeOfPoint_algebraMap

L529 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.hasValue_placeOfPoint_algebraMap

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Values
variable {k : Type*} [Field k]

Lean source · statement

theorem hasValue_placeOfPoint_algebraMap (b : k) (P : k[X]) :
    (placeOfPoint k b).HasValue (algebraMap k[X] (RatFunc k) P) (P.eval b)

theorem

hasValue_placeOfPoint_div

L555 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.hasValue_placeOfPoint_div

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Values
variable {k : Type*} [Field k]

Lean source · statement

theorem hasValue_placeOfPoint_div (b : k) (P : k[X]) {Q : k[X]} (hQ : Q.eval b ≠ 0) :
    (placeOfPoint k b).HasValue (algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k) Q)
      (P.eval b / Q.eval b)

theorem

hasValue_placeOfPoint_div_divisorPolynomial

L561 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.hasValue_placeOfPoint_div_divisorPolynomial

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Values
variable {k : Type*} [Field k]

Lean source · statement

theorem hasValue_placeOfPoint_div_divisorPolynomial {E : Divisor k (RatFunc k)} {b : k}
    (hb : E (placeOfPoint k b) = 0) (P : k[X]) :
    (placeOfPoint k b).HasValue
      (algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k) (divisorPolynomial k E))
      (P.eval b / (divisorPolynomial k E).eval b)

theorem

algebraMap_residueField_placeOfPoint_surjective

L568 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.algebraMap_residueField_placeOfPoint_surjective

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Values
variable {k : Type*} [Field k]

Lean source · statement

theorem algebraMap_residueField_placeOfPoint_surjective (b : k) :
    Function.Surjective (algebraMap k (placeOfPoint k b).ResidueField)

def

nodePoly

L597 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.nodePoly

Documentation

The monic polynomial with a simple zero at each point in the finite node set.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Pencil
variable {k : Type*} [Field k]

Lean source · statement

def nodePoly (Z : Finset k) : k[X]

theorem

nodePoly_monic

L599 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.nodePoly_monic

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Pencil
variable {k : Type*} [Field k]

Lean source · statement

theorem nodePoly_monic (Z : Finset k) : (nodePoly Z).Monic

theorem

natDegree_nodePoly

L602 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.natDegree_nodePoly

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Pencil
variable {k : Type*} [Field k]

Lean source · statement

theorem natDegree_nodePoly (Z : Finset k) : (nodePoly Z).natDegree = Z.card

theorem

eval_nodePoly

L606 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.eval_nodePoly

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Pencil
variable {k : Type*} [Field k]

Lean source · statement

theorem eval_nodePoly (Z : Finset k) (a : k) : (nodePoly Z).eval a = ∏ z ∈ Z, (a - z)

theorem

eval_nodePoly_ne_zero

L609 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.eval_nodePoly_ne_zero

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Pencil
variable {k : Type*} [Field k]

Lean source · statement

theorem eval_nodePoly_ne_zero {Z : Finset k} {a : k} (ha : a ∉ Z) : (nodePoly Z).eval a ≠ 0

theorem

eval_nodePoly_eq_zero

L615 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.eval_nodePoly_eq_zero

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Pencil
variable {k : Type*} [Field k]

Lean source · statement

theorem eval_nodePoly_eq_zero {Z : Finset k} {a : k} (ha : a ∈ Z) : (nodePoly Z).eval a = 0

theorem

exists_pencil

L619 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.exists_pencil

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Pencil
variable {k : Type*} [Field k]

Lean source · statement

theorem exists_pencil [Infinite k] (h : k[X]) (b₀ β : k) (Zv Za : Finset k)
    (w : k → k) (bad : Finset k) (hb₀v : b₀ ∉ Zv) (hb₀a : b₀ ∉ Za) (hva : Disjoint Zv Za)
    (hha : ∀ a ∈ Za, h.eval a ≠ 0) :
    ∃ S : k[X], S.natDegree ≤ Zv.card ∧ S.eval b₀ ≠ 0 ∧
      (∀ z ∈ Zv, (z - b₀) * S.eval z = (w z - β) * h.eval z) ∧
      (∀ a ∈ Za, (C β * h + (X - C b₀) * S).eval a / h.eval a ∉ bad)

theorem

sum_single_one_apply

L690 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.sum_single_one_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section AllFinite
variable {k : Type*} [Field k]
open scoped Classical in

Lean source · full declaration

theorem sum_single_one_apply {F : Type*} [Field F] [Algebra k F] (U : Finset (Place k F))
    (v : Place k F) :
    (∑ u ∈ U, Finsupp.single u (1 : ℤ)) v = if v ∈ U then 1 else 0 := by
  classical
  simp only [Finset.sum_apply', Finsupp.single_apply]
  split_ifs with hv
  · rw [Finset.sum_eq_single_of_mem v hv (fun u _ huv => ite_eq_right huv), ite_eq_left rfl]
  · exact Finset.sum_eq_zero fun u hu => ite_eq_right (fun h : u = v => hv (h ▸ hu))

def

finsetPoints

L700 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.finsetPoints

Documentation

The finite points whose places belong to the chosen finite set of places.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section AllFinite
variable {k : Type*} [Field k]

Lean source · statement

def finsetPoints (S : Finset (Place k (RatFunc k))) : Finset k

theorem

mem_finsetPoints

L703 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.mem_finsetPoints

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section AllFinite
variable {k : Type*} [Field k]

Lean source · statement

theorem mem_finsetPoints {S : Finset (Place k (RatFunc k))} {a : k} :
    a ∈ finsetPoints S ↔ placeOfPoint k a ∈ S

theorem

image_finsetPoints

L708 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.image_finsetPoints

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section AllFinite
variable {k : Type*} [Field k]
open scoped Classical in

Lean source · statement

theorem image_finsetPoints [IsAlgClosed k] [DecidableEq (RatFunc k)]
    {S : Finset (Place k (RatFunc k))} (hS : ∀ v ∈ S, v ≠ placeInfty k) :
    (finsetPoints S).image (placeOfPoint k) = S

theorem

card_finsetPoints

L722 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.card_finsetPoints

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section AllFinite
variable {k : Type*} [Field k]

Lean source · statement

theorem card_finsetPoints [IsAlgClosed k] [DecidableEq (RatFunc k)]
    {S : Finset (Place k (RatFunc k))} (hS : ∀ v ∈ S, v ≠ placeInfty k) :
    (finsetPoints S).card = S.card

theorem

div_sub_algebraMap

L729 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.div_sub_algebraMap

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section AllFinite
variable {k : Type*} [Field k]

Lean source · statement

theorem div_sub_algebraMap (P h : k[X]) (hh : algebraMap k[X] (RatFunc k) h ≠ 0) (γ : k) :
    algebraMap k[X] (RatFunc k) P / algebraMap k[X] (RatFunc k) h - algebraMap k (RatFunc k) γ
      = algebraMap k[X] (RatFunc k) (P - C γ * h) / algebraMap k[X] (RatFunc k) h

theorem

exists_interp_of_forall_ne_placeInfty

L735 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.exists_interp_of_forall_ne_placeInfty

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section AllFinite
variable {k : Type*} [Field k]

Lean source · statement

theorem exists_interp_of_forall_ne_placeInfty [IsAlgClosed k] [DecidableEq (RatFunc k)]
    (U Zv Za : Finset (Place k (RatFunc k))) (t₀ : Place k (RatFunc k)) (β : k)
    (val : Place k (RatFunc k) → k) (bad : Finset k)
    (hUZv : Disjoint U Zv) (hUZa : Disjoint U Za) (hZ : Disjoint Zv Za)
    (ht₀U : t₀ ∉ U) (ht₀v : t₀ ∉ Zv) (ht₀a : t₀ ∉ Za)
    (hcard : Zv.card + 1 ≤ U.card)
    (hU : ∀ v ∈ U, v ≠ placeInfty k) (hZv : ∀ v ∈ Zv, v ≠ placeInfty k)
    (hZa : ∀ v ∈ Za, v ≠ placeInfty k) (ht₀ : t₀ ≠ placeInfty k) :
    ∃ g : RatFunc k,
      g ∈ riemannRochSpace (∑ u ∈ U, Finsupp.single u (1 : ℤ)) ∧
      t₀.ord (g - algebraMap k (RatFunc k) β) = 1 ∧
      (∀ z ∈ Zv, z.HasValue g (val z)) ∧
      (∀ z ∈ Za, ∃ γ : k, γ ∉ bad ∧ z.HasValue g γ)

theorem

X_sub_C_eq_algebraMap

L851 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.X_sub_C_eq_algebraMap

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

theorem X_sub_C_eq_algebraMap (c : k) :
    (RatFunc.X - RatFunc.C c : RatFunc k) = algebraMap k[X] (RatFunc k) (X - C c)

theorem

ratFunc_X_sub_C_ne_zero

L855 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.ratFunc_X_sub_C_ne_zero

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

theorem ratFunc_X_sub_C_ne_zero (c : k) : (RatFunc.X - RatFunc.C c : RatFunc k) ≠ 0

def

moebiusFun

L860 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.moebiusFun

Documentation

The rational function (X - c)⁻¹ defining the chosen Möbius coordinate.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

def moebiusFun (c : k) : RatFunc k

theorem

moebiusFun_ne_C

L862 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.moebiusFun_ne_C

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

theorem moebiusFun_ne_C (c : k) : ¬ ∃ c' : k, moebiusFun k c = RatFunc.C c'

theorem

transcendental_moebiusFun

L876 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.transcendental_moebiusFun

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

theorem transcendental_moebiusFun (c : k) : Transcendental k (moebiusFun k c)

theorem

adjoin_moebiusFun

L879 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.adjoin_moebiusFun

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

theorem adjoin_moebiusFun (c : k) : k⟮moebiusFun k c⟯ = ⊤

def

moebiusAlgHom

L890 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.moebiusAlgHom

Documentation

The algebra homomorphism sending the rational-function variable to (X - c)⁻¹.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

def moebiusAlgHom (c : k) : RatFunc k →ₐ[k] RatFunc k

theorem

moebiusAlgHom_X

L894 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.moebiusAlgHom_X

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

theorem moebiusAlgHom_X (c : k) : moebiusAlgHom k c RatFunc.X = moebiusFun k c

theorem

moebiusAlgHom_bijective

L898 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.moebiusAlgHom_bijective

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

theorem moebiusAlgHom_bijective (c : k) : Function.Bijective (moebiusAlgHom k c)

def

moebius

L910 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.moebius

Documentation

The Möbius algebra automorphism sending the rational-function variable to (X - c)⁻¹.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

def moebius (c : k) : RatFunc k ≃ₐ[k] RatFunc k

theorem

moebius_X

L913 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.moebius_X

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · statement

theorem moebius_X (c : k) : moebius k c RatFunc.X = moebiusFun k c

theorem

congrEquiv_moebius_placeInfty

L916 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.RationalFunctionField.congrEquiv_moebius_placeInfty

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial IntermediateField
section Moebius
variable (k : Type*) [Field k]

Lean source · full declaration

theorem congrEquiv_moebius_placeInfty [IsAlgClosed k] [DecidableEq (RatFunc k)] (c : k) :
    Place.congrEquiv (moebius k c).toRingEquiv (fun a => (moebius k c).commutes a) (placeInfty k)
      = placeOfPoint k c := by
  classical
  set w := Place.congrEquiv (moebius k c).toRingEquiv (fun a => (moebius k c).commutes a)
    (placeInfty k) with hw
  have h1 : w.ord ((moebius k c) RatFunc.X) = (placeInfty k).ord RatFunc.X := by
    rw [hw, Place.congrEquiv_apply]
    exact Place.ord_congrRingEquiv _ _ _ _
  rw [moebius_X, moebiusFun, Place.ord_inv, ord_placeInfty RatFunc.X_ne_zero,
    RatFunc.intDegree_X] at h1
  have hord : w.ord (RatFunc.X - RatFunc.C c) = 1 := by omega
  clear h1
  rcases eq_placeOfPoint_or_eq_placeInfty k w with ⟨a, ha⟩ | ha
  · rw [ha] at hord ⊢
    rw [X_sub_C_eq_algebraMap, ord_placeOfPoint_algebraMap a (X_sub_C_ne_zero c),
      rootMultiplicity_X_sub_C] at hord
    split_ifs at hord with hac
    · rw [hac]
    · exact absurd hord (by norm_num)
  · rw [ha, X_sub_C_eq_algebraMap, ord_placeInfty ((map_ne_zero_iff _
      (IsFractionRing.injective k[X] (RatFunc k))).mpr (X_sub_C_ne_zero c)),
      RatFunc.intDegree_polynomial, natDegree_X_sub_C] at hord
    norm_num at hord

theorem

exists_mem_riemannRochSpace_ord_sub_eq_one_hasValue_of_ringEquiv_ratFunc'

L945 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve.exists_mem_riemannRochSpace_ord_sub_eq_one_hasValue_of_ringEquiv_ratFunc'

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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
noncomputable section
open IsLocalRing Polynomial
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem exists_mem_riemannRochSpace_ord_sub_eq_one_hasValue_of_ringEquiv_ratFunc'
    {k F : Type*} [Field k] [IsAlgClosed k] [Field F] [Algebra k F]
    (e : RatFunc k ≃+* F) (he : ∀ c : k, e (algebraMap k (RatFunc k) c) = algebraMap k F c)
    (U Zv Za : Finset (Place k F)) (t₀ : Place k F) (β : k)
    (val : Place k F → k) (bad : Finset k)
    (hUZv : Disjoint U Zv) (hUZa : Disjoint U Za) (hZ : Disjoint Zv Za)
    (ht₀U : t₀ ∉ U) (ht₀v : t₀ ∉ Zv) (ht₀a : t₀ ∉ Za)
    (hcard : Zv.card + 1 ≤ U.card) :
    ∃ g : F,
      g ∈ riemannRochSpace (∑ u ∈ U, Finsupp.single u (1 : ℤ)) ∧
      t₀.ord (g - algebraMap k F β) = 1 ∧
      (∀ z ∈ Zv, z.HasValue g (val z)) ∧
      (∀ z ∈ Za, ∃ γ : k, γ ∉ bad ∧ z.HasValue g γ)

theorem

exists_mem_riemannRochSpace_ord_sub_eq_one_hasValue_of_ringEquiv_ratFunc

L1030 ↗

AlgebraicCurve.exists_mem_riemannRochSpace_ord_sub_eq_one_hasValue_of_ringEquiv_ratFunc

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer
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 _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs.RRSpaceRationalUniformizer.AlgebraicCurve in

Lean source · statement

theorem
  _root_.AlgebraicCurve.exists_mem_riemannRochSpace_ord_sub_eq_one_hasValue_of_ringEquiv_ratFunc
    {k F : Type*} [Field k] [IsAlgClosed k] [Field F] [Algebra k F]
    (e : RatFunc k ≃+* F) (he : ∀ c : k, e (algebraMap k (RatFunc k) c) = algebraMap k F c)
    (U Zv Za : Finset (Place k F)) (t₀ : Place k F) (β : k)
    (val : Place k F → k) (bad : Finset k)
    (hUZv : Disjoint U Zv) (hUZa : Disjoint U Za) (hZ : Disjoint Zv Za)
    (ht₀U : t₀ ∉ U) (ht₀v : t₀ ∉ Zv) (ht₀a : t₀ ∉ Za)
    (hcard : Zv.card + 1 ≤ U.card) :
    ∃ g : F,
      g ∈ riemannRochSpace (∑ u ∈ U, Finsupp.single u (1 : ℤ)) ∧
      t₀.ord (g - algebraMap k F β) = 1 ∧
      (∀ z ∈ Zv, z.HasValue g (val z)) ∧
      (∀ z ∈ Za, ∃ γ : k, γ ∉ bad ∧ z.HasValue g γ)

Module documentation

Exists mem riemann Roch Space ord sub eq one has Value of ring Equiv rat Func

Declarations