Module

Place_CanonicalLocalResidueDataK_res_differentialCoeff_D_mul_inv_eq_one.lean

Nyll.AlgebraicCurves.Places.Place_CanonicalLocalResidueDataK_res_differentialCoeff_D_mul_inv_eq_one

4 declarations indexed from sourceView source ↗

Module documentation

Place Canonical Local Residue Data K res differential Coeff D mul inv eq one

Imports5

Imported by2

theorem

mem_of_ord_nonneg

L39 ↗

AlgebraicCurves.Places.Proofs.LocalResidueSimplePole.AlgebraicCurve.T1ResInv.mem_of_ord_nonneg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.LocalResidueSimplePole
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace T1ResInv
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring

theorem

differentialCoeff_add''

L47 ↗

AlgebraicCurves.Places.Proofs.LocalResidueSimplePole.AlgebraicCurve.T1ResInv.differentialCoeff_add''

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.LocalResidueSimplePole
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace T1ResInv
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem differentialCoeff_add'' [v.DCoordGenerates] [Nontrivial Ω[F⁄K]] (ω₁ ω₂ : Ω[F⁄K]) :
    v.differentialCoeff (ω₁ + ω₂) = v.differentialCoeff ω₁ + v.differentialCoeff ω₂

theorem

res_uniformizer_inv

L52 ↗

AlgebraicCurves.Places.Proofs.LocalResidueSimplePole.AlgebraicCurve.T1ResInv.res_uniformizer_inv

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.LocalResidueSimplePole
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace T1ResInv
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

Lean source · statement

theorem res_uniformizer_inv (R : v.CanonicalLocalResidueDataK) : R.res v.uniformizer⁻¹ = 1

theorem

res_differentialCoeff_D_mul_inv_eq_one

L69 ↗

AlgebraicCurve.Place.CanonicalLocalResidueDataK.res_differentialCoeff_D_mul_inv_eq_one

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.LocalResidueSimplePole
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.LocalResidueSimplePole.AlgebraicCurve
  AlgebraicCurve.T1ResInv in

Lean source · statement

theorem
  _root_.AlgebraicCurve.Place.CanonicalLocalResidueDataK.res_differentialCoeff_D_mul_inv_eq_one
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : AlgebraicCurve.Place K F) [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
    (hint : ∀ h : F, h ∈ v.toValuationSubring →
      v.differentialCoeff (KaehlerDifferential.D K F h) ∈ v.toValuationSubring)
    (R : v.CanonicalLocalResidueDataK) {t : F} (ht : v.ord t = 1) :
    R.res (v.differentialCoeff (KaehlerDifferential.D K F t) * t⁻¹) = 1

Module documentation

Place Canonical Local Residue Data K res differential Coeff D mul inv eq one

Declarations

mem_of_ord_nonneg

differentialCoeff_add''

res_uniformizer_inv

res_differentialCoeff_D_mul_inv_eq_one