NYLL
Module

Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.lean

Nyll.AlgebraicCurves.Places.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
65 declarations indexed from sourceView source ↗

Module documentation

Place exists Unique sub algebra Map mem nonunits of eval pderiv ne zero

Imports2
Imported by1

Declarations

theorem

sub_C_eval_mem_span

L33 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.sub_C_eval_mem_span
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Poly
variable {K : Type*} [Field K]
Lean source · full declaration
theorem sub_C_eval_mem_span {σ : Type*} (p : σ → K) (G : MvPolynomial σ K) :
    G - C (eval p G) ∈ Ideal.span (Set.range fun i => (X i - C (p i) : MvPolynomial σ K)) := by
  induction G using MvPolynomial.induction_on with
  | C c => simp
  | add G H hG hH =>
    have : G + H - C (eval p (G + H)) = (G - C (eval p G)) + (H - C (eval p H)) := by
      simp only [map_add]; ring
    rw [this]
    exact Ideal.add_mem _ hG hH
  | mul_X G i hG =>
    have : G * X i - C (eval p (G * X i)) =
        (G - C (eval p G)) * X i + C (eval p G) * (X i - C (p i)) := by
      simp only [map_mul, eval_X]; ring
    rw [this]
    exact Ideal.add_mem _ (Ideal.mul_mem_right _ _ hG)
      (Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨i, rfl⟩))
theorem

aeval_self_eq_eval

L50 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.aeval_self_eq_eval
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Poly
variable {K : Type*} [Field K]
Lean source · statement
theorem aeval_self_eq_eval {σ : Type*} (p : σ → K) (G : MvPolynomial σ K) : aeval p G = eval p G
def

subY

L55 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.subY
Documentation

Substitution of the first coordinate by a scalar, retaining the second as the polynomial variable.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Poly
variable {K : Type*} [Field K]
Lean source · statement
def subY (a : K) : MvPolynomial (Fin 2) K →ₐ[K] Polynomial K
theorem

eval_subY

L58 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.eval_subY
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Poly
variable {K : Type*} [Field K]
Lean source · statement
theorem eval_subY (a b : K) (G : MvPolynomial (Fin 2) K) :
    (subY a G).eval b = eval ![a, b] G
theorem

derivative_subY

L69 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.derivative_subY
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Poly
variable {K : Type*} [Field K]
Lean source · statement
theorem derivative_subY (a : K) (G : MvPolynomial (Fin 2) K) :
    Polynomial.derivative (subY a G) = subY a (pderiv 1 G)
def

ιY

L83 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.ιY
Documentation

The embedding of univariate polynomials using the second coordinate variable.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Poly
variable {K : Type*} [Field K]
Lean source · statement
def ιY : Polynomial K →ₐ[K] MvPolynomial (Fin 2) K
theorem

sub_ιY_subY_mem_span

L85 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.sub_ιY_subY_mem_span
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Poly
variable {K : Type*} [Field K]
Lean source · statement
theorem sub_ιY_subY_mem_span (a : K) (G : MvPolynomial (Fin 2) K) :
    G - ιY (subY a G) ∈ Ideal.span ({X 0 - C a} : Set (MvPolynomial (Fin 2) K))
def

A

L116 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.A
Documentation

The coordinate subalgebra generated by the two selected elements of the function field.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Setup
variable (K : Type*) {F : Type*} [Field K] [Field F] [Algebra K F] (x y : F)
Lean source · statement
def A : Subalgebra K F
def

θ

L119 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.θ
Documentation

The polynomial evaluation map with codomain restricted to the coordinate subalgebra.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Setup
variable (K : Type*) {F : Type*} [Field K] [Field F] [Algebra K F] (x y : F)
Lean source · statement
def θ : MvPolynomial (Fin 2) K →ₐ[K] A K x y
theorem

θ_surjective

L121 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.θ_surjective
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Setup
variable (K : Type*) {F : Type*} [Field K] [Field F] [Algebra K F] (x y : F)
Lean source · statement
theorem θ_surjective : Function.Surjective (θ K x y)
theorem

coe_θ

L123 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.coe_θ
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Setup
variable (K : Type*) {F : Type*} [Field K] [Field F] [Algebra K F] (x y : F)
Lean source · statement
theorem coe_θ (G : MvPolynomial (Fin 2) K) : ((θ K x y G : A K x y) : F) = aeval
  ![x, y] G
theorem

ker_θ

L126 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.ker_θ
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Setup
variable (K : Type*) {F : Type*} [Field K] [Field F] [Algebra K F] (x y : F)
Lean source · statement
theorem ker_θ : RingHom.ker (θ K x y) = RingHom.ker (aeval ![x, y] : MvPolynomial (Fin 2) K →ₐ[K]
  F)
def

ev

L133 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.ev
Documentation

Evaluation on the coordinate algebra at a point satisfying its defining equation.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Setup
variable (K : Type*) {F : Type*} [Field K] [Field F] [Algebra K F] (x y : F)
variable {K x y} {f : MvPolynomial (Fin 2) K} {a b : K}
Lean source · statement
def ev (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
    (hab : eval ![a, b] f = 0) : A K x y →ₐ[K] K
theorem

ev_θ

L153 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.ev_θ
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Setup2
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
theorem ev_θ (G : MvPolynomial (Fin 2) K) : ev hker hab (θ K x y G) = eval ![a, b] G
theorem

sub_algebraMap_ev_mem

L164 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.sub_algebraMap_ev_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Setup2
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
theorem sub_algebraMap_ev_mem (z : A K x y) :
    z - algebraMap K (A K x y) (ev hker hab z) ∈
      Ideal.span ({θ K x y (X 0 - C a), θ K x y (X 1 - C b)} : Set (A K x y))
theorem

ev_X0_sub

L181 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.ev_X0_sub
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Setup2
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
theorem ev_X0_sub : ev hker hab (θ K x y (X 0 - C a)) = 0
theorem

ev_X1_sub

L182 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.ev_X1_sub
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Setup2
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
theorem ev_X1_sub : ev hker hab (θ K x y (X 1 - C b)) = 0
def

𝔮

L194 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.𝔮
Documentation

The maximal ideal of the coordinate algebra defined by evaluation at the selected point.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
def 𝔮 : Ideal (A K x y)
instance

𝔮_isPrime

L196 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.𝔮_isPrime
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
instance 𝔮_isPrime : (𝔮 hker hab).IsPrime
theorem

mem_𝔮

L198 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.mem_𝔮
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
theorem mem_𝔮 (z : A K x y) : z ∈ 𝔮 hker hab ↔ ev hker hab z = 0
theorem

θ_X0_sub_mem

L200 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.θ_X0_sub_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
theorem θ_X0_sub_mem : θ K x y (X 0 - C a) ∈ 𝔮 hker hab
theorem

θ_X1_sub_mem

L202 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.θ_X1_sub_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
theorem θ_X1_sub_mem : θ K x y (X 1 - C b) ∈ 𝔮 hker hab
theorem

𝔮_eq_span

L205 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.𝔮_eq_span
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
theorem 𝔮_eq_span : 𝔮 hker hab = Ideal.span ({θ K x y (X 0 - C a), θ K x y (X 1 - C b)} : Set (A K
  x y))
theorem

primeCompl_le_nonZeroDivisors

L216 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.primeCompl_le_nonZeroDivisors
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
Lean source · statement
theorem primeCompl_le_nonZeroDivisors : (𝔮 hker hab).primeCompl ≤ nonZeroDivisors (A K x y)
theorem

isFractionRing_A

L225 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.isFractionRing_A
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
include hF in
Lean source · statement
theorem isFractionRing_A : IsFractionRing (A K x y) F
instance

isNoetherianRing_A

L239 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.isNoetherianRing_A
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
instance isNoetherianRing_A : IsNoetherianRing (A K x y)
def

O

L250 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.O
Documentation

The local coordinate subalgebra inside the function field at the selected point.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
def O : Subalgebra (A K x y) F
instance

isLocalization_O

L254 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.isLocalization_O
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
instance isLocalization_O : IsLocalization.AtPrime (O hker hab hF) (𝔮 hker hab)
instance

isLocalRing_O

L258 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.isLocalRing_O
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
instance isLocalRing_O : IsLocalRing (O hker hab hF)
instance

isNoetherianRing_O

L261 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.isNoetherianRing_O
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
instance isNoetherianRing_O : IsNoetherianRing (O hker hab hF)
theorem

maximalIdeal_O

L264 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.maximalIdeal_O
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
theorem maximalIdeal_O : IsLocalRing.maximalIdeal (O hker hab hF) = (𝔮 hker hab).map (algebraMap (A
  K x y) (O hker hab hF))
def

tO

L269 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.tO
Documentation

The first coordinate difference from the selected point, in the local coordinate algebra.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
def tO : O hker hab hF
def

sO

L271 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.sO
Documentation

The second coordinate difference from the selected point, in the local coordinate algebra.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
def sO : O hker hab hF
theorem

coe_tO

L273 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.coe_tO
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
theorem coe_tO : ((tO hker hab hF : O hker hab hF) : F) = x - algebraMap K F a
theorem

coe_sO

L276 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.coe_sO
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
theorem coe_sO : ((sO hker hab hF : O hker hab hF) : F) = y - algebraMap K F b
theorem

maximalIdeal_eq_span_pair

L280 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.maximalIdeal_eq_span_pair
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Local
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hab : eval ![a, b] f = 0)
variable (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
Lean source · statement
theorem maximalIdeal_eq_span_pair :
    IsLocalRing.maximalIdeal (O hker hab hF) = Ideal.span {tO hker hab hF, sO hker hab hF}
theorem

mk_mem_maximalIdeal

L289 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.mk_mem_maximalIdeal
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section LocalGeneric
Lean source · statement
theorem mk_mem_maximalIdeal {R : Type*} [CommRing R] [IsLocalRing R] {I : Ideal R}
    [IsLocalRing (R ⧸ I)] (hI : I ≤ IsLocalRing.maximalIdeal R) {m : R}
    (hm : m ∈ IsLocalRing.maximalIdeal R) : Ideal.Quotient.mk I m ∈ IsLocalRing.maximalIdeal (R ⧸
      I)
theorem

isUnit_add_mul_of_mem_maximalIdeal

L306 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.isUnit_add_mul_of_mem_maximalIdeal
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section LocalGeneric
Lean source · statement
theorem isUnit_add_mul_of_mem_maximalIdeal {S : Type*} [CommRing S] [IsLocalRing S] {u m : S} (z :
  S)
    (hu : IsUnit u) (hm : m ∈ IsLocalRing.maximalIdeal S) : IsUnit (u + m * z)
theorem

x_ne_algebraMap

L330 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.x_ne_algebraMap
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
include hker hab hsmooth in
Lean source · statement
theorem x_ne_algebraMap : x ≠ algebraMap K F a
theorem

θ_f

L349 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.θ_f
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
include hf in
Lean source · statement
theorem θ_f : θ K x y f = 0
theorem

tO_mem

L351 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.tO_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem tO_mem : tO hker hab hF ∈ IsLocalRing.maximalIdeal (O hker hab hF)
theorem

sO_mem

L354 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.sO_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem sO_mem : sO hker hab hF ∈ IsLocalRing.maximalIdeal (O hker hab hF)
theorem

sO_mem_span_tO

L358 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.sO_mem_span_tO
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
include hf hsmooth in
Lean source · statement
theorem sO_mem_span_tO : sO hker hab hF ∈ Ideal.span {tO hker hab hF}
theorem

maximalIdeal_eq_span

L424 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.maximalIdeal_eq_span
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
include hf hsmooth in
Lean source · statement
theorem maximalIdeal_eq_span :
    IsLocalRing.maximalIdeal (O hker hab hF) = Ideal.span {tO hker hab hF}
theorem

tO_ne_zero

L434 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.tO_ne_zero
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
include hsmooth in
Lean source · statement
theorem tO_ne_zero : tO hker hab hF ≠ 0
theorem

maximalIdeal_isPrincipal

L440 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.maximalIdeal_isPrincipal
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
include hf hsmooth in
Lean source · statement
theorem maximalIdeal_isPrincipal : (IsLocalRing.maximalIdeal (O hker hab hF)).IsPrincipal
theorem

isPrincipalIdealRing_O

L444 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.isPrincipalIdealRing_O
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
include hf hsmooth in
Lean source · statement
theorem isPrincipalIdealRing_O : IsPrincipalIdealRing (O hker hab hF)
theorem

valuationRing_O

L448 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.valuationRing_O
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section Principal
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
include hf hsmooth in
Lean source · statement
theorem valuationRing_O : ValuationRing (O hker hab hF)
theorem

coe_algebraMap_O

L464 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.coe_algebraMap_O
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem coe_algebraMap_O (z : A K x y) : ((algebraMap (A K x y) (O hker hab hF) z : O hker hab hF)
  : F) = z
theorem

mem_O_of_mem_A

L467 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.mem_O_of_mem_A
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem mem_O_of_mem_A {z : F} (hz : z ∈ A K x y) : z ∈ O hker hab hF
theorem

isFractionRing_O

L471 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.isFractionRing_O
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem isFractionRing_O : IsFractionRing (O hker hab hF) F
theorem

inv_notMem_O_of_mem_maximalIdeal

L480 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.inv_notMem_O_of_mem_maximalIdeal
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem inv_notMem_O_of_mem_maximalIdeal {o : O hker hab hF} (ho : o ∈ IsLocalRing.maximalIdeal (O
  hker hab hF))
    (ho0 : (o : F) ≠ 0) : (o : F)⁻¹ ∉ O hker hab hF
def

V

L490 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.V
Documentation

The valuation ring obtained from the local coordinate algebra at a smooth point.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
include hf hsmooth in
Lean source · full declaration
def V : ValuationSubring F where
  toSubring := (O hker hab hF).toSubring
  mem_or_inv_mem' z := by
    have := isFractionRing_O hker hF hab
    have := valuationRing_O hf hker hF hab hsmooth
    rcases (ValuationRing.iff_isInteger_or_isInteger (O hker hab hF) F).mp inferInstance z with ⟨o,
      ho⟩ | ⟨o, ho⟩
    · left; rw [← ho]; exact o.2
    · right; rw [← ho]; exact o.2
theorem

mem_V_iff

L500 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.mem_V_iff
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem mem_V_iff (z : F) : z ∈ V hf hker hF hab hsmooth ↔ z ∈ O hker hab hF
def

P

L503 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.P
Documentation

The place of the function field associated with the selected smooth point.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
include hf hsmooth in
Lean source · full declaration
def P : AlgebraicCurve.Place K F where
  toValuationSubring := V hf hker hF hab hsmooth
  algebraMap_mem' c := by
    rw [mem_V_iff, IsScalarTower.algebraMap_apply K (A K x y) F]
    exact mem_O_of_mem_A hker hF hab (algebraMap K (A K x y) c).2
  ne_top' := by
    intro htop
    have hmem : (x - algebraMap K F a)⁻¹ ∈ V hf hker hF hab hsmooth := by rw [htop]; trivial
    rw [mem_V_iff] at hmem
    have h := inv_notMem_O_of_mem_maximalIdeal hker hF hab (tO_mem hker hF hab)
      (by rw [coe_tO]; exact sub_ne_zero.mpr (x_ne_algebraMap hker hab hsmooth))
    rw [coe_tO] at h
    exact h hmem
  isPrincipalIdealRing' := isPrincipalIdealRing_O hf hker hF hab hsmooth
theorem

P_toValuationSubring_mem_iff

L518 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.P_toValuationSubring_mem_iff
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem P_toValuationSubring_mem_iff (z : F) :
    z ∈ (P hf hker hF hab hsmooth).toValuationSubring ↔ z ∈ O hker hab hF
theorem

x_sub_mem_nonunits

L521 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.x_sub_mem_nonunits
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem x_sub_mem_nonunits : x - algebraMap K F a ∈ (P hf hker hF hab
  hsmooth).toValuationSubring.nonunits
theorem

y_sub_mem_nonunits

L530 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.y_sub_mem_nonunits
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem y_sub_mem_nonunits : y - algebraMap K F b ∈ (P hf hker hF hab
  hsmooth).toValuationSubring.nonunits
theorem

mul_mem_nonunits

L541 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.mul_mem_nonunits
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem mul_mem_nonunits (W : ValuationSubring F) {c n : F} (hc : c ∈ W) (hn : n ∈ W.nonunits) :
    c * n ∈ W.nonunits
theorem

𝔮_isMaximal

L550 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.𝔮_isMaximal
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
Lean source · statement
theorem 𝔮_isMaximal : (𝔮 hker hab).IsMaximal
theorem

A_le_W

L560 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.A_le_W
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
variable (W : AlgebraicCurve.Place K F)
  (hWx : x - algebraMap K F a ∈ W.toValuationSubring.nonunits)
  (hWy : y - algebraMap K F b ∈ W.toValuationSubring.nonunits)
include hWx hWy in
Lean source · statement
theorem A_le_W : ∀ z : A K x y, (z : F) ∈ W.toValuationSubring
theorem

coe_mem_nonunits_iff

L579 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.coe_mem_nonunits_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
variable (W : AlgebraicCurve.Place K F)
  (hWx : x - algebraMap K F a ∈ W.toValuationSubring.nonunits)
  (hWy : y - algebraMap K F b ∈ W.toValuationSubring.nonunits)
include hWx hWy in
Lean source · statement
theorem coe_mem_nonunits_iff (z : A K x y) :
    (z : F) ∈ W.toValuationSubring.nonunits ↔ z ∈ 𝔮 hker hab
theorem

O_le_W

L616 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.O_le_W
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
variable (W : AlgebraicCurve.Place K F)
  (hWx : x - algebraMap K F a ∈ W.toValuationSubring.nonunits)
  (hWy : y - algebraMap K F b ∈ W.toValuationSubring.nonunits)
include hWx hWy in
Lean source · statement
theorem O_le_W : ∀ z : F, z ∈ O hker hab hF → z ∈ W.toValuationSubring
theorem

eq_P

L642 ↗
AlgebraicCurves.Places.Proofs.Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero.SmoothPointDVR.eq_P
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
namespace SmoothPointDVR
open MvPolynomial
section ThePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x y : F} {f : MvPolynomial (Fin 2) K} {a
  b : K}
  (hf : aeval ![x, y] f = 0)
  (hker : ∀ g : MvPolynomial (Fin 2) K, aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
  (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
  (hab : eval ![a, b] f = 0)
  (hsmooth : eval ![a, b] (pderiv 1 f) ≠ 0)
variable (W : AlgebraicCurve.Place K F)
  (hWx : x - algebraMap K F a ∈ W.toValuationSubring.nonunits)
  (hWy : y - algebraMap K F b ∈ W.toValuationSubring.nonunits)
include hWx hWy in
Lean source · statement
theorem eq_P : W = P hf hker hF hab hsmooth
theorem

existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero

L687 ↗
AlgebraicCurve.Place.existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
open SmoothPointDVR in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.existsUnique_sub_algebraMap_mem_nonunits_of_eval_pderiv_ne_zero
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (x y : F) (f : MvPolynomial (Fin 2) K)
    (hf : MvPolynomial.aeval ![x, y] f = 0)
    (hker : ∀ g : MvPolynomial (Fin 2) K, MvPolynomial.aeval ![x, y] g = 0 → g ∈ Ideal.span {f})
    (hF : Subfield.closure (Set.range (algebraMap K F) ∪ {x, y}) = ⊤)
    (a b : K) (hab : MvPolynomial.eval ![a, b] f = 0)
    (hsmooth : MvPolynomial.eval ![a, b] (MvPolynomial.pderiv 1 f) ≠ 0) :
    ∃! v : AlgebraicCurve.Place K F,
      x - algebraMap K F a ∈ v.toValuationSubring.nonunits ∧
        y - algebraMap K F b ∈ v.toValuationSubring.nonunits

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