Module

Finrank_riemannRochSpace_eq_degree_add_one_of_ringEquiv_ratFunc.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Finrank_riemannRochSpace_eq_degree_add_one_of_ringEquiv_ratFunc

70 declarations indexed from sourceView source ↗

Module documentation

Finrank riemann Roch Space eq degree add one of ring Equiv rat Func

Imports10

Imported by1

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.All

theorem

hasValue_zero

L54 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.Place.hasValue_zero

Source context 14 commands

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

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

Lean source · statement

theorem hasValue_zero (v : Place K F) : v.HasValue (0 : F) 0

theorem

add

L62 ↗

AlgebraicCurve.Place.HasValue.add

Source context 16 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.HasValue.add {g g' : F} {a a' : K} (h : v.HasValue g
  a) (h' : v.HasValue g' a') :
    v.HasValue (g + g') (a + a')

theorem

neg

L75 ↗

AlgebraicCurve.Place.HasValue.neg

Source context 17 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.HasValue.neg {g : F} {a : K} (h : v.HasValue g a) :
  v.HasValue (-g) (-a)

theorem

sub

L85 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.Place.HasValue.sub

Source context 17 commands

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

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

Lean source · statement

theorem HasValue.sub {g g' : F} {a a' : K} (h : v.HasValue g a) (h' : v.HasValue g' a') :
    v.HasValue (g - g') (a - a')

theorem

smul

L91 ↗

AlgebraicCurve.Place.HasValue.smul

Source context 18 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.HasValue.smul {g : F} {a : K} (c : K) (h : v.HasValue
  g a) : v.HasValue (c • g) (c * a)

theorem

mem_toValuationSubring_of_mem_riemannRochSpace

L99 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.Place.mem_toValuationSubring_of_mem_riemannRochSpace

Source context 17 commands

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

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

Lean source · statement

theorem mem_toValuationSubring_of_mem_riemannRochSpace {D : Divisor K F} {f : F}
    (hf : f ∈ riemannRochSpace D) (hv : D v ≤ 0) : f ∈ v.toValuationSubring

theorem

ord_pos_of_eq_zero

L107 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.Place.HasValue.ord_pos_of_eq_zero

Source context 18 commands

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

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

Lean source · statement

theorem HasValue.ord_pos_of_eq_zero {g : F} (h : v.HasValue g 0) (hg : g ≠ 0) : 0 < v.ord g

def

nodeCompatiblePairs

L121 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.nodeCompatiblePairs

Documentation

Pairs of Riemann–Roch sections with a common residue value at each pair of places.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section NodePairs
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

def nodeCompatiblePairs (E₁ E₂ : Divisor K F) {ι : Type*} (v₁ v₂ : ι → Place K F) :
    Submodule K (F × F) where
  carrier := {p | p.1 ∈ riemannRochSpace E₁ ∧ p.2 ∈ riemannRochSpace E₂ ∧
    ∀ i, ∃ c : K, (v₁ i).HasValue p.1 c ∧ (v₂ i).HasValue p.2 c}
  zero_mem' := ⟨Submodule.zero_mem _, Submodule.zero_mem _,
    fun i => ⟨0, Place.hasValue_zero _, Place.hasValue_zero _⟩⟩
  add_mem' := by
    rintro p q ⟨hp1, hp2, hp⟩ ⟨hq1, hq2, hq⟩
    refine ⟨Submodule.add_mem _ hp1 hq1, Submodule.add_mem _ hp2 hq2, fun i => ?_⟩
    obtain ⟨c, hc1, hc2⟩ := hp i
    obtain ⟨d, hd1, hd2⟩ := hq i
    exact ⟨c + d, hc1.add hd1, hc2.add hd2⟩
  smul_mem' := by
    rintro a p ⟨hp1, hp2, hp⟩
    refine ⟨Submodule.smul_mem _ a hp1, Submodule.smul_mem _ a hp2, fun i => ?_⟩
    obtain ⟨c, hc1, hc2⟩ := hp i
    exact ⟨a * c, hc1.smul a, hc2.smul a⟩

theorem

mem_nodeCompatiblePairs_iff

L139 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.mem_nodeCompatiblePairs_iff

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section NodePairs
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_nodeCompatiblePairs_iff {E₁ E₂ : Divisor K F} {ι : Type*} {v₁ v₂ : ι → Place K F}
    {p : F × F} :
    p ∈ nodeCompatiblePairs E₁ E₂ v₁ v₂ ↔ p.1 ∈ riemannRochSpace E₁ ∧ p.2 ∈ riemannRochSpace E₂ ∧
      ∀ i, ∃ c : K, (v₁ i).HasValue p.1 c ∧ (v₂ i).HasValue p.2 c

theorem

nodeCompatiblePairs_le_comp

L145 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.nodeCompatiblePairs_le_comp

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
section NodePairs
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem nodeCompatiblePairs_le_comp {E₁ E₂ : Divisor K F} {ι ι' : Type*} (v₁ v₂ : ι → Place K F)
    (u : ι' → ι) :
    nodeCompatiblePairs E₁ E₂ v₁ v₂ ≤ nodeCompatiblePairs E₁ E₂ (v₁ ∘ u) (v₂ ∘ u)

def

divisorPoints

L169 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L175 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L182 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L185 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L189 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L193 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L223 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L228 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L239 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L245 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L250 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L262 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L276 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L285 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L302 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L310 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L337 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L349 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L383 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L403 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L434 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L445 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L451 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L457 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L465 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L473 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L494 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L503 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L507 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L513 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L536 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L562 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L568 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

L575 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.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.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
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

wEvalAt

L605 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.wEvalAt

Documentation

The linear map evaluating a degree-bounded polynomial at the chosen points and multiplying by the chosen weights.

Source context 17 commands

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

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

Lean source · full declaration

def wEvalAt (a w : ι → k) (n : ℕ) : degreeLT k n →ₗ[k] (ι → k) where
  toFun P := fun i => w i * (P : k[X]).eval (a i)
  map_add' P Q := by ext i; simp [mul_add]
  map_smul' c P := by ext i; simp; ring

theorem

wEvalAt_apply

L610 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.wEvalAt_apply

Source context 17 commands

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

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

Lean source · statement

theorem wEvalAt_apply (a w : ι → k) (n : ℕ) (P : degreeLT k n) (i : ι) :
    wEvalAt a w n P i = w i * (P : k[X]).eval (a i)

theorem

wEvalAt_surjective

L616 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.wEvalAt_surjective

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Interp
variable {k : Type*} [Field k] {ι : Type*}
variable [Fintype ι] [DecidableEq ι]
omit [DecidableEq ι] in

Lean source · statement

theorem wEvalAt_surjective {a w : ι → k} (ha : Function.Injective a) (hw : ∀ i, w i ≠ 0) {n : ℕ}
    (hn : Fintype.card ι ≤ n) : Function.Surjective (wEvalAt a w n)

theorem

finrank_ker_coprod_neg_add

L635 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.finrank_ker_coprod_neg_add

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open Polynomial
open scoped Polynomial
section Interp
variable {k : Type*} [Field k] {ι : Type*}
variable [Fintype ι] [DecidableEq ι]
variable {V₁ V₂ W : Type*} [AddCommGroup V₁] [Module k V₁] [AddCommGroup V₂] [Module k V₂]
  [AddCommGroup W] [Module k W]
omit [Fintype ι] [DecidableEq ι] in

Lean source · statement

theorem finrank_ker_coprod_neg_add [FiniteDimensional k V₁] [FiniteDimensional k V₂]
  [FiniteDimensional k W]
    (e₁ : V₁ →ₗ[k] W) (e₂ : V₂ →ₗ[k] W) (h : Function.Surjective e₁ ∨ Function.Surjective e₂) :
    Module.finrank k (LinearMap.ker (e₁.coprod (-e₂))) + Module.finrank k W
      = Module.finrank k V₁ + Module.finrank k V₂

theorem

nodeCompatiblePairs_eq_map

L659 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.nodeCompatiblePairs_eq_map

Source context 19 commands

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

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

Lean source · full declaration

theorem nodeCompatiblePairs_eq_map {E₁ E₂ : Divisor k (RatFunc k)} (hE₁ : 0 ≤ E₁) (hE₂ : 0 ≤ E₂)
    (a b : ι → k) (haE : ∀ i, E₁ (placeOfPoint k (a i)) = 0) (hbE : ∀ i, E₂ (placeOfPoint k (b i))
      = 0) :
    nodeCompatiblePairs E₁ E₂ (fun i => placeOfPoint k (a i)) (fun i => placeOfPoint k (b i))
      = Submodule.map
          ((divDivisorPolynomial E₁ ∘ₗ (degreeLT k (E₁.degree.toNat + 1)).subtype).prodMap
            (divDivisorPolynomial E₂ ∘ₗ (degreeLT k (E₂.degree.toNat + 1)).subtype))
          (LinearMap.ker
            ((wEvalAt a (fun i => ((divisorPolynomial k E₁).eval (a i))⁻¹) (E₁.degree.toNat +
              1)).coprod
              (-(wEvalAt b (fun i => ((divisorPolynomial k E₂).eval (b i))⁻¹) (E₂.degree.toNat +
                1))))) := by
  classical
  have hd₁ := degree_nonneg hE₁
  have hd₂ := degree_nonneg hE₂
  ext ⟨g₁, g₂⟩
  simp only [mem_nodeCompatiblePairs_iff, Submodule.mem_map, LinearMap.mem_ker,
    LinearMap.coprod_apply,
    LinearMap.neg_apply, LinearMap.prodMap_apply, LinearMap.coe_comp, Function.comp_apply,
    Submodule.coe_subtype, divDivisorPolynomial_apply, Prod.mk.injEq, Prod.exists]
  constructor
  · rintro ⟨hg₁, hg₂, hnode⟩
    obtain ⟨P₁, hP₁, rfl⟩ := exists_eq_div_divisorPolynomial_of_mem hE₁ hg₁
    obtain ⟨P₂, hP₂, rfl⟩ := exists_eq_div_divisorPolynomial_of_mem hE₂ hg₂
    refine ⟨⟨P₁, mem_degreeLT_succ_iff.mpr
      (by omega)⟩, ⟨P₂, mem_degreeLT_succ_iff.mpr (by omega)⟩, ?_, rfl, rfl⟩
    ext i
    obtain ⟨c, hc₁, hc₂⟩ := hnode i
    have h₁ := hc₁.unique (hasValue_placeOfPoint_div_divisorPolynomial (haE i) P₁)
    have h₂ := hc₂.unique (hasValue_placeOfPoint_div_divisorPolynomial (hbE i) P₂)
    simp only [Pi.add_apply, Pi.neg_apply, wEvalAt_apply, Pi.zero_apply]
    rw [inv_mul_eq_div, inv_mul_eq_div, ← h₁, ← h₂, add_neg_cancel]
  · rintro ⟨P₁, P₂, hker, rfl, rfl⟩
    refine ⟨div_divisorPolynomial_mem_riemannRochSpace hE₁ ?_,
      div_divisorPolynomial_mem_riemannRochSpace hE₂ ?_, fun i => ?_⟩
    · have := mem_degreeLT_succ_iff.mp P₁.2; omega
    · have := mem_degreeLT_succ_iff.mp P₂.2; omega
    refine ⟨(P₁ : k[X]).eval (a i) / (divisorPolynomial k E₁).eval (a i),
      hasValue_placeOfPoint_div_divisorPolynomial (haE i) _, ?_⟩
    have hi := congrFun hker i
    simp only [Pi.add_apply, Pi.neg_apply, wEvalAt_apply, Pi.zero_apply, add_neg_eq_zero,
      inv_mul_eq_div] at hi
    rw [hi]
    exact hasValue_placeOfPoint_div_divisorPolynomial (hbE i) _

theorem

finiteDimensional_nodeCompatiblePairs

L705 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.finiteDimensional_nodeCompatiblePairs

Source context 19 commands

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

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

Lean source · full declaration

theorem finiteDimensional_nodeCompatiblePairs {E₁ E₂ : Divisor k (RatFunc k)} (hE₁ : 0 ≤ E₁) (hE₂
  : 0 ≤ E₂)
    (a b : ι → k) (haE : ∀ i, E₁ (placeOfPoint k (a i)) = 0) (hbE : ∀ i, E₂ (placeOfPoint k (b i))
      = 0) :
    FiniteDimensional k
      (nodeCompatiblePairs E₁ E₂ (fun i => placeOfPoint k (a i)) (fun i => placeOfPoint k (b i)))
        := by
  classical
  rw [nodeCompatiblePairs_eq_map hE₁ hE₂ a b haE hbE]
  infer_instance

theorem

finrank_nodeCompatiblePairs_add_card

L720 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.finrank_nodeCompatiblePairs_add_card

Source context 21 commands

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

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

Lean source · full declaration

theorem finrank_nodeCompatiblePairs_add_card {E₁ E₂ : Divisor k (RatFunc k)} (hE₁ : 0 ≤ E₁) (hE₂ :
  0 ≤ E₂)
    (a b : ι → k) (ha : Function.Injective a) (hb : Function.Injective b)
    (haE : ∀ i, E₁ (placeOfPoint k (a i)) = 0) (hbE : ∀ i, E₂ (placeOfPoint k (b i)) = 0)
    (hcard : Fintype.card ι ≤ max E₁.degree.toNat E₂.degree.toNat + 1) :
    Module.finrank k (nodeCompatiblePairs E₁ E₂ (fun i => placeOfPoint k (a i)) (fun i =>
      placeOfPoint k (b i)))
      + Fintype.card ι = (E₁.degree.toNat + 1) + (E₂.degree.toNat + 1) := by
  classical
  rw [nodeCompatiblePairs_eq_map hE₁ hE₂ a b haE hbE]
  have hinj : Function.Injective
      ((divDivisorPolynomial E₁ ∘ₗ (degreeLT k (E₁.degree.toNat + 1)).subtype).prodMap
        (divDivisorPolynomial E₂ ∘ₗ (degreeLT k (E₂.degree.toNat + 1)).subtype)) :=
    Function.Injective.prodMap ((divDivisorPolynomial_injective E₁).comp Subtype.val_injective)
      ((divDivisorPolynomial_injective E₂).comp Subtype.val_injective)
  rw [← (Submodule.equivMapOfInjective _ hinj _).finrank_eq]
  have key := finrank_ker_coprod_neg_add
    (wEvalAt a (fun i => ((divisorPolynomial k E₁).eval (a i))⁻¹) (E₁.degree.toNat + 1))
    (wEvalAt b (fun i => ((divisorPolynomial k E₂).eval (b i))⁻¹) (E₂.degree.toNat + 1)) ?_
  · rw [finrank_degreeLT, finrank_degreeLT, Module.finrank_fintype_fun_eq_card] at key
    exact key
  · rcases le_max_iff.mp (Nat.sub_le_iff_le_add.mpr hcard) with h | h
    · left
      exact wEvalAt_surjective ha (fun i => inv_ne_zero (eval_divisorPolynomial_ne_zero (haE i)))
        (by omega)
    · right
      exact wEvalAt_surjective hb (fun i => inv_ne_zero (eval_divisorPolynomial_ne_zero (hbE i)))
        (by omega)

theorem

finrank_nodeCompatiblePairs_add_min_le

L751 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.finrank_nodeCompatiblePairs_add_min_le

Source context 21 commands

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

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

Lean source · full declaration

theorem finrank_nodeCompatiblePairs_add_min_le {E₁ E₂ : Divisor k (RatFunc k)} (hE₁ : 0 ≤ E₁) (hE₂
  : 0 ≤ E₂)
    (a b : ι → k) (ha : Function.Injective a) (hb : Function.Injective b)
    (haE : ∀ i, E₁ (placeOfPoint k (a i)) = 0) (hbE : ∀ i, E₂ (placeOfPoint k (b i)) = 0) :
    Module.finrank k (nodeCompatiblePairs E₁ E₂ (fun i => placeOfPoint k (a i)) (fun i =>
      placeOfPoint k (b i)))
      + min (Fintype.card ι) (max E₁.degree.toNat E₂.degree.toNat + 1)
      ≤ (E₁.degree.toNat + 1) + (E₂.degree.toNat + 1) := by
  classical
  set m := min (Fintype.card ι) (max E₁.degree.toNat E₂.degree.toNat + 1) with hm
  let u : Fin m ↪ ι := (Fin.castLEEmb (min_le_left _ _)).trans (Fintype.equivFin ι).symm.toEmbedding
  have hle := nodeCompatiblePairs_le_comp (E₁ := E₁) (E₂ := E₂)
    (fun i => placeOfPoint k (a i)) (fun i => placeOfPoint k (b i)) u
  have heq := finrank_nodeCompatiblePairs_add_card hE₁ hE₂ (a ∘ u) (b ∘ u)
    (ha.comp u.injective) (hb.comp u.injective) (fun i => haE (u i)) (fun i => hbE (u i))
    (by rw [Fintype.card_fin]; exact min_le_right _ _)
  rw [Fintype.card_fin] at heq
  have : FiniteDimensional k (nodeCompatiblePairs E₁ E₂ ((fun i => placeOfPoint k (a i)) ∘ u)
      ((fun i => placeOfPoint k (b i)) ∘ u)) :=
    finiteDimensional_nodeCompatiblePairs hE₁ hE₂ (a ∘ u) (b ∘ u) (fun i => haE (u i)) (fun i =>
      hbE (u i))
  have hmono := Submodule.finrank_mono hle
  change Module.finrank k _ ≤ Module.finrank k
    (nodeCompatiblePairs E₁ E₂ (fun i => placeOfPoint k ((a ∘ u) i)) (fun i => placeOfPoint k ((b
      ∘ u) i))) at hmono
  omega

theorem

congrResidueAlgEquiv_residue

L796 ↗

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

Source context 16 commands

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

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

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

L803 ↗

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

Source context 16 commands

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

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

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

L823 ↗

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

Source context 16 commands

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

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

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

degree_mapDomain_congrEquiv

L839 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.Place.degree_mapDomain_congrEquiv

Source context 16 commands

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

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

Lean source · statement

theorem degree_mapDomain_congrEquiv (D : Divisor K F) :
    Divisor.degree (Finsupp.mapDomain (congrEquiv e he) D) = Divisor.degree D

theorem

mapDomain_congrEquiv_mapDomain_symm

L847 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.Place.mapDomain_congrEquiv_mapDomain_symm

Source context 16 commands

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

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

Lean source · statement

theorem mapDomain_congrEquiv_mapDomain_symm (D' : Divisor K F') :
    Finsupp.mapDomain (congrEquiv e he) (Finsupp.mapDomain (congrEquiv e he).symm D') = D'

theorem

mapDomain_symm_apply

L851 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.Place.mapDomain_symm_apply

Source context 16 commands

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

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

Lean source · statement

theorem mapDomain_symm_apply (D' : Divisor K F') (v : Place K F) :
    (Finsupp.mapDomain (congrEquiv e he).symm D') v = D' (congrEquiv e he v)

theorem

nodeCompatiblePairs_mapDomain_congrEquiv

L865 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.nodeCompatiblePairs_mapDomain_congrEquiv

Source context 13 commands

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

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

Lean source · full declaration

theorem nodeCompatiblePairs_mapDomain_congrEquiv (E₁ E₂ : Divisor K F) {ι : Type*} (v₁ v₂ : ι →
  Place K F) :
    nodeCompatiblePairs (Finsupp.mapDomain (Place.congrEquiv e he) E₁) (Finsupp.mapDomain
      (Place.congrEquiv e he) E₂)
        (fun i => Place.congrEquiv e he (v₁ i)) (fun i => Place.congrEquiv e he (v₂ i))
      = Submodule.map (((AlgEquiv.ofRingEquiv (f := e) he).toLinearEquiv.prodCongr
          (AlgEquiv.ofRingEquiv (f := e) he).toLinearEquiv) : F × F →ₗ[K] F' × F')
          (nodeCompatiblePairs E₁ E₂ v₁ v₂) := by
  ext ⟨g₁', g₂'⟩
  obtain ⟨g₁, rfl⟩ := e.surjective g₁'
  obtain ⟨g₂, rfl⟩ := e.surjective g₂'
  have hmem : (e g₁, e g₂) ∈ Submodule.map (((AlgEquiv.ofRingEquiv (f := e)
    he).toLinearEquiv.prodCongr
          (AlgEquiv.ofRingEquiv (f := e) he).toLinearEquiv) : F × F →ₗ[K] F' × F')
          (nodeCompatiblePairs E₁ E₂ v₁ v₂) ↔ (g₁, g₂) ∈ nodeCompatiblePairs E₁ E₂ v₁ v₂ := by
    constructor
    · rintro ⟨⟨f₁, f₂⟩, hf, hfe⟩
      have h1 : e f₁ = e g₁ := congrArg Prod.fst hfe
      have h2 : e f₂ = e g₂ := congrArg Prod.snd hfe
      obtain rfl := e.injective h1
      obtain rfl := e.injective h2
      exact hf
    · intro h
      exact ⟨(g₁, g₂), h, rfl⟩
  rw [hmem, mem_nodeCompatiblePairs_iff, mem_nodeCompatiblePairs_iff,
    Place.mem_riemannRochSpace_mapDomain_congrEquiv_iff,
      Place.mem_riemannRochSpace_mapDomain_congrEquiv_iff]
  simp only [Place.congrEquiv_apply, Place.hasValue_congrRingEquiv_iff]

theorem

finrank_nodeCompatiblePairs_mapDomain_congrEquiv

L894 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.finrank_nodeCompatiblePairs_mapDomain_congrEquiv

Source context 13 commands

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

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

Lean source · full declaration

theorem finrank_nodeCompatiblePairs_mapDomain_congrEquiv (E₁ E₂ : Divisor K F) {ι : Type*}
    (v₁ v₂ : ι → Place K F) :
    Module.finrank K (nodeCompatiblePairs (Finsupp.mapDomain (Place.congrEquiv e he) E₁)
        (Finsupp.mapDomain (Place.congrEquiv e he) E₂)
        (fun i => Place.congrEquiv e he (v₁ i)) (fun i => Place.congrEquiv e he (v₂ i)))
      = Module.finrank K (nodeCompatiblePairs E₁ E₂ v₁ v₂) := by
  rw [nodeCompatiblePairs_mapDomain_congrEquiv]
  exact LinearEquiv.finrank_map_eq _ _

theorem

finrank_riemannRochSpace_of_ringEquiv

L914 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.finrank_riemannRochSpace_of_ringEquiv

Source context 16 commands

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

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

Lean source · statement

theorem finrank_riemannRochSpace_of_ringEquiv
    (e : RatFunc k ≃+* F) (he : ∀ c : k, e (algebraMap k (RatFunc k) c) = algebraMap k F c)
    {E : Divisor k F} (hE : 0 ≤ E) :
    Module.finrank k (riemannRochSpace E) = E.degree.toNat + 1

theorem

degree_nonneg_of_ringEquiv

L943 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.degree_nonneg_of_ringEquiv

Source context 16 commands

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

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

Lean source · statement

theorem degree_nonneg_of_ringEquiv
    (e : RatFunc k ≃+* F) (he : ∀ c : k, e (algebraMap k (RatFunc k) c) = algebraMap k F c)
    {E : Divisor k F} (hE : 0 ≤ E) : 0 ≤ E.degree

theorem

finiteDimensional_riemannRochSpace_of_ringEquiv

L951 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.finiteDimensional_riemannRochSpace_of_ringEquiv

Source context 16 commands

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

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

Lean source · statement

theorem finiteDimensional_riemannRochSpace_of_ringEquiv
    (e : RatFunc k ≃+* F) (he : ∀ c : k, e (algebraMap k (RatFunc k) c) = algebraMap k F c)
    {E : Divisor k F} (hE : 0 ≤ E) :
    FiniteDimensional k (riemannRochSpace E)

theorem

finrank_nodeCompatiblePairs_add_min_le_of_ringEquiv

L963 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.finrank_nodeCompatiblePairs_add_min_le_of_ringEquiv

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
section Model
variable {k F : Type*} [Field k] [IsAlgClosed k] [DecidableEq (RatFunc k)] [Field F] [Algebra k F]
variable {ι : Type*} [Fintype ι] [DecidableEq ι]
omit [DecidableEq ι] in
omit [DecidableEq (RatFunc k)] in

Lean source · full declaration

theorem finrank_nodeCompatiblePairs_add_min_le_of_ringEquiv
    (e : RatFunc k ≃+* F) (he : ∀ c : k, e (algebraMap k (RatFunc k) c) = algebraMap k F c)
    {E₁ E₂ : Divisor k F} (hE₁ : 0 ≤ E₁) (hE₂ : 0 ≤ E₂)
    (a b : ι → k) (ha : Function.Injective a) (hb : Function.Injective b)
    (haE : ∀ i, E₁ (Place.congrEquiv e he (placeOfPoint k (a i))) = 0)
    (hbE : ∀ i, E₂ (Place.congrEquiv e he (placeOfPoint k (b i))) = 0) :
    Module.finrank k (nodeCompatiblePairs E₁ E₂
        (fun i => Place.congrEquiv e he (placeOfPoint k (a i)))
        (fun i => Place.congrEquiv e he (placeOfPoint k (b i))))
      + min (Fintype.card ι) (max E₁.degree.toNat E₂.degree.toNat + 1)
      ≤ (E₁.degree.toNat + 1) + (E₂.degree.toNat + 1) := by
  classical
  set E₁₀ : Divisor k (RatFunc k) := Finsupp.mapDomain (Place.congrEquiv e he).symm E₁ with hE₁₀
  set E₂₀ : Divisor k (RatFunc k) := Finsupp.mapDomain (Place.congrEquiv e he).symm E₂ with hE₂₀
  have h1 : E₁ = Finsupp.mapDomain (Place.congrEquiv e he) E₁₀ :=
    (Place.mapDomain_congrEquiv_mapDomain_symm e he E₁).symm
  have h2 : E₂ = Finsupp.mapDomain (Place.congrEquiv e he) E₂₀ :=
    (Place.mapDomain_congrEquiv_mapDomain_symm e he E₂).symm
  have key := finrank_nodeCompatiblePairs_add_min_le (k := k) (E₁ := E₁₀) (E₂ := E₂₀)
    (fun v => by rw [hE₁₀, Place.mapDomain_symm_apply]; exact hE₁ _)
    (fun v => by rw [hE₂₀, Place.mapDomain_symm_apply]; exact hE₂ _)
    a b ha hb
    (fun i => by rw [hE₁₀, Place.mapDomain_symm_apply]; exact haE i)
    (fun i => by rw [hE₂₀, Place.mapDomain_symm_apply]; exact hbE i)
  rw [h1, h2, finrank_nodeCompatiblePairs_mapDomain_congrEquiv, Place.degree_mapDomain_congrEquiv,
    Place.degree_mapDomain_congrEquiv]
  exact key

theorem

finrank_nodeCompatiblePairs_add_card_of_ringEquiv

L993 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField.finrank_nodeCompatiblePairs_add_card_of_ringEquiv

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
section Model
variable {k F : Type*} [Field k] [IsAlgClosed k] [DecidableEq (RatFunc k)] [Field F] [Algebra k F]
variable {ι : Type*} [Fintype ι] [DecidableEq ι]
omit [DecidableEq ι] in
omit [DecidableEq (RatFunc k)] in

Lean source · full declaration

theorem finrank_nodeCompatiblePairs_add_card_of_ringEquiv
    (e : RatFunc k ≃+* F) (he : ∀ c : k, e (algebraMap k (RatFunc k) c) = algebraMap k F c)
    {E₁ E₂ : Divisor k F} (hE₁ : 0 ≤ E₁) (hE₂ : 0 ≤ E₂)
    (a b : ι → k) (ha : Function.Injective a) (hb : Function.Injective b)
    (haE : ∀ i, E₁ (Place.congrEquiv e he (placeOfPoint k (a i))) = 0)
    (hbE : ∀ i, E₂ (Place.congrEquiv e he (placeOfPoint k (b i))) = 0)
    (hcard : Fintype.card ι ≤ max E₁.degree.toNat E₂.degree.toNat + 1) :
    Module.finrank k (nodeCompatiblePairs E₁ E₂
        (fun i => Place.congrEquiv e he (placeOfPoint k (a i)))
        (fun i => Place.congrEquiv e he (placeOfPoint k (b i))))
      + Fintype.card ι = (E₁.degree.toNat + 1) + (E₂.degree.toNat + 1) := by
  classical
  set E₁₀ : Divisor k (RatFunc k) := Finsupp.mapDomain (Place.congrEquiv e he).symm E₁ with hE₁₀
  set E₂₀ : Divisor k (RatFunc k) := Finsupp.mapDomain (Place.congrEquiv e he).symm E₂ with hE₂₀
  have h1 : E₁ = Finsupp.mapDomain (Place.congrEquiv e he) E₁₀ :=
    (Place.mapDomain_congrEquiv_mapDomain_symm e he E₁).symm
  have h2 : E₂ = Finsupp.mapDomain (Place.congrEquiv e he) E₂₀ :=
    (Place.mapDomain_congrEquiv_mapDomain_symm e he E₂).symm
  have hd1 : E₁₀.degree = E₁.degree := by rw [h1, Place.degree_mapDomain_congrEquiv]
  have hd2 : E₂₀.degree = E₂.degree := by rw [h2, Place.degree_mapDomain_congrEquiv]
  have key := finrank_nodeCompatiblePairs_add_card (k := k) (E₁ := E₁₀) (E₂ := E₂₀)
    (fun v => by rw [hE₁₀, Place.mapDomain_symm_apply]; exact hE₁ _)
    (fun v => by rw [hE₂₀, Place.mapDomain_symm_apply]; exact hE₂ _)
    a b ha hb
    (fun i => by rw [hE₁₀, Place.mapDomain_symm_apply]; exact haE i)
    (fun i => by rw [hE₂₀, Place.mapDomain_symm_apply]; exact hbE i)
    (by rw [hd1, hd2]; exact hcard)
  rw [h1, h2, finrank_nodeCompatiblePairs_mapDomain_congrEquiv, Place.degree_mapDomain_congrEquiv,
    Place.degree_mapDomain_congrEquiv]
  exact key

theorem

cardA

L1036 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.FltWs24.P1.cardA

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
section Cards
open _root_.AlgebraicCurve
open
  _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve
open FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField

Lean source · statement

theorem FltWs24.P1.cardA
    {k : Type*} [Field k] [IsAlgClosed k] (E : Divisor k (RatFunc k)) (hE : 0 ≤ E) :
    (Module.finrank k (riemannRochSpace E) : ℤ) = E.degree + 1

theorem

cardB

L1044 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.FltWs24.P1.cardB

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
section Cards
open _root_.AlgebraicCurve
open
  _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve
open FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField

Lean source · statement

theorem FltWs24.P1.cardB
    {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)
    {ι : Type*} [Fintype ι]
    (E₁ E₂ : Divisor k F) (hE₁ : 0 ≤ E₁) (hE₂ : 0 ≤ E₂)
    (a b : ι → k) (ha : Function.Injective a) (hb : Function.Injective b)
    (haE : ∀ i, E₁ (Place.congrEquiv e he (RationalFunctionField.placeOfPoint k (a i))) = 0)
    (hbE : ∀ i, E₂ (Place.congrEquiv e he (RationalFunctionField.placeOfPoint k (b i))) = 0)
    (T : Submodule k (F × F))
    (hT : ∀ p, p ∈ T ↔ p.1 ∈ riemannRochSpace E₁ ∧ p.2 ∈ riemannRochSpace E₂ ∧
      ∀ i, ∃ c : k, (Place.congrEquiv e he (RationalFunctionField.placeOfPoint k (a i))).HasValue
        p.1 c ∧
        (Place.congrEquiv e he (RationalFunctionField.placeOfPoint k (b i))).HasValue p.2 c) :
    (Module.finrank k T : ℤ) + min (Fintype.card ι : ℤ) (max E₁.degree E₂.degree + 1)
      ≤ (E₁.degree + 1) + (E₂.degree + 1)

theorem

cardC

L1071 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.FltWs24.P1.cardC

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
section Cards
open _root_.AlgebraicCurve
open
  _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve
open FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField

Lean source · statement

theorem FltWs24.P1.cardC
    {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)
    {ι : Type*} [Fintype ι]
    (E₁ E₂ : Divisor k F) (hE₁ : 0 ≤ E₁) (hE₂ : 0 ≤ E₂)
    (a b : ι → k) (ha : Function.Injective a) (hb : Function.Injective b)
    (haE : ∀ i, E₁ (Place.congrEquiv e he (RationalFunctionField.placeOfPoint k (a i))) = 0)
    (hbE : ∀ i, E₂ (Place.congrEquiv e he (RationalFunctionField.placeOfPoint k (b i))) = 0)
    (hcard : (Fintype.card ι : ℤ) ≤ max E₁.degree E₂.degree + 1)
    (T : Submodule k (F × F))
    (hT : ∀ p, p ∈ T ↔ p.1 ∈ riemannRochSpace E₁ ∧ p.2 ∈ riemannRochSpace E₂ ∧
      ∀ i, ∃ c : k, (Place.congrEquiv e he (RationalFunctionField.placeOfPoint k (a i))).HasValue
        p.1 c ∧
        (Place.congrEquiv e he (RationalFunctionField.placeOfPoint k (b i))).HasValue p.2 c) :
    (Module.finrank k T : ℤ) + Fintype.card ι = (E₁.degree + 1) + (E₂.degree + 1)

theorem

cardD

L1099 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.FltWs24.P1.cardD

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing
open _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs
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
section Cards
open _root_.AlgebraicCurve
open
  _root_.AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve
open FinrankRRSpaceDegreeAddOneRing.AlgebraicCurve.RationalFunctionField

Lean source · statement

theorem FltWs24.P1.cardD
    {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)
    (E : Divisor k F) (hE : 0 ≤ E) :
    (Module.finrank k (riemannRochSpace E) : ℤ) = E.degree + 1

theorem

finrank_riemannRochSpace_eq_degree_add_one_of_ringEquiv_ratFunc

L1114 ↗

AlgebraicCurve.finrank_riemannRochSpace_eq_degree_add_one_of_ringEquiv_ratFunc

Source context 6 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.finrank_riemannRochSpace_eq_degree_add_one_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)
    (E : Divisor k F) (hE : 0 ≤ E) :
    (Module.finrank k (riemannRochSpace E) : ℤ) = E.degree + 1

Module documentation

Finrank riemann Roch Space eq degree add one of ring Equiv rat Func

Declarations