Module

Place_diffCoeff_smul_D_of_ord_eq_one.lean

Nyll.AlgebraicCurves.Places.Place_diffCoeff_smul_D_of_ord_eq_one

2 declarations indexed from sourceView source ↗

Module documentation

Place diff Coeff smul D of ord eq one

Imports4

Imported by11

theorem

exists_eq_smul_D

L48 ↗

AlgebraicCurves.Places.Proofs.Place_diffCoeff_smul_D_of_ord_eq_one.exists_eq_smul_D

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_diffCoeff_smul_D_of_ord_eq_one
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
  instIsScalarTowerResidueFieldRestrictPushforward
  instAlgebraResidueFieldRestrictPushforward
  instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
  AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
  AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
  AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
  AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
noncomputable section

Lean source · statement

theorem exists_eq_smul_D {K F : Type*} [Field K] [Field F] [Algebra K F] [PerfectField K]
    (x : F) [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : AlgebraicCurve.Place K F) {t : F} (ht : v.ord t = 1) (ω : Ω[F⁄K]) :
    ∃ g : F, ω = g • KaehlerDifferential.D K F t

theorem

diffCoeff_smul_D_of_ord_eq_one

L59 ↗

AlgebraicCurve.Place.diffCoeff_smul_D_of_ord_eq_one