NYLL
Module

Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero.lean

Nyll.AlgebraicCurves.Places.Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero
6 declarations indexed from sourceView source ↗

Module documentation

Place ramification Index Along eq one of ord eval derivative eq zero

Imports1
Imported by1

Declarations

theorem

ord_nonneg_of_mem

L36 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero.AlgebraicCurve.Place.SimpleRootEngineAux.ord_nonneg_of_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace SimpleRootEngineAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F)
Lean source · statement
theorem ord_nonneg_of_mem {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L51 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero.AlgebraicCurve.Place.SimpleRootEngineAux.mem_of_ord_nonneg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace SimpleRootEngineAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F)
Lean source · statement
theorem mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring
theorem

isUnit_of_ord_eq_zero

L59 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero.AlgebraicCurve.Place.SimpleRootEngineAux.isUnit_of_ord_eq_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace SimpleRootEngineAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F)
Lean source · statement
theorem isUnit_of_ord_eq_zero (y : v.toValuationSubring) (hy0 : y ≠ 0) (h : v.ord (y : F) = 0) :
    IsUnit y
theorem

residue_eq_zero_of_ord_pos

L75 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero.AlgebraicCurve.Place.SimpleRootEngineAux.residue_eq_zero_of_ord_pos
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace SimpleRootEngineAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F)
Lean source · statement
theorem residue_eq_zero_of_ord_pos (y : v.toValuationSubring) (h : 0 < v.ord (y : F)) :
    IsLocalRing.residue v.toValuationSubring y = 0
theorem

ord_eq_zero_of_residue_ne_zero

L83 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero.AlgebraicCurve.Place.SimpleRootEngineAux.ord_eq_zero_of_residue_ne_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero
open Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace SimpleRootEngineAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F)
Lean source · statement
theorem ord_eq_zero_of_residue_ne_zero (y : v.toValuationSubring)
    (h : IsLocalRing.residue v.toValuationSubring y ≠ 0) :
    v.ord (y : F) = 0 ∧ (y : F) ≠ 0
theorem

ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero

L96 ↗
AlgebraicCurve.Place.ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero
open Polynomial
open _root_.AlgebraicCurve AlgebraicCurve _root_.AlgebraicCurve.Place AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndexAlong_eq_one_of_ord_eval_derivative_eq_zero
    {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (w : AlgebraicCurve.Place K F')
    (z : F') (hgen : ∀ x : F', ∃ p : Polynomial F, Polynomial.eval₂ φ.toRingHom z p = x)
    (g : Polynomial F) (hg : g.Monic)
    (hgO : ∀ i : ℕ, 0 ≤ (w.restrictAlong φ hφ).ord (g.coeff i))
    (hgz : Polynomial.eval₂ φ.toRingHom z g = 0)
    (hne : Polynomial.eval₂ φ.toRingHom z (Polynomial.derivative g) ≠ 0)
    (hsimple : w.ord (Polynomial.eval₂ φ.toRingHom z (Polynomial.derivative g)) = 0) :
    AlgebraicCurve.Place.ramificationIndexAlong φ w = 1

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