Module

RationalFunctionField_deg_eq_one_of_forall_ne_ofHeightOneSpectrum.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_deg_eq_one_of_forall_ne_ofHeightOneSpectrum

2 declarations indexed from sourceView source ↗

Module documentation

RationalFunctionField deg eq one of forall ne ofHeightOneSpectrum

A place of a rational function field outside the polynomial height-one spectrum has residue degree one.

Imports6

Mathlib.FieldTheory.RatFunc.Degree
Mathlib.FieldTheory.RatFunc.Valuation
Nyll.AlgebraicCurves.Divisors.ClassGroup
Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_toValuationSubring_eq_of_forall_ne_ofHeightOneSpectrum
Nyll.AlgebraicCurves.Places.Rational.Basic
Mathlib.FieldTheory.RatFunc.Basic

Imported by5

theorem

exists_sub_algebraMap_intDegree_neg

L56 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_deg_eq_one_of_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.RationalFunctionField.WFg.exists_sub_algebraMap_intDegree_neg

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_deg_eq_one_of_forall_ne_ofHeightOneSpectrum
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
open _root_.AlgebraicCurve
namespace WFg
variable (K : Type*) [Field K] [DecidableEq (RatFunc K)]

Lean source · statement

theorem exists_sub_algebraMap_intDegree_neg {x : RatFunc K}
    (hx : RatFunc.inftyValuation K x ≤ 1) :
    ∃ c : K, x - algebraMap K (RatFunc K) c = 0 ∨
      (x - algebraMap K (RatFunc K) c).intDegree < 0

theorem

deg_eq_one_of_forall_ne_ofHeightOneSpectrum

L111 ↗

AlgebraicCurve.RationalFunctionField.deg_eq_one_of_forall_ne_ofHeightOneSpectrum

Source context 8 commands