Module

IsRegularDiff_dlog_of_dvd_ord.lean

Nyll.AlgebraicCurves.Differentials.IsRegularDiff_dlog_of_dvd_ord

5 declarations indexed from sourceView source ↗

Module documentation

Is Regular Diff dlog of dvd ord

Imports4

Imported by3

theorem

diffCoeff_eq_of_eq_smul

L39 ↗

AlgebraicCurves.Differentials.Proofs.IsRegularDiff_dlog_of_dvd_ord.AlgebraicCurve.CartierB.diffCoeff_eq_of_eq_smul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsRegularDiff_dlog_of_dvd_ord
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CartierB
open _root_.AlgebraicCurve
section Helpers
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem diffCoeff_eq_of_eq_smul {t : F} (hdt : D K F t ≠ 0) {ω : Ω[F⁄K]} {c : F}
    (h : ω = c • D K F t) : Place.diffCoeff t ω = c

theorem

D_pow_p

L48 ↗

AlgebraicCurves.Differentials.Proofs.IsRegularDiff_dlog_of_dvd_ord.AlgebraicCurve.CartierB.D_pow_p

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsRegularDiff_dlog_of_dvd_ord
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CartierB
open _root_.AlgebraicCurve
section Helpers
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem D_pow_p (p : ℕ) [Fact p.Prime] [CharP K p] (a : F) :
    D K F (a ^ p) = 0

theorem

dlog_mul

L55 ↗

AlgebraicCurves.Differentials.Proofs.IsRegularDiff_dlog_of_dvd_ord.AlgebraicCurve.CartierB.dlog_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsRegularDiff_dlog_of_dvd_ord
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CartierB
open _root_.AlgebraicCurve
section Helpers
variable {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem dlog_mul {a b : F} (ha : a ≠ 0) (hb : b ≠ 0) :
    (a * b)⁻¹ • D K F (a * b) = a⁻¹ • D K F a + b⁻¹ • D K F b

theorem

isRegularDiff_dlog_of_dvd_ord_impl

L64 ↗

AlgebraicCurves.Differentials.Proofs.IsRegularDiff_dlog_of_dvd_ord.AlgebraicCurve.CartierB.isRegularDiff_dlog_of_dvd_ord_impl

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsRegularDiff_dlog_of_dvd_ord
universe u v
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace CartierB
open _root_.AlgebraicCurve

Lean source · statement

theorem isRegularDiff_dlog_of_dvd_ord_impl
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
    [AlgebraicCurve.IsCurveOver K F] (p : ℕ) [Fact p.Prime]
    [CharP K p] [PerfectField K]
    (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {g : F} (hdvd : ∀ v : AlgebraicCurve.Place K F, (p : ℤ) ∣ v.ord g) :
    AlgebraicCurve.IsRegularDiff K F (g⁻¹ • D K F g)

theorem

isRegularDiff_dlog_of_dvd_ord

L118 ↗

AlgebraicCurve.isRegularDiff_dlog_of_dvd_ord

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.IsRegularDiff_dlog_of_dvd_ord
universe u v
open KaehlerDifferential

Lean source · statement

theorem _root_.AlgebraicCurve.isRegularDiff_dlog_of_dvd_ord
    {K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
    [AlgebraicCurve.IsCurveOver K F] (p : ℕ) [Fact p.Prime]
    [CharP K p] [PerfectField K]
    (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    {g : F} (hdvd : ∀ v : AlgebraicCurve.Place K F, (p : ℤ) ∣ v.ord g) :
    AlgebraicCurve.IsRegularDiff K F (g⁻¹ • D K F g)

Module documentation

Is Regular Diff dlog of dvd ord

Declarations

diffCoeff_eq_of_eq_smul

D_pow_p

dlog_mul

isRegularDiff_dlog_of_dvd_ord_impl

isRegularDiff_dlog_of_dvd_ord