Module

Place_ordDiff_zero_of_perfectField.lean

Nyll.AlgebraicCurves.Places.Place_ordDiff_zero_of_perfectField

2 declarations indexed from sourceView source ↗

Module documentation

Place ord Diff zero of perfect Field

Imports5

Imported by3

theorem

ordDiff_smul_D_uniformizer

L50 ↗

AlgebraicCurves.Places.Proofs.Place_ordDiff_zero_of_perfectField.ordDiff_smul_D_uniformizer

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_zero_of_perfectField
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
open AlgebraicCurve

Lean source · statement

theorem ordDiff_smul_D_uniformizer {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) (g : F) :
    v.ordDiff (g • KaehlerDifferential.D K F v.uniformizer_alt) = v.ord g

theorem

ordDiff_zero_of_perfectField

L61 ↗

AlgebraicCurve.Place.ordDiff_zero_of_perfectField