NYLL
Module

PullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver.lean

Nyll.AlgebraicCurves.Differentials.PullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver
4 declarations indexed from sourceView source ↗

Module documentation

Pullback Along mem regular Differentials of mem of is Curve Over

Imports5
Imported by1

Declarations

theorem

mem_inv_smul_iff

L45 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver.RegPull.mem_inv_smul_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace PullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver
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
open scoped Pointwise
namespace RegPull
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_inv_smul_iff (w : F ≃ₐ[K] F) (v : Place K F) (f : F) :
    f ∈ (w⁻¹ • v).toValuationSubring ↔ w f ∈ v.toValuationSubring
theorem

exists_mem_D_eq_smul_dCoord

L50 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver.RegPull.exists_mem_D_eq_smul_dCoord
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace PullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver
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
open scoped Pointwise
namespace RegPull
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_mem_D_eq_smul_dCoord [PerfectField K] [Algebra.EssFiniteType K F] [IsCurveOver K F]
    [∀ w : Place K F, w.DCoordGenerates] (v : Place K F) {g : F} (hg : g ∈ v.toValuationSubring) :
    ∃ c ∈ v.toValuationSubring, KaehlerDifferential.D K F g = c • v.dCoord
theorem

main

L86 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver.RegPull.main
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace PullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver
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
open scoped Pointwise
namespace RegPull
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]
    [∀ v : Place K F, v.DCoordGenerates]
    (w : F ≃ₐ[K] F) {ω : Ω[F⁄K]} (hω : ω ∈ regularDifferentials K F) :
    Differential.pullbackAlong (w : F →ₐ[K] F) ω ∈ regularDifferentials K F
theorem

pullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver

L107 ↗
AlgebraicCurve.pullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace PullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver
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
open scoped Pointwise
open AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.pullbackAlong_mem_regularDifferentials_of_mem_of_isCurveOver
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    [PerfectField K] [Algebra.EssFiniteType K F] [AlgebraicCurve.IsCurveOver K F]
    [∀ v : AlgebraicCurve.Place K F, v.DCoordGenerates]
    (w : F ≃ₐ[K] F) {ω : Ω[F⁄K]} (hω : ω ∈ AlgebraicCurve.regularDifferentials K F) :
    AlgebraicCurve.Differential.pullbackAlong (w : F →ₐ[K] 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.