A chosen element of order one at the place, or zero if no such element exists.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
open Classical indef uniformizer_alt : FSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem ord_uniformizer_alt (h : ∃ t : F, v.ord t = 1) : v.ord v.uniformizer_alt = 1A chosen coefficient expressing the differential as a multiple of D t, or zero if none exists.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
open Classical indef diffCoeff (t : F) (ω : Ω[F⁄K]) : FSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem diffCoeff_smul_D {t : F} {ω : Ω[F⁄K]} (h : ∃ g : F, ω = g • D K F t) :
diffCoeff t ω • D K F t = ωSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem diffCoeff_of_not_exists {t : F} {ω : Ω[F⁄K]} (h : ¬ ∃ g : F, ω = g • D K F t) :
diffCoeff t ω = 0The order of the differential coefficient with respect to the chosen uniformizer.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)def ordDiff (ω : Ω[F⁄K]) : ℤSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem ordDiff_def (ω : Ω[F⁄K]) : v.ordDiff ω = v.ord (diffCoeff v.uniformizer_alt ω)A differential is regular when its order is nonnegative at every place.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) indef IsRegularDiff (ω : Ω[F⁄K]) : PropSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) intheorem isRegularDiff_iff (ω : Ω[F⁄K]) :
IsRegularDiff K F ω ↔ ∀ v : Place K F, 0 ≤ v.ordDiff ωThe submodule spanned by the differentials that are regular at every place.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) indef regularDiffs : Submodule K Ω[F⁄K]Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) intheorem mem_regularDiffs_of_isRegularDiff {ω : Ω[F⁄K]} (h : IsRegularDiff K F ω) :
ω ∈ regularDiffs K FSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) intheorem regularDiffs_eq_span :
regularDiffs K F = Submodule.span K {ω : Ω[F⁄K] | IsRegularDiff K F ω}The map on Kähler differentials induced by the given homomorphism of function fields.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
section Pullback
variable {F' : Type*} [Field F'] [Algebra K F']def pullbackDiff (φ : F →ₐ[K] F') : Ω[F⁄K] →ₗ[K] Ω[F'⁄K]Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable (K F) in
variable (K F) in
section Pullback
variable {F' : Type*} [Field F'] [Algebra K F']theorem pullbackDiff_D (φ : F →ₐ[K] F') (x : F) :
pullbackDiff φ (D K F x) = D K F' (φ x)