NYLL
Module

RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap
7 declarations indexed from sourceView source ↗

Module documentation

RationalFunctionField degree eq zero of forall eq ord algebraMap

The orders of a rational function after an algebraic field embedding form a divisor of degree zero.

Imports10
Imported by3

Declarations

def

heightOneSpectrumOfIrreducible

L62 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap.AlgebraicCurve.RationalFunctionField.WFj.heightOneSpectrumOfIrreducible
Documentation

The height-one polynomial prime generated by the irreducible polynomial.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] 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 _root_.AlgebraicCurve
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField hiding finitePlace
  heightOneSpectrumOfIrreducible_asIdeal heightOneSpectrumOfIrreducible
open _root_.AlgebraicCurve
namespace WFj
variable (K : Type*) [Field K]
Lean source · full declaration
def heightOneSpectrumOfIrreducible {p : K[X]} (hp : Irreducible p) :
    HeightOneSpectrum K[X] where
  asIdeal := Ideal.span {p}
  isPrime := (PrincipalIdealRing.isMaximal_of_irreducible hp).isPrime
  ne_bot := by simpa [Ideal.span_singleton_eq_bot] using hp.ne_zero
theorem

heightOneSpectrumOfIrreducible_asIdeal

L68 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap.AlgebraicCurve.RationalFunctionField.WFj.heightOneSpectrumOfIrreducible_asIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] 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 _root_.AlgebraicCurve
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField hiding finitePlace
  heightOneSpectrumOfIrreducible_asIdeal heightOneSpectrumOfIrreducible
open _root_.AlgebraicCurve
namespace WFj
variable (K : Type*) [Field K]
Lean source · statement
theorem heightOneSpectrumOfIrreducible_asIdeal {p : K[X]} (hp : Irreducible p) :
    (heightOneSpectrumOfIrreducible K hp).asIdeal = Ideal.span {p}
def

finitePlace

L72 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap.AlgebraicCurve.RationalFunctionField.WFj.finitePlace
Documentation

The finite rational-function-field place associated to the irreducible polynomial.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] 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 _root_.AlgebraicCurve
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField hiding finitePlace
  heightOneSpectrumOfIrreducible_asIdeal heightOneSpectrumOfIrreducible
open _root_.AlgebraicCurve
namespace WFj
variable (K : Type*) [Field K]
Lean source · statement
def finitePlace {p : K[X]} (hp : Irreducible p) : Place K (RatFunc K)
theorem

ne_finitePlace_of_forall_ne

L77 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap.AlgebraicCurve.RationalFunctionField.WFj.ne_finitePlace_of_forall_ne
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] 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 _root_.AlgebraicCurve
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField hiding finitePlace
  heightOneSpectrumOfIrreducible_asIdeal heightOneSpectrumOfIrreducible
open _root_.AlgebraicCurve
namespace WFj
variable (K : Type*) [Field K]
variable {K}
Lean source · statement
theorem ne_finitePlace_of_forall_ne {v : Place K (RatFunc K)}
    (hv : ∀ w : HeightOneSpectrum K[X], v ≠ Place.ofHeightOneSpectrum w) {p : K[X]} (hp :
      Irreducible p) :
    v ≠ finitePlace K hp
theorem

single_add_single_apply_eq_ord

L83 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap.AlgebraicCurve.RationalFunctionField.WFj.single_add_single_apply_eq_ord
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] 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 _root_.AlgebraicCurve
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField hiding finitePlace
  heightOneSpectrumOfIrreducible_asIdeal heightOneSpectrumOfIrreducible
open _root_.AlgebraicCurve
namespace WFj
variable (K : Type*) [Field K]
variable {K}
Lean source · statement
theorem single_add_single_apply_eq_ord {vinf : Place K (RatFunc K)}
    (hvinf : ∀ w : HeightOneSpectrum K[X], vinf ≠ Place.ofHeightOneSpectrum w)
    {p : K[X]} (hp : Irreducible p) (v : Place K (RatFunc K)) :
    (Finsupp.single (finitePlace K hp) (1 : ℤ)
        + Finsupp.single vinf (-(p.natDegree : ℤ))) v
      = v.ord (algebraMap K[X] (RatFunc K) p)
theorem

degree_single_add_single

L122 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap.AlgebraicCurve.RationalFunctionField.WFj.degree_single_add_single
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] 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 _root_.AlgebraicCurve
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField hiding finitePlace
  heightOneSpectrumOfIrreducible_asIdeal heightOneSpectrumOfIrreducible
open _root_.AlgebraicCurve
namespace WFj
variable (K : Type*) [Field K]
variable {K}
Lean source · statement
theorem degree_single_add_single {vinf : Place K (RatFunc K)}
    (hvinf : ∀ w : HeightOneSpectrum K[X], vinf ≠ Place.ofHeightOneSpectrum w)
    {p : K[X]} (hp : Irreducible p) :
    Divisor.degree (Finsupp.single (finitePlace K hp) (1 : ℤ)
        + Finsupp.single vinf (-(p.natDegree : ℤ))) = 0
theorem

degree_eq_zero_of_forall_eq_ord_algebraMap

L140 ↗
AlgebraicCurve.RationalFunctionField.degree_eq_zero_of_forall_eq_ord_algebraMap
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_degree_eq_zero_of_forall_eq_ord_algebraMap
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] 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 _root_.AlgebraicCurve
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
Lean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.degree_eq_zero_of_forall_eq_ord_algebraMap
  {K : Type*} [Field K] (q : Polynomial K) : ∀ D : Divisor K (RatFunc K), (∀ v : Place K
  (RatFunc K), D v = v.ord (algebraMap (Polynomial K) (RatFunc K) q)) → Divisor.degree D = 0

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