NYLL
Module

Place_exists_of_isPrime_over_valuationSubring.lean

Nyll.AlgebraicCurves.Places.Place_exists_of_isPrime_over_valuationSubring
125 declarations indexed from sourceView source ↗

Module documentation

Place exists of is Prime over valuation Subring

Imports21
  • Mathlib.RingTheory.IntegralClosure.GoingDown
  • Mathlib.RingTheory.Polynomial.IsIntegral
  • Mathlib.RingTheory.Valuation.LocalSubring
  • Mathlib.RingTheory.Algebraic.Basic
  • Nyll.AlgebraicCurves.Places.OverDVR
  • Mathlib.FieldTheory.IsAlgClosed.Basic
  • Mathlib.Algebra.Polynomial.Lifts
  • Mathlib.RingTheory.Ideal.Quotient.Operations
  • Nyll.AlgebraicCurves.Divisors.ClassGroup
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.RingTheory.Valuation.ValuationSubring
  • Mathlib.RingTheory.PrincipalIdealDomain
  • Mathlib.Algebra.CharP.Basic
  • Mathlib.Data.Int.CharZero
  • Mathlib.Data.Nat.Prime.Int
  • Mathlib.RingTheory.DedekindDomain.IntegralClosure
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.Ideal.Maximal
  • Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
  • Mathlib.FieldTheory.Separable
Imported by1

Declarations

theorem

closureConstantsAdjoin_eq_range_aeval

L51 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.ValuationSubring.closureConstantsAdjoin_eq_range_aeval
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
Lean source · statement
theorem closureConstantsAdjoin_eq_range_aeval (x : F) :
    Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x}) =
      (aeval (R := A) x).toRingHom.range
theorem

aeval_injective_of_transcendental

L75 ↗
ValuationSubring.aeval_injective_of_transcendental
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
Lean source · statement
theorem _root_.ValuationSubring.aeval_injective_of_transcendental {x : F} (hx :
  Transcendental K x) :
    Function.Injective (aeval (R := A) x)
theorem

aeval_mem_closure

L88 ↗
ValuationSubring.aeval_mem_closure
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.aeval_mem_closure (x : F) (p : A[X]) :
    aeval x p ∈ Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x})
def

polynomialEquivClosure

L95 ↗
ValuationSubring.polynomialEquivClosure
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
def _root_.ValuationSubring.polynomialEquivClosure {x : F} (hx :
  Transcendental K x) :
    A[X] ≃+* Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x})
theorem

polynomialEquivClosure_apply

L109 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.ValuationSubring.polynomialEquivClosure_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem polynomialEquivClosure_apply {x : F} (hx : Transcendental K x) (p : A[X]) :
    (A.polynomialEquivClosure hx p : F) = aeval x p
theorem

isIntegrallyClosed_closure

L112 ↗
ValuationSubring.isIntegrallyClosed_closure
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (A : ValuationSubring K)
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.isIntegrallyClosed_closure {x : F} (hx : Transcendental K
  x) :
    IsIntegrallyClosed (Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {x}))
theorem

isIntegral_iff_exists_monic_eval₂

L126 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.Subring.isIntegral_iff_exists_monic_eval₂
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
namespace Subring
open _root_.Subring
open _root_.Subring
variable {F : Type*} [Field F]
Lean source · statement
theorem isIntegral_iff_exists_monic_eval₂ (S : Subring F) (b : F) :
    IsIntegral S b ↔ ∃ p : Polynomial S, p.Monic ∧ Polynomial.eval₂ S.subtype b p = 0
theorem

exists_ideal_le_comap_eq_of_isIntegral

L130 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.Subring.exists_ideal_le_comap_eq_of_isIntegral
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
namespace Subring
open _root_.Subring
open _root_.Subring
variable {F : Type*} [Field F]
Lean source · statement
theorem exists_ideal_le_comap_eq_of_isIntegral {S B : Subring F} (hSB : S ≤ B)
    [IsIntegrallyClosed S] (hint : ∀ b : B, IsIntegral S (b : F))
    {p q : Ideal S} [p.IsPrime] [q.IsPrime] (hpq : p ≤ q)
    (Q : Ideal B) [Q.IsPrime] (hQ : Q.comap (Subring.inclusion hSB) = q) :
    ∃ P : Ideal B, P ≤ Q ∧ P.IsPrime ∧ P.comap (Subring.inclusion hSB) = p
theorem

algebraMap_mem

L169 ↗
AlgebraicCurve.Place.algebraMap_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.algebraMap_mem (a : K) : algebraMap K F a ∈
  w.toValuationSubring
theorem

algebraMap_mem_nonunits_iff

L174 ↗
AlgebraicCurve.Place.algebraMap_mem_nonunits_iff
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.algebraMap_mem_nonunits_iff (a : K) :
    algebraMap K F a ∈ w.toValuationSubring.nonunits ↔ a = 0
theorem

mul_mem_nonunits

L186 ↗
AlgebraicCurve.Place.mul_mem_nonunits
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mul_mem_nonunits {x y : F} (hx : x ∈
  w.toValuationSubring.nonunits)
    (hy : y ∈ w.toValuationSubring) : x * y ∈ w.toValuationSubring.nonunits
theorem

mem_of_ord_pos

L199 ↗
AlgebraicCurve.Place.mem_of_ord_pos
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_of_ord_pos {f : F} (h : 0 < w.ord f) : f ∈
  w.toValuationSubring
theorem

mem_nonunits_iff_ord_pos

L210 ↗
AlgebraicCurve.Place.mem_nonunits_iff_ord_pos
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : 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.mem_nonunits_iff_ord_pos {f : F} (hf : f ≠ 0) :
    f ∈ w.toValuationSubring.nonunits ↔ 0 < w.ord f
def

HasValueAt

L226 ↗
AlgebraicCurve.Place.HasValueAt
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : 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
def _root_.AlgebraicCurve.Place.HasValueAt (f : F) (a : K) : Prop
theorem

hasValueAt_iff

L230 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.hasValueAt_iff
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem hasValueAt_iff (f : F) (a : K) :
    w.HasValueAt f a ↔ f - algebraMap K F a ∈ w.toValuationSubring.nonunits
theorem

hasValueAt_iff_ord_pos

L233 ↗
AlgebraicCurve.Place.hasValueAt_iff_ord_pos
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.hasValueAt_iff_ord_pos {f : F} {a : K} (h : f ≠
  algebraMap K F a) :
    w.HasValueAt f a ↔ 0 < w.ord (f - algebraMap K F a)
theorem

hasValueAt_of_ord_pos

L239 ↗
AlgebraicCurve.Place.hasValueAt_of_ord_pos
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.hasValueAt_of_ord_pos {f : F} {a : K} (h : 0 < w.ord (f
  - algebraMap K F a)) :
    w.HasValueAt f a
theorem

hasValueAt_algebraMap

L248 ↗
AlgebraicCurve.Place.hasValueAt_algebraMap
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.hasValueAt_algebraMap (a : K) : w.HasValueAt
  (algebraMap K F a) a
theorem

hasValueAt_zero_iff

L254 ↗
AlgebraicCurve.Place.hasValueAt_zero_iff
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.hasValueAt_zero_iff (f : F) : w.HasValueAt f 0 ↔ f ∈
  w.toValuationSubring.nonunits
theorem

mem_of_hasValueAt

L260 ↗
AlgebraicCurve.Place.mem_of_hasValueAt
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_of_hasValueAt {f : F} {a : K} (h : w.HasValueAt f
  a) : f ∈ w.toValuationSubring
theorem

unique

L268 ↗
AlgebraicCurve.Place.HasValueAt.unique
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace HasValueAt
variable {w} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.HasValueAt.unique {f : F} {a b : K} (ha : w.HasValueAt
  f a) (hb : w.HasValueAt f b) :
    a = b
theorem

add

L280 ↗
AlgebraicCurve.Place.HasValueAt.add
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace HasValueAt
variable {w} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.HasValueAt.add {f g : F} {a b : K} (hf : w.HasValueAt f
  a) (hg : w.HasValueAt g b) :
    w.HasValueAt (f + g) (a + b)
theorem

neg

L292 ↗
AlgebraicCurve.Place.HasValueAt.neg
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace HasValueAt
variable {w} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.HasValueAt.neg {f : F} {a : K} (hf : w.HasValueAt f a)
  : w.HasValueAt (-f) (-a)
theorem

mul

L303 ↗
AlgebraicCurve.Place.HasValueAt.mul
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace HasValueAt
variable {w} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.HasValueAt.mul {f g : F} {a b : K} (hf : w.HasValueAt f
  a) (hg : w.HasValueAt g b) :
    w.HasValueAt (f * g) (a * b)
theorem

pow

L319 ↗
AlgebraicCurve.Place.HasValueAt.pow
Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace HasValueAt
variable {w} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.HasValueAt.pow {f : F} {a : K} (hf : w.HasValueAt f a)
  (n : ℕ) :
    w.HasValueAt (f ^ n) (a ^ n)
theorem

inv

L332 ↗
AlgebraicCurve.Place.HasValueAt.inv
Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace HasValueAt
variable {w} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.HasValueAt.inv {f : F} {a : K} (hf : w.HasValueAt f a)
  (ha : a ≠ 0) :
    w.HasValueAt f⁻¹ a⁻¹
theorem

div

L359 ↗
AlgebraicCurve.Place.HasValueAt.div
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace HasValueAt
variable {w} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.HasValueAt.div {f g : F} {a b : K} (hf : w.HasValueAt f
  a) (hg : w.HasValueAt g b)
    (hb : b ≠ 0) : w.HasValueAt (f / g) (a / b)
theorem

hasValueAt_iff_residue

L368 ↗
AlgebraicCurve.Place.hasValueAt_iff_residue
Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.hasValueAt_iff_residue {f : F} (hf : f ∈
  w.toValuationSubring) (a : K) :
    w.HasValueAt f a ↔
      residue w.toValuationSubring ⟨f, hf⟩ = algebraMap K w.ResidueField a
theorem

exists_hasValueAt

L379 ↗
AlgebraicCurve.Place.exists_hasValueAt
Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_hasValueAt (hw : Function.Surjective (algebraMap
  K w.ResidueField)) {f : F}
    (hf : f ∈ w.toValuationSubring) : ∃ a : K, w.HasValueAt f a
theorem

surjective_algebraMap_residueField_of_isAlgClosed

L387 ↗
AlgebraicCurve.Place.surjective_algebraMap_residueField_of_isAlgClosed
Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.surjective_algebraMap_residueField_of_isAlgClosed
  [IsAlgClosed K]
    [Module.Finite K w.ResidueField] : Function.Surjective (algebraMap K w.ResidueField)
theorem

surjective_algebraMap_residueField_of_deg_eq_one

L395 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.surjective_algebraMap_residueField_of_deg_eq_one
Source context 33 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem surjective_algebraMap_residueField_of_deg_eq_one [IsAlgClosed K] (h : w.deg = 1) :
    Function.Surjective (algebraMap K w.ResidueField)
def

compSubring

L402 ↗
AlgebraicCurve.Place.compSubring
Source context 34 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
Lean source · full declaration
def _root_.AlgebraicCurve.Place.compSubring : Subring F where
  carrier := {f | ∃ a : A, w.HasValueAt f a}
  mul_mem' := by
    rintro f g ⟨a, ha⟩ ⟨b, hb⟩
    exact ⟨a * b, by simpa using ha.mul hb⟩
  one_mem' := ⟨1, by simpa using w.hasValueAt_algebraMap 1⟩
  add_mem' := by
    rintro f g ⟨a, ha⟩ ⟨b, hb⟩
    exact ⟨a + b, by simpa using ha.add hb⟩
  zero_mem' := ⟨0, by simpa using w.hasValueAt_algebraMap 0⟩
  neg_mem' := by
    rintro f ⟨a, ha⟩
    exact ⟨-a, by simpa using ha.neg⟩
theorem

mem_compSubring_iff

L418 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.mem_compSubring_iff
Source context 36 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem mem_compSubring_iff {f : F} : f ∈ w.compSubring A ↔ ∃ a : A, w.HasValueAt f a
theorem

mem_compSubring_of_hasValueAt

L422 ↗
AlgebraicCurve.Place.mem_compSubring_of_hasValueAt
Source context 37 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_compSubring_of_hasValueAt {f : F} {a : K} (ha : a ∈
  A) (h : w.HasValueAt f a) :
    f ∈ w.compSubring A
theorem

compSubring_le

L429 ↗
AlgebraicCurve.Place.compSubring_le
Source context 38 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.compSubring_le : w.compSubring A ≤
  w.toValuationSubring.toSubring
theorem

mem_compSubring_of_mem_nonunits

L436 ↗
AlgebraicCurve.Place.mem_compSubring_of_mem_nonunits
Source context 39 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_compSubring_of_mem_nonunits {f : F} (hf : f ∈
  w.toValuationSubring.nonunits) :
    f ∈ w.compSubring A
theorem

algebraMap_mem_compSubring_iff

L443 ↗
AlgebraicCurve.Place.algebraMap_mem_compSubring_iff
Source context 40 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.algebraMap_mem_compSubring_iff (a : K) : algebraMap K F
  a ∈ w.compSubring A ↔ a ∈ A
def

value

L454 ↗
AlgebraicCurve.Place.value
Source context 41 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · full declaration
def _root_.AlgebraicCurve.Place.value : w.compSubring A →+* A where
  toFun f := Classical.choose f.2
  map_one' := Subtype.ext <|
    (Classical.choose_spec (w.compSubring A).one_mem).unique (by
      simpa using w.hasValueAt_algebraMap 1)
  map_mul' f g := Subtype.ext <|
    (Classical.choose_spec (mul_mem f.2 g.2)).unique (by
      simpa using (Classical.choose_spec f.2).mul (Classical.choose_spec g.2))
  map_zero' := Subtype.ext <|
    (Classical.choose_spec (w.compSubring A).zero_mem).unique (by
      simpa using w.hasValueAt_algebraMap 0)
  map_add' f g := Subtype.ext <|
    (Classical.choose_spec (add_mem f.2 g.2)).unique (by
      simpa using (Classical.choose_spec f.2).add (Classical.choose_spec g.2))
theorem

hasValueAt_value

L471 ↗
AlgebraicCurve.Place.hasValueAt_value
Source context 42 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.hasValueAt_value (f : w.compSubring A) : w.HasValueAt
  (f : F) (w.value A f : K)
theorem

value_eq_of_hasValueAt

L477 ↗
AlgebraicCurve.Place.value_eq_of_hasValueAt
Source context 44 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.value_eq_of_hasValueAt {f : w.compSubring A} {a : A} (h
  : w.HasValueAt (f : F) a) :
    w.value A f = a
theorem

ord_sub_value_pos

L484 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.ord_sub_value_pos
Source context 46 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem ord_sub_value_pos {f : w.compSubring A} (hf : (f : F) ≠ algebraMap K F (w.value A
  f)) :
    0 < w.ord ((f : F) - algebraMap K F (w.value A f))
theorem

value_eq_of_ord_pos

L490 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.value_eq_of_ord_pos
Source context 47 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
Lean source · statement
theorem value_eq_of_ord_pos {f : w.compSubring A} {a : A}
    (h : 0 < w.ord ((f : F) - algebraMap K F a)) : w.value A f = a
theorem

value_algebraMap

L494 ↗
AlgebraicCurve.Place.value_algebraMap
Source context 47 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.value_algebraMap (a : A) :
    w.value A ⟨algebraMap K F a, (w.algebraMap_mem_compSubring_iff A a).mpr a.2⟩ = a
theorem

value_surjective

L499 ↗
AlgebraicCurve.Place.value_surjective
Source context 48 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.value_surjective : Function.Surjective (w.value A)
theorem

value_eq_zero_of_mem_nonunits

L504 ↗
AlgebraicCurve.Place.value_eq_zero_of_mem_nonunits
Source context 50 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.value_eq_zero_of_mem_nonunits {f : w.compSubring A}
    (hf : (f : F) ∈ w.toValuationSubring.nonunits) : w.value A f = 0
def

centre

L510 ↗
AlgebraicCurve.Place.centre
Source context 51 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
Lean source · statement
def _root_.AlgebraicCurve.Place.centre : Ideal (w.compSubring A)
instance

centre_isPrime

L514 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.centre_isPrime
Source context 52 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
instance centre_isPrime : (w.centre A).IsPrime
instance

centre_isMaximal

L516 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.centre_isMaximal
Source context 52 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
instance centre_isMaximal : (w.centre A).IsMaximal
theorem

mem_centre_iff

L520 ↗
AlgebraicCurve.Place.mem_centre_iff
Source context 53 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_centre_iff (f : w.compSubring A) : f ∈ w.centre A ↔
  w.value A f ∈ maximalIdeal A
theorem

mem_centre_iff_of_hasValueAt

L526 ↗
AlgebraicCurve.Place.mem_centre_iff_of_hasValueAt
Source context 55 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_centre_iff_of_hasValueAt {f : w.compSubring A} {a :
  A} (h : w.HasValueAt (f : F) a) :
    f ∈ w.centre A ↔ a ∈ maximalIdeal A
theorem

mem_centre_iff_of_ord_pos

L533 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.mem_centre_iff_of_ord_pos
Source context 57 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem mem_centre_iff_of_ord_pos {f : w.compSubring A} {a : A}
    (h : 0 < w.ord ((f : F) - algebraMap K F a)) : f ∈ w.centre A ↔ a ∈ maximalIdeal A
theorem

mem_centre_of_mem_nonunits

L538 ↗
AlgebraicCurve.Place.mem_centre_of_mem_nonunits
Source context 58 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_centre_of_mem_nonunits {f : w.compSubring A}
    (hf : (f : F) ∈ w.toValuationSubring.nonunits) : f ∈ w.centre A
theorem

mem_centre_of_ord_pos

L545 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.mem_centre_of_ord_pos
Source context 60 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem mem_centre_of_ord_pos {f : w.compSubring A} (hf : 0 < w.ord (f : F)) : f ∈ w.centre
  A
theorem

algebraMap_mem_centre_iff

L549 ↗
AlgebraicCurve.Place.algebraMap_mem_centre_iff
Source context 60 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.algebraMap_mem_centre_iff (a : A) :
    (⟨algebraMap K F a, (w.algebraMap_mem_compSubring_iff A a).mpr a.2⟩ : w.compSubring A)
        ∈ w.centre A ↔ a ∈ maximalIdeal A
theorem

mem_compSubring_or_inv_mem

L556 ↗
AlgebraicCurve.Place.mem_compSubring_or_inv_mem
Source context 61 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_compSubring_or_inv_mem (hw : Function.Surjective
  (algebraMap K w.ResidueField))
    (f : F) : f ∈ w.compSubring A ∨ f⁻¹ ∈ w.compSubring A
def

compValuationSubring

L593 ↗
AlgebraicCurve.Place.compValuationSubring
Source context 62 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
def _root_.AlgebraicCurve.Place.compValuationSubring (hw : Function.Surjective (algebraMap
  K w.ResidueField)) :
    ValuationSubring F
theorem

compValuationSubring_toSubring

L600 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.compValuationSubring_toSubring
Source context 63 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem compValuationSubring_toSubring (hw : Function.Surjective (algebraMap K
  w.ResidueField)) :
    (w.compValuationSubring A hw).toSubring = w.compSubring A
theorem

mem_compValuationSubring_iff

L604 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.mem_compValuationSubring_iff
Source context 63 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem mem_compValuationSubring_iff (hw : Function.Surjective (algebraMap K
  w.ResidueField))
    (f : F) : f ∈ w.compValuationSubring A hw ↔ f ∈ w.compSubring A
theorem

mem_compSubring_of_isIntegral

L608 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.mem_compSubring_of_isIntegral
Source context 63 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem mem_compSubring_of_isIntegral (hw : Function.Surjective (algebraMap K
  w.ResidueField))
    {S : Subring F} (hS : S ≤ w.compSubring A) {f : F} (hf : IsIntegral S f) :
    f ∈ w.compSubring A
theorem

mem_compSubring_of_isIntegral'

L623 ↗
AlgebraicCurve.Place.mem_compSubring_of_isIntegral'
Source context 63 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_compSubring_of_isIntegral' [IsAlgClosed K] {S :
  Subring F} (hS : S ≤ w.compSubring A)
    {f : F} (hf : IsIntegral S f) : f ∈ w.compSubring A
theorem

exists_unique_valueHom

L668 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.exists_unique_valueHom
Source context 64 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem exists_unique_valueHom [IsAlgClosed K] (g : F) (B₀ : Subring F)
    (hint : ∀ b : B₀,
      ∃ p : Polynomial (Subring.closure (algebraMap K F '' (A : Set K) ∪ {g})),
        p.Monic ∧
          Polynomial.eval₂ (Subring.closure (algebraMap K F '' (A : Set K) ∪ {g})).subtype
            (b : F) p = 0)
    (hw : ∃ a : A, g - algebraMap K F (a : K) ∈ w.toValuationSubring.nonunits) :
    ∃! φ : B₀ →+* A, ∀ b : B₀,
      (b : F) - algebraMap K F ((φ b : A) : K) ∈ w.toValuationSubring.nonunits
theorem

residue_comp_value_surjective

L695 ↗
AlgebraicCurve.Place.residue_comp_value_surjective
Source context 65 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.residue_comp_value_surjective {B : Subring F} (hB : B ≤
  w.compSubring A)
    (hconst : ∀ a : A, algebraMap K F a ∈ B) :
    Function.Surjective
      (((IsLocalRing.residue A).comp (w.value A)).comp (Subring.inclusion hB))
theorem

ker_residue_comp_value

L708 ↗
AlgebraicCurve.Place.ker_residue_comp_value
Source context 67 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ker_residue_comp_value {B : Subring F} (hB : B ≤
  w.compSubring A) :
    RingHom.ker (((IsLocalRing.residue A).comp (w.value A)).comp (Subring.inclusion hB)) =
      (w.centre A).comap (Subring.inclusion hB)
theorem

centre_comap_isMaximal

L718 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.centre_comap_isMaximal
Source context 69 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
Lean source · statement
theorem centre_comap_isMaximal {B : Subring F} (hB : B ≤ w.compSubring A)
    (hconst : ∀ a : A, algebraMap K F a ∈ B) :
    ((w.centre A).comap (Subring.inclusion hB)).IsMaximal
theorem

sub_value_mem_centre_comap

L725 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.sub_value_mem_centre_comap
Source context 70 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
Lean source · statement
theorem sub_value_mem_centre_comap {B : Subring F} (hB : B ≤ w.compSubring A)
    (hconst : ∀ a : A, algebraMap K F a ∈ B) (b : B) :
    b - ⟨algebraMap K F (w.value A ⟨b, hB b.2⟩ : K), hconst _⟩ ∈
      (w.centre A).comap (Subring.inclusion hB)
theorem

algebraMap_mem_centre_comap_iff

L739 ↗
AlgebraicCurve.Place.algebraMap_mem_centre_comap_iff
Source context 71 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
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] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable (A : ValuationSubring K)
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
open _root_.AlgebraicCurve.Place
variable {A} in
variable {A} in
variable {A} in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.algebraMap_mem_centre_comap_iff {B : Subring F} (hB : B
  ≤ w.compSubring A)
    (hconst : ∀ a : A, algebraMap K F a ∈ B) (a : A) :
    (⟨algebraMap K F a, hconst a⟩ : B) ∈ (w.centre A).comap (Subring.inclusion hB) ↔
      a ∈ maximalIdeal A
theorem

algebraMap_bijective_of_isIntegral_of_isAlgClosed

L758 ↗
ValuationSubring.algebraMap_bijective_of_isIntegral_of_isAlgClosed
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
Lean source · statement
theorem _root_.ValuationSubring.algebraMap_bijective_of_isIntegral_of_isAlgClosed
  [IsAlgClosed K]
    (R : Type*) [CommRing R] [IsDomain R] [Algebra A R] [FaithfulSMul A R]
    [Algebra.IsIntegral A R] : Function.Bijective (algebraMap A R)
abbrev

constants

L796 ↗
ValuationSubring.constants
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
open _root_.ValuationSubring
section Quotient
open Polynomial
variable {F : Type*} [Field F] [Algebra K F]
Lean source · statement
abbrev _root_.ValuationSubring.constants : A →+* F
theorem

exists_sub_constants_mem

L801 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.ValuationSubring.exists_sub_constants_mem
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
open _root_.ValuationSubring
section Quotient
open Polynomial
variable {F : Type*} [Field F] [Algebra K F]
open _root_.ValuationSubring
variable {A}
Lean source · statement
theorem exists_sub_constants_mem [IsAlgClosed K] {x : F} {B : Subring F}
    (hconst : ∀ a : A, A.constants a ∈ B) (hxB : x ∈ B)
    (hint : ∀ b : B, IsIntegral (Subring.closure (Set.range (A.constants (F := F)) ∪ {x})) (b : F))
    (𝔭 : Ideal B) [𝔭.IsPrime]
    (hbot : ∀ a : A, (⟨A.constants a, hconst a⟩ : B) ∈ 𝔭 → a = 0)
    (a₀ : A) (hx : (⟨x, hxB⟩ : B) - ⟨A.constants a₀, hconst a₀⟩ ∈ 𝔭) (b : B) :
    ∃ a : A, b - ⟨A.constants a, hconst a⟩ ∈ 𝔭
theorem

constants_unique_mod

L888 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.ValuationSubring.constants_unique_mod
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
open _root_.ValuationSubring
section Quotient
open Polynomial
variable {F : Type*} [Field F] [Algebra K F]
open _root_.ValuationSubring
variable {A}
Lean source · statement
theorem constants_unique_mod {B : Subring F} (hconst : ∀ a : A, A.constants a ∈ B)
    (𝔭 : Ideal B) (hbot : ∀ a : A, (⟨A.constants a, hconst a⟩ : B) ∈ 𝔭 → a = 0)
    {a c : A} (h : (⟨A.constants a, hconst a⟩ : B) - ⟨A.constants c, hconst c⟩ ∈ 𝔭) : a = c
theorem

exists_valuationSubring_dominating

L912 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.Subring.exists_valuationSubring_dominating
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace Subring
open _root_.Subring
open _root_.Subring
variable {F : Type*} [Field F] {B : Subring F}
Lean source · statement
theorem exists_valuationSubring_dominating (𝔭 : Ideal B) [𝔭.IsPrime] :
    ∃ O : ValuationSubring F, B ≤ O.toSubring ∧ ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭
theorem

ne_top_of_dominating

L938 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.Subring.ne_top_of_dominating
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace Subring
open _root_.Subring
open _root_.Subring
variable {F : Type*} [Field F] {B : Subring F}
Lean source · statement
theorem ne_top_of_dominating {𝔭 : Ideal B} {O : ValuationSubring F}
    (hdom : ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭) (h𝔭 : 𝔭 ≠ ⊥) : O ≠ ⊤
theorem

algebraMap_mem_of_dominating

L949 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.Subring.algebraMap_mem_of_dominating
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace Subring
open _root_.Subring
open _root_.Subring
variable {F : Type*} [Field F] {B : Subring F}
Lean source · statement
theorem algebraMap_mem_of_dominating {K : Type*} [Field K] [Algebra K F] (A :
  ValuationSubring K)
    (hconst : ∀ a : A, algebraMap K F a ∈ B) {𝔭 : Ideal B} {O : ValuationSubring F}
    (hle : B ≤ O.toSubring) (hdom : ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭)
    (hbot : ∀ a : A, (⟨algebraMap K F a, hconst a⟩ : B) ∈ 𝔭 → a = 0) (c : K) :
    algebraMap K F c ∈ O
def

centreOver

L975 ↗
ValuationSubring.centreOver
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (O : ValuationSubring F)
Lean source · statement
def _root_.ValuationSubring.centreOver (hO : ∀ r : R, algebraMap R F r ∈ O) : Ideal R
instance

centreOver_isPrime

L979 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.ValuationSubring.centreOver_isPrime
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (O : ValuationSubring F)
open _root_.ValuationSubring
Lean source · statement
instance centreOver_isPrime (hO : ∀ r : R, algebraMap R F r ∈ O) : (O.centreOver
  hO).IsPrime
theorem

mem_centreOver_iff

L984 ↗
ValuationSubring.mem_centreOver_iff
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (O : ValuationSubring F)
open _root_.ValuationSubring
omit [IsDedekindDomain R] [IsFractionRing R F] in
Lean source · statement
theorem _root_.ValuationSubring.mem_centreOver_iff (hO : ∀ r : R, algebraMap R F r ∈ O) {r
  : R} :
    r ∈ O.centreOver hO ↔ algebraMap R F r ∈ O.nonunits
theorem

inv_algebraMap_mem

L992 ↗
ValuationSubring.inv_algebraMap_mem
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (O : ValuationSubring F)
open _root_.ValuationSubring
open _root_.ValuationSubring
omit [IsDedekindDomain R] [IsFractionRing R F] in
Lean source · statement
theorem _root_.ValuationSubring.inv_algebraMap_mem (hO : ∀ r : R, algebraMap R F r ∈ O) {s
  : R}
    (hs : s ∉ O.centreOver hO) : (algebraMap R F s)⁻¹ ∈ O
theorem

centreOver_ne_bot

L1003 ↗
ValuationSubring.centreOver_ne_bot
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (O : ValuationSubring F)
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.centreOver_ne_bot (hO : ∀ r : R, algebraMap R F r ∈ O) (hne
  : O ≠ ⊤) :
    O.centreOver hO ≠ ⊥
def

centreHeightOneSpectrum

L1017 ↗
ValuationSubring.centreHeightOneSpectrum
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (O : ValuationSubring F)
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
def _root_.ValuationSubring.centreHeightOneSpectrum (hO : ∀ r : R, algebraMap R F r ∈ O)
  (hne : O ≠ ⊤) :
    HeightOneSpectrum R
theorem

valuationSubringAtPrime_centre_le

L1024 ↗
ValuationSubring.valuationSubringAtPrime_centre_le
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (O : ValuationSubring F)
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.valuationSubringAtPrime_centre_le (hO : ∀ r : R, algebraMap
  R F r ∈ O) (hne : O ≠ ⊤) :
    HeightOneSpectrum.valuationSubringAtPrime F (O.centreHeightOneSpectrum hO hne) ≤ O
theorem

eq_valuationSubringAtPrime_centre

L1032 ↗
ValuationSubring.eq_valuationSubringAtPrime_centre
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (O : ValuationSubring F)
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.eq_valuationSubringAtPrime_centre (hO : ∀ r : R, algebraMap
  R F r ∈ O) (hne : O ≠ ⊤) :
    O = HeightOneSpectrum.valuationSubringAtPrime F (O.centreHeightOneSpectrum hO hne)
theorem

isPrincipalIdealRing_of_dedekind_le

L1039 ↗
ValuationSubring.isPrincipalIdealRing_of_dedekind_le
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (O : ValuationSubring F)
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.isPrincipalIdealRing_of_dedekind_le (hO : ∀ r : R,
  algebraMap R F r ∈ O) (hne : O ≠ ⊤) :
    IsPrincipalIdealRing O
def

ofValuationSubringOver

L1059 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.ofValuationSubringOver
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
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]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
Lean source · full declaration
def ofValuationSubringOver (O : ValuationSubring F) (hO : ∀ r : R, algebraMap R F r ∈ O)
    (hne : O ≠ ⊤) (hK : ∀ c : K, algebraMap K F c ∈ O) : Place K F where
  toValuationSubring := O
  algebraMap_mem' := hK
  ne_top' := hne
  isPrincipalIdealRing' := O.isPrincipalIdealRing_of_dedekind_le hO hne
theorem

ofValuationSubringOver_toValuationSubring

L1066 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.ofValuationSubringOver_toValuationSubring
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
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]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
Lean source · statement
theorem ofValuationSubringOver_toValuationSubring (O : ValuationSubring F)
    (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) (hK : ∀ c : K, algebraMap K F c ∈ O) :
    (ofValuationSubringOver O hO hne hK).toValuationSubring = O
theorem

mem_nonunits_ofValuationSubringOver_iff

L1070 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.mem_nonunits_ofValuationSubringOver_iff
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
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]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
Lean source · statement
theorem mem_nonunits_ofValuationSubringOver_iff (O : ValuationSubring F)
    (hO : ∀ r : R, algebraMap R F r ∈ O) (hne : O ≠ ⊤) (hK : ∀ c : K, algebraMap K F c ∈ O)
    {B : Subring F} {𝔭 : Ideal B} (hdom : ∀ b : B, (b : F) ∈ O.nonunits ↔ b ∈ 𝔭) (b : B) :
    (b : F) ∈ (ofValuationSubringOver O hO hne hK).toValuationSubring.nonunits ↔ b ∈ 𝔭
theorem

exists_ne_map_eq_of_sum_eq_zero

L1088 ↗
Valuation.exists_ne_map_eq_of_sum_eq_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
namespace Valuation
open _root_.Valuation
open _root_.Valuation
variable {R Γ₀ : Type*} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀]
Lean source · statement
theorem _root_.Valuation.exists_ne_map_eq_of_sum_eq_zero {ι : Type*} (v :
  Valuation R Γ₀)
    {s : Finset ι} {f : ι → R} (hs : ∑ i ∈ s, f i = 0) {j : ι} (hj : j ∈ s)
    (hj0 : v (f j) ≠ 0) (hmax : ∀ i ∈ s, v (f i) ≤ v (f j)) :
    ∃ i ∈ s, i ≠ j ∧ v (f i) = v (f j)
theorem

natCast_mem_ker

L1114 ↗
ValuationSubring.natCast_mem_ker
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
variable {k : Type*} [Field k]
Lean source · statement
theorem _root_.ValuationSubring.natCast_mem_ker (ℓ : ℕ) [CharP k ℓ] (red : A →+* k) :
    ((ℓ : ℕ) : A) ∈ RingHom.ker red
theorem

natCast_mem_maximalIdeal

L1120 ↗
ValuationSubring.natCast_mem_maximalIdeal
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
variable {k : Type*} [Field k]
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.natCast_mem_maximalIdeal (ℓ : ℕ) [CharP k ℓ] (red : A →+*
  k) :
    ((ℓ : ℕ) : A) ∈ maximalIdeal A
theorem

isUnit_intCast_of_not_dvd

L1127 ↗
ValuationSubring.isUnit_intCast_of_not_dvd
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
variable {k : Type*} [Field k]
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.isUnit_intCast_of_not_dvd (ℓ : ℕ) [Fact ℓ.Prime] [CharP k
  ℓ] (red : A →+* k)
    {m : ℤ} (hm : ¬ (ℓ : ℤ) ∣ m) : IsUnit ((m : ℤ) : A)
theorem

map_intCast_eq_zero_of_not_isUnit

L1147 ↗
ValuationSubring.map_intCast_eq_zero_of_not_isUnit
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
variable {k : Type*} [Field k]
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.map_intCast_eq_zero_of_not_isUnit (ℓ : ℕ) [Fact ℓ.Prime]
  [CharP k ℓ] (red : A →+* k)
    {m : ℤ} (hm : ¬ IsUnit ((m : ℤ) : A)) : red (m : A) = 0
theorem

map_eq_zero_of_rat_mem_maximalIdeal

L1160 ↗
ValuationSubring.map_eq_zero_of_rat_mem_maximalIdeal
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
variable {k : Type*} [Field k]
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.map_eq_zero_of_rat_mem_maximalIdeal (ℓ : ℕ) [Fact ℓ.Prime]
  [CharP k ℓ]
    (red : A →+* k) (φ : ℚ →+* K) (r : ℚ) (hrA : φ r ∈ A)
    (hr : (⟨φ r, hrA⟩ : A) ∈ maximalIdeal A) : red ⟨φ r, hrA⟩ = 0
theorem

exists_pow_valuation_eq_of_isRoot

L1196 ↗
ValuationSubring.exists_pow_valuation_eq_of_isRoot
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
variable {k : Type*} [Field k]
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.exists_pow_valuation_eq_of_isRoot (φ : ℚ →+* K) {x : K}
  (hx0 : x ≠ 0)
    {p : ℚ[X]} (hp0 : p ≠ 0) (hpx : p.eval₂ φ x = 0) :
    ∃ n : ℕ, 0 < n ∧ ∃ r : ℚ, r ≠ 0 ∧ A.valuation (x ^ n) = A.valuation (φ r)
theorem

ker_eq_maximalIdeal_of_isAlgebraic

L1236 ↗
ValuationSubring.ker_eq_maximalIdeal_of_isAlgebraic
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
variable {k : Type*} [Field k]
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem _root_.ValuationSubring.ker_eq_maximalIdeal_of_isAlgebraic [Algebra ℚ K]
  [Algebra.IsAlgebraic ℚ K]
    (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) :
    RingHom.ker red = maximalIdeal A
theorem

exists_mul_eq_one_of_map_ne_zero

L1271 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.ValuationSubring.exists_mul_eq_one_of_map_ne_zero
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
variable {k : Type*} [Field k]
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem exists_mul_eq_one_of_map_ne_zero [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K]
    (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) {a : A} (ha : red a ≠ 0) :
    ∃ b : A, red a * red b = 1
theorem

ker_eq_maximalIdeal_apply

L1283 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.ValuationSubring.ker_eq_maximalIdeal_apply
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)
variable {k : Type*} [Field k]
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
Lean source · statement
theorem ker_eq_maximalIdeal_apply [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K]
    (ℓ : ℕ) [Fact ℓ.Prime] [CharP k ℓ] (red : A →+* k) (a : A) :
    red a = 0 ↔ a ∈ maximalIdeal A
theorem

isPrincipalIdealRing_adjoin_singleton

L1301 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.isPrincipalIdealRing_adjoin_singleton
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {j : F}
Lean source · statement
theorem isPrincipalIdealRing_adjoin_singleton (hj : Transcendental K j) :
    IsPrincipalIdealRing (Algebra.adjoin K ({j} : Set F))
theorem

isDedekindDomain_adjoin_singleton

L1306 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.isDedekindDomain_adjoin_singleton
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {j : F}
Lean source · statement
theorem isDedekindDomain_adjoin_singleton (hj : Transcendental K j) :
    IsDedekindDomain (Algebra.adjoin K ({j} : Set F))
theorem

isDedekindDomain_integralClosure_adjoin

L1311 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.isDedekindDomain_integralClosure_adjoin
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {j : F}
Lean source · statement
theorem isDedekindDomain_integralClosure_adjoin (hj : Transcendental K j)
    [FiniteDimensional K⟮j⟯ F] [Algebra.IsSeparable K⟮j⟯ F] :
    IsDedekindDomain (integralClosure (Algebra.adjoin K ({j} : Set F)) F)
theorem

isFractionRing_integralClosure_adjoin

L1317 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.isFractionRing_integralClosure_adjoin
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {j : F}
Lean source · statement
theorem isFractionRing_integralClosure_adjoin (hj : Transcendental K j)
    [FiniteDimensional K⟮j⟯ F] :
    IsFractionRing (integralClosure (Algebra.adjoin K ({j} : Set F)) F) F
theorem

integralClosure_adjoin_le_valuationSubring

L1323 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.integralClosure_adjoin_le_valuationSubring
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {j : F}
Lean source · statement
theorem integralClosure_adjoin_le_valuationSubring (O : ValuationSubring F)
    (hK : ∀ c : K, algebraMap K F c ∈ O) (hjO : j ∈ O)
    (r : integralClosure (Algebra.adjoin K ({j} : Set F)) F) : (r : F) ∈ O
theorem

algebraMap_mem_integralClosure_adjoin

L1342 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.algebraMap_mem_integralClosure_adjoin
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {j : F}
Lean source · statement
theorem algebraMap_mem_integralClosure_adjoin (c : K) :
    algebraMap K F c ∈ integralClosure (Algebra.adjoin K ({j} : Set F)) F
theorem

self_mem_integralClosure_adjoin

L1347 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.self_mem_integralClosure_adjoin
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {j : F}
Lean source · statement
theorem self_mem_integralClosure_adjoin :
    j ∈ integralClosure (Algebra.adjoin K ({j} : Set F)) F
theorem

le_integralClosure_adjoin_of_isIntegral

L1356 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.le_integralClosure_adjoin_of_isIntegral
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {j : F}
Lean source · statement
theorem le_integralClosure_adjoin_of_isIntegral {S B : Subring F}
    (hS : S ≤ (Algebra.adjoin K ({j} : Set F)).toSubring)
    (hint : ∀ b : B, IsIntegral S (b : F)) (b : B) :
    (b : F) ∈ integralClosure (Algebra.adjoin K ({j} : Set F)) F
theorem

isAlgClosed_of_surjective

L1378 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.ValuationSubring.isAlgClosed_of_surjective
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K) {k : Type*} [Field k]
Lean source · statement
theorem isAlgClosed_of_surjective [IsAlgClosed K] (red : A →+* k)
    (hred : Function.Surjective red) : IsAlgClosed k
def

imagePrime

L1404 ↗
RingHom.imagePrime
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace RingHom
open _root_.RingHom
open _root_.RingHom
variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C)
Lean source · statement
def _root_.RingHom.imagePrime (𝔮 : Ideal B) : Ideal π.range
theorem

rangeRestrict_mem_imagePrime_iff

L1408 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.RingHom.rangeRestrict_mem_imagePrime_iff
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace RingHom
open _root_.RingHom
open _root_.RingHom
variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C)
open _root_.RingHom
variable {π} in
Lean source · statement
theorem rangeRestrict_mem_imagePrime_iff {𝔮 : Ideal B} (hker : ker π ≤ 𝔮) (b : B) :
    π.rangeRestrict b ∈ π.imagePrime 𝔮 ↔ b ∈ 𝔮
theorem

mk_mem_imagePrime_iff

L1414 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.RingHom.mk_mem_imagePrime_iff
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace RingHom
open _root_.RingHom
open _root_.RingHom
variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C)
open _root_.RingHom
variable {π} in
variable {π} in
Lean source · statement
theorem mk_mem_imagePrime_iff {𝔮 : Ideal B} (hker : ker π ≤ 𝔮) (b : B)
    (hb : π b ∈ π.range := π.mem_range_self b) :
    (⟨π b, hb⟩ : π.range) ∈ π.imagePrime 𝔮 ↔ b ∈ 𝔮
theorem

mem_imagePrime_iff

L1420 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.RingHom.mem_imagePrime_iff
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace RingHom
open _root_.RingHom
open _root_.RingHom
variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C)
open _root_.RingHom
variable {π} in
variable {π} in
variable {π} in
Lean source · statement
theorem mem_imagePrime_iff {𝔮 : Ideal B} (y : π.range) :
    y ∈ π.imagePrime 𝔮 ↔ ∃ b ∈ 𝔮, π.rangeRestrict b = y
theorem

imagePrime_ne_top

L1425 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.RingHom.imagePrime_ne_top
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace RingHom
open _root_.RingHom
open _root_.RingHom
variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C)
open _root_.RingHom
variable {π} in
variable {π} in
variable {π} in
variable {π} in
Lean source · statement
theorem imagePrime_ne_top {𝔮 : Ideal B} (hker : ker π ≤ 𝔮) (h𝔮 : 𝔮 ≠ ⊤) :
    π.imagePrime 𝔮 ≠ ⊤
theorem

imagePrime_isPrime

L1433 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.RingHom.imagePrime_isPrime
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace RingHom
open _root_.RingHom
open _root_.RingHom
variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C)
open _root_.RingHom
variable {π} in
variable {π} in
variable {π} in
variable {π} in
variable {π} in
Lean source · statement
theorem imagePrime_isPrime {𝔮 : Ideal B} [𝔮.IsPrime] (hker : ker π ≤ 𝔮) :
    (π.imagePrime 𝔮).IsPrime
theorem

imagePrime_isMaximal

L1438 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.RingHom.imagePrime_isMaximal
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace RingHom
open _root_.RingHom
open _root_.RingHom
variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C)
open _root_.RingHom
variable {π} in
variable {π} in
variable {π} in
variable {π} in
variable {π} in
variable {π} in
Lean source · statement
theorem imagePrime_isMaximal {𝔮 : Ideal B} [h : 𝔮.IsMaximal] (hker : ker π ≤ 𝔮) :
    (π.imagePrime 𝔮).IsMaximal
theorem

eq_zero_of_const_mem_imagePrime

L1444 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.RingHom.eq_zero_of_const_mem_imagePrime
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace RingHom
open _root_.RingHom
open _root_.RingHom
variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C)
open _root_.RingHom
variable {π} in
variable {π} in
variable {π} in
variable {π} in
variable {π} in
variable {π} in
variable {π} in
Lean source · statement
theorem eq_zero_of_const_mem_imagePrime {A k : Type*} [CommRing A] [CommRing k]
    (σ : A →+* B) (red : A →+* k) (ι : k →+* C) (hcompat : ∀ a : A, π (σ a) = ι (red a))
    (hred : Function.Surjective red) {𝔮 : Ideal B} (hker : ker π ≤ 𝔮)
    (h𝔮 : ∀ a : A, σ a ∈ 𝔮 → red a = 0) (c : k) (hc : ι c ∈ π.range)
    (hmem : (⟨ι c, hc⟩ : π.range) ∈ π.imagePrime 𝔮) : c = 0
theorem

const_mem_range

L1455 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.RingHom.const_mem_range
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace RingHom
open _root_.RingHom
open _root_.RingHom
variable {B C : Type*} [CommRing B] [CommRing C] (π : B →+* C)
open _root_.RingHom
variable {π} in
variable {π} in
variable {π} in
variable {π} in
variable {π} in
variable {π} in
variable {π} in
variable {π} in
Lean source · statement
theorem const_mem_range {A k : Type*} [CommRing A] [CommRing k]
    (σ : A →+* B) (red : A →+* k) (ι : k →+* C) (hcompat : ∀ a : A, π (σ a) = ι (red a))
    (hred : Function.Surjective red) (c : k) : ι c ∈ π.range
theorem

eq_zero_of_X_sub_C_dvd_C

L1473 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.eq_zero_of_X_sub_C_dvd_C
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open 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]
Lean source · statement
theorem eq_zero_of_X_sub_C_dvd_C {R : Type*} [CommRing R] {a₀ a : R}
    (h : (Polynomial.X - Polynomial.C a₀) ∣ Polynomial.C a) : a = 0
theorem

exists_place_centre_comap_eq

L1479 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.exists_place_centre_comap_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open 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]
Lean source · statement
theorem exists_place_centre_comap_eq [IsAlgClosed K] (A : ValuationSubring K) {j : F}
    (hj : Transcendental K j) [FiniteDimensional K⟮j⟯ F] [Algebra.IsSeparable K⟮j⟯ F]
    {B : Subring F} (hconst : ∀ a : A, algebraMap K F a ∈ B) (hjB : j ∈ B)
    (hint : ∀ b : B,
      IsIntegral (Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {j})) (b : F))
    (𝔮 : Ideal B) [𝔮.IsPrime]
    (h𝔮A : ∀ a : A, (⟨algebraMap K F a, hconst a⟩ : B) ∈ 𝔮 ↔ a ∈ IsLocalRing.maximalIdeal A)
    (a₀ : A) (hja : (⟨j, hjB⟩ : B) - ⟨algebraMap K F a₀, hconst a₀⟩ ∈ 𝔮) :
    ∃ (w : Place K F) (hB : B ≤ w.compSubring A),
      (w.centre A).comap (Subring.inclusion hB) = 𝔮 ∧ w.HasValueAt j a₀
theorem

finite_residueField_of_adjoin_simple_eq_top_of_mem

L1609 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.finite_residueField_of_adjoin_simple_eq_top_of_mem
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
Lean source · statement
theorem finite_residueField_of_adjoin_simple_eq_top_of_mem {x : E} (hx : Transcendental K x)
    (htop : IntermediateField.adjoin K ({x} : Set E) = ⊤) (v : Place K E)
    (hxv : x ∈ v.toValuationSubring) : Module.Finite K v.ResidueField
theorem

adjoin_simple_inv_eq

L1695 ↗
IntermediateField.adjoin_simple_inv_eq
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
Lean source · statement
theorem _root_.IntermediateField.adjoin_simple_inv_eq (x : E) :
    IntermediateField.adjoin K ({x⁻¹} : Set E) = IntermediateField.adjoin K ({x} : Set E)
theorem

finite_residueField_of_adjoin_simple_eq_top

L1705 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.finite_residueField_of_adjoin_simple_eq_top
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
Lean source · statement
theorem finite_residueField_of_adjoin_simple_eq_top {x : E} (hx : Transcendental K x)
    (htop : IntermediateField.adjoin K ({x} : Set E) = ⊤) (v : Place K E) :
    Module.Finite K v.ResidueField
theorem

finiteResidue_of_adjoin_simple_eq_top

L1717 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.finiteResidue_of_adjoin_simple_eq_top
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K E : Type*} [Field K] [Field E] [Algebra K E]
Lean source · statement
theorem finiteResidue_of_adjoin_simple_eq_top {x : E} (hx : Transcendental K x)
    (htop : IntermediateField.adjoin K ({x} : Set E) = ⊤) (v : Place K E) : v.FiniteResidue
theorem

eq_of_forall_mem_nonunits_iff

L1732 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.ValuationSubring.eq_of_forall_mem_nonunits_iff
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
namespace ValuationSubring
open _root_.ValuationSubring
open _root_.ValuationSubring
variable {F : Type*} [Field F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
Lean source · statement
theorem eq_of_forall_mem_nonunits_iff {O₁ O₂ : ValuationSubring F}
    (h₁ : ∀ r : R, algebraMap R F r ∈ O₁) (hne₁ : O₁ ≠ ⊤)
    (h₂ : ∀ r : R, algebraMap R F r ∈ O₂) (hne₂ : O₂ ≠ ⊤)
    (h : ∀ r : R, algebraMap R F r ∈ O₁.nonunits ↔ algebraMap R F r ∈ O₂.nonunits) :
    O₁ = O₂
theorem

eq_of_forall_mem_nonunits_iff

L1757 ↗
AlgebraicCurve.Place.eq_of_forall_mem_nonunits_iff
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open 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]
Lean source · statement
theorem _root_.AlgebraicCurve.Place.eq_of_forall_mem_nonunits_iff (R : Type*) [CommRing R]
  [IsDedekindDomain R]
    [Algebra R F] [IsFractionRing R F] {v₁ v₂ : Place K F}
    (h₁ : ∀ r : R, algebraMap R F r ∈ v₁.toValuationSubring)
    (h₂ : ∀ r : R, algebraMap R F r ∈ v₂.toValuationSubring)
    (h : ∀ r : R, algebraMap R F r ∈ v₁.toValuationSubring.nonunits ↔
      algebraMap R F r ∈ v₂.toValuationSubring.nonunits) : v₁ = v₂
theorem

eq_of_forall_mem_nonunits_iff_of_surjective

L1768 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.eq_of_forall_mem_nonunits_iff_of_surjective
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open 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]
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem eq_of_forall_mem_nonunits_iff_of_surjective (R : Type*) [CommRing R]
  [IsDedekindDomain R]
    [Algebra R F] [IsFractionRing R F] {v₁ v₂ : Place K F}
    (h₁ : ∀ r : R, algebraMap R F r ∈ v₁.toValuationSubring)
    (h₂ : ∀ r : R, algebraMap R F r ∈ v₂.toValuationSubring)
    {ι : Type*} (f : ι → F) (hsurj : ∀ r : R, ∃ i, f i = algebraMap R F r)
    (h : ∀ i, f i ∈ v₁.toValuationSubring.nonunits ↔ f i ∈ v₂.toValuationSubring.nonunits) :
    v₁ = v₂
theorem

integralClosure_adjoin_le_of_forall_isIntegral_mem

L1782 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.integralClosure_adjoin_le_of_forall_isIntegral_mem
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open 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]
open _root_.AlgebraicCurve.Place
variable (K) in
Lean source · statement
theorem integralClosure_adjoin_le_of_forall_isIntegral_mem {j : F} {S : Subring F}
    (hK : ∀ c : K, algebraMap K F c ∈ S) (hj : j ∈ S)
    (hS : ∀ x : F, (∃ p : Polynomial S, p.Monic ∧ Polynomial.eval₂ S.subtype x p = 0) → x ∈ S)
    (r : integralClosure (Algebra.adjoin K ({j} : Set F)) F) : (r : F) ∈ S
theorem

exists_eq_of_integralClosure_adjoin

L1796 ↗
AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring.AlgebraicCurve.Place.exists_eq_of_integralClosure_adjoin
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open 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]
open _root_.AlgebraicCurve.Place
variable (K) in
Lean source · statement
theorem exists_eq_of_integralClosure_adjoin {j : F} {B : Type*} (π : B → F) {S : Subring F}
    (hrange : ∀ x, x ∈ S ↔ ∃ b, π b = x)
    (hK : ∀ c : K, algebraMap K F c ∈ S) (hj : j ∈ S)
    (hS : ∀ x : F, (∃ p : Polynomial S, p.Monic ∧ Polynomial.eval₂ S.subtype x p = 0) → x ∈ S)
    (r : integralClosure (Algebra.adjoin K ({j} : Set F)) F) :
    ∃ b, π b = algebraMap (integralClosure (Algebra.adjoin K ({j} : Set F)) F) F r
theorem

exists_of_isPrime_over_valuationSubring

L1808 ↗
AlgebraicCurve.Place.exists_of_isPrime_over_valuationSubring
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_of_isPrime_over_valuationSubring
open Polynomial
noncomputable section
open IsLocalRing
noncomputable section
open IsLocalRing IsDedekindDomain
open IsLocalRing Polynomial
noncomputable section
open scoped IntermediateField.algebraAdjoinAdjoin
open IntermediateField Polynomial
open Polynomial
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_of_isPrime_over_valuationSubring {K F : Type*} [Field K]
  [Field F]
    [Algebra K F] [IsAlgClosed K] (A : ValuationSubring K) {j : F} (hj : Transcendental K j)
    [FiniteDimensional (IntermediateField.adjoin K ({j} : Set F)) F]
    [Algebra.IsSeparable (IntermediateField.adjoin K ({j} : Set F)) F]
    {B : Subring F} (hconst : ∀ a : A, algebraMap K F a ∈ B) (hjB : j ∈ B)
    (hint : ∀ b : B,
      IsIntegral (Subring.closure (Set.range ((algebraMap K F).comp A.subtype) ∪ {j})) (b : F))
    (𝔮 : Ideal B) [𝔮.IsPrime]
    (h𝔮A : ∀ a : A, a ∈ IsLocalRing.maximalIdeal A → (⟨algebraMap K F a, hconst a⟩ : B) ∈ 𝔮)
    (a₀ : A) (hja : (⟨j, hjB⟩ : B) - ⟨algebraMap K F a₀, hconst a₀⟩ ∈ 𝔮) :
    ∃ w : AlgebraicCurve.Place K F,
      0 < w.ord (j - algebraMap K F a₀) ∧
      ∀ b : B, b ∈ 𝔮 ↔ ∃ a : A, a ∈ IsLocalRing.maximalIdeal A ∧
        ((b : F) - algebraMap K F a) ∈ w.toValuationSubring.nonunits

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