NYLL
Module

PullbackAlong_mem_regularDifferentials_of_mem_of_algEquiv.lean

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

Module documentation

Pullback Along mem regular Differentials of mem of alg Equiv

Imports6
Imported by1

Declarations

theorem

mem_of_ord_nonneg

L45 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_mem_of_algEquiv.RegPullIso.mem_of_ord_nonneg
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_algEquiv
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
namespace RegPullIso
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem mem_of_ord_nonneg {L : Type*} [Field L] [Algebra K L] (v : Place K L) {f : L} (h : 0 ≤
  v.ord f) :
    f ∈ v.toValuationSubring
def

pullPlace

L53 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_mem_of_algEquiv.RegPullIso.pullPlace
Documentation

The place pulled back along an algebra isomorphism of function fields.

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_algEquiv
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
namespace RegPullIso
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
def pullPlace (Φ : F ≃ₐ[K] F') (w : Place K F') : Place K F
theorem

mem_pullPlace_iff

L58 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_mem_of_algEquiv.RegPullIso.mem_pullPlace_iff
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_algEquiv
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
namespace RegPullIso
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem mem_pullPlace_iff (Φ : F ≃ₐ[K] F') (w : Place K F') (f : F) :
    f ∈ (pullPlace Φ w).toValuationSubring ↔ Φ f ∈ w.toValuationSubring
theorem

exists_mem_D_eq_smul_dCoord

L63 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_mem_of_algEquiv.RegPullIso.exists_mem_D_eq_smul_dCoord
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_algEquiv
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
namespace RegPullIso
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K 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

L100 ↗
AlgebraicCurves.Differentials.Proofs.PullbackAlong_mem_regularDifferentials_of_mem_of_algEquiv.RegPullIso.main
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_algEquiv
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
namespace RegPullIso
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem main [PerfectField K] [Algebra.EssFiniteType K F'] [IsCurveOver K F']
    [∀ w : Place K F', w.DCoordGenerates]
    (Φ : F ≃ₐ[K] F') {η : Ω[F⁄K]} (hη : η ∈ regularDifferentials K F) :
    Differential.pullbackAlong (Φ : F →ₐ[K] F') η ∈ regularDifferentials K F'
theorem

pullbackAlong_mem_regularDifferentials_of_mem_of_algEquiv

L120 ↗
AlgebraicCurve.pullbackAlong_mem_regularDifferentials_of_mem_of_algEquiv
Source context 6 commands

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

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