NYLL
Module

Eq_zero_or_exists_eq_weilOfKaehler_smul_of_mem_omegaSpace.lean

Nyll.AlgebraicCurves.Cohomology.RiemannRoch.Eq_zero_or_exists_eq_weilOfKaehler_smul_of_mem_omegaSpace
4 declarations indexed from sourceView source ↗

Module documentation

Eq zero or exists eq weil Of Kaehler smul of mem omega Space

Imports4
Imported by1

Declarations

theorem

kaehlerResidueTerm_smulF_left

L50 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.EqZeroOrExistsWeilOfKaehlerSmul.ModularCurve.OmegaSide.A.kaehlerResidueTerm_smulF_left
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.EqZeroOrExistsWeilOfKaehlerSmul
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
namespace ModularCurve
namespace OmegaSide
namespace A
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem kaehlerResidueTerm_smulF_left [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
    [HasCanonicalLocalResidueKStar K F]
    (f : F) (ω : Ω[F⁄K]) (α : Place K F → F) (v : Place K F) :
    kaehlerResidueTerm (f • ω) α v = kaehlerResidueTerm ω (mulAdele K f α) v
theorem

weilOfKaehler_smulF

L58 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.EqZeroOrExistsWeilOfKaehlerSmul.ModularCurve.OmegaSide.A.weilOfKaehler_smulF
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.EqZeroOrExistsWeilOfKaehlerSmul
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
namespace ModularCurve
namespace OmegaSide
namespace A
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem weilOfKaehler_smulF [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
    [HasCanonicalLocalResidueKStar K F] [HasPrincipalDivisors K F] [HasCanonicalDivisor (K := K)
      (F := F)]
    {f : F} {ω : Ω[F⁄K]} (hω : ω ≠ 0) (hf : f ≠ 0) :
    weilOfKaehler K F (ω := f • ω) (smul_ne_zero hf hω) = weilSmul K F f (weilOfKaehler K F hω)
theorem

eq_zero_or_exists_eq_weilOfKaehler_smul'

L70 ↗
AlgebraicCurves.Cohomology.RiemannRoch.Proofs.EqZeroOrExistsWeilOfKaehlerSmul.ModularCurve.OmegaSide.A.eq_zero_or_exists_eq_weilOfKaehler_smul'
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.EqZeroOrExistsWeilOfKaehlerSmul
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
namespace ModularCurve
namespace OmegaSide
namespace A
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem eq_zero_or_exists_eq_weilOfKaehler_smul'
    [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)] [Nonempty (Place K F)]
    [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]] [HasCanonicalLocalResidueKStar K F]
    (hRI : RiemannIndexFormula K F) (hagree : WeilKaehlerAgree K F)
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (D : Divisor K F)
    (μ : Module.Dual K (adeleSpace K F)) (hμ : μ ∈ omegaSpace (K := K) (F := F) D) :
    μ = 0 ∨ ∃ (f : F) (hf : f ≠ 0), μ = weilOfKaehler K F (ω := f • ω₀) (smul_ne_zero hf hω₀)
theorem

eq_zero_or_exists_eq_weilOfKaehler_smul_of_mem_omegaSpace

L98 ↗
AlgebraicCurve.eq_zero_or_exists_eq_weilOfKaehler_smul_of_mem_omegaSpace
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.EqZeroOrExistsWeilOfKaehlerSmul
attribute [-instance]
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
  AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
  AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open ModularCurve.OmegaSide.A in
Lean source · statement
theorem _root_.AlgebraicCurve.eq_zero_or_exists_eq_weilOfKaehler_smul_of_mem_omegaSpace
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    [IsCurveOver K F] [HasCanonicalDivisor (K := K) (F := F)] [Nonempty (Place K F)]
    [∀ v : Place K F, v.DCoordGenerates] [Nontrivial Ω[F⁄K]] [HasCanonicalLocalResidueKStar K F]
    (hRI : RiemannIndexFormula K F) (hagree : WeilKaehlerAgree K F)
    {ω₀ : Ω[F⁄K]} (hω₀ : ω₀ ≠ 0) (D : Divisor K F)
    (μ : Module.Dual K (adeleSpace K F)) (hμ : μ ∈ omegaSpace (K := K) (F := F) D) :
    μ = 0 ∨ ∃ (f : F) (hf : f ≠ 0), μ = weilOfKaehler K F (ω := f • ω₀) (smul_ne_zero hf hω₀)

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