NYLL
Module

Place_ramificationIndex_eq_ramificationIdx_fiberCenter.lean

Nyll.AlgebraicCurves.Places.Place_ramificationIndex_eq_ramificationIdx_fiberCenter
5 declarations indexed from sourceView source ↗

Module documentation

Place ramification Index eq ramification Idx fiber Center

Imports2
Imported by9

Declarations

theorem

eq_ord_of_addHom_of_nonneg_iff

L43 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndex.AlgebraicCurve.Place.eq_ord_of_addHom_of_nonneg_iff
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndex
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Uniqueness
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
Lean source · statement
theorem eq_ord_of_addHom_of_nonneg_iff (φ : F → ℤ)
    (hmul : ∀ x y, x ≠ 0 → y ≠ 0 → φ (x * y) = φ x + φ y)
    (hone : ∃ t, t ≠ 0 ∧ φ t = 1)
    (hiff : ∀ x, x ≠ 0 → (0 ≤ φ x ↔ x ∈ w.toValuationSubring))
    {x : F} (hx : x ≠ 0) : φ x = w.ord x
theorem

neg_log_valuation_fiberCenter_eq_ord

L118 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndex.AlgebraicCurve.Place.neg_log_valuation_fiberCenter_eq_ord
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndex
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ValuationDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem neg_log_valuation_fiberCenter_eq_ord (hw : w.restrict F = v) {x : F'} (hx : x ≠ 0) :
    -log ((fiberCenter F' v hw).valuation F' x) = w.ord x
theorem

le_ord_iff_mem_pow_fiberCenter

L157 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndex.AlgebraicCurve.Place.le_ord_iff_mem_pow_fiberCenter
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndex
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ValuationDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem le_ord_iff_mem_pow_fiberCenter (hw : w.restrict F = v)
    {c : integralClosureAt F' v} (hc : c ≠ 0) (n : ℕ) :
    (n : ℤ) ≤ w.ord (algebraMap (integralClosureAt F' v) F' c) ↔
      c ∈ (fiberCenter F' v hw).asIdeal ^ n
theorem

ramificationIndex_eq_ramificationIdx_fiberCenter

L180 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndex.AlgebraicCurve.Place.ramificationIndex_eq_ramificationIdx_fiberCenter
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndex
open _root_.AlgebraicCurves.Places.Proofs
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
section ValuationDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem ramificationIndex_eq_ramificationIdx_fiberCenter (hw : w.restrict F = v) :
    w.ramificationIndex F =
      (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
        (fiberCenter F' v hw).asIdeal
theorem

ramificationIndex_eq_ramificationIdx_fiberCenter

L216 ↗
AlgebraicCurve.Place.ramificationIndex_eq_ramificationIdx_fiberCenter
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndex
open _root_.AlgebraicCurves.Places.Proofs
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndex_eq_ramificationIdx_fiberCenter {K F F' :
  Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower
  K F F'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (v : Place K F) {w : Place K F'}
    (hw : w.restrict F = v) :
    w.ramificationIndex F = (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
      (Place.fiberCenter F' v hw).asIdeal

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