NYLL
Module

Place_ramificationIndex_eq_one_of_forall_dvd_ord.lean

Nyll.AlgebraicCurves.Places.Place_ramificationIndex_eq_one_of_forall_dvd_ord
27 declarations indexed from sourceView source ↗

Module documentation

Place ramification Index eq one of forall dvd ord

Imports14
Imported by2

Declarations

theorem

mem_of_ord_nonneg

L46 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.Place.mem_of_ord_nonneg
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable (v : 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_mk_of_ord_eq_zero

L54 ↗
AlgebraicCurve.Place.isUnit_mk_of_ord_eq_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isUnit_mk_of_ord_eq_zero {f : F} (hf : f ≠ 0) (h :
  v.ord f = 0) :
    IsUnit (⟨f, v.mem_of_ord_nonneg hf h.ge⟩ : v.toValuationSubring)
theorem

residue_ne_zero_of_ord_eq_zero

L66 ↗
AlgebraicCurve.Place.residue_ne_zero_of_ord_eq_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.residue_ne_zero_of_ord_eq_zero {f : F} (hf : f ≠ 0) (h
  : v.ord f = 0) :
    residue v.toValuationSubring (⟨f, v.mem_of_ord_nonneg hf h.ge⟩ : v.toValuationSubring)
      ≠ 0
theorem

evalAt_ne_zero

L73 ↗
AlgebraicCurve.Place.evalAt_ne_zero
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_ne_zero (hv : v.IsRational) {f : F} (hf : f ≠
  0) (h : v.ord f = 0) :
    v.evalAt f ≠ 0
theorem

evalAt_algebraMap

L82 ↗
AlgebraicCurve.Place.evalAt_algebraMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_algebraMap (a : K) : v.evalAt (algebraMap K F
  a) = a
theorem

forall_pow_ne_mul_pow

L114 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.forall_pow_ne_mul_pow
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section Swap
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} {f : F} {α : L}
Lean source · statement
theorem forall_pow_ne_mul_pow (hf : ∀ g : F, g ^ p ≠ f) {h : F} (hh : h ≠ 0) :
    ∀ g : F, g ^ p ≠ f * h ^ p
theorem

mul_algebraMap_pow_eq

L120 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.mul_algebraMap_pow_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section Swap
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} {f : F} {α : L}
Lean source · statement
theorem mul_algebraMap_pow_eq (hα : α ^ p = algebraMap F L f) (h : F) :
    (α * algebraMap F L h) ^ p = algebraMap F L (f * h ^ p)
theorem

adjoin_mul_algebraMap_eq_top

L124 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.adjoin_mul_algebraMap_eq_top
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section Swap
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} {f : F} {α : L}
Lean source · statement
theorem adjoin_mul_algebraMap_eq_top (htop : F⟮α⟯ = ⊤) {h : F} (hh : h ≠ 0) :
    F⟮α * algebraMap F L h⟯ = ⊤
theorem

not_mem_range_of_pow_eq

L132 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.not_mem_range_of_pow_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section Swap
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} {f : F} {α : L}
Lean source · statement
theorem not_mem_range_of_pow_eq (hf : ∀ g : F, g ^ p ≠ f) (hα : α ^ p = algebraMap F L f) :
    α ∉ Set.range (algebraMap F L)
theorem

sub_algebraMap_ne_zero

L138 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.sub_algebraMap_ne_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section Swap
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} {f : F} {α : L}
Lean source · statement
theorem sub_algebraMap_ne_zero (hf : ∀ g : F, g ^ p ≠ f) (hα : α ^ p = algebraMap F L f)
    (c : F) : α - algebraMap F L c ≠ 0
theorem

irreducible_X_pow_sub_C

L145 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.irreducible_X_pow_sub_C
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section Pure
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} [hp : Fact p.Prime] {f : F} {α : L}
Lean source · statement
theorem irreducible_X_pow_sub_C (hf : ∀ g : F, g ^ p ≠ f) : Irreducible (X ^ p - C f)
theorem

ne_zero_of_forall_pow_ne

L147 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.ne_zero_of_forall_pow_ne
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section Pure
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} [hp : Fact p.Prime] {f : F} {α : L}
Lean source · statement
theorem ne_zero_of_forall_pow_ne (hf : ∀ g : F, g ^ p ≠ f) : f ≠ 0
theorem

isIntegral_of_pow_eq

L150 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.isIntegral_of_pow_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section Pure
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} [hp : Fact p.Prime] {f : F} {α : L}
Lean source · statement
theorem isIntegral_of_pow_eq (hα : α ^ p = algebraMap F L f) : IsIntegral F α
theorem

minpoly_eq_of_pow_eq

L153 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.minpoly_eq_of_pow_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section Pure
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} [hp : Fact p.Prime] {f : F} {α : L}
Lean source · statement
theorem minpoly_eq_of_pow_eq (hf : ∀ g : F, g ^ p ≠ f) (hα : α ^ p = algebraMap F L f) :
    minpoly F α = X ^ p - C f
theorem

norm_root_sub_algebraMap

L159 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.norm_root_sub_algebraMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section Pure
variable {F L : Type*} [Field F] [Field L] [Algebra F L]
variable {p : ℕ} [hp : Fact p.Prime] {f : F} {α : L}
Lean source · statement
theorem norm_root_sub_algebraMap (hf : ∀ g : F, g ^ p ≠ f) (hα : α ^ p = algebraMap F L f)
    (htop : F⟮α⟯ = ⊤) (c : F) :
    Algebra.norm F (α - algebraMap F L c) = (-1) ^ p * (c ^ p - f)
theorem

ord_norm_root_sub_algebraMap

L195 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.KummerCover.ord_norm_root_sub_algebraMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace KummerCover
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
section OrdNorm
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra F L]
variable {p : ℕ} [hp : Fact p.Prime] {f : F} {α : L}
Lean source · statement
theorem ord_norm_root_sub_algebraMap (v : Place K F) (hf : ∀ g : F, g ^ p ≠ f)
    (hα : α ^ p = algebraMap F L f) (htop : F⟮α⟯ = ⊤) (c : F) :
    v.ord (Algebra.norm F (α - algebraMap F L c)) = v.ord (f - c ^ p)
theorem

ord_le_ord_norm_of_forall_ord_nonneg

L213 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.Place.ord_le_ord_norm_of_forall_ord_nonneg
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
Lean source · statement
theorem ord_le_ord_norm_of_forall_ord_nonneg (v : Place K F) {x : L} (hx : x ≠ 0)
    (hnonneg : ∀ w' ∈ v.fiberOver L, 0 ≤ w'.ord x) {w : Place K L} (hw : w ∈ v.fiberOver L) :
    w.ord x ≤ v.ord (Algebra.norm F x)
theorem

ord_le_ord_norm_of_forall_ord_nonneg'

L223 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.Place.ord_le_ord_norm_of_forall_ord_nonneg'
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
Lean source · statement
theorem ord_le_ord_norm_of_forall_ord_nonneg' {x : L} (hx : x ≠ 0) (w : Place K L)
    (hnonneg : ∀ w' : Place K L, w'.restrict F = w.restrict F → 0 ≤ w'.ord x) :
    w.ord x ≤ (w.restrict F).ord (Algebra.norm F x)
theorem

residue_mk_algebraMap

L232 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.Place.residue_mk_algebraMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
section ResidueGeomSum
open IsLocalRing
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem residue_mk_algebraMap (a : K) :
    residue v.toValuationSubring ⟨algebraMap K F a, v.algebraMap_mem' a⟩
      = algebraMap K v.ResidueField a
theorem

residue_geom_sum₂_of_residue_eq

L236 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.Place.residue_geom_sum₂_of_residue_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
section ResidueGeomSum
open IsLocalRing
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem residue_geom_sum₂_of_residue_eq {x y : F} (hx : x ∈ v.toValuationSubring)
    (hy : y ∈ v.toValuationSubring) {r : v.ResidueField}
    (hxr : residue v.toValuationSubring ⟨x, hx⟩ = r)
    (hyr : residue v.toValuationSubring ⟨y, hy⟩ = r) (n : ℕ)
    (hS : (∑ j ∈ Finset.range n, x ^ j * y ^ (n - 1 - j)) ∈ v.toValuationSubring) :
    residue v.toValuationSubring ⟨∑ j ∈ Finset.range n, x ^ j * y ^ (n - 1 - j), hS⟩
      = n * r ^ (n - 1)
theorem

exists_ord_mul_pow_eq_zero

L256 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.Place.exists_ord_mul_pow_eq_zero
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
section Normalize
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_ord_mul_pow_eq_zero (v : Place K F) {p : ℕ} {f : F} (hf0 : f ≠ 0)
    (hord : (p : ℤ) ∣ v.ord f) : ∃ h : F, h ≠ 0 ∧ v.ord (f * h ^ p) = 0
theorem

ord_eq_zero_of_pow_eq_of_ord_restrict_eq_zero

L273 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.Place.ord_eq_zero_of_pow_eq_of_ord_restrict_eq_zero
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
section FibreUnit
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [Algebra.IsIntegral F L]
Lean source · statement
theorem ord_eq_zero_of_pow_eq_of_ord_restrict_eq_zero (w : Place K L) {p : ℕ} (hp : p ≠ 0)
    {f₁ : F} {β : L} (hβ : β ^ p = algebraMap F L f₁) (h0 : (w.restrict F).ord f₁ = 0) :
    w.ord β = 0
theorem

ord_eq_zero_iff_isUnit

L284 ↗
AlgebraicCurve.Place.ord_eq_zero_iff_isUnit
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
section OrdResidueKit
open IsLocalRing
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_eq_zero_iff_isUnit {g : F} (hg : g ≠ 0) (hmem : g
  ∈ v.toValuationSubring) :
    v.ord g = 0 ↔ IsUnit (⟨g, hmem⟩ : v.toValuationSubring)
theorem

ord_eq_zero_of_residue_ne_zero

L291 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.Place.ord_eq_zero_of_residue_ne_zero
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
section OrdResidueKit
open IsLocalRing
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_eq_zero_of_residue_ne_zero {g : F} (hg : g ≠ 0) (hmem : g ∈
  v.toValuationSubring)
    (hres : residue v.toValuationSubring ⟨g, hmem⟩ ≠ 0) :
    v.ord g = 0
theorem

one_le_ord_of_residue_eq_zero

L302 ↗
AlgebraicCurve.Place.one_le_ord_of_residue_eq_zero
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
section OrdResidueKit
open IsLocalRing
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.one_le_ord_of_residue_eq_zero {g : F} (hg : g ≠ 0)
  (hmem : g ∈ v.toValuationSubring)
    (hres : residue v.toValuationSubring ⟨g, hmem⟩ = 0) :
    1 ≤ v.ord g
theorem

one_le_ord_sub_evalAt

L314 ↗
AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.Place.one_le_ord_sub_evalAt
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place hiding mem_of_ord_nonneg
variable {K F L : Type*} [Field K] [Field F] [Field L] [Algebra K F] [Algebra K L] [Algebra F L]
  [IsScalarTower K F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] [CharZero F]
section OrdResidueKit
open IsLocalRing
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem one_le_ord_sub_evalAt (hv : v.IsRational) {f : F} (hf : f ≠ 0) (hord : v.ord f = 0)
    (hfc : f ≠ algebraMap K F (v.evalAt f)) :
    1 ≤ v.ord (f - algebraMap K F (v.evalAt f))
theorem

ramificationIndex_eq_one_of_forall_dvd_ord

L355 ↗
AlgebraicCurve.Place.ramificationIndex_eq_one_of_forall_dvd_ord
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders
open IsLocalRing
open Polynomial IntermediateField
open _root_.AlgebraicCurve hiding Place.mem_of_ord_nonneg in
open _root_.AlgebraicCurve.Place
  hiding mem_of_ord_nonneg in
open
  _root_.AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.PlaceUnramifiedDivisibleOrders.AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndex_eq_one_of_forall_dvd_ord {K F L : Type*}
  [Field K] [Field F] [Field L]
    [Algebra K F] [Algebra K L] [Algebra F L] [IsScalarTower K F L]
    [FiniteDimensional F L] [Algebra.IsSeparable F L]
    {p : ℕ} [Fact p.Prime] {f : F} {α : L} [CharZero F]
    (hf : ∀ g : F, g ^ p ≠ f)
    (hα : α ^ p = algebraMap F L f) (htop : F⟮α⟯ = ⊤)
    (hord : ∀ v : Place K F, (p : ℤ) ∣ v.ord f)
    (w : Place K L) (hw_rat : w.IsRational) :
    w.ramificationIndex F = 1

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