NYLL
Module

Place_ord_diffCoeff_D_nonneg.lean

Nyll.AlgebraicCurves.Places.Place_ord_diffCoeff_D_nonneg
11 declarations indexed from sourceView source ↗

Module documentation

Place ord diff Coeff D nonneg

Imports14
Imported by4

Declarations

theorem

polyMem

L49 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg.AlgebraicCurve.FF2R4.polyMem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem polyMem {K : Type*} [Field K] (u : Place K (RatFunc K))
    (hX : (RatFunc.X : RatFunc K) ∈ u.toValuationSubring) (p : Polynomial K) :
    algebraMap (Polynomial K) (RatFunc K) p ∈ u.toValuationSubring
theorem

isLocalization_valuationSubring

L63 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg.AlgebraicCurve.FF2R4.isLocalization_valuationSubring
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem isLocalization_valuationSubring {K Φ : Type*} [Field K] [Field Φ] [Algebra K Φ]
    (w : Place K Φ) {R : Type*} [CommRing R] [IsDedekindDomain R] [Algebra R Φ]
    [IsFractionRing R Φ] (P : HeightOneSpectrum R) [Algebra R w.toValuationSubring]
    (halg : ∀ r : R, (algebraMap R w.toValuationSubring r : Φ) = algebraMap R Φ r)
    (heq : w.toValuationSubring = HeightOneSpectrum.valuationSubringAtPrime Φ P)
    (hmem : ∀ {r : R}, r ≠ 0 → (r ∈ P.asIdeal ↔ 0 < w.ord (algebraMap R Φ r))) :
    IsLocalization P.asIdeal.primeCompl w.toValuationSubring
theorem

isAlgebraic_residue

L109 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg.AlgebraicCurve.FF2R4.isAlgebraic_residue
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem isAlgebraic_residue {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
    [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)]
    {x : S} (hx : ∃ p : Polynomial R, p.Monic ∧ Polynomial.eval₂ (algebraMap R S) x p = 0) :
    IsAlgebraic (IsLocalRing.ResidueField R) (IsLocalRing.residue S x)
def

toValuationSubringOfRestrictEq

L129 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg.AlgebraicCurve.FF2R4.toValuationSubringOfRestrictEq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def toValuationSubringOfRestrictEq (hw : w.restrict F = v) :
    integralClosureAt F' v →+* w.toValuationSubring
theorem

coe_toValuationSubringOfRestrictEq

L135 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg.AlgebraicCurve.FF2R4.coe_toValuationSubringOfRestrictEq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem coe_toValuationSubringOfRestrictEq (hw : w.restrict F = v)
    (c : integralClosureAt F' v) :
    (toValuationSubringOfRestrictEq hw c : F')
      = algebraMap (integralClosureAt F' v) F' c
def

residueOfCenter

L140 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg.AlgebraicCurve.FF2R4.residueOfCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable {v : Place K F} {w : Place K F'}
Lean source · statement
def residueOfCenter (hw : w.restrict F = v) :
    integralClosureAt F' v →+* w.ResidueField
theorem

residueOfCenter_apply

L144 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg.AlgebraicCurve.FF2R4.residueOfCenter_apply
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable {v : Place K F} {w : Place K F'}
omit [FiniteDimensional F F'] in
Lean source · statement
theorem residueOfCenter_apply (hw : w.restrict F = v) (c : integralClosureAt F' v) :
    residueOfCenter hw c = IsLocalRing.residue w.toValuationSubring
      (toValuationSubringOfRestrictEq hw c)
theorem

surjective_residueOfCenter

L148 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg.AlgebraicCurve.FF2R4.surjective_residueOfCenter
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4
open _root_.AlgebraicCurve.Place
section Dict
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F] [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
  [FiniteDimensional F F'] [Algebra.IsSeparable F F']
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem surjective_residueOfCenter (hw : w.restrict F = v) :
    Function.Surjective (residueOfCenter hw)
theorem

engine

L212 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg.AlgebraicCurve.FF2R4.engine
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem engine {K : Type*} [Field K] [CharZero K] {F : Type*} [Field F] [Algebra K F]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
    (x : F) [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : Place K F) {u : Place K (RatFunc K)} (hu : Place.restrict (RatFunc K) v = u)
    (ht : v.ord (algebraMap (RatFunc K) F RatFunc.X) = 1)
    {f : F} (hf : 0 ≤ v.ord f) :
    0 ≤ v.ord (Place.diffCoeff (algebraMap (RatFunc K) F RatFunc.X) (D K F f))
theorem

ord_diffCoeff_D_nonneg

L447 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg.AlgebraicCurve.FF2R4.ord_diffCoeff_D_nonneg
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_diffCoeff_D_nonneg {K F : Type*} [Field K] [Field F] [Algebra K F] [CharZero K]
    (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : AlgebraicCurve.Place K F) {t : F} (ht : v.ord t = 1) {f : F} (hf : 0 ≤ v.ord f) :
    0 ≤ v.ord (AlgebraicCurve.Place.diffCoeff t (KaehlerDifferential.D K F f))
theorem

ord_diffCoeff_D_nonneg

L489 ↗
AlgebraicCurve.Place.ord_diffCoeff_D_nonneg
Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_diffCoeff_D_nonneg {K F : Type*} [Field K] [Field F]
  [Algebra K F] [CharZero K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] (v : AlgebraicCurve.Place K F)
      {t : F}
    (ht : v.ord t = 1) {f : F} (hf : 0 ≤ v.ord f) :
    0 ≤ v.ord (AlgebraicCurve.Place.diffCoeff t (KaehlerDifferential.D K F f))

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