NYLL
Module

Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials.lean

Nyll.AlgebraicCurves.Differentials.Residues.Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials
6 declarations indexed from sourceView source ↗

Module documentation

Sum eq zero of forall has Simple Residue of mem polar Differentials

Imports15
Imported by3

Declarations

theorem

residueTheoremK

L68 ↗
AlgebraicCurves.Differentials.Residues.Proofs.Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials.AlgebraicCurve.ResThm.residueTheoremK
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open KaehlerDifferential IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResThm
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable [IsAlgClosed K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
Lean source · statement
theorem residueTheoremK : ResidueTheoremK K F
theorem

trace_res_differentialCoeff_of_hasSimpleResidue

L101 ↗
AlgebraicCurves.Differentials.Residues.Proofs.Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials.AlgebraicCurve.ResThm.trace_res_differentialCoeff_of_hasSimpleResidue
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open KaehlerDifferential IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResThm
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable [IsAlgClosed K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
variable {K F}
omit [Algebra.EssFiniteType K F] [HasCanonicalDivisor (K := K) (F := F)] in
Lean source · statement
theorem trace_res_differentialCoeff_of_hasSimpleResidue {v : Place K F} {ω : Ω[F⁄K]} {a : K}
    (h : v.HasSimpleResidue ω a) :
    Algebra.trace K v.ResidueField
        ((HasCanonicalLocalResidueKStar.dataKStar v).res (v.differentialCoeff ω)) = a
theorem

res_differentialCoeff_eq_zero_of_isRegularAt

L111 ↗
AlgebraicCurves.Differentials.Residues.Proofs.Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials.AlgebraicCurve.ResThm.res_differentialCoeff_eq_zero_of_isRegularAt
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open KaehlerDifferential IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResThm
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable [IsAlgClosed K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
variable {K F}
omit [Algebra.EssFiniteType K F] [HasCanonicalDivisor (K := K) (F := F)] in
Lean source · statement
theorem res_differentialCoeff_eq_zero_of_isRegularAt {v : Place K F} {ω : Ω[F⁄K]}
    (h : v.IsRegularAt ω) :
    (HasCanonicalLocalResidueKStar.dataKStar v).res (v.differentialCoeff ω) = 0
theorem

eq_zero_of_hasSimpleResidue_zero

L118 ↗
AlgebraicCurves.Differentials.Residues.Proofs.Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials.AlgebraicCurve.ResThm.eq_zero_of_hasSimpleResidue_zero
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open KaehlerDifferential IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResThm
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable [IsAlgClosed K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
variable {K F}
omit [Algebra.EssFiniteType K F] [HasCanonicalDivisor (K := K) (F := F)] in
Lean source · statement
theorem eq_zero_of_hasSimpleResidue_zero {v : Place K F} {a : K} (h : v.HasSimpleResidue (0 :
  Ω[F⁄K]) a) :
    a = 0
theorem

main

L125 ↗
AlgebraicCurves.Differentials.Residues.Proofs.Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials.AlgebraicCurve.ResThm.main
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
noncomputable section
open KaehlerDifferential IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace ResThm
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
variable [IsAlgClosed K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
  [HasCanonicalDivisor (K := K) (F := F)] [∀ v : Place K F, v.DCoordGenerates]
variable {K F}
Lean source · statement
theorem main (S : Finset (Place K F)) (ω : Ω[F⁄K])
    (hω : ω ∈ polarDifferentials K F (S : Set (Place K F)))
    (a : Place K F → K) (ha : ∀ v ∈ S, v.HasSimpleResidue ω (a v)) :
    ∑ v ∈ S, a v = 0
theorem

sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials

L163 ↗
AlgebraicCurve.sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Residues.Proofs
namespace Sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
Lean source · statement
theorem _root_.AlgebraicCurve.sum_eq_zero_of_forall_hasSimpleResidue_of_mem_polarDifferentials
    {K F : Type*} [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [Algebra.EssFiniteType K F]
    [AlgebraicCurve.IsCurveOver K F] [AlgebraicCurve.HasCanonicalDivisor (K := K) (F := F)]
    (S : Finset (AlgebraicCurve.Place K F)) (ω : Ω[F⁄K])
    (hω : ω ∈ AlgebraicCurve.polarDifferentials K F (S : Set (AlgebraicCurve.Place K F)))
    (a : AlgebraicCurve.Place K F → K) (ha : ∀ v ∈ S, v.HasSimpleResidue ω (a v)) :
    ∑ v ∈ S, a v = 0

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