Module

Weil.lean

Nyll.AlgebraicCurves.Differentials.Kaehler.Weil

10 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

Residue functionals of nonzero Kähler differentials, their canonical-divisor bounds, and the associated residue pairing.

Imports1

Nyll.AlgebraicCurves.Differentials.Residues.Basic

Imported by29

theorem

kaehlerResidueTerm_eq_zero_of_adeleBdd_canonical

L32 ↗

AlgebraicCurve.kaehlerResidueTerm_eq_zero_of_adeleBdd_canonical

Source context 5 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]

Lean source · statement

theorem kaehlerResidueTerm_eq_zero_of_adeleBdd_canonical
    [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : Place K F → F} (hα : α ∈ adeleBdd (canonicalDivisorOf hω)) (v : Place K F) :
    kaehlerResidueTerm ω α v = 0

theorem

kaehlerResidueTerm_support_subset

L50 ↗

AlgebraicCurve.kaehlerResidueTerm_support_subset

Source context 5 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]

Lean source · statement

theorem kaehlerResidueTerm_support_subset
    [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {D : Divisor K F} {α : Place K F → F} (hα : α ∈ adeleBdd D) :
    Function.support (kaehlerResidueTerm ω α) ⊆ ↑(D - canonicalDivisorOf hω).support

theorem

kaehlerResidueTerm_support_finite

L72 ↗

AlgebraicCurve.kaehlerResidueTerm_support_finite

Source context 5 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]

Lean source · statement

theorem kaehlerResidueTerm_support_finite
    [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {D : Divisor K F} {α : Place K F → F} (hα : α ∈ adeleBdd D) :
    (Function.support (kaehlerResidueTerm ω α)).Finite

theorem

kaehlerResidueTerm_support_finite_of_adeleSpace

L79 ↗

AlgebraicCurve.kaehlerResidueTerm_support_finite_of_adeleSpace

Source context 5 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]

Lean source · statement

theorem kaehlerResidueTerm_support_finite_of_adeleSpace
    [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
    [Nontrivial Ω[F⁄K]] {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : Place K F → F} (hα : α ∈ adeleSpace K F) :
    (Function.support (kaehlerResidueTerm ω α)).Finite

def

weilOfKaehler

L93 ↗

AlgebraicCurve.weilOfKaehler

Documentation

The adele linear functional obtained by summing the traced residues of a nonzero differential.

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]
variable (K F) in

Lean source · full declaration

def weilOfKaehler {ω : Ω[F⁄K]} (hω : ω ≠ 0) : Module.Dual K (adeleSpace K F) where
  toFun α := ∑ᶠ v, kaehlerResidueTerm ω (α : Place K F → F) v
  map_add' α β := by
    have hsupα := kaehlerResidueTerm_support_finite_of_adeleSpace hω α.2
    have hsupβ := kaehlerResidueTerm_support_finite_of_adeleSpace hω β.2
    rw [← finsum_add_distrib hsupα hsupβ]
    refine finsum_congr fun v => ?_
    unfold kaehlerResidueTerm
    rw [Submodule.coe_add, Pi.add_apply, add_mul, map_add, map_add]
  map_smul' c α := by
    simp only [RingHom.id_apply]
    rw [smul_finsum]
    refine finsum_congr fun v => ?_
    unfold kaehlerResidueTerm
    rw [Submodule.coe_smul, Pi.smul_apply, Algebra.smul_def, mul_assoc,
      ← Algebra.smul_def, map_smul, map_smul]

theorem

weilOfKaehler_apply

L110 ↗

AlgebraicCurve.weilOfKaehler_apply

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]
variable (K F) in

Lean source · statement

theorem weilOfKaehler_apply {ω : Ω[F⁄K]} (hω : ω ≠ 0) (α : adeleSpace K F) :
    weilOfKaehler K F hω α = ∑ᶠ v, kaehlerResidueTerm ω (α : Place K F → F) v

theorem

weilOfKaehler_vanish_adeleBdd_canonical

L113 ↗

AlgebraicCurve.weilOfKaehler_vanish_adeleBdd_canonical

Source context 7 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]
variable (K F) in

Lean source · statement

theorem weilOfKaehler_vanish_adeleBdd_canonical {ω : Ω[F⁄K]} (hω : ω ≠ 0)
    {α : adeleSpace K F} (hα : (α : Place K F → F) ∈ adeleBdd (canonicalDivisorOf hω)) :
    weilOfKaehler K F hω α = 0

def

ResidueTheorem

L123 ↗

AlgebraicCurve.ResidueTheorem

Documentation

The residue functional of every nonzero differential vanishes on diagonal functions.

Source context 8 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]
variable (K F) in
variable (K F)

Lean source · statement

def ResidueTheorem [HasPrincipalDivisors K F] : Prop

def

WeilKaehlerAgree

L133 ↗

AlgebraicCurve.WeilKaehlerAgree

Documentation

A nonzero differential gives a nonzero residue functional with its canonical divisor as maximal bounding divisor.

Source context 10 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]
variable (K F) in
variable (K F)
variable {K F}
variable (K F)

Lean source · statement

def WeilKaehlerAgree : Prop

def

ResiduePairingSurjective

L145 ↗

AlgebraicCurve.ResiduePairingSurjective

Documentation

The residue pairing is surjective for a nonzero functional with a maximal bounding divisor.

Source context 12 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable [HasCanonicalLocalResidueKStar K F]
variable [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
  [Nontrivial Ω[F⁄K]]
variable (K F) in
variable (K F)
variable {K F}
variable (K F)
variable {K F}
variable (K F)

Lean source · statement

def ResiduePairingSurjective : Prop

Module documentation

Differentials, residues, and divisor correspondences

Declarations