NYLL
Module

WeilOfKaehler_omegaSpace_le_canonical.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.WeilOfKaehler_omegaSpace_le_canonical
11 declarations indexed from sourceView source ↗

Module documentation

Weil Of Kaehler omega Space le canonical

Imports1
Imported by1

Declarations

theorem

ord_nonneg_of_mem

L39 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem {f : F} (hf : f ∈
  v.toValuationSubring) : 0 ≤ v.ord f
theorem

kaehlerResidueTerm_single_of_ne

L57 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical.AlgebraicCurve.kaehlerResidueTerm_single_of_ne
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section SingleEval
variable [HasCanonicalLocalResidueKStar K F]
open scoped Classical in
Lean source · statement
theorem kaehlerResidueTerm_single_of_ne {ω : Ω[F⁄K]} {v : Place K F} {g : F}
    {w : Place K F} (hw : w ≠ v) :
    kaehlerResidueTerm ω (Pi.single v g) w = 0
theorem

weilOfKaehler_single_s6

L67 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical.AlgebraicCurve.weilOfKaehler_single_s6
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section SingleEval
variable [HasCanonicalLocalResidueKStar K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]
open scoped Classical in
Lean source · statement
theorem weilOfKaehler_single_s6 {ω : Ω[F⁄K]} (hω : ω ≠ 0) (v : Place K F) (g : F) :
    weilOfKaehler K F hω (adeleSingle v g)
      = Algebra.trace K v.ResidueField (v.localResidue (g * v.differentialCoeff ω))
theorem

localResidue_mul_uniformizer_inv

L87 ↗
AlgebraicCurve.Place.localResidue_mul_uniformizer_inv
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section SimplePoleProbe
variable [HasCanonicalLocalResidueKStar K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.localResidue_mul_uniformizer_inv (c :
  v.toValuationSubring) :
    v.localResidue ((c : F) * v.uniformizer⁻¹) = IsLocalRing.residue _ c
def

simplePoleProbe

L105 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical.AlgebraicCurve.simplePoleProbe
Documentation

A single-place adele probing the residue coefficient of the specified differential.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section SimplePoleProbe
variable [HasCanonicalLocalResidueKStar K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]
Lean source · statement
def simplePoleProbe {ω : Ω[F⁄K]} (_hω : ω ≠ 0) (v : Place K F)
    (c : v.toValuationSubring) : adeleSpace K F
theorem

weilOfKaehler_simplePoleProbe

L109 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical.AlgebraicCurve.weilOfKaehler_simplePoleProbe
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section SimplePoleProbe
variable [HasCanonicalLocalResidueKStar K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem weilOfKaehler_simplePoleProbe {ω : Ω[F⁄K]} (hω : ω ≠ 0) (v : Place K F)
    (c : v.toValuationSubring) :
    weilOfKaehler K F hω (simplePoleProbe hω v c)
      = Algebra.trace K v.ResidueField (IsLocalRing.residue _ c)
theorem

simplePoleProbe_mem_adeleBdd

L120 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical.AlgebraicCurve.simplePoleProbe_mem_adeleBdd
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section SimplePoleProbe
variable [HasCanonicalLocalResidueKStar K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]
open scoped Classical in
omit [HasCanonicalLocalResidueKStar K F] [Nontrivial Ω[F⁄K]] in
Lean source · statement
theorem simplePoleProbe_mem_adeleBdd {ω : Ω[F⁄K]} (hω : ω ≠ 0) (v : Place K F)
    (c : v.toValuationSubring) {D : Divisor K F} (hDv : canonicalDivisorOf hω v < D v) :
    (simplePoleProbe hω v c : Place K F → F) ∈ adeleBdd D
theorem

exists_trace_residue_ne_zero

L147 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical.AlgebraicCurve.Place.exists_trace_residue_ne_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem Place.exists_trace_residue_ne_zero [HasSeparableResidue K F] (v : Place K F) :
    ∃ c : v.toValuationSubring,
      Algebra.trace K v.ResidueField (IsLocalRing.residue _ c) ≠ 0
theorem

trace_residueField_eq_zero_of_weilOfKaehler_mem

L161 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical.AlgebraicCurve.trace_residueField_eq_zero_of_weilOfKaehler_mem
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Maximality
variable [HasCanonicalLocalResidueKStar K F] [HasCanonicalDivisor (K := K) (F := F)]
  [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem trace_residueField_eq_zero_of_weilOfKaehler_mem {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {D : Divisor K F} (hD : weilOfKaehler K F hω ∈ omegaSpace D)
    {v : Place K F} (hDv : canonicalDivisorOf hω v < D v) :
    (Algebra.trace K v.ResidueField : _ →ₗ[K] K) = 0
theorem

weilOfKaehler_omegaSpace_le_canonical_s6

L170 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical.AlgebraicCurve.weilOfKaehler_omegaSpace_le_canonical_s6
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Maximality
variable [HasCanonicalLocalResidueKStar K F] [HasCanonicalDivisor (K := K) (F := F)]
  [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem weilOfKaehler_omegaSpace_le_canonical_s6 [HasSeparableResidue K F]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) {D : Divisor K F}
    (hD : weilOfKaehler K F hω ∈ omegaSpace D) :
    D ≤ canonicalDivisorOf hω
theorem

weilOfKaehler_omegaSpace_le_canonical

L182 ↗
AlgebraicCurve.weilOfKaehler_omegaSpace_le_canonical
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.WeilOfKaehler_omegaSpace_le_canonical
noncomputable section
open _root_.IsDedekindDomain
open _root_.WithZero
open _root_.Module
open _root_.IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem _root_.AlgebraicCurve.weilOfKaehler_omegaSpace_le_canonical {K F : Type*} [Field K] [Field
  F] [Algebra K F] [HasCanonicalLocalResidueKStar K F] [HasCanonicalDivisor (K := K) (F := F)] [∀
  v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]] [HasSeparableResidue K F]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) {D : Divisor K F}
    (hD : weilOfKaehler K F hω ∈ omegaSpace D) :
    D ≤ canonicalDivisorOf hω

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