NYLL
Module

Dlog_mem_regularDifferentials_of_forall_dvd_ord.lean

Nyll.AlgebraicCurves.Differentials.Dlog_mem_regularDifferentials_of_forall_dvd_ord
5 declarations indexed from sourceView source ↗

Module documentation

Dlog mem regular Differentials of forall dvd ord

Imports5
Imported by1

Declarations

theorem

dlog_inv

L52 ↗
AlgebraicCurves.Differentials.Proofs.Dlog_mem_regularDifferentials_of_forall_dvd_ord.P2mWs11R5.dlog_inv
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dlog_mem_regularDifferentials_of_forall_dvd_ord
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R5
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem dlog_inv {g : F} (hg : g ≠ 0) : kw_hwcd_dlog K g⁻¹ = - kw_hwcd_dlog K g
theorem

dlog_zpow

L57 ↗
AlgebraicCurves.Differentials.Proofs.Dlog_mem_regularDifferentials_of_forall_dvd_ord.P2mWs11R5.dlog_zpow
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dlog_mem_regularDifferentials_of_forall_dvd_ord
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R5
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem dlog_zpow (n : ℤ) {g : F} (hg : g ≠ 0) : kw_hwcd_dlog K (g ^ n) = n • kw_hwcd_dlog K g
theorem

charP_zsmul_eq_zero

L63 ↗
AlgebraicCurves.Differentials.Proofs.Dlog_mem_regularDifferentials_of_forall_dvd_ord.P2mWs11R5.charP_zsmul_eq_zero
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dlog_mem_regularDifferentials_of_forall_dvd_ord
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R5
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem charP_zsmul_eq_zero (p : ℕ) [CharP F p] (ω : Ω[F⁄K]) : (p : ℤ) • ω = 0
theorem

main

L66 ↗
AlgebraicCurves.Differentials.Proofs.Dlog_mem_regularDifferentials_of_forall_dvd_ord.P2mWs11R5.main
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dlog_mem_regularDifferentials_of_forall_dvd_ord
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
open AlgebraicCurve KaehlerDifferential
namespace P2mWs11R5
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem main [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
    [∀ w : Place K F, w.DCoordGenerates] (p : ℕ) [Fact p.Prime] [CharP F p]
    {f : F} (hf : f ≠ 0) (h : ∀ v : Place K F, (p : ℤ) ∣ v.ord f) :
    f⁻¹ • KaehlerDifferential.D K F f ∈ AlgebraicCurve.regularDifferentials K F
theorem

dlog_mem_regularDifferentials_of_forall_dvd_ord

L102 ↗
AlgebraicCurve.dlog_mem_regularDifferentials_of_forall_dvd_ord
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Dlog_mem_regularDifferentials_of_forall_dvd_ord
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
open AlgebraicCurve KaehlerDifferential
Lean source · statement
theorem _root_.AlgebraicCurve.dlog_mem_regularDifferentials_of_forall_dvd_ord
    (K F : Type*) [Field K] [Field F] [Algebra K F] [PerfectField K] [Algebra.EssFiniteType K F]
    [AlgebraicCurve.IsCurveOver K F] [∀ w : AlgebraicCurve.Place K F, w.DCoordGenerates]
    (p : ℕ) [Fact p.Prime] [CharP F p]
    {f : F} (hf : f ≠ 0) (h : ∀ v : AlgebraicCurve.Place K F, (p : ℤ) ∣ v.ord f) :
    f⁻¹ • KaehlerDifferential.D K F f ∈ AlgebraicCurve.regularDifferentials K F

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.