NYLL
Module

WeilKaehlerAgree_of_residueTheorem.lean

Nyll.AlgebraicCurves.Differentials.Residues.WeilKaehlerAgree_of_residueTheorem
15 declarations indexed from sourceView source ↗

Module documentation

Weil Kaehler Agree of residue Theorem

Imports2
Imported by1

Declarations

theorem

ord_nonneg_of_mem

L40 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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

L58 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.AlgebraicCurve.kaehlerResidueTerm_single_of_ne
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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

L68 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.AlgebraicCurve.weilOfKaehler_single_s6
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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

L88 ↗
AlgebraicCurve.Place.localResidue_mul_uniformizer_inv
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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

L106 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.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.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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

L110 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.AlgebraicCurve.weilOfKaehler_simplePoleProbe
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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

L121 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.AlgebraicCurve.simplePoleProbe_mem_adeleBdd
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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

L149 ↗
AlgebraicCurve.Place.exists_trace_residue_ne_zero
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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 scoped _root_.AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.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

weilOfKaehler_ne_zero_s6

L167 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.AlgebraicCurve.weilOfKaehler_ne_zero_s6
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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 _root_.AlgebraicCurve
section Nonvanishing
variable [HasCanonicalLocalResidueKStar K F] [HasCanonicalDivisor (K := K) (F := F)]
  [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem weilOfKaehler_ne_zero_s6 [HasSeparableResidue K F] [Nonempty (Place K F)]
    {ω : Ω[F⁄K]} (hω : ω ≠ 0) : weilOfKaehler K F hω ≠ 0
theorem

trace_residueField_eq_zero_of_weilOfKaehler_mem

L182 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.AlgebraicCurve.trace_residueField_eq_zero_of_weilOfKaehler_mem
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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 _root_.AlgebraicCurve
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

L191 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.AlgebraicCurve.weilOfKaehler_omegaSpace_le_canonical_s6
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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 _root_.AlgebraicCurve
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

weilKaehlerAgree_of_residueTheorem_s6

L208 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.AlgebraicCurve.weilKaehlerAgree_of_residueTheorem_s6
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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 _root_.AlgebraicCurve
section Discharge
variable [HasCanonicalLocalResidueKStar K F] [HasCanonicalDivisor (K := K) (F := F)]
  [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem weilKaehlerAgree_of_residueTheorem_s6 [HasSeparableResidue K F] [Nonempty (Place K F)]
    (hRT : ∀ [HasPrincipalDivisors K F], ResidueTheorem K F) : WeilKaehlerAgree K F
theorem

gate_weilKaehlerAgree_recovers_adeleBdd_vanish

L215 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.AlgebraicCurve.gate_weilKaehlerAgree_recovers_adeleBdd_vanish
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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 _root_.AlgebraicCurve
section Discharge
variable [HasCanonicalLocalResidueKStar K F] [HasCanonicalDivisor (K := K) (F := F)]
  [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem gate_weilKaehlerAgree_recovers_adeleBdd_vanish [HasSeparableResidue K F]
    [Nonempty (Place K F)] [HasPrincipalDivisors K F]
    (hRT : ResidueTheorem K F) {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : adeleSpace K F} (hα : (α : Place K F → F) ∈ adeleBdd (canonicalDivisorOf hω)) :
    weilOfKaehler K F hω α = 0
theorem

gate_canonicalDivisor_maximal_fixedPoint

L222 ↗
AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem.AlgebraicCurve.gate_canonicalDivisor_maximal_fixedPoint
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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 _root_.AlgebraicCurve
section Discharge
variable [HasCanonicalLocalResidueKStar K F] [HasCanonicalDivisor (K := K) (F := F)]
  [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
Lean source · statement
theorem gate_canonicalDivisor_maximal_fixedPoint [HasSeparableResidue K F]
    [Nonempty (Place K F)] [HasPrincipalDivisors K F]
    (hRT : ResidueTheorem K F) {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
    weilOfKaehler K F hω ∈ omegaSpace (canonicalDivisorOf hω) ∧
      ∀ D, weilOfKaehler K F hω ∈ omegaSpace D → D ≤ canonicalDivisorOf hω
theorem

weilKaehlerAgree_of_residueTheorem

L231 ↗
AlgebraicCurve.weilKaehlerAgree_of_residueTheorem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs.WeilKaehlerAgree_of_residueTheorem
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 _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.weilKaehlerAgree_of_residueTheorem {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] [Nonempty (Place K F)]
    (hRT : ∀ [HasPrincipalDivisors K F], ResidueTheorem K F) : WeilKaehlerAgree K F

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