NYLL
Module

PullbackAlong_mem_regularDifferentials_of_isIntegral.lean

Nyll.AlgebraicCurves.Differentials.PullbackAlong_mem_regularDifferentials_of_isIntegral
6 declarations indexed from sourceView source ↗

Module documentation

Pullback Along mem regular Differentials of is Integral

Imports6
Imported by1

Declarations

theorem

mem_iff_ord_nonneg

L44 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral.PBRegSol.mem_iff_ord_nonneg
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferential
namespace PBRegSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_iff_ord_nonneg (v : Place K F) {f : F} (hf : f ≠ 0) : f ∈ v.toValuationSubring ↔ 0 ≤
  v.ord f
theorem

ord_nonneg_of_mem

L50 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral.PBRegSol.ord_nonneg_of_mem
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferential
namespace PBRegSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_nonneg_of_mem (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L56 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral.PBRegSol.mem_of_ord_nonneg
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferential
namespace PBRegSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_of_ord_nonneg (v : Place K F) {f : F} (hf : 0 ≤ v.ord f) : f ∈ v.toValuationSubring
theorem

ord_neg_one

L62 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral.PBRegSol.ord_neg_one
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferential
namespace PBRegSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem ord_neg_one (v : Place K F) : v.ord (-1 : F) = 0
theorem

exists_D_eq_smul_dCoord

L68 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral.PBRegSol.exists_D_eq_smul_dCoord
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferential
namespace PBRegSol
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_D_eq_smul_dCoord [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
    [∀ w : Place K F, w.DCoordGenerates] (w : Place K F) {g : F} (hg : g ∈ w.toValuationSubring) :
    ∃ c ∈ w.toValuationSubring, D K F g = c • w.dCoord
theorem

pullbackAlong_mem_regularDifferentials_of_isIntegral

L93 ↗
AlgebraicCurve.pullbackAlong_mem_regularDifferentials_of_isIntegral
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_isIntegral
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve AlgebraicCurve.Differential KaehlerDifferential
open PBRegSol in
Lean source · statement
theorem _root_.AlgebraicCurve.pullbackAlong_mem_regularDifferentials_of_isIntegral
    {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    [PerfectField K] [AlgebraicCurve.IsCurveOver K F] [AlgebraicCurve.IsCurveOver K F']
      [Algebra.EssFiniteType K F']
    [∀ v : AlgebraicCurve.Place K F, v.DCoordGenerates] [∀ w : AlgebraicCurve.Place K F',
      w.DCoordGenerates]
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    {ω : Ω[F⁄K]} (hω : ω ∈ AlgebraicCurve.regularDifferentials K F) :
    AlgebraicCurve.Differential.pullbackAlong φ ω ∈ 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.