Module

Place_mem_comap_iff_ord_nonneg.lean

Nyll.AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg

6 declarations indexed from sourceView source ↗

Module documentation

Place mem comap iff ord nonneg

Imports1

Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by2

theorem

ord_nonneg_of_mem

L39 ↗

AlgebraicCurve.Place.ord_nonneg_of_mem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem {f : F} (hf : f ∈
  v.toValuationSubring) : 0 ≤ v.ord f

theorem

mem_of_ord_nonneg

L56 ↗

AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
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_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord
  f) :
    f ∈ v.toValuationSubring

theorem

mem_iff_ord_nonneg

L66 ↗

AlgebraicCurve.Place.mem_iff_ord_nonneg

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section SinglePlace
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.mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

theorem

algebraMap_ne_zero

L83 ↗

AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg.AlgebraicCurve.Place.algebraMap_ne_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F'] [Algebra F F']

Lean source · statement

theorem algebraMap_ne_zero {f : F} (hf : f ≠ 0) : algebraMap F F' f ≠ 0

theorem

rowMain

L89 ↗

AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg.AlgebraicCurve.Place.rowMain

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Restrict
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F'] [Algebra F F']
variable (w : Place K F')
variable {w} in

Lean source · statement

theorem rowMain {f : F} (hf : f ≠ 0) :
    f ∈ w.toValuationSubring.comap (algebraMap F F') ↔
      0 ≤ w.ord (algebraMap F F' f)

theorem

mem_comap_iff_ord_nonneg

L105 ↗

AlgebraicCurve.Place.mem_comap_iff_ord_nonneg

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg
open IsDedekindDomain WithZero IsLocalRing
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Place_mem_comap_iff_ord_nonneg.AlgebraicCurve in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_comap_iff_ord_nonneg {K F F' : Type*} [Field K] [Field F]
  [Field F'] [Algebra K F'] [Algebra F F'] {w : Place K F'} {f : F} (hf : f ≠ 0) :
    f ∈ w.toValuationSubring.comap (algebraMap F F') ↔
      0 ≤ w.ord (algebraMap F F' f)

Module documentation

Place mem comap iff ord nonneg

Declarations

ord_nonneg_of_mem

mem_of_ord_nonneg

mem_iff_ord_nonneg

algebraMap_ne_zero

rowMain

mem_comap_iff_ord_nonneg