NYLL
Module

WeilReciprocity_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Geometry.WeilReciprocity_of_isAlgClosed
6 declarations indexed from sourceView source ↗

Module documentation

Weil Reciprocity of is Alg Closed

Imports20
Imported by4

Declarations

theorem

finsupp_prod_zpow_const

L58 ↗
AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed.WRpAux.finsupp_prod_zpow_const
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
namespace WRpAux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
theorem finsupp_prod_zpow_const {c : K} (hc : c ≠ 0) (D : Divisor K F) :
    (D.prod fun _ n => c ^ n) = c ^ (D.sum fun _ n => n) := by
  classical
  unfold Finsupp.prod Finsupp.sum
  induction D.support using Finset.cons_induction with
  | empty => simp
  | cons a s ha ih => rw [Finset.prod_cons, Finset.sum_cons, zpow_add₀ hc, ih]
theorem

degree_eq_sum_of_rational

L66 ↗
AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed.WRpAux.degree_eq_sum_of_rational
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
namespace WRpAux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
theorem degree_eq_sum_of_rational (D : Divisor K F)
    (hrat : ∀ v ∈ D.support, Place.IsRational v) :
    Divisor.degree D = D.sum fun _ n => n := by
  unfold Divisor.degree
  rw [Finsupp.liftAddHom_apply]
  refine Finsupp.sum_congr fun v hv => ?_
  rw [AddMonoidHom.mulRight_apply, (AlgebraicCurve.Place.isRational_iff_deg_eq_one v).1 (hrat v hv),
    Nat.cast_one, mul_one]
theorem

evalFun_nsmul

L75 ↗
AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed.WRpAux.evalFun_nsmul
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
namespace WRpAux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem evalFun_nsmul (f : F) (D : Divisor K F) (hD : ∀ v ∈ D.support, Place.evalAt v f ≠ 0) (n :
  ℕ) :
    Divisor.evalFun f (n • D) = Divisor.evalFun f D ^ n
theorem

evalFun_pow

L84 ↗
AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed.WRpAux.evalFun_pow
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
namespace WRpAux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem evalFun_pow (g : F) (D : Divisor K F) (hrat : ∀ v ∈ D.support, Place.IsRational v)
    (hg : ∀ v ∈ D.support, g ∈ v.toValuationSubring) (n : ℕ) :
    Divisor.evalFun (g ^ n) D = Divisor.evalFun g D ^ n
theorem

ratFuncAlgHom_fieldRange_eq_adjoin

L96 ↗
AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed.WRpAux.ratFuncAlgHom_fieldRange_eq_adjoin
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
namespace WRpAux
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ratFuncAlgHom_fieldRange_eq_adjoin (φ : RatFunc K →ₐ[K] F) :
    φ.fieldRange = IntermediateField.adjoin K ({φ RatFunc.X} : Set F)
theorem

weilReciprocity_of_isAlgClosed

L129 ↗
AlgebraicCurve.weilReciprocity_of_isAlgClosed
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.WeilReciprocity_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve
open WRpAux
Lean source · statement
theorem _root_.AlgebraicCurve.weilReciprocity_of_isAlgClosed (K F : Type*) [Field K] [IsAlgClosed
  K] [Field F] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
  [FiniteDimensional (RatFunc K) F] [HasPrincipalDivisors K F] : WeilReciprocity K F

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