Module

Logarithmic.lean

Nyll.AlgebraicCurves.Differentials.Logarithmic

12 declarations indexed from sourceView source ↗

Module documentation

Logarithmic

Imports1

Nyll.AlgebraicCurves.Differentials.Order

Imported by4

theorem

kw_hwcd_mem_of_ord_nonneg

L33 ↗

AlgebraicCurve.Place.kw_hwcd_mem_of_ord_nonneg

Documentation

Membership in a place's valuation ring, expressed by nonnegative order.

Source context 6 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem kw_hwcd_mem_of_ord_nonneg {z : F} (h : 0 ≤ v.ord z) :
    z ∈ v.toValuationSubring

theorem

kw_hwcd_ord_nonneg_of_mem

L44 ↗

AlgebraicCurve.Place.kw_hwcd_ord_nonneg_of_mem

Documentation

Elements of a place's valuation ring have nonnegative order.

Source context 6 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem kw_hwcd_ord_nonneg_of_mem {z : F} (hz : z ∈ v.toValuationSubring) :
    0 ≤ v.ord z

theorem

kw_hwcd_ord_algebraMap

L83 ↗

AlgebraicCurve.Place.kw_hwcd_ord_algebraMap

Documentation

A nonzero constant has order zero at every place.

Source context 6 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem kw_hwcd_ord_algebraMap {a : K} (ha : a ≠ 0) :
    v.ord (algebraMap K F a) = 0

def

kw_hwcd_dlog

L98 ↗

AlgebraicCurve.kw_hwcd_dlog

Documentation

The logarithmic differential df / f.

Source context 4 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def kw_hwcd_dlog (K : Type*) [Field K] {F : Type*} [Field F] [Algebra K F] (f : F) :
    Ω[F⁄K]

theorem

kw_hwcd_dlog_zero

L102 ↗

AlgebraicCurve.kw_hwcd_dlog_zero

Source context 4 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem kw_hwcd_dlog_zero : kw_hwcd_dlog K (0 : F) = 0

theorem

kw_hwcd_dlog_one

L105 ↗

AlgebraicCurve.kw_hwcd_dlog_one

Source context 4 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem kw_hwcd_dlog_one : kw_hwcd_dlog K (1 : F) = 0

theorem

kw_hwcd_dlog_mul

L108 ↗

AlgebraicCurve.kw_hwcd_dlog_mul

Source context 4 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem kw_hwcd_dlog_mul {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) :
    kw_hwcd_dlog K (f * g) = kw_hwcd_dlog K f + kw_hwcd_dlog K g

theorem

kw_hwcd_dlog_pow

L115 ↗

AlgebraicCurve.kw_hwcd_dlog_pow

Source context 4 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem kw_hwcd_dlog_pow (n : ℕ) {f : F} (hf : f ≠ 0) :
    kw_hwcd_dlog K (f ^ n) = n • kw_hwcd_dlog K f

theorem

kw_hwcd_dlog_pow_char

L122 ↗

AlgebraicCurve.kw_hwcd_dlog_pow_char

Source context 4 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem kw_hwcd_dlog_pow_char (ℓ : ℕ) [CharP F ℓ] {f : F} (hf : f ≠ 0) :
    kw_hwcd_dlog K (f ^ ℓ) = 0

theorem

kw_hwcd_differentialCoeff_add

L130 ↗

AlgebraicCurve.kw_hwcd_differentialCoeff_add

Source context 6 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Regular
variable [∀ w : Place K F, w.DCoordGenerates] [Nontrivial Ω[F⁄K]]

Lean source · statement

theorem kw_hwcd_differentialCoeff_add (v : Place K F) (ω ω' : Ω[F⁄K]) :
    v.differentialCoeff (ω + ω')
      = v.differentialCoeff ω + v.differentialCoeff ω'

def

kw_hwcd_regularDifferentials

L137 ↗

AlgebraicCurve.kw_hwcd_regularDifferentials

Documentation

Differentials regular at every place.

Source context 6 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Regular
variable [∀ w : Place K F, w.DCoordGenerates] [Nontrivial Ω[F⁄K]]

Lean source · full declaration

def kw_hwcd_regularDifferentials (K F : Type*) [Field K] [Field F] [Algebra K F]
    [∀ w : Place K F, w.DCoordGenerates] [Nontrivial Ω[F⁄K]] : Submodule K Ω[F⁄K] where
  carrier := {ω | ∀ v : Place K F, 0 ≤ v.ordDifferential ω}
  zero_mem' := by
    intro v
    rw [Place.ordDifferential, v.differentialCoeff_zero, v.ord_zero]
  add_mem' := by
    intro ω ω' hω hω' v
    rw [Place.ordDifferential, kw_hwcd_differentialCoeff_add]
    have h₁ : v.differentialCoeff ω ∈ v.toValuationSubring :=
      Place.kw_hwcd_mem_of_ord_nonneg v (hω v)
    have h₂ : v.differentialCoeff ω' ∈ v.toValuationSubring :=
      Place.kw_hwcd_mem_of_ord_nonneg v (hω' v)
    exact v.kw_hwcd_ord_nonneg_of_mem (add_mem h₁ h₂)
  smul_mem' := by
    intro a ω hω v
    rcases eq_or_ne a 0 with rfl | ha
    · rw [zero_smul, Place.ordDifferential, v.differentialCoeff_zero, v.ord_zero]
    have hsmul : a • ω = (algebraMap K F a) • ω := (algebraMap_smul F a ω).symm
    rw [Place.ordDifferential, hsmul, v.differentialCoeff_smul]
    rcases eq_or_ne (v.differentialCoeff ω) 0 with hc | hc
    · rw [hc, mul_zero, v.ord_zero]
    have hmap : algebraMap K F a ≠ 0 :=
      (map_ne_zero_iff _ (algebraMap K F).injective).mpr ha
    rw [v.ord_mul hmap hc, v.kw_hwcd_ord_algebraMap ha, zero_add]
    exact hω v

theorem

kw_hwcd_mem_regularDifferentials_iff

L164 ↗

AlgebraicCurve.kw_hwcd_mem_regularDifferentials_iff

Source context 6 commands

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

open KaehlerDifferential
noncomputable section
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Regular
variable [∀ w : Place K F, w.DCoordGenerates] [Nontrivial Ω[F⁄K]]

Lean source · statement

theorem kw_hwcd_mem_regularDifferentials_iff {ω : Ω[F⁄K]} :
    ω ∈ kw_hwcd_regularDifferentials K F
      ↔ ∀ v : Place K F, 0 ≤ v.ordDifferential ω

Module documentation

Logarithmic

Declarations