NYLL
Module

Place_ordDifferential_D_eq_zero_of_constantFieldExtension_of_forall_mem.lean

Nyll.AlgebraicCurves.Places.Place_ordDifferential_D_eq_zero_of_constantFieldExtension_of_forall_mem
29 declarations indexed from sourceView source ↗

Module documentation

Place ord Differential D eq zero of constant Field Extension of forall mem

Imports7
Imported by2

Declarations

theorem

ord_nonneg_of_mem

L56 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.ord_nonneg_of_mem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Toolkit
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem ord_nonneg_of_mem {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

one_le_ord_of_mem_of_inv_not_mem

L71 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.one_le_ord_of_mem_of_inv_not_mem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Toolkit
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem one_le_ord_of_mem_of_inv_not_mem {f : F} (h1 : f ∈ v.toValuationSubring)
    (h2 : f⁻¹ ∉ v.toValuationSubring) : 1 ≤ v.ord f
theorem

mem_iff_ord_nonneg

L88 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.mem_iff_ord_nonneg
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Toolkit
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem mem_iff_ord_nonneg (f : F) : f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f
theorem

irreducible_unifElt

L97 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.irreducible_unifElt
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Toolkit
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem irreducible_unifElt :
    Irreducible (IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose
theorem

coe_unifElt

L101 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.coe_unifElt
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Toolkit
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem coe_unifElt :
    ((IsDiscreteValuationRing.exists_irreducible v.toValuationSubring).choose : F)
      = v.uniformizer
theorem

uniformizer_mem

L105 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.uniformizer_mem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Toolkit
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem uniformizer_mem : v.uniformizer ∈ v.toValuationSubring
theorem

ord_eq_zero_of_isUnit

L108 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.ord_eq_zero_of_isUnit
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Toolkit
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem ord_eq_zero_of_isUnit {a : v.toValuationSubring} (ha : IsUnit a) : v.ord (a : F) = 0
theorem

mem_maximalIdeal_of_not_isUnit

L112 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.mem_maximalIdeal_of_not_isUnit
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Toolkit
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem mem_maximalIdeal_of_not_isUnit {a : v.toValuationSubring} (ha : ¬IsUnit a) :
    a ∈ IsLocalRing.maximalIdeal v.toValuationSubring
theorem

not_isUnit_of_mem_maximalIdeal

L116 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.not_isUnit_of_mem_maximalIdeal
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Toolkit
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem not_isUnit_of_mem_maximalIdeal {a : v.toValuationSubring}
    (ha : a ∈ IsLocalRing.maximalIdeal v.toValuationSubring) : ¬IsUnit a
theorem

mul_uniformizer_mem_maximalIdeal

L120 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.mul_uniformizer_mem_maximalIdeal
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Toolkit
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem mul_uniformizer_mem_maximalIdeal {d : F} (hd : d ∈ v.toValuationSubring) :
    (⟨d * v.uniformizer, mul_mem hd (uniformizer_mem v)⟩ : v.toValuationSubring)
      ∈ IsLocalRing.maximalIdeal v.toValuationSubring
theorem

finiteDimensional_adjoin_of_transcendental

L134 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.finiteDimensional_adjoin_of_transcendental
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section BasisD
open scoped Polynomial
open KaehlerDifferential TensorProduct IntermediateField
open scoped IntermediateField.algebraAdjoinAdjoin in
Lean source · statement
theorem finiteDimensional_adjoin_of_transcendental {L F : Type*} [Field L] [Field F] [Algebra L F]
    (hF : ∃ x : F, Transcendental L x ∧
      FiniteDimensional (IntermediateField.adjoin L ({x} : Set F)) F)
    {f : F} (hf : Transcendental L f) :
    FiniteDimensional (IntermediateField.adjoin L ({f} : Set F)) F
def

polyBasis

L184 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.polyBasis
Documentation

The one-element basis of polynomial differentials given by the variable differential.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section BasisD
open scoped Polynomial
open KaehlerDifferential TensorProduct IntermediateField
variable (K : Type*) [Field K]
Lean source · statement
def polyBasis : Module.Basis (Fin 1) K[X] Ω[K[X]⁄K]
theorem

polyBasis_zero

L187 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.polyBasis_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section BasisD
open scoped Polynomial
open KaehlerDifferential TensorProduct IntermediateField
variable (K : Type*) [Field K]
Lean source · statement
theorem polyBasis_zero : polyBasis K 0 = D K K[X] Polynomial.X
def

ratFuncBasis

L191 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.ratFuncBasis
Documentation

The one-element basis of rational-function differentials obtained by localization.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section BasisD
open scoped Polynomial
open KaehlerDifferential TensorProduct IntermediateField
variable (K : Type*) [Field K]
Lean source · statement
def ratFuncBasis : Module.Basis (Fin 1) (RatFunc K) Ω[(RatFunc K)⁄K]
theorem

ratFuncBasis_zero

L197 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.ratFuncBasis_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section BasisD
open scoped Polynomial
open KaehlerDifferential TensorProduct IntermediateField
variable (K : Type*) [Field K]
Lean source · statement
theorem ratFuncBasis_zero : ratFuncBasis K 0 = D K (RatFunc K) RatFunc.X
def

towerBasis

L208 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.towerBasis
Documentation

Extend the differential basis along the separable function-field extension.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section BasisD
open scoped Polynomial
open KaehlerDifferential TensorProduct IntermediateField
variable (K : Type*) [Field K]
variable {F : Type*} [Field F] [Algebra K F]
Lean source · statement
def towerBasis [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra.IsSeparable (RatFunc K) F] : Module.Basis (Fin 1) F Ω[F⁄K]
theorem

towerBasis_zero

L214 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.towerBasis_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section BasisD
open scoped Polynomial
open KaehlerDifferential TensorProduct IntermediateField
variable (K : Type*) [Field K]
variable {F : Type*} [Field F] [Algebra K F]
Lean source · statement
theorem towerBasis_zero [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [Algebra.IsSeparable (RatFunc K) F] :
    towerBasis K (F := F) 0 = D K F (algebraMap (RatFunc K) F RatFunc.X)
theorem

exists_basis_D

L222 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.exists_basis_D
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section BasisD
open scoped Polynomial
open KaehlerDifferential TensorProduct IntermediateField
variable (K : Type*) [Field K]
variable {F : Type*} [Field F] [Algebra K F]
Lean source · statement
theorem exists_basis_D (F : Type*) [Field F] [Algebra K F] [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    {t : F} (ht : Transcendental K t) :
    ∃ b : Module.Basis (Fin 1) F (Ω[F⁄K]), b 0 = D K F t
theorem

D_ne_zero_of_transcendental

L251 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.D_ne_zero_of_transcendental
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section BasisD
open scoped Polynomial
open KaehlerDifferential TensorProduct IntermediateField
variable (K : Type*) [Field K]
variable {F : Type*} [Field F] [Algebra K F]
Lean source · statement
theorem D_ne_zero_of_transcendental (F : Type*) [Field F] [Algebra K F] [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    {t : F} (ht : Transcendental K t) : D K F t ≠ 0
def

coeffLin

L268 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.coeffLin
Documentation

The linear functional extracting the coefficient of the chosen local differential.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Coeff
open KaehlerDifferential
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · full declaration
def coeffLin (w : Place K F) [w.DCoordGenerates] [Nontrivial Ω[F⁄K]] :
    Ω[F⁄K] →ₗ[F] F where
  toFun := w.differentialCoeff
  map_add' ω₁ ω₂ := w.differentialCoeff_unique
    (by rw [add_smul, w.differentialCoeff_smul_dCoord, w.differentialCoeff_smul_dCoord])
  map_smul' c ω := by
    simp only [RingHom.id_apply, smul_eq_mul]
    exact w.differentialCoeff_smul c ω
theorem

coeffLin_apply

L277 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.coeffLin_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Coeff
open KaehlerDifferential
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem coeffLin_apply (w : Place K F) [w.DCoordGenerates] [Nontrivial Ω[F⁄K]] (ω : Ω[F⁄K]) :
    coeffLin w ω = w.differentialCoeff ω
def

coeffDer

L281 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.coeffDer
Documentation

The derivation obtained by taking the local coefficient of a universal differential.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Coeff
open KaehlerDifferential
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
def coeffDer (w : Place K F) [w.DCoordGenerates] [Nontrivial Ω[F⁄K]] :
    Derivation K F F
theorem

coeffDer_apply

L285 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.coeffDer_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Coeff
open KaehlerDifferential
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem coeffDer_apply (w : Place K F) [w.DCoordGenerates] [Nontrivial Ω[F⁄K]] (f : F) :
    coeffDer w f = w.differentialCoeff (D K F f)
theorem

coeffDer_uniformizer

L288 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.coeffDer_uniformizer
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Coeff
open KaehlerDifferential
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem coeffDer_uniformizer (w : Place K F) [w.DCoordGenerates] [Nontrivial Ω[F⁄K]] :
    coeffDer w w.uniformizer = 1
theorem

differentialCoeff_D_mem

L292 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.differentialCoeff_D_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section Coeff
open KaehlerDifferential
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem differentialCoeff_D_mem [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
    [∀ w : Place K F, w.DCoordGenerates] (w : Place K F) {z : F}
    (hz : z ∈ w.toValuationSubring) :
    w.differentialCoeff (D K F z) ∈ w.toValuationSubring
theorem

isUnit_natCast

L331 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.isUnit_natCast
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section OrdDrop
open KaehlerDifferential
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isUnit_natCast [CharZero K] (w : Place K F) (n : ℕ) (hn : n ≠ 0) :
    IsUnit (⟨((n : ℕ) : F), natCast_mem w.toValuationSubring n⟩ : w.toValuationSubring)
theorem

coeffDer_of_one_le_ord

L345 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.coeffDer_of_one_le_ord
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section OrdDrop
open KaehlerDifferential
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem coeffDer_of_one_le_ord [CharZero K] [PerfectField K] [Algebra.EssFiniteType K F]
    [IsCurveOver K F] [∀ w : Place K F, w.DCoordGenerates] (w : Place K F) {α : F} (hα0 : α ≠ 0)
    (hα : 1 ≤ w.ord α) :
    coeffDer w α ≠ 0 ∧ w.ord (coeffDer w α) = w.ord α - 1
theorem

ordDifferential_D_eq_zero_of_forall_mem

L403 ↗
AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero.W7XNewPlaces.ordDifferential_D_eq_zero_of_forall_mem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
namespace W7XNewPlaces
section MainTheorem
open KaehlerDifferential IntermediateField
Lean source · statement
theorem ordDifferential_D_eq_zero_of_forall_mem (K F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K' F']
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (w : Place K' F') (hw : ∀ f : F, algebraMap F F' f ∈ w.toValuationSubring)
    {x : F} (hx : Transcendental K' (algebraMap F F' x)) :
    w.differentialCoeff (KaehlerDifferential.D K' F' (algebraMap F F' x)) ≠ 0 ∧
      w.ordDifferential (KaehlerDifferential.D K' F' (algebraMap F F' x)) = 0
theorem

ordDifferential_D_eq_zero_of_constantFieldExtension_of_forall_mem

L524 ↗
AlgebraicCurve.Place.ordDifferential_D_eq_zero_of_constantFieldExtension_of_forall_mem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceOrdDifferentialDZero
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
open W7XNewPlaces in
Lean source · statement
theorem
  _root_.AlgebraicCurve.Place.ordDifferential_D_eq_zero_of_constantFieldExtension_of_forall_mem (K
  F K' F' : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [CharZero K]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    [IsCurveOver K' F']
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    (w : Place K' F') (hw : ∀ f : F, algebraMap F F' f ∈ w.toValuationSubring)
    {x : F} (hx : Transcendental K' (algebraMap F F' x)) :
    w.differentialCoeff (KaehlerDifferential.D K' F' (algebraMap F F' x)) ≠ 0 ∧
      w.ordDifferential (KaehlerDifferential.D K' F' (algebraMap F F' x)) = 0

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