AlgebraicCurve.weilReciprocity_algebraMap
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.WeilReciprocity_algebraMap
attribute [-instance]
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.weilReciprocity_algebraMap {K F F' : Type*} [Field K] [Field F]
[Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F'] [FiniteDimensional
F F'] [Algebra.IsSeparable F F'] [CharZero F] [HasPrincipalDivisors K F] [HasPrincipalDivisors K
F'] (hbase : WeilReciprocity K F) {f : F'} {g : F} (hf : f ≠ 0) (hg : g ≠ 0) (Df Dg : Divisor K
F') (hDf : ∀ w : Place K F', Df w = w.ord f) (hDg : ∀ w : Place K F', Dg w = w.ord (algebraMap F
F' g)) (hdisj : ∀ w : Place K F', w.ord f = 0 ∨ w.ord (algebraMap F F' g) = 0) (hratf : ∀ w ∈
Df.support, Place.IsRational w) (hratF : ∀ v : Place K F, v.IsRational) (hratfib : ∀ v : Place K
F, v.ord g ≠ 0 → ∀ w ∈ v.fiber F', Place.IsRational w) : Divisor.evalFun f Dg = Divisor.evalFun
(algebraMap F F' g) Df