Module

Exists_mem_riemannRochSpace_not_mem_sub_single_of_ringEquiv_ratFunc.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Exists_mem_riemannRochSpace_not_mem_sub_single_of_ringEquiv_ratFunc

72 declarations indexed from sourceView source ↗

Module documentation

Exists mem riemann Roch Space not mem sub single of ring Equiv rat Func

Imports10

Imported by1

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.All

theorem

hasValue_zero

L51 ↗

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L59 ↗

AlgebraicCurve.Place.HasValue.add

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L72 ↗

AlgebraicCurve.Place.HasValue.neg

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L82 ↗

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

const_mul

L88 ↗

AlgebraicCurve.Place.HasValue.const_mul

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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.const_mul {g : F} {a : K} (c : K) (h :
  v.HasValue g a) :
    v.HasValue (c • g) (c * a)

theorem

pow

L98 ↗

AlgebraicCurve.Place.HasValue.pow

Source context 18 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.HasValue.pow {g : F} {a : K} (h : v.HasValue g a) (n :
  ℕ) : v.HasValue (g ^ n) (a ^ n)

theorem

zpow

L110 ↗

AlgebraicCurve.Place.HasValue.zpow

Source context 19 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.HasValue.zpow {g : F} {a : K} (h : v.HasValue g a) (ha
  : a ≠ 0) (n : ℤ) :
    v.HasValue (g ^ n) (a ^ n)

theorem

prod

L124 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.Place.HasValue.prod

Source context 19 commands

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

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

Lean source · statement

theorem HasValue.prod {ι : Type*} (s : Finset ι) {g : ι → F} {a : ι → K}
    (h : ∀ i ∈ s, v.HasValue (g i) (a i)) : v.HasValue (∏ i ∈ s, g i) (∏ i ∈ s, a i)

theorem

ord_prod

L133 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.Place.ord_prod

Source context 18 commands

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

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

Lean source · statement

theorem ord_prod {ι : Type*} (s : Finset ι) {g : ι → F} (h : ∀ i ∈ s, g i ≠ 0) :
    v.ord (∏ i ∈ s, g i) = ∑ i ∈ s, v.ord (g i)

def

twistedPairs

L151 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.twistedPairs

Documentation

Pairs in two Riemann-Roch spaces satisfying the prescribed weighted value conditions.

Source context 11 commands

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

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

Lean source · full declaration

def twistedPairs (E₁ E₂ : Divisor K F) {ι : Type*} (v₁ v₂ : ι → Place K F) (t₁ t₂ : ι → F)
    (lam : ι → K) : Submodule K (F × F) where
  carrier := {p | p.1 ∈ riemannRochSpace E₁ ∧ p.2 ∈ riemannRochSpace E₂ ∧
    ∀ i, ∃ c : K, (v₁ i).HasValue (t₁ i * p.1) (lam i * c) ∧ (v₂ i).HasValue (t₂ i * p.2) c}
  zero_mem' := ⟨Submodule.zero_mem _, Submodule.zero_mem _, fun i =>
    ⟨0, by simpa using Place.hasValue_zero (v₁ i), by simpa using Place.hasValue_zero (v₂ i)⟩⟩
  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
    refine ⟨c + d, ?_, ?_⟩
    · simpa [mul_add] using hc1.add hd1
    · simpa [mul_add] using 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
    refine ⟨a * c, ?_, ?_⟩
    · have := hc1.const_mul a
      rw [Prod.smul_fst, mul_smul_comm]
      convert this using 1
      ring
    · have := hc2.const_mul a
      rw [Prod.smul_snd, mul_smul_comm]
      exact this

theorem

mem_twistedPairs_iff

L178 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.mem_twistedPairs_iff

Source context 11 commands

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

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

Lean source · statement

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

theorem

twistedPairs_le_comp

L184 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.twistedPairs_le_comp

Source context 11 commands

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

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

Lean source · statement

theorem twistedPairs_le_comp {E₁ E₂ : Divisor K F} {ι ι' : Type*} (v₁ v₂ : ι → Place K F)
    (t₁ t₂ : ι → F) (lam : ι → K) (u : ι' → ι) :
    twistedPairs E₁ E₂ v₁ v₂ t₁ t₂ lam
      ≤ twistedPairs E₁ E₂ (v₁ ∘ u) (v₂ ∘ u) (t₁ ∘ u) (t₂ ∘ u) (lam ∘ u)

def

divisorPoints

L209 ↗

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

Documentation

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L215 ↗

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

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

theorem

algebraMap_X_sub_C

L219 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.algebraMap_X_sub_C

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 algebraMap_X_sub_C (a : k) :
    algebraMap k[X] (RatFunc k) (X - C a) = RatFunc.X - RatFunc.C a

theorem

ratFunc_X_sub_C_ne_zero

L223 ↗

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

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 ratFunc_X_sub_C_ne_zero (a : k) : (RatFunc.X - RatFunc.C a : RatFunc k) ≠ 0

theorem

ord_placeOfPoint_X_sub_C

L228 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_X_sub_C

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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}
open scoped Classical in

Lean source · full declaration

theorem ord_placeOfPoint_X_sub_C (a b : k) :
    (placeOfPoint k b).ord (RatFunc.X - RatFunc.C a : RatFunc k) = if b = a then 1 else 0 := by
  rw [← algebraMap_X_sub_C, ord_placeOfPoint_algebraMap b (X_sub_C_ne_zero a)]
  split_ifs with h
  · subst h
    exact_mod_cast rootMultiplicity_X_sub_C_self
  · rw [Nat.cast_eq_zero]
    refine rootMultiplicity_eq_zero ?_
    rw [IsRoot, eval_sub, eval_X, eval_C]
    exact sub_ne_zero.mpr h

theorem

ord_placeInfty_X_sub_C

L239 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.ord_placeInfty_X_sub_C

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 ord_placeInfty_X_sub_C [DecidableEq (RatFunc k)] (a : k) :
    (placeInfty k).ord (RatFunc.X - RatFunc.C a : RatFunc k) = -1

def

divisorFn

L248 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.divisorFn

Documentation

The product of rational linear factors with exponents given by the divisor.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 divisorFn (E : Divisor k (RatFunc k)) (S : Finset k) : RatFunc k

theorem

divisorFn_ne_zero

L251 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.divisorFn_ne_zero

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 divisorFn_ne_zero (E : Divisor k (RatFunc k)) (S : Finset k) : divisorFn k E S ≠ 0

theorem

divisorFn_eq_of_subset

L254 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.divisorFn_eq_of_subset

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 divisorFn_eq_of_subset {E : Divisor k (RatFunc k)} {S : Finset k} (hS : divisorPoints k E
  ⊆ S) :
    divisorFn k E S = divisorFn k E (divisorPoints k E)

theorem

divisorFn_insert_erase

L262 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.divisorFn_insert_erase

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 divisorFn_insert_erase [DecidableEq k] (E : Divisor k (RatFunc k)) (b : k) :
    divisorFn k E (divisorPoints k E)
      = (RatFunc.X - RatFunc.C b) ^ (E (placeOfPoint k b)) * divisorFn k E ((divisorPoints k
        E).erase b)

theorem

ord_placeOfPoint_divisorFn

L270 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_divisorFn

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_divisorFn {E : Divisor k (RatFunc k)} {S : Finset k} (hS : divisorPoints
  k E ⊆ S)
    (b : k) : (placeOfPoint k b).ord (divisorFn k E S) = E (placeOfPoint k b)

theorem

ord_placeInfty_divisorFn

L283 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.ord_placeInfty_divisorFn

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_divisorFn [DecidableEq (RatFunc k)] (E : Divisor k (RatFunc k)) (S : Finset
  k) :
    (placeInfty k).ord (divisorFn k E S) = -∑ a ∈ S, E (placeOfPoint k a)

theorem

support_subset_insert

L290 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L299 ↗

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

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_sum_of_subset

L316 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.degree_eq_sum_of_subset

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_of_subset [IsAlgClosed k] [DecidableEq (RatFunc k)] {E : Divisor k (RatFunc
  k)}
    {S : Finset k} (hS : divisorPoints k E ⊆ S) :
    E.degree = (∑ a ∈ S, E (placeOfPoint k a)) + E (placeInfty k)

theorem

algebraMap_ne_zero'

L344 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.algebraMap_ne_zero'

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 algebraMap_ne_zero' {P : k[X]} (hP : P ≠ 0) : algebraMap k[X] (RatFunc k) P ≠ 0

theorem

mem_degreeLT_iff_natDegree

L347 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.mem_degreeLT_iff_natDegree

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 mem_degreeLT_iff_natDegree {P : k[X]} {n : ℕ} : P ∈ degreeLT k n ↔ P = 0 ∨ P.natDegree < n

theorem

ord_placeOfPoint_div_divisorFn

L355 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_div_divisorFn

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_divisorFn {E : Divisor k (RatFunc k)} {S : Finset k}
    (hS : divisorPoints k E ⊆ S) {P : k[X]} (hP : P ≠ 0) (b : k) :
    (placeOfPoint k b).ord (algebraMap k[X] (RatFunc k) P / divisorFn k E S)
      = (rootMultiplicity b P : ℤ) - E (placeOfPoint k b)

theorem

ord_placeInfty_div_divisorFn

L364 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.ord_placeInfty_div_divisorFn

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_placeInfty_div_divisorFn [DecidableEq (RatFunc k)] (E : Divisor k (RatFunc k)) (S :
  Finset k)
    {P : k[X]} (hP : P ≠ 0) :
    (placeInfty k).ord (algebraMap k[X] (RatFunc k) P / divisorFn k E S)
      = (∑ a ∈ S, E (placeOfPoint k a)) - P.natDegree

theorem

exists_eq_algebraMap_of_forall_ord_nonneg

L375 ↗

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_divisorFn_mem_riemannRochSpace

L412 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.div_divisorFn_mem_riemannRochSpace

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_divisorFn_mem_riemannRochSpace (E : Divisor k (RatFunc k)) {P : k[X]}
    (hP : P ∈ degreeLT k (E.degree + 1).toNat) :
    algebraMap k[X] (RatFunc k) P / divisorFn k E (divisorPoints k E) ∈ riemannRochSpace E

theorem

exists_eq_div_divisorFn_of_mem

L435 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.exists_eq_div_divisorFn_of_mem

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_divisorFn_of_mem (E : Divisor k (RatFunc k)) {f : RatFunc k}
    (hf : f ∈ riemannRochSpace E) :
    ∃ P : k[X], P ∈ degreeLT k (E.degree + 1).toNat ∧
      f = algebraMap k[X] (RatFunc k) P / divisorFn k E (divisorPoints k E)

def

divDivisorFn

L465 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.divDivisorFn

Documentation

Embed a polynomial into the function field and divide by the divisor function.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 divDivisorFn (E : Divisor k (RatFunc k)) : k[X] →ₗ[k] RatFunc k

theorem

divDivisorFn_apply

L471 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.divDivisorFn_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 divDivisorFn_apply (E : Divisor k (RatFunc k)) (P : k[X]) :
    divDivisorFn E P = algebraMap k[X] (RatFunc k) P / divisorFn k E (divisorPoints k E)

theorem

divDivisorFn_injective

L476 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.divDivisorFn_injective

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 divDivisorFn_injective (E : Divisor k (RatFunc k)) : Function.Injective (divDivisorFn E)

def

riemannRochSpaceEquiv

L483 ↗

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

Documentation

The polynomial description of the Riemann-Roch space on the rational function field.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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)) :
    degreeLT k (E.degree + 1).toNat ≃ₗ[k] riemannRochSpace E

theorem

finrank_degreeLT

L496 ↗

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

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L500 ↗

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

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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)) :
    Module.finrank k (riemannRochSpace E) = (E.degree + 1).toNat

theorem

hasValue_placeOfPoint_algebraMap

L525 ↗

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_X_sub_C

L551 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.hasValue_placeOfPoint_X_sub_C

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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_X_sub_C (b a : k) :
    (placeOfPoint k b).HasValue (RatFunc.X - RatFunc.C a : RatFunc k) (b - a)

def

divisorFnEval

L558 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.divisorFnEval

Documentation

Evaluate the product of divisor-weighted linear factors at a base-field point.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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]
variable (k) in

Lean source · statement

def divisorFnEval (E : Divisor k (RatFunc k)) (S : Finset k) (b : k) : k

theorem

divisorFnEval_ne_zero

L561 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.divisorFnEval_ne_zero

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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]
variable (k) in

Lean source · statement

theorem divisorFnEval_ne_zero (E : Divisor k (RatFunc k)) {S : Finset k} {b : k} (hb : b ∉ S) :
    divisorFnEval k E S b ≠ 0

theorem

hasValue_placeOfPoint_divisorFn

L565 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.hasValue_placeOfPoint_divisorFn

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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]
variable (k) in

Lean source · statement

theorem hasValue_placeOfPoint_divisorFn (E : Divisor k (RatFunc k)) {S : Finset k} {b : k} (hb : b
  ∉ S) :
    (placeOfPoint k b).HasValue (divisorFn k E S) (divisorFnEval k E S b)

theorem

hasValue_placeOfPoint_twist

L571 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.hasValue_placeOfPoint_twist

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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]
variable (k) in

Lean source · statement

theorem hasValue_placeOfPoint_twist [DecidableEq k] (E : Divisor k (RatFunc k)) (b : k) (P : k[X]) :
    (placeOfPoint k b).HasValue
      ((RatFunc.X - RatFunc.C b) ^ (E (placeOfPoint k b)) *
        (algebraMap k[X] (RatFunc k) P / divisorFn k E (divisorPoints k E)))
      (P.eval b / divisorFnEval k E ((divisorPoints k E).erase b) b)

def

wEvalAt

L608 ↗

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

Documentation

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L613 ↗

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

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L619 ↗

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

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L638 ↗

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

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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₂

def

twistWeight

L662 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.twistWeight

Documentation

The inverse value of the divisor function with the selected point omitted.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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] [DecidableEq k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
variable {ι : Type*}

Lean source · statement

def twistWeight (E : Divisor k (RatFunc k)) (b : k) : k

theorem

twistWeight_ne_zero

L666 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.twistWeight_ne_zero

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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] [DecidableEq k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
variable {ι : Type*}
omit [IsAlgClosed k] [DecidableEq (RatFunc k)] in

Lean source · statement

theorem twistWeight_ne_zero (E : Divisor k (RatFunc k)) (b : k) : twistWeight E b ≠ 0

theorem

hasValue_twist'

L670 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.hasValue_twist'

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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] [DecidableEq k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
variable {ι : Type*}
omit [IsAlgClosed k] [DecidableEq (RatFunc k)] in

Lean source · statement

theorem hasValue_twist' (E : Divisor k (RatFunc k)) (b : k) (P : k[X]) :
    (placeOfPoint k b).HasValue
      ((RatFunc.X - RatFunc.C b) ^ (E (placeOfPoint k b)) *
        (algebraMap k[X] (RatFunc k) P / divisorFn k E (divisorPoints k E)))
      (twistWeight E b * P.eval b)

def

twistFn

L679 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.twistFn

Documentation

The rational linear factor at the selected point raised to the divisor coefficient.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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] [DecidableEq k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
variable {ι : Type*}

Lean source · statement

def twistFn (E : Divisor k (RatFunc k)) (b : k) : RatFunc k

theorem

twistedPairs_eq_map

L684 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.twistedPairs_eq_map

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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] [DecidableEq k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
variable {ι : Type*}
omit [DecidableEq (RatFunc k)] in

Lean source · full declaration

theorem twistedPairs_eq_map (E₁ E₂ : Divisor k (RatFunc k)) (a b : ι → k) (lam : ι → k) :
    twistedPairs E₁ E₂ (fun i => placeOfPoint k (a i)) (fun i => placeOfPoint k (b i))
        (fun i => twistFn E₁ (a i)) (fun i => twistFn E₂ (b i)) lam
      = Submodule.map
          ((divDivisorFn E₁ ∘ₗ (degreeLT k (E₁.degree + 1).toNat).subtype).prodMap
            (divDivisorFn E₂ ∘ₗ (degreeLT k (E₂.degree + 1).toNat).subtype))
          (LinearMap.ker
            ((wEvalAt a (fun i => twistWeight E₁ (a i)) (E₁.degree + 1).toNat).coprod
              (-(wEvalAt b (fun i => lam i * twistWeight E₂ (b i)) (E₂.degree + 1).toNat)))) := by
  classical
  ext ⟨g₁, g₂⟩
  simp only [twistFn, mem_twistedPairs_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, divDivisorFn_apply, Prod.mk.injEq, Prod.exists]
  constructor
  · rintro ⟨hg₁, hg₂, hnode⟩
    obtain ⟨P₁, hP₁, rfl⟩ := exists_eq_div_divisorFn_of_mem E₁ hg₁
    obtain ⟨P₂, hP₂, rfl⟩ := exists_eq_div_divisorFn_of_mem E₂ hg₂
    refine ⟨⟨P₁, hP₁⟩, ⟨P₂, hP₂⟩, ?_, rfl, rfl⟩
    ext i
    obtain ⟨c, hc₁, hc₂⟩ := hnode i
    have h₁ := hc₁.unique (hasValue_twist' E₁ (a i) P₁)
    have h₂ := hc₂.unique (hasValue_twist' E₂ (b i) P₂)
    simp only [Pi.add_apply, Pi.neg_apply, wEvalAt_apply, Pi.zero_apply]
    rw [mul_assoc, ← h₂, ← h₁, add_neg_cancel]
  · rintro ⟨P₁, P₂, hker, rfl, rfl⟩
    refine ⟨div_divisorFn_mem_riemannRochSpace E₁ P₁.2, div_divisorFn_mem_riemannRochSpace E₂ P₂.2,
      fun i => ?_⟩
    refine ⟨twistWeight E₂ (b i) * (P₂ : k[X]).eval (b i), ?_, hasValue_twist' E₂ (b i) _⟩
    have hi := congrFun hker i
    simp only [Pi.add_apply, Pi.neg_apply, wEvalAt_apply, Pi.zero_apply, add_neg_eq_zero] at hi
    have := hasValue_twist' E₁ (a i) (P₁ : k[X])
    rwa [hi, mul_assoc] at this

theorem

finiteDimensional_twistedPairs

L720 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.finiteDimensional_twistedPairs

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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] [DecidableEq k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
variable {ι : Type*}
omit [DecidableEq k] [DecidableEq (RatFunc k)] in

Lean source · full declaration

theorem finiteDimensional_twistedPairs (E₁ E₂ : Divisor k (RatFunc k)) (a b : ι → k) (lam : ι → k) :
    FiniteDimensional k
      (twistedPairs E₁ E₂ (fun i => placeOfPoint k (a i)) (fun i => placeOfPoint k (b i))
        (fun i => twistFn E₁ (a i)) (fun i => twistFn E₂ (b i)) lam) := by
  classical
  rw [twistedPairs_eq_map E₁ E₂ a b lam]
  infer_instance

theorem

finrank_twistedPairs_add_card

L732 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.finrank_twistedPairs_add_card

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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] [DecidableEq k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
variable {ι : Type*}
variable [Fintype ι] [DecidableEq ι]
omit [DecidableEq ι] in
omit [DecidableEq k] [DecidableEq (RatFunc k)] in

Lean source · full declaration

theorem finrank_twistedPairs_add_card (E₁ E₂ : Divisor k (RatFunc k))
    (a b : ι → k) (ha : Function.Injective a) (hb : Function.Injective b)
    (lam : ι → k) (hlam : ∀ i, lam i ≠ 0)
    (hcard : Fintype.card ι ≤ max (E₁.degree + 1).toNat (E₂.degree + 1).toNat) :
    Module.finrank k (twistedPairs E₁ E₂ (fun i => placeOfPoint k (a i)) (fun i => placeOfPoint k
      (b i))
        (fun i => twistFn E₁ (a i)) (fun i => twistFn E₂ (b i)) lam)
      + Fintype.card ι = (E₁.degree + 1).toNat + (E₂.degree + 1).toNat := by
  classical
  rw [twistedPairs_eq_map E₁ E₂ a b lam]
  have hinj : Function.Injective
      ((divDivisorFn E₁ ∘ₗ (degreeLT k (E₁.degree + 1).toNat).subtype).prodMap
        (divDivisorFn E₂ ∘ₗ (degreeLT k (E₂.degree + 1).toNat).subtype)) :=
    Function.Injective.prodMap ((divDivisorFn_injective E₁).comp Subtype.val_injective)
      ((divDivisorFn_injective E₂).comp Subtype.val_injective)
  rw [← (Submodule.equivMapOfInjective _ hinj _).finrank_eq]
  have key := finrank_ker_coprod_neg_add
    (wEvalAt a (fun i => twistWeight E₁ (a i)) (E₁.degree + 1).toNat)
    (wEvalAt b (fun i => lam i * twistWeight E₂ (b i)) (E₂.degree + 1).toNat) ?_
  · rw [finrank_degreeLT, finrank_degreeLT, Module.finrank_fintype_fun_eq_card] at key
    exact key
  · rcases le_max_iff.mp hcard with h | h
    · left
      exact wEvalAt_surjective ha (fun i => twistWeight_ne_zero E₁ (a i)) h
    · right
      exact wEvalAt_surjective hb (fun i => mul_ne_zero (hlam i) (twistWeight_ne_zero E₂ (b i))) h

theorem

finrank_twistedPairs_add_min_le

L761 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.finrank_twistedPairs_add_min_le

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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] [DecidableEq k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
variable {ι : Type*}
variable [Fintype ι] [DecidableEq ι]
omit [DecidableEq ι] in
omit [DecidableEq k] [DecidableEq (RatFunc k)] in

Lean source · full declaration

theorem finrank_twistedPairs_add_min_le (E₁ E₂ : Divisor k (RatFunc k))
    (a b : ι → k) (ha : Function.Injective a) (hb : Function.Injective b)
    (lam : ι → k) (hlam : ∀ i, lam i ≠ 0) :
    Module.finrank k (twistedPairs E₁ E₂ (fun i => placeOfPoint k (a i)) (fun i => placeOfPoint k
      (b i))
        (fun i => twistFn E₁ (a i)) (fun i => twistFn E₂ (b i)) lam)
      + min (Fintype.card ι) (max (E₁.degree + 1).toNat (E₂.degree + 1).toNat)
      ≤ (E₁.degree + 1).toNat + (E₂.degree + 1).toNat := by
  classical
  set m := min (Fintype.card ι) (max (E₁.degree + 1).toNat (E₂.degree + 1).toNat) with hm
  let u : Fin m ↪ ι := (Fin.castLEEmb (min_le_left _ _)).trans (Fintype.equivFin ι).symm.toEmbedding
  have hle := twistedPairs_le_comp (E₁ := E₁) (E₂ := E₂)
    (fun i => placeOfPoint k (a i)) (fun i => placeOfPoint k (b i))
    (fun i => twistFn E₁ (a i)) (fun i => twistFn E₂ (b i)) lam u
  have heq := finrank_twistedPairs_add_card E₁ E₂ (a ∘ u) (b ∘ u)
    (ha.comp u.injective) (hb.comp u.injective) (lam ∘ u) (fun i => hlam (u i))
    (by rw [Fintype.card_fin]; exact min_le_right _ _)
  rw [Fintype.card_fin] at heq
  have : FiniteDimensional k (twistedPairs E₁ E₂ ((fun i => placeOfPoint k (a i)) ∘ u)
      ((fun i => placeOfPoint k (b i)) ∘ u) ((fun i => twistFn E₁ (a i)) ∘ u) ((fun i => twistFn
        E₂ (b i)) ∘ u)
      (lam ∘ u)) :=
    finiteDimensional_twistedPairs E₁ E₂ (a ∘ u) (b ∘ u) (lam ∘ u)
  have hmono := Submodule.finrank_mono hle
  change Module.finrank k _ ≤ Module.finrank k
    (twistedPairs E₁ E₂ (fun i => placeOfPoint k ((a ∘ u) i)) (fun i => placeOfPoint k ((b ∘ u) i))
      (fun i => twistFn E₁ ((a ∘ u) i)) (fun i => twistFn E₂ ((b ∘ u) i)) (lam ∘ u)) at hmono
  omega

theorem

congrResidueAlgEquiv_residue

L808 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L815 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L835 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L851 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L859 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

L863 ↗

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

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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

twistedPairs_mapDomain_congrEquiv

L878 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.twistedPairs_mapDomain_congrEquiv

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 CongrTwisted
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 twistedPairs_mapDomain_congrEquiv (E₁ E₂ : Divisor K F) {ι : Type*} (v₁ v₂ : ι → Place K F)
    (t₁ t₂ : ι → F) (lam : ι → K) :
    twistedPairs (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))
        (fun i => e (t₁ i)) (fun i => e (t₂ i)) lam
      = Submodule.map (((AlgEquiv.ofRingEquiv (f := e) he).toLinearEquiv.prodCongr
          (AlgEquiv.ofRingEquiv (f := e) he).toLinearEquiv) : F × F →ₗ[K] F' × F')
          (twistedPairs E₁ E₂ v₁ v₂ t₁ t₂ lam) := 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')
          (twistedPairs E₁ E₂ v₁ v₂ t₁ t₂ lam) ↔ (g₁, g₂) ∈ twistedPairs E₁ E₂ v₁ v₂ t₁ t₂ lam := 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_twistedPairs_iff, mem_twistedPairs_iff,
    Place.mem_riemannRochSpace_mapDomain_congrEquiv_iff,
      Place.mem_riemannRochSpace_mapDomain_congrEquiv_iff]
  simp only [Place.congrEquiv_apply, ← map_mul, Place.hasValue_congrRingEquiv_iff]

theorem

finrank_twistedPairs_mapDomain_congrEquiv

L908 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.finrank_twistedPairs_mapDomain_congrEquiv

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 CongrTwisted
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_twistedPairs_mapDomain_congrEquiv (E₁ E₂ : Divisor K F) {ι : Type*}
    (v₁ v₂ : ι → Place K F) (t₁ t₂ : ι → F) (lam : ι → K) :
    Module.finrank K (twistedPairs (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))
        (fun i => e (t₁ i)) (fun i => e (t₂ i)) lam)
      = Module.finrank K (twistedPairs E₁ E₂ v₁ v₂ t₁ t₂ lam) := by
  rw [twistedPairs_mapDomain_congrEquiv]
  exact LinearEquiv.finrank_map_eq _ _

theorem

finrank_twistedPairs_add_min_le_of_ringEquiv

L932 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.finrank_twistedPairs_add_min_le_of_ringEquiv

Source context 16 commands

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

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

Lean source · full declaration

theorem finrank_twistedPairs_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)
    (a b : ι → k) (ha : Function.Injective a) (hb : Function.Injective b)
    (lam : ι → k) (hlam : ∀ i, lam i ≠ 0) :
    Module.finrank k (twistedPairs E₁ E₂
        (fun i => Place.congrEquiv e he (placeOfPoint k (a i)))
        (fun i => Place.congrEquiv e he (placeOfPoint k (b i)))
        (fun i => e ((RatFunc.X - RatFunc.C (a i)) ^ (E₁ (Place.congrEquiv e he (placeOfPoint k (a
          i))))))
        (fun i => e ((RatFunc.X - RatFunc.C (b i)) ^ (E₂ (Place.congrEquiv e he (placeOfPoint k (b
          i))))))
        lam)
      + min (Fintype.card ι) (max (E₁.degree + 1).toNat (E₂.degree + 1).toNat)
      ≤ (E₁.degree + 1).toNat + (E₂.degree + 1).toNat := 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 ht1 : ∀ i, E₁ (Place.congrEquiv e he (placeOfPoint k (a i))) = E₁₀ (placeOfPoint k (a i)) :=
    fun i => (Place.mapDomain_symm_apply e he E₁ _).symm
  have ht2 : ∀ i, E₂ (Place.congrEquiv e he (placeOfPoint k (b i))) = E₂₀ (placeOfPoint k (b i)) :=
    fun i => (Place.mapDomain_symm_apply e he E₂ _).symm
  have key := finrank_twistedPairs_add_min_le (k := k) E₁₀ E₂₀ a b ha hb lam hlam
  have hfin := finrank_twistedPairs_mapDomain_congrEquiv e he E₁₀ E₂₀
    (fun i => placeOfPoint k (a i)) (fun i => placeOfPoint k (b i))
    (fun i => twistFn E₁₀ (a i)) (fun i => twistFn E₂₀ (b i)) lam
  rw [← hfin, ← h1, ← h2, hd1, hd2] at key
  have hsub : twistedPairs E₁ E₂
        (fun i => Place.congrEquiv e he (placeOfPoint k (a i)))
        (fun i => Place.congrEquiv e he (placeOfPoint k (b i)))
        (fun i => e ((RatFunc.X - RatFunc.C (a i)) ^ (E₁ (Place.congrEquiv e he (placeOfPoint k (a
          i))))))
        (fun i => e ((RatFunc.X - RatFunc.C (b i)) ^ (E₂ (Place.congrEquiv e he (placeOfPoint k (b
          i))))))
        lam
      = twistedPairs E₁ E₂
        (fun i => Place.congrEquiv e he (placeOfPoint k (a i)))
        (fun i => Place.congrEquiv e he (placeOfPoint k (b i)))
        (fun i => e (twistFn E₁₀ (a i))) (fun i => e (twistFn E₂₀ (b i))) lam := by
    ext p
    simp only [mem_twistedPairs_iff, twistFn, ht1, ht2]
  rw [hsub]
  exact key

theorem

exists_mem_riemannRochSpace_forall_hasValue_twist

L1005 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.exists_mem_riemannRochSpace_forall_hasValue_twist

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 Avoidance
variable {k : Type*} [Field k] [DecidableEq k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
variable {ι : Type*} [Fintype ι] [DecidableEq ι]
omit [DecidableEq ι] in
omit [DecidableEq k] [DecidableEq (RatFunc k)] in

Lean source · statement

theorem exists_mem_riemannRochSpace_forall_hasValue_twist (E : Divisor k (RatFunc k))
    (hE : Fintype.card ι ≤ (E.degree + 1).toNat) (a : ι → k) (ha : Function.Injective a) (c : ι →
      k) :
    ∃ p ∈ riemannRochSpace E, ∀ i, (placeOfPoint k (a i)).HasValue (twistFn E (a i) * p) (c i)

theorem

exists_mem_riemannRochSpace_ord_eq

L1020 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.exists_mem_riemannRochSpace_ord_eq

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle
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 Avoidance
variable {k : Type*} [Field k] [DecidableEq k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
variable {ι : Type*} [Fintype ι] [DecidableEq ι]
omit [DecidableEq k] [Fintype ι] [DecidableEq ι] in
omit [DecidableEq (RatFunc k)] in

Lean source · statement

theorem exists_mem_riemannRochSpace_ord_eq (E : Divisor k (RatFunc k)) (hE : 0 ≤ E.degree)
    (w : Place k (RatFunc k)) :
    ∃ p ∈ riemannRochSpace E, p ≠ 0 ∧ w.ord p = -E w

theorem

exists_mem_riemannRochSpace_forall_hasValue_twist_of_ringEquiv

L1057 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.exists_mem_riemannRochSpace_forall_hasValue_twist_of_ringEquiv

Source context 19 commands

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

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

Lean source · statement

theorem exists_mem_riemannRochSpace_forall_hasValue_twist_of_ringEquiv
    (e : RatFunc k ≃+* F) (he : ∀ c : k, e (algebraMap k (RatFunc k) c) = algebraMap k F c)
    (E : Divisor k F) (hE : Fintype.card ι ≤ (E.degree + 1).toNat)
    (a : ι → k) (ha : Function.Injective a) (c : ι → k) :
    ∃ p ∈ riemannRochSpace E, ∀ i,
      (Place.congrEquiv e he (placeOfPoint k (a i))).HasValue
        (e ((RatFunc.X - RatFunc.C (a i)) ^ (E (Place.congrEquiv e he (placeOfPoint k (a i))))) *
          p) (c i)

theorem

exists_mem_riemannRochSpace_ord_eq_of_ringEquiv

L1081 ↗

AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsMemRRSpaceNotMemSubSingle.AlgebraicCurve.RationalFunctionField.exists_mem_riemannRochSpace_ord_eq_of_ringEquiv

Source context 19 commands

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

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

Lean source · statement

theorem exists_mem_riemannRochSpace_ord_eq_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.degree) (w : Place k F) :
    ∃ p ∈ riemannRochSpace E, p ≠ 0 ∧ w.ord p = -E w

theorem

exists_mem_riemannRochSpace_not_mem_sub_single_of_ringEquiv_ratFunc

L1109 ↗

AlgebraicCurve.exists_mem_riemannRochSpace_not_mem_sub_single_of_ringEquiv_ratFunc

Source context 5 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.exists_mem_riemannRochSpace_not_mem_sub_single_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.degree) (w : Place k F) :
    ∃ p ∈ riemannRochSpace E, p ∉ riemannRochSpace (E - Finsupp.single w 1)

Module documentation

Exists mem riemann Roch Space not mem sub single of ring Equiv rat Func

Declarations