NYLL
Module

RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
12 declarations indexed from sourceView source ↗

Module documentation

RationalFunctionField exists forall ne ofHeightOneSpectrum

A rational function field has a place outside the places arising from polynomial height-one primes.

Imports5
Imported by5

Declarations

theorem

adicValuation_valuationSubring'

L46 ↗
AlgebraicCurve.Place.adicValuation_valuationSubring'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.adicValuation_valuationSubring' :
    v.adicValuation.valuationSubring = v.toValuationSubring
theorem

mem_iff_adicValuation_le_one'

L58 ↗
AlgebraicCurve.Place.mem_iff_adicValuation_le_one'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_iff_adicValuation_le_one' {f : F} :
    f ∈ v.toValuationSubring ↔ v.adicValuation f ≤ 1
theorem

adicValuation_isRankOneDiscrete'

L64 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.Place.adicValuation_isRankOneDiscrete'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem adicValuation_isRankOneDiscrete' : v.adicValuation.IsRankOneDiscrete
theorem

adicValuation_isTrivialOn'

L67 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.Place.adicValuation_isTrivialOn'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem adicValuation_isTrivialOn' : v.adicValuation.IsTrivialOn K
theorem

isEquiv_adicValuation_of_valuationSubring_eq'

L71 ↗
AlgebraicCurve.Place.isEquiv_adicValuation_of_valuationSubring_eq'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isEquiv_adicValuation_of_valuationSubring_eq' {Γ :
  Type*}
    [LinearOrderedCommGroupWithZero Γ] {w : Valuation F Γ}
    (h : w.valuationSubring = v.toValuationSubring) : w.IsEquiv v.adicValuation
theorem

ord_eq_zero_iff_adicValuation_eq_one'

L79 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.Place.ord_eq_zero_iff_adicValuation_eq_one'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_eq_zero_iff_adicValuation_eq_one' {f : F} (hf : f ≠ 0) :
    v.ord f = 0 ↔ v.adicValuation f = 1
theorem

isEquiv_adicValuation_ofHeightOneSpectrum'

L95 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.Place.isEquiv_adicValuation_ofHeightOneSpectrum'
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section OfHeightOneSpectrum
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
  [Algebra K R] [IsScalarTower K R F]
Lean source · statement
theorem isEquiv_adicValuation_ofHeightOneSpectrum' (w : HeightOneSpectrum R) :
    (w.valuation F).IsEquiv (ofHeightOneSpectrum (K := K) w).adicValuation
theorem

nontrivial_valueGroup_inftyValuation

L111 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.RationalFunctionField.nontrivial_valueGroup_inftyValuation
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section PlaceInfty
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem nontrivial_valueGroup_inftyValuation :
    Nontrivial (MonoidWithZeroHom.valueGroup (.ofClass (RatFunc.inftyValuation K)))
def

placeInfty'

L120 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.RationalFunctionField.placeInfty'
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section PlaceInfty
variable [DecidableEq (RatFunc K)]
Lean source · full declaration
def placeInfty' : Place K (RatFunc K) where
  toValuationSubring := (RatFunc.inftyValuation K).valuationSubring
  algebraMap_mem' a := by
    rw [Valuation.mem_valuationSubring_iff]
    exact Valuation.IsTrivialOn.valuation_algebraMap_le_one (v := RatFunc.inftyValuation K) a
  ne_top' := by
    have := nontrivial_valueGroup_inftyValuation K
    simp only [ne_eq, Valuation.valuationSubring_eq_top_iff, not_not]
    infer_instance
  isPrincipalIdealRing' :=
    haveI := nontrivial_valueGroup_inftyValuation K
    (Valuation.valuationSubring_isDiscreteValuationRing
      (RatFunc.inftyValuation K)).toIsPrincipalIdealRing
theorem

placeInfty'_ne_ofHeightOneSpectrum

L134 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.RationalFunctionField.placeInfty'_ne_ofHeightOneSpectrum
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section PlaceInfty
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem placeInfty'_ne_ofHeightOneSpectrum (w : HeightOneSpectrum K[X]) :
    placeInfty' K ≠ Place.ofHeightOneSpectrum w
theorem

rowMain

L147 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.RationalFunctionField.rowMain
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
Lean source · statement
theorem rowMain :
    ∃ v : Place K (RatFunc K), ∀ w : HeightOneSpectrum K[X], v ≠ Place.ofHeightOneSpectrum w
theorem

exists_forall_ne_ofHeightOneSpectrum

L164 ↗
AlgebraicCurve.RationalFunctionField.exists_forall_ne_ofHeightOneSpectrum
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
open _root_.AlgebraicCurve in
with_weak_namespace _root_.AlgebraicCurves.Places.Rational.Proofs
open
  RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum.AlgebraicCurve
in
with_weak_namespace RationalFunctionField_exists_forall_ne_ofHeightOneSpectrum
Lean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.exists_forall_ne_ofHeightOneSpectrum {K :
  Type*} [Field K] :
    ∃ v : Place K (RatFunc K), ∀ w : IsDedekindDomain.HeightOneSpectrum (Polynomial K),
      v ≠ Place.ofHeightOneSpectrum w

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