Uniformizer differentials, their coefficients, and differential orders at places of a function field.
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 {K F}
variable (v : Place K F)def uniformizer : FSurrounding 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 {K F}
variable (v : Place K F)theorem ord_uniformizer : v.ord v.uniformizer = 1Surrounding 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 {K F}
variable (v : Place K F)theorem uniformizer_ne_zero : v.uniformizer ≠ 0The Kähler differential of the chosen uniformizer.
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 {K F}
variable (v : Place K F)def dCoord : Ω[F⁄K]The differential of the uniformizer spans the space of field differentials.
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 {K F}
variable (v : Place K F)class DCoordGenerates : Prop where
/-- The singleton uniformizer differential spans the whole differential module. -/
span_eq_top : Submodule.span F {v.dCoord} = ⊤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 {K F}
variable (v : Place K F)theorem dCoord_ne_zero [v.DCoordGenerates] [Nontrivial Ω[F⁄K]] : v.dCoord ≠ 0A chosen coefficient expressing the differential as a multiple of the uniformizer differential, or zero when no coefficient exists.
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 {K F}
variable (v : Place K F)def differentialCoeff (ω : Ω[F⁄K]) : FSurrounding 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 {K F}
variable (v : Place K F)theorem exists_eq_smul_dCoord [v.DCoordGenerates] (ω : Ω[F⁄K]) :
∃ f : F, ω = f • v.dCoordSurrounding 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 {K F}
variable (v : Place K F)theorem differentialCoeff_smul_dCoord [v.DCoordGenerates] (ω : Ω[F⁄K]) :
v.differentialCoeff ω • v.dCoord = ω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 {K F}
variable (v : Place K F)theorem differentialCoeff_unique [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
{ω : Ω[F⁄K]} {f : F} (hf : ω = f • v.dCoord) : v.differentialCoeff ω = fSurrounding 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 {K F}
variable (v : Place K F)theorem differentialCoeff_dCoord [v.DCoordGenerates] [Nontrivial Ω[F⁄K]] :
v.differentialCoeff v.dCoord = 1Surrounding 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 {K F}
variable (v : Place K F)theorem differentialCoeff_zero [v.DCoordGenerates] [Nontrivial Ω[F⁄K]] :
v.differentialCoeff (0 : Ω[F⁄K]) = 0Surrounding 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 {K F}
variable (v : Place K F)theorem differentialCoeff_smul [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
(c : F) (ω : Ω[F⁄K]) :
v.differentialCoeff (c • ω) = c * v.differentialCoeff ωThe order of the differential coefficient at this place.
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 {K F}
variable (v : Place K F)def ordDifferential (ω : Ω[F⁄K]) : ℤ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 {K F}
variable (v : Place K F)theorem gate_ordDifferential_dCoord [v.DCoordGenerates] [Nontrivial Ω[F⁄K]] :
v.ordDifferential v.dCoord = 0Surrounding 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 {K F}
variable (v : Place K F)theorem ordDifferential_smul [v.DCoordGenerates] [Nontrivial Ω[F⁄K]]
{c : F} (hc : c ≠ 0) {ω : Ω[F⁄K]} (hω : v.differentialCoeff ω ≠ 0) :
v.ordDifferential (c • ω) = v.ord c + v.ordDifferential ω