Module

Divisor_pushforwardNormFormula_of_isSeparable.lean

Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardNormFormula_of_isSeparable

70 declarations indexed from sourceView source ↗

Module documentation

Divisor pushforward Norm Formula of is Separable

Imports13

Nyll.AlgebraicCurves.Divisors.Maps
Mathlib.RingTheory.DedekindDomain.IntegralClosure
Mathlib.RingTheory.DedekindDomain.Factorization
Mathlib.Algebra.Polynomial.Lifts
Mathlib.FieldTheory.Minpoly.Field
Mathlib.RingTheory.RamificationInertia.Basic
Mathlib.RingTheory.Ideal.Norm.RelNorm
Nyll.AlgebraicCurves.FunctionFields.RelNorm_eq_pow_of_isMaximal_of_isSeparable
Nyll.AlgebraicCurves.Places.Place_ord_nonneg_of_mem
Nyll.AlgebraicCurves.Places.Place_mem_of_ord_nonneg
Nyll.AlgebraicCurves.Places.Place_mem_iff_ord_nonneg
Nyll.AlgebraicCurves.Places.Place_exists_ord_pos
Nyll.AlgebraicCurves.Places.Rational.Basic

Imported by5

theorem

ord_neg

L53 ↗

AlgebraicCurve.Place.ord_neg

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section IntegrallyClosed
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_neg (f : F) : w.ord (-f) = w.ord f

theorem

mem_of_eval_monic_eq_zero

L58 ↗

AlgebraicCurve.Place.mem_of_eval_monic_eq_zero

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section IntegrallyClosed
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_of_eval_monic_eq_zero {P : Polynomial F} (hP :
  P.Monic)
    (hcoeff : ∀ i, P.coeff i ∈ w.toValuationSubring) {x : F} (hx : P.eval x = 0) :
    x ∈ w.toValuationSubring

theorem

mem_maximalIdeal_iff_ord_pos

L75 ↗

AlgebraicCurve.Place.mem_maximalIdeal_iff_ord_pos

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section IntegrallyClosed
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.mem_maximalIdeal_iff_ord_pos {x : F} (hx : x ≠ 0)
    (hmem : x ∈ w.toValuationSubring) :
    (⟨x, hmem⟩ : w.toValuationSubring) ∈ IsLocalRing.maximalIdeal w.toValuationSubring ↔
      0 < w.ord x

theorem

aeval_mem

L96 ↗

AlgebraicCurve.Place.aeval_mem

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section SupportTransfer
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F'] [Algebra F F']
  [FiniteDimensional F F']
variable (w : Place K F')
omit [FiniteDimensional F F'] in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.aeval_mem {Q : Polynomial F} {x : F'}
    (hcoeff : ∀ i, algebraMap F F' (Q.coeff i) ∈ w.toValuationSubring)
    (hx : x ∈ w.toValuationSubring) :
    Polynomial.aeval x Q ∈ w.toValuationSubring

theorem

exists_coeff_ord_ne_zero

L105 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.exists_coeff_ord_ne_zero

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section SupportTransfer
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F'] [Algebra F F']
  [FiniteDimensional F F']
variable (w : Place K F')
open _root_.AlgebraicCurve.Place

Lean source · statement

theorem exists_coeff_ord_ne_zero {f : F'} (hf : f ≠ 0) (hford : w.ord f ≠ 0) :
    ∃ i < (minpoly F f).natDegree, (minpoly F f).coeff i ≠ 0 ∧
      w.ord (algebraMap F F' ((minpoly F f).coeff i)) ≠ 0

def

chartHom

L155 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.chartHom

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)

Lean source · statement

def chartHom (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    R →+* w.toValuationSubring

theorem

coe_chartHom

L160 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.coe_chartHom

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
omit [IsDedekindDomain R] [IsFractionRing R F] in

Lean source · statement

theorem coe_chartHom (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) (r : R) :
    (chartHom w hw r : F) = algebraMap R F r

def

center

L165 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.center

Documentation

The centre ideal obtained by pulling back the maximal ideal of the place.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in

Lean source · statement

def center (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) : Ideal R

instance

(anonymous instance)

L168 ↗

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in

Lean source · statement

instance (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    (center R w hw).IsPrime

theorem

mem_center_iff

L173 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.mem_center_iff

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
omit [IsDedekindDomain R] [IsFractionRing R F] in

Lean source · statement

theorem mem_center_iff (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) {r : R} :
    r ∈ center R w hw ↔
      (⟨algebraMap R F r, hw r⟩ : w.toValuationSubring) ∈
        IsLocalRing.maximalIdeal w.toValuationSubring

theorem

mem_center_iff_ord_pos

L179 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.mem_center_iff_ord_pos

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in

Lean source · statement

theorem mem_center_iff_ord_pos (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring)
    {r : R} (hr : r ≠ 0) :
    r ∈ center R w hw ↔ 0 < w.ord (algebraMap R F r)

theorem

inv_algebraMap_mem

L186 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.inv_algebraMap_mem

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
omit [IsDedekindDomain R] [IsFractionRing R F] in

Lean source · statement

theorem inv_algebraMap_mem (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring)
    {s : R} (hs : IsUnit (chartHom w hw s)) :
    (algebraMap R F s)⁻¹ ∈ w.toValuationSubring

theorem

center_ne_bot

L199 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.center_ne_bot

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in

Lean source · statement

theorem center_ne_bot (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    center R w hw ≠ ⊥

def

centerHeightOneSpectrum

L217 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.centerHeightOneSpectrum

Documentation

The centre regarded as a height-one prime of the base ring.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
variable (R) in

Lean source · statement

def centerHeightOneSpectrum (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    HeightOneSpectrum R

theorem

centerHeightOneSpectrum_asIdeal

L221 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
variable (R) in

Lean source · statement

theorem centerHeightOneSpectrum_asIdeal
    (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    (centerHeightOneSpectrum R w hw).asIdeal = center R w hw

theorem

valuationSubringAtPrime_centerHeightOneSpectrum_le

L225 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.valuationSubringAtPrime_centerHeightOneSpectrum_le

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
variable (R) in

Lean source · statement

theorem valuationSubringAtPrime_centerHeightOneSpectrum_le
    (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    HeightOneSpectrum.valuationSubringAtPrime F (centerHeightOneSpectrum R w hw) ≤
      w.toValuationSubring

theorem

toValuationSubring_eq_of_forall_mem

L234 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.toValuationSubring_eq_of_forall_mem

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
variable (R) in

Lean source · statement

theorem toValuationSubring_eq_of_forall_mem
    (hw : ∀ r : R, algebraMap R F r ∈ w.toValuationSubring) :
    w.toValuationSubring =
      HeightOneSpectrum.valuationSubringAtPrime F (centerHeightOneSpectrum R w hw)

theorem

finite_setOf_forall_mem_and_ord_pos

L241 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.finite_setOf_forall_mem_and_ord_pos

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Chart
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F]
variable (w : Place K F)
variable (R) in
variable (R) in

Lean source · statement

theorem finite_setOf_forall_mem_and_ord_pos {r₀ : R} (hr₀ : r₀ ≠ 0) :
    {w : Place K F | (∀ r : R, algebraMap R F r ∈ w.toValuationSubring) ∧
      0 < w.ord (algebraMap R F r₀)}.Finite

theorem

finite_setOf_restrict_eq

L267 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.finite_setOf_restrict_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section FiberFiniteness
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']

Lean source · statement

theorem finite_setOf_restrict_eq (v : Place K F) :
    {w : Place K F' | w.restrict F = v}.Finite

theorem

eq_ord_of_addHom_of_nonneg_iff

L331 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.eq_ord_of_addHom_of_nonneg_iff

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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

def

valuationSubringAlgebra

L404 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.valuationSubringAlgebra

Documentation

The valuation-subring algebra structure induced by the original field extension map.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in

Lean source · statement

def valuationSubringAlgebra (v : Place K F) : Algebra v.toValuationSubring F'

instance

(anonymous instance)

L413 ↗

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Setup
variable (v : Place K F)

Lean source · statement

instance (priority := 100) : IsScalarTower v.toValuationSubring F F'

abbrev

integralClosureAt

L418 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.integralClosureAt

Documentation

The integral closure of the base place valuation subring in the extension field.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

abbrev integralClosureAt : Type _

instance

(anonymous instance)

L420 ↗

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

instance : IsDedekindDomain (integralClosureAt F' v)

instance

(anonymous instance)

L423 ↗

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

instance : IsFractionRing (integralClosureAt F' v) F'

instance

(anonymous instance)

L426 ↗

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

instance : Module.Finite v.toValuationSubring (integralClosureAt F' v)

theorem

algebraMap_integralClosureAt_injective

L431 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.algebraMap_integralClosureAt_injective

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Setup
variable (v : Place K F)
variable (F') in
omit [Algebra K F'] [IsScalarTower K F F'] [FiniteDimensional F F']
  [Algebra.IsSeparable F F'] in

Lean source · statement

theorem algebraMap_integralClosureAt_injective :
    Function.Injective
      (algebraMap v.toValuationSubring (integralClosureAt F' v))

instance

(anonymous instance)

L443 ↗

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

instance : Module.IsTorsionFree v.toValuationSubring (integralClosureAt F' v)

theorem

maximalIdeal_ne_bot

L451 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.maximalIdeal_ne_bot

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Setup
variable (v : Place K F)
variable (F') in

Lean source · statement

theorem maximalIdeal_ne_bot :
    IsLocalRing.maximalIdeal v.toValuationSubring ≠ ⊥

theorem

forall_mem_of_restrict_eq

L464 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.forall_mem_of_restrict_eq

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Center
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in

Lean source · statement

theorem forall_mem_of_restrict_eq (hw : w.restrict F = v) (c : integralClosureAt F' v) :
    algebraMap (integralClosureAt F' v) F' c ∈ w.toValuationSubring

def

fiberCenter

L480 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.fiberCenter

Documentation

The height-one centre of an extending place in the integral closure.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in

Lean source · statement

def fiberCenter (hw : w.restrict F = v) : HeightOneSpectrum (integralClosureAt F' v)

theorem

mem_fiberCenter_iff_ord_pos

L483 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.mem_fiberCenter_iff_ord_pos

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in

Lean source · statement

theorem mem_fiberCenter_iff_ord_pos (hw : w.restrict F = v) {c : integralClosureAt F' v}
    (hc : c ≠ 0) :
    c ∈ (fiberCenter F' v hw).asIdeal ↔
      0 < w.ord (algebraMap (integralClosureAt F' v) F' c)

theorem

toValuationSubring_eq_of_restrict_eq

L489 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.toValuationSubring_eq_of_restrict_eq

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in

Lean source · statement

theorem toValuationSubring_eq_of_restrict_eq (hw : w.restrict F = v) :
    w.toValuationSubring =
      HeightOneSpectrum.valuationSubringAtPrime F' (fiberCenter F' v hw)

theorem

mem_maximalIdeal_iff_ord_pos'

L494 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.mem_maximalIdeal_iff_ord_pos'

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in

Lean source · statement

theorem mem_maximalIdeal_iff_ord_pos' {r : v.toValuationSubring} (hr : r ≠ 0) :
    r ∈ IsLocalRing.maximalIdeal v.toValuationSubring ↔
      0 < v.ord (algebraMap v.toValuationSubring F r)

theorem

algebraMap_integralClosureAt_ne_zero

L503 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.algebraMap_integralClosureAt_ne_zero

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in
omit [Algebra K F'] [IsScalarTower K F F'] [FiniteDimensional F F']
  [Algebra.IsSeparable F F'] in

Lean source · statement

theorem algebraMap_integralClosureAt_ne_zero {r : v.toValuationSubring} (hr : r ≠ 0) :
    algebraMap v.toValuationSubring (integralClosureAt F' v) r ≠ 0

theorem

ord_algebraMap_integralClosureAt

L507 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.ord_algebraMap_integralClosureAt

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in
omit [FiniteDimensional F F'] in

Lean source · statement

theorem ord_algebraMap_integralClosureAt (hw : w.restrict F = v) (r : v.toValuationSubring) :
    w.ord (algebraMap (integralClosureAt F' v) F'
        (algebraMap v.toValuationSubring (integralClosureAt F' v) r))
      = w.ramificationIndex F * v.ord (algebraMap v.toValuationSubring F r)

theorem

fiberCenter_liesOver

L514 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.fiberCenter_liesOver

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Center
variable {v : Place K F} {w : Place K F'}
variable (F' v) in

Lean source · statement

theorem fiberCenter_liesOver (hw : w.restrict F = v) :
    (fiberCenter F' v hw).asIdeal.LiesOver
      (IsLocalRing.maximalIdeal v.toValuationSubring)

theorem

neg_log_valuation_fiberCenter_eq_ord

L540 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.neg_log_valuation_fiberCenter_eq_ord

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
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

L579 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.le_ord_iff_mem_pow_fiberCenter

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
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

L602 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.ramificationIndex_eq_ramificationIdx_fiberCenter

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
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

def

toValuationSubringOfRestrictEq

L635 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.toValuationSubringOfRestrictEq

Documentation

The map from the integral closure to the valuation subring of the extending place.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}

Lean source · statement

def toValuationSubringOfRestrictEq (hw : w.restrict F = v) :
    integralClosureAt F' v →+* w.toValuationSubring

theorem

coe_toValuationSubringOfRestrictEq

L641 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.coe_toValuationSubringOfRestrictEq

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in

Lean source · statement

theorem coe_toValuationSubringOfRestrictEq (hw : w.restrict F = v)
    (c : integralClosureAt F' v) :
    (toValuationSubringOfRestrictEq hw c : F')
      = algebraMap (integralClosureAt F' v) F' c

def

residueOfCenter

L647 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.residueOfCenter

Documentation

The residue homomorphism on the integral closure, induced by the valuation ring at w.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}

Lean source · statement

def residueOfCenter (hw : w.restrict F = v) :
    integralClosureAt F' v →+* w.ResidueField

theorem

residueOfCenter_apply

L651 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.residueOfCenter_apply

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in

Lean source · statement

theorem residueOfCenter_apply (hw : w.restrict F = v) (c : integralClosureAt F' v) :
    residueOfCenter hw c = IsLocalRing.residue w.toValuationSubring
      (toValuationSubringOfRestrictEq hw c)

theorem

ker_residueOfCenter

L655 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.ker_residueOfCenter

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}

Lean source · statement

theorem ker_residueOfCenter (hw : w.restrict F = v) :
    RingHom.ker (residueOfCenter hw) = (fiberCenter F' v hw).asIdeal

theorem

surjective_residueOfCenter

L661 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.surjective_residueOfCenter

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}

Lean source · statement

theorem surjective_residueOfCenter (hw : w.restrict F = v) :
    Function.Surjective (residueOfCenter hw)

def

residueFieldEquivQuotientCenter

L724 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.residueFieldEquivQuotientCenter

Documentation

The quotient by the fibre centre identified with the residue field of w.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}

Lean source · statement

def residueFieldEquivQuotientCenter (hw : w.restrict F = v) :
    integralClosureAt F' v ⧸ (fiberCenter F' v hw).asIdeal ≃+* w.ResidueField

theorem

residueFieldEquivQuotientCenter_mk

L729 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.residueFieldEquivQuotientCenter_mk

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}

Lean source · statement

theorem residueFieldEquivQuotientCenter_mk (hw : w.restrict F = v)
    (c : integralClosureAt F' v) :
    residueFieldEquivQuotientCenter hw (Ideal.Quotient.mk _ c) = residueOfCenter hw c

def

placeCongrEquiv

L739 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.placeCongrEquiv

Documentation

The valuation-subring equivalence induced by equality of two places.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}

Lean source · full declaration

def placeCongrEquiv {u u' : Place K F} (h : u = u') :
    u.toValuationSubring ≃+* u'.toValuationSubring where
  toFun x := ⟨x.1, h ▸ x.2⟩
  invFun x := ⟨x.1, h.symm ▸ x.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_mul' _ _ := rfl
  map_add' _ _ := rfl

theorem

coe_placeCongrEquiv

L748 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.coe_placeCongrEquiv

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}

Lean source · statement

theorem coe_placeCongrEquiv {u u' : Place K F} (h : u = u') (x : u.toValuationSubring) :
    (placeCongrEquiv h x : F) = (x : F)

def

restrictResidueFieldEquiv

L752 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.restrictResidueFieldEquiv

Documentation

The residue-field equivalence induced by equality of the restricted and base places.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}

Lean source · statement

def restrictResidueFieldEquiv (hw : w.restrict F = v) :
    (w.restrict F).ResidueField ≃+* IsLocalRing.ResidueField v.toValuationSubring

theorem

restrictResidueFieldEquiv_residue

L756 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.restrictResidueFieldEquiv_residue

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in

Lean source · statement

theorem restrictResidueFieldEquiv_residue (hw : w.restrict F = v)
    (a : (w.restrict F).toValuationSubring) :
    restrictResidueFieldEquiv hw (IsLocalRing.residue _ a)
      = IsLocalRing.residue _ (placeCongrEquiv hw a)

theorem

inertiaDeg_eq_inertiaDeg_fiberCenter

L763 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.inertiaDeg_eq_inertiaDeg_fiberCenter

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section ResidueDictionary
variable {v : Place K F} {w : Place K F'}

Lean source · statement

theorem inertiaDeg_eq_inertiaDeg_fiberCenter (hw : w.restrict F = v) :
    w.inertiaDeg F =
      (fiberCenter F' v hw).asIdeal.inertiaDeg v.toValuationSubring

def

placeOfPrime

L799 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.placeOfPrime

Documentation

The extending place given by a height-one prime of the integral closure.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Bijection
variable {v : Place K F}

Lean source · full declaration

def placeOfPrime (P : HeightOneSpectrum (integralClosureAt F' v)) : Place K F' where
  toValuationSubring := HeightOneSpectrum.valuationSubringAtPrime F' P
  algebraMap_mem' := fun a => by
    rw [HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring,
      Valuation.mem_valuationSubring_iff]
    have h1 : algebraMap K F' a = algebraMap (integralClosureAt F' v) F'
        (algebraMap v.toValuationSubring (integralClosureAt F' v)
          (algebraMap K v.toValuationSubring a)) := by
      rw [← IsScalarTower.algebraMap_apply,
        IsScalarTower.algebraMap_apply v.toValuationSubring F F',
        ← IsScalarTower.algebraMap_apply K v.toValuationSubring F,
        ← IsScalarTower.algebraMap_apply K F F']
    rw [h1]
    exact P.valuation_le_one _
  ne_top' := by
    rw [HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring]
    simp only [ne_eq, Valuation.valuationSubring_eq_top_iff, not_not]
    infer_instance
  isPrincipalIdealRing' := by
    rw [HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring]
    exact isPrincipalIdealRing_valuationSubring P

theorem

placeOfPrime_toValuationSubring

L821 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.placeOfPrime_toValuationSubring

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Bijection
variable {v : Place K F}

Lean source · statement

theorem placeOfPrime_toValuationSubring (P : HeightOneSpectrum (integralClosureAt F' v)) :
    (placeOfPrime P).toValuationSubring = HeightOneSpectrum.valuationSubringAtPrime F' P

theorem

restrict_placeOfPrime

L825 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.restrict_placeOfPrime

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Bijection
variable {v : Place K F}

Lean source · statement

theorem restrict_placeOfPrime (P : HeightOneSpectrum (integralClosureAt F' v)) :
    (placeOfPrime P).restrict F = v

theorem

fiberCenter_placeOfPrime

L843 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.fiberCenter_placeOfPrime

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Bijection
variable {v : Place K F}

Lean source · statement

theorem fiberCenter_placeOfPrime (P : HeightOneSpectrum (integralClosureAt F' v)) :
    fiberCenter F' v (restrict_placeOfPrime P) = P

theorem

eq_of_fiberCenter_eq

L855 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.eq_of_fiberCenter_eq

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Bijection
variable {v : Place K F}

Lean source · statement

theorem eq_of_fiberCenter_eq {w w' : Place K F'} (hw : w.restrict F = v)
    (hw' : w'.restrict F = v)
    (h : fiberCenter F' v hw = fiberCenter F' v hw') : w = w'

theorem

sum_ramificationIndex_mul_inertiaDeg_infra

L867 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.sum_ramificationIndex_mul_inertiaDeg_infra

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace 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']
variable (F') in
attribute [local instance 0] valuationSubringAlgebra
section Assembly
variable (v : Place K F)

Lean source · statement

theorem sum_ramificationIndex_mul_inertiaDeg_infra [HasPrincipalDivisors K F'] :
    ∑ w ∈ v.fiber F', (w.ramificationIndex F : ℤ) * (w.inertiaDeg F : ℤ)
      = (Module.finrank F F' : ℤ)

instance

instSumRamificationInertia

L904 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.instSumRamificationInertia

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
namespace AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

instance instSumRamificationInertia {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'] [HasPrincipalDivisors K F'] :
    SumRamificationInertia K F F'

theorem

ord_coe_eq_of_span_singleton_eq_pow_maximalIdeal

L926 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.ord_coe_eq_of_span_singleton_eq_pow_maximalIdeal

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section DVR
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem ord_coe_eq_of_span_singleton_eq_pow_maximalIdeal {r : v.toValuationSubring} {n : ℕ}
    (h : Ideal.span {r} = IsLocalRing.maximalIdeal v.toValuationSubring ^ n) :
    v.ord (r : F) = n

theorem

relNorm_fiberCenter

L959 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.relNorm_fiberCenter

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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']
namespace Place
open _root_.AlgebraicCurve.Place
section IdealNorm
variable {v : Place K F} {w : Place K F'}

Lean source · statement

theorem relNorm_fiberCenter (hw : w.restrict F = v) :
    Ideal.relNorm v.toValuationSubring (fiberCenter F' v hw).asIdeal
      = IsLocalRing.maximalIdeal v.toValuationSubring ^ w.inertiaDeg F

theorem

count_normalizedFactors_span_singleton

L970 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.count_normalizedFactors_span_singleton

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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']
namespace Place
open _root_.AlgebraicCurve.Place
section IdealNorm
variable {v : Place K F} {w : Place K F'}

Lean source · statement

theorem count_normalizedFactors_span_singleton
    (hw : w.restrict F = v) {c : integralClosureAt F' v} (hc : c ≠ 0) :
    (normalizedFactors (Ideal.span {c})).count (fiberCenter F' v hw).asIdeal
      = (w.ord (algebraMap (integralClosureAt F' v) F' c)).toNat

theorem

relNorm_span_singleton

L986 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.relNorm_span_singleton

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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']
namespace Place
open _root_.AlgebraicCurve.Place
section IdealNorm
variable {v : Place K F} {w : Place K F'}

Lean source · statement

theorem relNorm_span_singleton [HasPrincipalDivisors K F'] {c : integralClosureAt F' v}
    (hc : c ≠ 0) :
    Ideal.relNorm v.toValuationSubring (Ideal.span {c})
      = IsLocalRing.maximalIdeal v.toValuationSubring
          ^ (∑ w ∈ v.fiber F',
              w.inertiaDeg F * (w.ord (algebraMap (integralClosureAt F' v) F' c)).toNat)

theorem

ord_norm_algebraMap_integralClosureAt

L1068 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.ord_norm_algebraMap_integralClosureAt

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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']
namespace Place
open _root_.AlgebraicCurve.Place
section ElementNorm
variable (v : Place K F)

Lean source · statement

theorem ord_norm_algebraMap_integralClosureAt [HasPrincipalDivisors K F']
    {c : integralClosureAt F' v} (hc : c ≠ 0) :
    v.ord (Algebra.norm F (algebraMap (integralClosureAt F' v) F' c))
      = ∑ w ∈ v.fiber F', (w.inertiaDeg F : ℤ)
          * w.ord (algebraMap (integralClosureAt F' v) F' c)

theorem

ord_norm_eq_sum_fiber

L1083 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Place.ord_norm_eq_sum_fiber

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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']
namespace Place
open _root_.AlgebraicCurve.Place
section ElementNorm
variable (v : Place K F)

Lean source · statement

theorem ord_norm_eq_sum_fiber [HasPrincipalDivisors K F'] {f : F'} (hf : f ≠ 0) :
    v.ord (Algebra.norm F f) = ∑ w ∈ v.fiber F', (w.inertiaDeg F : ℤ) * w.ord f

theorem

pushforwardNormFormula_infra

L1117 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Divisor.pushforwardNormFormula_infra

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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']
namespace Divisor
open _root_.AlgebraicCurve.Divisor

Lean source · statement

theorem pushforwardNormFormula_infra [HasPrincipalDivisors K F'] :
    Divisor.PushforwardNormFormula K F F'

theorem

pushforward_div

L1136 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Divisor.pushforward_div

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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']
namespace Divisor
open _root_.AlgebraicCurve.Divisor
variable (F) in

Lean source · statement

theorem pushforward_div [HasPrincipalDivisors K F'] {f : F'} (hf : f ≠ 0)
    {D : Divisor K F'} (hD : ∀ w, D w = w.ord f)
    {E : Divisor K F} (hE : ∀ v, E v = v.ord (Algebra.norm F f)) :
    pushforward F D = E

theorem

isPrincipal_pushforward_infra

L1143 ↗

AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable.AlgebraicCurve.Divisor.isPrincipal_pushforward_infra

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
attribute [local instance 0] Place.valuationSubringAlgebra
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']
namespace Divisor
open _root_.AlgebraicCurve.Divisor
variable (F) in
variable (F) in

Lean source · statement

theorem isPrincipal_pushforward_infra [HasPrincipalDivisors K F'] {D : Divisor K F'}
    (hD : IsPrincipal D) : IsPrincipal (pushforward F D)

theorem

pushforwardNormFormula_of_isSeparable

L1151 ↗

AlgebraicCurve.Divisor.pushforwardNormFormula_of_isSeparable

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_isSeparable
open _root_.AlgebraicCurve
noncomputable section
noncomputable section
open IsDedekindDomain Polynomial
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid

Lean source · statement

theorem _root_.AlgebraicCurve.Divisor.pushforwardNormFormula_of_isSeparable {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'] [HasPrincipalDivisors K F'] :
  Divisor.PushforwardNormFormula K F F'

Module documentation

Divisor pushforward Norm Formula of is Separable

Declarations