AlgebraicCurve.Place.exists_irreducible_dCoord_eq_D_and_hasPoleOrderLE_iff
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_exists_irreducible_dCoord_eq_D_and_hasPoleOrderLE_iff
open KaehlerDifferentialLean source · statement
theorem _root_.AlgebraicCurve.Place.exists_irreducible_dCoord_eq_D_and_hasPoleOrderLE_iff
{K F : Type*} [Field K] [Field F] [Algebra K F] (v : AlgebraicCurve.Place K F) :
∃ π : v.toValuationSubring, Irreducible π ∧
v.dCoord = KaehlerDifferential.D K F (π : F) ∧
(∀ (n : ℕ) (ω : Ω[F⁄K]), v.HasPoleOrderLE n ω ↔
∃ f : F, (π : F) ^ n * f ∈ v.toValuationSubring ∧ ω = f • v.dCoord) ∧
(∀ (n : ℕ) (g : F), v.FnPoleOrderLE n g ↔ (π : F) ^ n * g ∈ v.toValuationSubring) ∧
(∀ (ω : Ω[F⁄K]) (a : K), v.HasLogResidue ω a ↔
∃ f : F, ω = f • v.dCoord ∧ v.HasValue ((π : F) * f) a)