NYLL
Module

RationalFunctionField_subsingleton_setOf_forall_ne_ofHeightOneSpectrum.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_subsingleton_setOf_forall_ne_ofHeightOneSpectrum
13 declarations indexed from sourceView source ↗

Module documentation

RationalFunctionField subsingleton setOf forall ne ofHeightOneSpectrum

The places of a rational function field outside the polynomial height-one spectrum form a subsingleton.

Imports5
Imported by13

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_subsingleton_setOf_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_subsingleton_setOf_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 ↗
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_subsingleton_setOf_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.adicValuation_isRankOneDiscrete' :
  v.adicValuation.IsRankOneDiscrete
theorem

adicValuation_isTrivialOn'

L69 ↗
AlgebraicCurve.Place.adicValuation_isTrivialOn'
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_subsingleton_setOf_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 _root_.AlgebraicCurve.Place.adicValuation_isTrivialOn' :
  v.adicValuation.IsTrivialOn K
theorem

isEquiv_adicValuation_of_valuationSubring_eq'

L75 ↗
AlgebraicCurve.Place.isEquiv_adicValuation_of_valuationSubring_eq'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_subsingleton_setOf_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
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'

L83 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_subsingleton_setOf_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.Place.ord_eq_zero_iff_adicValuation_eq_one'
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_subsingleton_setOf_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
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'

L99 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_subsingleton_setOf_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.Place.isEquiv_adicValuation_ofHeightOneSpectrum'
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_subsingleton_setOf_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
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

L115 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_subsingleton_setOf_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_subsingleton_setOf_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'

L124 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_subsingleton_setOf_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_subsingleton_setOf_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

L138 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_subsingleton_setOf_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_subsingleton_setOf_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

eq_ofHeightOneSpectrum_or_eq_placeInfty'

L151 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_subsingleton_setOf_forall_ne_ofHeightOneSpectrum.AlgebraicCurve.RationalFunctionField.eq_ofHeightOneSpectrum_or_eq_placeInfty'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_subsingleton_setOf_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 eq_ofHeightOneSpectrum_or_eq_placeInfty' [DecidableEq (RatFunc K)]
    (v : Place K (RatFunc K)) :
    (∃ w : HeightOneSpectrum K[X], v = Place.ofHeightOneSpectrum w) ∨ v = placeInfty' K
theorem

rowMain

L163 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_subsingleton_setOf_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_subsingleton_setOf_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}.Subsingleton
theorem

subsingleton_setOf_forall_ne_ofHeightOneSpectrum

L186 ↗
AlgebraicCurve.RationalFunctionField.subsingleton_setOf_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_subsingleton_setOf_forall_ne_ofHeightOneSpectrum
open _root_.AlgebraicCurve in
with_weak_namespace _root_.AlgebraicCurves.Places.Rational.Proofs
open
  RationalFunctionField_subsingleton_setOf_forall_ne_ofHeightOneSpectrum.AlgebraicCurve
in
with_weak_namespace RationalFunctionField_subsingleton_setOf_forall_ne_ofHeightOneSpectrum
Lean source · statement
theorem
  _root_.AlgebraicCurve.RationalFunctionField.subsingleton_setOf_forall_ne_ofHeightOneSpectrum
  {K : Type*} [Field K] :
    {v : Place K (RatFunc K) | ∀ w : IsDedekindDomain.HeightOneSpectrum (Polynomial K),
      v ≠ Place.ofHeightOneSpectrum w}.Subsingleton

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