NYLL
Module

Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord.lean

Nyll.AlgebraicCurves.Places.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
9 declarations indexed from sourceView source ↗

Module documentation

Place mul diff Coeff D div mem and eval At eq int Cast ord

Imports6
Imported by2

Declarations

theorem

mul_derivation_mul_div_mul

L42 ↗
AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord.AlgebraicCurve.Place.mul_derivation_mul_div_mul
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section LogDeriv
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mul_derivation_mul_div_mul (δ : Derivation K F F) (t : F) {f g : F} (hf : f ≠ 0) (hg : g ≠
  0) :
    t * δ (f * g) / (f * g) = t * δ f / f + t * δ g / g
theorem

mul_derivation_inv_div_inv

L49 ↗
AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord.AlgebraicCurve.Place.mul_derivation_inv_div_inv
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section LogDeriv
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mul_derivation_inv_div_inv (δ : Derivation K F F) (t : F) {f : F} (hf : f ≠ 0) :
    t * δ f⁻¹ / f⁻¹ = -(t * δ f / f)
theorem

mul_derivation_zpow_div_zpow

L55 ↗
AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord.AlgebraicCurve.Place.mul_derivation_zpow_div_zpow
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section LogDeriv
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mul_derivation_zpow_div_zpow (δ : Derivation K F F) (t : F) {a : F} (ha : a ≠ 0) (n : ℤ) :
    t * δ (a ^ n) / a ^ n = (n : F) * (t * δ a / a)
theorem

diffCoeff_eq_of_eq_smul_D_of_ord_eq_one

L75 ↗
AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord.AlgebraicCurve.Place.diffCoeff_eq_of_eq_smul_D_of_ord_eq_one
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section DerivOfUniformizer
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [PerfectField K]
Lean source · statement
theorem diffCoeff_eq_of_eq_smul_D_of_ord_eq_one (x : F)
    [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : Place K F) {t : F} (ht : v.ord t = 1) {ω : Ω[F⁄K]} {g : F}
    (h : ω = g • KaehlerDifferential.D K F t) :
    diffCoeff t ω = g
def

derivationOfOrdEqOne

L85 ↗
AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord.AlgebraicCurve.Place.derivationOfOrdEqOne
Documentation

The derivation obtained by taking the differential coefficient with respect to a uniformizer.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section DerivOfUniformizer
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [PerfectField K]
Lean source · full declaration
def derivationOfOrdEqOne (x : F)
    [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : Place K F) {t : F} (ht : v.ord t = 1) : Derivation K F F where
  toFun f := diffCoeff t (KaehlerDifferential.D K F f)
  map_add' f g := by
    refine diffCoeff_eq_of_eq_smul_D_of_ord_eq_one x v ht ?_
    rw [map_add, add_smul, diffCoeff_smul_D_of_ord_eq_one x v ht,
      diffCoeff_smul_D_of_ord_eq_one x v ht]
  map_smul' a f := by
    refine diffCoeff_eq_of_eq_smul_D_of_ord_eq_one x v ht ?_
    rw [Derivation.map_smul, RingHom.id_apply, smul_assoc, diffCoeff_smul_D_of_ord_eq_one x v ht]
  map_one_eq_zero' := by
    change diffCoeff t (KaehlerDifferential.D K F 1) = 0
    refine diffCoeff_eq_of_eq_smul_D_of_ord_eq_one x v ht ?_
    rw [Derivation.map_one_eq_zero, zero_smul]
  leibniz' f g := by
    change diffCoeff t (KaehlerDifferential.D K F (f * g)) =
      f • diffCoeff t (KaehlerDifferential.D K F g) + g • diffCoeff t (KaehlerDifferential.D K F f)
    refine diffCoeff_eq_of_eq_smul_D_of_ord_eq_one x v ht ?_
    rw [Derivation.leibniz, add_smul, smul_eq_mul, smul_eq_mul, mul_smul, mul_smul,
      diffCoeff_smul_D_of_ord_eq_one x v ht, diffCoeff_smul_D_of_ord_eq_one x v ht]
theorem

derivationOfOrdEqOne_apply

L107 ↗
AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord.AlgebraicCurve.Place.derivationOfOrdEqOne_apply
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section DerivOfUniformizer
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [PerfectField K]
Lean source · statement
theorem derivationOfOrdEqOne_apply (x : F)
    [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : Place K F) {t : F} (ht : v.ord t = 1) (f : F) :
    derivationOfOrdEqOne x v ht f = diffCoeff t (KaehlerDifferential.D K F f)
theorem

derivationOfOrdEqOne_self

L112 ↗
AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord.AlgebraicCurve.Place.derivationOfOrdEqOne_self
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section DerivOfUniformizer
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [PerfectField K]
Lean source · statement
theorem derivationOfOrdEqOne_self (x : F)
    [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : Place K F) {t : F} (ht : v.ord t = 1) :
    derivationOfOrdEqOne x v ht t = 1
theorem

derivationOfOrdEqOne_mem

L118 ↗
AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord.AlgebraicCurve.Place.derivationOfOrdEqOne_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section DerivOfUniformizer
variable {K F : Type*} [Field K] [Field F] [Algebra K F] [PerfectField K]
Lean source · statement
theorem derivationOfOrdEqOne_mem (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : Place K F) {t : F} (ht : v.ord t = 1) {f : F} (hf : f ∈ v.toValuationSubring) :
    derivationOfOrdEqOne x v ht f ∈ v.toValuationSubring
theorem

mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord

L134 ↗
AlgebraicCurve.Place.mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
open _root_.AlgebraicCurve
open _root_.KaehlerDifferential
open Place_mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord.AlgebraicCurve.Place in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mul_diffCoeff_D_div_mem_and_evalAt_eq_intCast_ord
    {K F : Type*} [Field K] [Field F] [Algebra K F] [PerfectField K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : Place K F) {t : F} (ht : v.ord t = 1) {f : F} (hf : f ≠ 0) :
    t * Place.diffCoeff t (KaehlerDifferential.D K F f) / f ∈ v.toValuationSubring ∧
      v.evalAt (t * Place.diffCoeff t (KaehlerDifferential.D K F f) / f) = ((v.ord f : ℤ) : K)

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