NYLL
Module

Divisor_pushforwardNormFormula_of_finiteDimensional.lean

Nyll.AlgebraicCurves.Divisors.Divisor_pushforwardNormFormula_of_finiteDimensional
26 declarations indexed from sourceView source ↗

Module documentation

Divisor pushforward Norm Formula of finite Dimensional

Imports4
Imported by2

Declarations

theorem

eq_ord_of_addHom_of_nonneg_iff

L42 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.eq_ord_of_addHom_of_nonneg_iff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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

L117 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.neg_log_valuation_fiberCenter_eq_ord
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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

L156 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.le_ord_iff_mem_pow_fiberCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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

L179 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.ramificationIndex_eq_ramificationIdx_fiberCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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
def

toValuationSubringOfRestrictEq

L211 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.toValuationSubringOfRestrictEq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L217 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.coe_toValuationSubringOfRestrictEq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L222 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.residueOfCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L226 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.residueOfCenter_apply
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L230 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.ker_residueOfCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L236 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.surjective_residueOfCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L298 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.residueFieldEquivQuotientCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L303 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.residueFieldEquivQuotientCenter_mk
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L312 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.placeCongrEquiv
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L321 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.coe_placeCongrEquiv
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L324 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.restrictResidueFieldEquiv
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L328 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.restrictResidueFieldEquiv_residue
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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

L335 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.inertiaDeg_eq_inertiaDeg_fiberCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
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 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
theorem

ord_coe_eq_of_span_singleton_eq_pow_maximalIdeal

L388 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.ord_coe_eq_of_span_singleton_eq_pow_maximalIdeal
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.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
instance

(anonymous instance)

L416 ↗
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
instance (v : Place K F) : CharZero v.toValuationSubring
theorem

relNorm_fiberCenter

L424 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.relNorm_fiberCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.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

L434 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.count_normalizedFactors_span_singleton
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section IdealNorm
variable {v : Place K F} {w : Place K F'}
omit [CharZero F] in
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

L450 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.relNorm_span_singleton
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section IdealNorm
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem relNorm_span_singleton {c : integralClosureAt F' v}
    (hc : c ≠ 0) :
    Ideal.relNorm v.toValuationSubring (Ideal.span {c})
      = IsLocalRing.maximalIdeal v.toValuationSubring
          ^ (∑ w ∈ v.fiberOver F',
              w.inertiaDeg F * (w.ord (algebraMap (integralClosureAt F' v) F' c)).toNat)
theorem

ord_norm_algebraMap_integralClosureAt

L533 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.ord_norm_algebraMap_integralClosureAt
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ElementNorm
variable (v : Place K F)
Lean source · statement
theorem ord_norm_algebraMap_integralClosureAt
    {c : integralClosureAt F' v} (hc : c ≠ 0) :
    v.ord (Algebra.norm F (algebraMap (integralClosureAt F' v) F' c))
      = ∑ w ∈ v.fiberOver F', (w.inertiaDeg F : ℤ)
          * w.ord (algebraMap (integralClosureAt F' v) F' c)
theorem

ord_norm_eq_sum_fiberOver

L548 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Place.ord_norm_eq_sum_fiberOver
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
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'] [CharZero F]
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section ElementNorm
variable (v : Place K F)
Lean source · statement
theorem ord_norm_eq_sum_fiberOver {f : F'} (hf : f ≠ 0) :
    v.ord (Algebra.norm F f) = ∑ w ∈ v.fiberOver F', (w.inertiaDeg F : ℤ) * w.ord f
theorem

pushforwardNormFormula_of_finiteDimensional

L583 ↗
AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Divisor.pushforwardNormFormula_of_finiteDimensional
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
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'] [CharZero F]
namespace Divisor
open _root_.AlgebraicCurve.Divisor
open _root_.AlgebraicCurve.Divisor
Lean source · statement
theorem pushforwardNormFormula_of_finiteDimensional :
    Divisor.PushforwardNormFormula K F F'
theorem

pushforwardNormFormula_of_finiteDimensional

L609 ↗
AlgebraicCurve.Divisor.pushforwardNormFormula_of_finiteDimensional
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_pushforwardNormFormula_of_finiteDimensional
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
open _root_.AlgebraicCurve
open Divisor_pushforwardNormFormula_of_finiteDimensional.AlgebraicCurve.Divisor
  renaming pushforwardNormFormula_of_finiteDimensional → pushforwardNormFormulaProof in
Lean source · statement
theorem _root_.AlgebraicCurve.Divisor.pushforwardNormFormula_of_finiteDimensional {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'] [CharZero F] :
    Divisor.PushforwardNormFormula K F F'

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