Module

Exists_ordDifferential_eq_neg_one_of_ne.lean

Nyll.AlgebraicCurves.Differentials.Exists_ordDifferential_eq_neg_one_of_ne

9 declarations indexed from sourceView source ↗

Module documentation

Exists ord Differential eq neg one of ne

Imports6

Imported by2

theorem

degree_eq_sum

L38 ↗

AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne.AlgebraicCurve.ThirdKind.degree_eq_sum

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ThirdKind
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · full declaration

theorem degree_eq_sum (D : Divisor K F) :
    Divisor.degree D = D.sum fun v n => n * (v.deg : ℤ) := by
  simp [Divisor.degree, Finsupp.liftAddHom_apply]

theorem

degree_nonneg_of_nonneg

L42 ↗

AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne.AlgebraicCurve.ThirdKind.degree_nonneg_of_nonneg

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ThirdKind
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem degree_nonneg_of_nonneg {D : Divisor K F} (hD : 0 ≤ D) : 0 ≤ Divisor.degree D

theorem

degree_nonneg_of_mem_lSpace

L47 ↗

AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne.AlgebraicCurve.ThirdKind.degree_nonneg_of_mem_lSpace

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ThirdKind
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem degree_nonneg_of_mem_lSpace [HasPrincipalDivisors K F] {D : Divisor K F} {f : F}
    (hf : f ∈ LSpace D) (hf0 : f ≠ 0) : 0 ≤ Divisor.degree D

theorem

lSpace_eq_bot_of_degree_neg

L58 ↗

AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne.AlgebraicCurve.ThirdKind.lSpace_eq_bot_of_degree_neg

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ThirdKind
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem lSpace_eq_bot_of_degree_neg [HasPrincipalDivisors K F] {D : Divisor K F}
    (hD : Divisor.degree D < 0) : LSpace D = ⊥

theorem

ell_eq_zero_of_degree_neg

L65 ↗

AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne.AlgebraicCurve.ThirdKind.ell_eq_zero_of_degree_neg

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ThirdKind
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ell_eq_zero_of_degree_neg [HasPrincipalDivisors K F] {D : Divisor K F}
    (hD : Divisor.degree D < 0) : ell D = 0

theorem

exists_mem_not_mem_not_mem

L69 ↗

AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne.AlgebraicCurve.ThirdKind.exists_mem_not_mem_not_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ThirdKind
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem exists_mem_not_mem_not_mem {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
    {A B C : Submodule R M} (hA : A < C) (hB : B < C) :
    ∃ x ∈ C, x ∉ A ∧ x ∉ B

theorem

differentialCoeff_ne_zero

L85 ↗

AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne.AlgebraicCurve.ThirdKind.differentialCoeff_ne_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ThirdKind
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem differentialCoeff_ne_zero (v : Place K F) [v.DCoordGenerates] {ω : Ω[F⁄K]}
    (hω : ω ≠ 0) : v.differentialCoeff ω ≠ 0

theorem

ordDifferential_smul_eq

L93 ↗

AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne.AlgebraicCurve.ThirdKind.ordDifferential_smul_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ThirdKind
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalDivisor (K := K) (F := F)]

Lean source · statement

theorem ordDifferential_smul_eq [∀ w : Place K F, w.DCoordGenerates] [Nontrivial (Ω[F⁄K])]
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) {h : F} (hh : h ≠ 0) (v : Place K F) :
    v.ordDifferential (h • ω₀) = v.ord h + canonicalDivisorOf hω₀ v

theorem

exists_ordDifferential_eq_neg_one_of_ne

L105 ↗

AlgebraicCurve.exists_ordDifferential_eq_neg_one_of_ne

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Exists_ordDifferential_eq_neg_one_of_ne
open KaehlerDifferential
open _root_.AlgebraicCurve
open AlgebraicCurve.ThirdKind

Lean source · statement

theorem _root_.AlgebraicCurve.exists_ordDifferential_eq_neg_one_of_ne {K F : Type*} [Field K]
  [Field F]
    [Algebra K F] [IsAlgClosed K] [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)]
    [∀ w : Place K F, w.DCoordGenerates] [Nontrivial (Ω[F⁄K])]
    (hRR : FunctionFieldRiemannRoch K F) {P Q : Place K F} (hPQ : P ≠ Q) :
    ∃ ω : Ω[F⁄K], ω ≠ 0 ∧ P.ordDifferential ω = -1 ∧ Q.ordDifferential ω = -1 ∧
      ∀ v : Place K F, v ≠ P → v ≠ Q → 0 ≤ v.ordDifferential ω

Module documentation

Exists ord Differential eq neg one of ne

Declarations