NYLL
Module

IsUnit_det_jetMatrix_iff_span_inf_riemannRochSpace_eq_bot.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.IsUnit_det_jetMatrix_iff_span_inf_riemannRochSpace_eq_bot
16 declarations indexed from sourceView source ↗

Module documentation

Is Unit det jet Matrix iff span inf riemann Roch Space eq bot

Imports6
Imported by1

Declarations

theorem

jetMult_eq_zero_of_forall_ne

L36 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.J2Sub.jetMult_eq_zero_of_forall_ne
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece0
open AlgebraicCurve
namespace J2Sub
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  {M : ℕ} {P : Fin M → Place K F} {t : Fin M → F} {e : Fin M → ℕ}
Lean source · statement
theorem jetMult_eq_zero_of_forall_ne {v : Place K F} (h : ∀ i, P i ≠ v) : jetMult P v = 0
theorem

jetMult_pos

L42 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.J2Sub.jetMult_pos
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece0
open AlgebraicCurve
namespace J2Sub
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  {M : ℕ} {P : Fin M → Place K F} {t : Fin M → F} {e : Fin M → ℕ}
Lean source · statement
theorem jetMult_pos (i : Fin M) : 0 < jetMult P (P i)
theorem

exists_row_of_lt_jetMult'

L48 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.J2Sub.exists_row_of_lt_jetMult'
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece0
open AlgebraicCurve
namespace J2Sub
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  {M : ℕ} {P : Fin M → Place K F} {t : Fin M → F} {e : Fin M → ℕ}
Lean source · statement
theorem exists_row_of_lt_jetMult' (hP : IsConfluentPattern P t e) (i : Fin M) (q : ℕ)
    (hq : q < jetMult P (P i)) : ∃ i', P i' = P i ∧ e i' = q
theorem

exists_row_of_lt_jetMult

L74 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.J2Sub.exists_row_of_lt_jetMult
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece0
open AlgebraicCurve
Lean source · statement
theorem J2Sub.exists_row_of_lt_jetMult {K F : Type*} [Field K] [Field F] [Algebra K F]
    {M : ℕ} {P : Fin M → Place K F} {t : Fin M → F} {e : Fin M → ℕ}
    (hP : IsConfluentPattern P t e) (i : Fin M) (q : ℕ) (hq : q < jetMult P (P i)) :
    ∃ i', P i' = P i ∧ t i' = t i ∧ e i' = q
theorem

jetMult_eq_zero_of_forall_ne'

L90 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.J2Sub.jetMult_eq_zero_of_forall_ne'
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece1
open AlgebraicCurve
namespace J2Sub
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {M : ℕ}
Lean source · statement
theorem jetMult_eq_zero_of_forall_ne' {P : Fin M → Place K F} {v : Place K F} (h : ∀ i, P i ≠ v) :
    jetMult P v = 0
theorem

jetDivisor_nonneg

L97 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.J2Sub.jetDivisor_nonneg
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece1
open AlgebraicCurve
namespace J2Sub
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {M : ℕ}
Lean source · statement
theorem jetDivisor_nonneg (P : Fin M → Place K F) (v : Place K F) : 0 ≤ jetDivisor P v
theorem

riemannRochSpace_sub_jetDivisor_le

L102 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.J2Sub.riemannRochSpace_sub_jetDivisor_le
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece1
open AlgebraicCurve
Lean source · statement
theorem J2Sub.riemannRochSpace_sub_jetDivisor_le {K F : Type*} [Field K] [Field F] [Algebra K F]
    (A : Divisor K F) {M : ℕ} (P : Fin M → Place K F) :
    riemannRochSpace (A - jetDivisor P) ≤ riemannRochSpace A
theorem

mem_toValuationSubring_of_mem_riemannRochSpace

L115 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.J2Sub.mem_toValuationSubring_of_mem_riemannRochSpace
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece1
open AlgebraicCurve
Lean source · statement
theorem J2Sub.mem_toValuationSubring_of_mem_riemannRochSpace {K F : Type*} [Field K] [Field F]
  [Algebra K F]
    {A : Divisor K F} {g : F} (hg : g ∈ riemannRochSpace A) {w : Place K F} (hA : A w = 0) :
    g ∈ w.toValuationSubring
theorem

mem_riemannRochSpace_sub_jetDivisor_iff

L125 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.J2Sub.mem_riemannRochSpace_sub_jetDivisor_iff
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece1
open AlgebraicCurve
Lean source · statement
theorem J2Sub.mem_riemannRochSpace_sub_jetDivisor_iff {K F : Type*} [Field K] [Field F] [Algebra K
  F]
    {A : Divisor K F} {M : ℕ} {P : Fin M → Place K F} (hA : ∀ i, A (P i) = 0)
    {g : F} (hg : g ∈ riemannRochSpace A) :
    g ∈ riemannRochSpace (A - jetDivisor P) ↔ ∀ i, g = 0 ∨ (jetMult P (P i) : ℤ) ≤ (P i).ord g
theorem

taylorCoeff_zero_fun

L161 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.ProofAuxJ2.taylorCoeff_zero_fun
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece2
open AlgebraicCurve
namespace ProofAuxJ2
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem taylorCoeff_zero_fun (v : Place K F) (hv : v.IsRational) {t : F} (ht : v.ord t = 1) (r :
  ℕ) :
    Place.taylorCoeff v t r (0 : F) = 0
theorem

taylorCoeff_sum_smul

L167 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.ProofAuxJ2.taylorCoeff_sum_smul
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece2
open AlgebraicCurve
namespace ProofAuxJ2
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem taylorCoeff_sum_smul (v : Place K F) (hv : v.IsRational) {t : F} (ht : v.ord t = 1) (r : ℕ)
    {M : ℕ} (f : Fin M → F) (hf : ∀ j, f j ∈ v.toValuationSubring) (c : Fin M → K) :
    Place.taylorCoeff v t r (∑ j, c j • f j) = ∑ j, c j * Place.taylorCoeff v t r (f j)
theorem

mem_O

L192 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.ProofAuxJ2.mem_O
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece2
open AlgebraicCurve
namespace ProofAuxJ2
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Main
variable (A : Divisor K F) {M : ℕ} (f : Fin M → F)
  (P : Fin M → Place K F) (t : Fin M → F) (e : Fin M → ℕ)
Lean source · statement
theorem mem_O (hA : ∀ i, A (P i) = 0) {g : F} (hg : g ∈ riemannRochSpace A) (i : Fin M) :
    g ∈ (P i).toValuationSubring
theorem

jetMatrix_mulVec

L196 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.ProofAuxJ2.jetMatrix_mulVec
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece2
open AlgebraicCurve
namespace ProofAuxJ2
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Main
variable (A : Divisor K F) {M : ℕ} (f : Fin M → F)
  (P : Fin M → Place K F) (t : Fin M → F) (e : Fin M → ℕ)
Lean source · statement
theorem jetMatrix_mulVec (hfA : ∀ j, f j ∈ riemannRochSpace A)
    (hrat : ∀ i, (P i).IsRational) (ht : ∀ i, (P i).ord (t i) = 1) (hA : ∀ i, A (P i) = 0)
    (c : Fin M → K) (i : Fin M) :
    (jetMatrix P t e f).mulVec c i = Place.taylorCoeff (P i) (t i) (e i) (∑ j, c j • f j)
theorem

rows_vanish_iff

L205 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.ProofAuxJ2.rows_vanish_iff
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece2
open AlgebraicCurve
namespace ProofAuxJ2
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Main
variable (A : Divisor K F) {M : ℕ} (f : Fin M → F)
  (P : Fin M → Place K F) (t : Fin M → F) (e : Fin M → ℕ)
Lean source · statement
theorem rows_vanish_iff (hP : IsConfluentPattern P t e) (hrat : ∀ i, (P i).IsRational)
    (ht : ∀ i, (P i).ord (t i) = 1) (hA : ∀ i, A (P i) = 0) {g : F} (hg : g ∈ riemannRochSpace A) :
    (∀ i, Place.taylorCoeff (P i) (t i) (e i) g = 0) ↔ g ∈ riemannRochSpace (A - jetDivisor P)
theorem

main

L230 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR.ProofAuxJ2.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece2
open AlgebraicCurve
namespace ProofAuxJ2
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Main
variable (A : Divisor K F) {M : ℕ} (f : Fin M → F)
  (P : Fin M → Place K F) (t : Fin M → F) (e : Fin M → ℕ)
Lean source · statement
theorem main (hf : LinearIndependent K f) (hfA : ∀ j, f j ∈ riemannRochSpace A)
    (hP : IsConfluentPattern P t e) (hrat : ∀ i, (P i).IsRational)
    (ht : ∀ i, (P i).ord (t i) = 1) (hA : ∀ i, A (P i) = 0) :
    IsUnit (jetMatrix P t e f).det ↔
      Submodule.span K (Set.range f) ⊓ riemannRochSpace (A - jetDivisor P) = ⊥
theorem

isUnit_det_jetMatrix_iff_span_inf_riemannRochSpace_eq_bot

L278 ↗
AlgebraicCurve.isUnit_det_jetMatrix_iff_span_inf_riemannRochSpace_eq_bot
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.IsUnitDetJetMatrixIffSpanInfRR
section ProofAuxPiece2
open AlgebraicCurve
open AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.isUnit_det_jetMatrix_iff_span_inf_riemannRochSpace_eq_bot
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (A : Divisor K F) {M : ℕ} (f : Fin M → F) (hf : LinearIndependent K f)
    (hfA : ∀ j, f j ∈ riemannRochSpace A)
    (P : Fin M → Place K F) (t : Fin M → F) (e : Fin M → ℕ)
    (hP : IsConfluentPattern P t e) (hrat : ∀ i, (P i).IsRational)
    (ht : ∀ i, (P i).ord (t i) = 1) (hA : ∀ i, A (P i) = 0) :
    IsUnit (jetMatrix P t e f).det ↔
      Submodule.span K (Set.range f) ⊓ riemannRochSpace (A - jetDivisor P) = ⊥

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