Module

LocalCoordinate.lean

Nyll.AlgebraicCurves.Differentials.LocalCoordinate

3 declarations indexed from sourceView source ↗

Module documentation

Imports2

Imported by2

def

AlgebraicCurve.Place.dCoordFn

Documentation

A chosen local coordinate whose differential is the distinguished local differential at a place.

Source context 4 commands

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

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

Lean source · statement

def dCoordFn (v : Place K F) : F

theorem

AlgebraicCurve.Place.ord_dCoordFn

Source context 4 commands

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

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

Lean source · statement

theorem ord_dCoordFn (v : Place K F) : v.ord v.dCoordFn = 1

theorem

AlgebraicCurve.Place.dCoord_eq_D_dCoordFn

Source context 4 commands

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

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

Lean source · statement

theorem dCoord_eq_D_dCoordFn (v : Place K F) :
    v.dCoord = KaehlerDifferential.D K F v.dCoordFn