NYLL
Module

Place_exists_toValuationSubring_eq_comap_of_ne_top.lean

Nyll.AlgebraicCurves.Places.Place_exists_toValuationSubring_eq_comap_of_ne_top
17 declarations indexed from sourceView source ↗

Module documentation

Place exists to Valuation Subring eq comap of ne top

Imports1
Imported by4

Declarations

theorem

ord_nonneg_of_mem

L37 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem
Source context 11 commands

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

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

L55 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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 13 commands

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

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

exists_ord_pos

L72 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top.AlgebraicCurve.Place.exists_ord_pos
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem exists_ord_pos : ∃ f : F, f ≠ 0 ∧ 0 < v.ord f
theorem

algebraMap_ne_zero

L86 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top.AlgebraicCurve.Place.algebraMap_ne_zero
Source context 11 commands

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

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

mem_comap_iff_ord_nonneg

L92 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top.AlgebraicCurve.Place.mem_comap_iff_ord_nonneg
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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 mem_comap_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ w.toValuationSubring.comap (algebraMap F F') ↔
      0 ≤ w.ord (algebraMap F F' f)
theorem

isUnit_mk_comap_iff

L99 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top.AlgebraicCurve.Place.isUnit_mk_comap_iff
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
variable {w} in
Lean source · statement
theorem isUnit_mk_comap_iff {f : F} (hf : f ≠ 0)
    (hmem : f ∈ w.toValuationSubring.comap (algebraMap F F')) :
    IsUnit (⟨f, hmem⟩ : w.toValuationSubring.comap (algebraMap F F')) ↔
      w.ord (algebraMap F F' f) = 0
theorem

exists_ord_algebraMap_pos

L124 ↗
AlgebraicCurve.Place.exists_ord_algebraMap_pos
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
variable {w} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_ord_algebraMap_pos (hne :
  w.toValuationSubring.comap (algebraMap F F') ≠ ⊤) :
    ∃ f : F, f ≠ 0 ∧ 0 < w.ord (algebraMap F F' f)
def

comapRamIdx

L142 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top.AlgebraicCurve.Place.comapRamIdx
Documentation

The least positive order attained by a nonzero element of the subfield, when one exists.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
variable {w} in
open _root_.AlgebraicCurve.Place
Lean source · statement
def comapRamIdx (F : Type*) [Field F] [Algebra F F'] : ℕ
theorem

comapRamIdx_le_ord

L145 ↗
AlgebraicCurve.Place.comapRamIdx_le_ord
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
variable {w} in
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.comapRamIdx_le_ord {f : F} (hf : f ≠ 0)
    (hpos : 0 < w.ord (algebraMap F F' f)) :
    (comapRamIdx (F := F) w : ℤ) ≤ w.ord (algebraMap F F' f)
theorem

comapRamIdx_set_nonempty

L158 ↗
AlgebraicCurve.Place.comapRamIdx_set_nonempty
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (hne : w.toValuationSubring.comap (algebraMap F F') ≠ ⊤)
include hne
Lean source · statement
theorem _root_.AlgebraicCurve.Place.comapRamIdx_set_nonempty :
    {n : ℕ | 0 < n ∧ ∃ f : F, f ≠ 0 ∧ w.ord (algebraMap F F' f) = n}.Nonempty
theorem

comapRamIdx_pos

L165 ↗
AlgebraicCurve.Place.comapRamIdx_pos
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (hne : w.toValuationSubring.comap (algebraMap F F') ≠ ⊤)
include hne
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.comapRamIdx_pos : 0 < comapRamIdx (F := F) w
theorem

exists_ord_eq_comapRamIdx

L170 ↗
AlgebraicCurve.Place.exists_ord_eq_comapRamIdx
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (hne : w.toValuationSubring.comap (algebraMap F F') ≠ ⊤)
include hne
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_ord_eq_comapRamIdx :
    ∃ f : F, f ≠ 0 ∧ w.ord (algebraMap F F' f) = comapRamIdx (F := F) w
theorem

comapRamIdx_dvd_ord

L176 ↗
AlgebraicCurve.Place.comapRamIdx_dvd_ord
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (hne : w.toValuationSubring.comap (algebraMap F F') ≠ ⊤)
include hne
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.comapRamIdx_dvd_ord {f : F} (hf : f ≠ 0) :
    (comapRamIdx (F := F) w : ℤ) ∣ w.ord (algebraMap F F' f)
theorem

irreducible_mk_comap'

L206 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top.AlgebraicCurve.Place.irreducible_mk_comap'
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (hne : w.toValuationSubring.comap (algebraMap F F') ≠ ⊤)
include hne
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem irreducible_mk_comap' {g : F} (hg0 : g ≠ 0)
    (hmem : g ∈ w.toValuationSubring.comap (algebraMap F F'))
    (hge : w.ord (algebraMap F F' g) = comapRamIdx (F := F) w) :
    Irreducible (⟨g, hmem⟩ : w.toValuationSubring.comap (algebraMap F F'))
theorem

isPrincipalIdealRing_comap'

L237 ↗
AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top.AlgebraicCurve.Place.isPrincipalIdealRing_comap'
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
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
variable {w} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (hne : w.toValuationSubring.comap (algebraMap F F') ≠ ⊤)
include hne
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem isPrincipalIdealRing_comap' :
    IsPrincipalIdealRing (w.toValuationSubring.comap (algebraMap F F'))
theorem

exists_toValuationSubring_eq_comap_of_ne_top

L289 ↗
AlgebraicCurve.Place.exists_toValuationSubring_eq_comap_of_ne_top
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_toValuationSubring_eq_comap_of_ne_top
open _root_.AlgebraicCurve AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_toValuationSubring_eq_comap_of_ne_top
    {K F K' F' : Type*} [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    (ι : F →+* F') (w : Place K' F')
    (hK : ∀ a : K, ι (algebraMap K F a) ∈ w.toValuationSubring)
    (hne : w.toValuationSubring.comap ι ≠ ⊤) :
    ∃ v : Place K F, v.toValuationSubring = w.toValuationSubring.comap ι

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