NYLL
Module

HasPrincipalDivisors_of_transcendental.lean

Nyll.AlgebraicCurves.Divisors.HasPrincipalDivisors_of_transcendental
30 declarations indexed from sourceView source ↗

Module documentation

Has Principal Divisors of transcendental

Imports11
Imported by4

Declarations

theorem

eq_ord_of_addHom_of_nonneg_iff

L49 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.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.HasPrincipalDivisors_of_transcendental
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

L126 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.neg_log_valuation_fiberCenter_eq_ord
Source context 14 commands

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

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

L165 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.le_ord_iff_mem_pow_fiberCenter
Source context 14 commands

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

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

L188 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.ramificationIndex_eq_ramificationIdx_fiberCenter
Source context 14 commands

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

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

L220 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.toValuationSubringOfRestrictEq
Source context 14 commands

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

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

L226 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.coe_toValuationSubringOfRestrictEq
Source context 15 commands

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

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

L231 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.residueOfCenter
Source context 14 commands

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

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

L235 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.residueOfCenter_apply
Source context 15 commands

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

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

L239 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.ker_residueOfCenter
Source context 14 commands

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

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

L245 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.surjective_residueOfCenter
Source context 14 commands

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

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

L307 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.residueFieldEquivQuotientCenter
Source context 14 commands

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

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

L312 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.residueFieldEquivQuotientCenter_mk
Source context 14 commands

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

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

L321 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.placeCongrEquiv
Source context 14 commands

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

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

L330 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.coe_placeCongrEquiv
Source context 14 commands

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

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

L333 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.restrictResidueFieldEquiv
Source context 14 commands

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

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

L337 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.restrictResidueFieldEquiv_residue
Source context 15 commands

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

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

L344 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.inertiaDeg_eq_inertiaDeg_fiberCenter
Source context 14 commands

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

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

aeval_mem

L387 ↗
AlgebraicCurve.Place.aeval_mem
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental
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 SupportTransfer
open Polynomial
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

L396 ↗
AlgebraicCurve.Place.exists_coeff_ord_ne_zero
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental
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 SupportTransfer
open Polynomial
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 _root_.AlgebraicCurve.Place.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
theorem

ord_coe_eq_of_span_singleton_eq_pow_maximalIdeal

L464 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.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.HasPrincipalDivisors_of_transcendental
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)

L492 ↗
Source context 11 commands

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

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

L500 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.Place.relNorm_fiberCenter
Source context 13 commands

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

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

L510 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.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.HasPrincipalDivisors_of_transcendental
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

L526 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.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.HasPrincipalDivisors_of_transcendental
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

L609 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.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.HasPrincipalDivisors_of_transcendental
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

L624 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.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.HasPrincipalDivisors_of_transcendental
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

L659 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.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.HasPrincipalDivisors_of_transcendental
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

finite_setOf_ord_ne_zero_of_finiteDimensional

L685 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.finite_setOf_ord_ne_zero_of_finiteDimensional
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental
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]
section T029
variable {K : Type*} [Field K] {F' : Type*} [Field F'] [Algebra K F']
  [Algebra (RatFunc K) F'] [IsScalarTower K (RatFunc K) F']
  [FiniteDimensional (RatFunc K) F'] [Algebra.IsSeparable (RatFunc K) F']
Lean source · statement
theorem finite_setOf_ord_ne_zero_of_finiteDimensional {f : F'} (hf : f ≠ 0) :
    {w : Place K F' | w.ord f ≠ 0}.Finite
theorem

hasPrincipalDivisors_of_finiteDimensional_ratFunc

L705 ↗
AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental.AlgebraicCurve.hasPrincipalDivisors_of_finiteDimensional_ratFunc
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental
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]
Lean source · statement
theorem hasPrincipalDivisors_of_finiteDimensional_ratFunc (K : Type*) [Field K] [CharZero
  K] (F' : Type*)
    [Field F'] [Algebra K F'] [Algebra (RatFunc K) F'] [IsScalarTower K (RatFunc K) F']
      [FiniteDimensional (RatFunc K) F'] :
    HasPrincipalDivisors K F'
theorem

hasPrincipalDivisors_of_transcendental

L732 ↗
AlgebraicCurve.hasPrincipalDivisors_of_transcendental
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.HasPrincipalDivisors_of_transcendental
noncomputable section
open IsDedekindDomain WithZero IsLocalRing UniqueFactorizationMonoid
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.hasPrincipalDivisors_of_transcendental (K : Type*) [Field K]
  [CharZero K] {F : Type*} [Field F]
    [Algebra K F] (x : F) (hx : Transcendental K x)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] : HasPrincipalDivisors K F

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