NYLL
Module

Place_ord_diffCoeff_D_nonneg_of_isSeparable.lean

Nyll.AlgebraicCurves.Places.Place_ord_diffCoeff_D_nonneg_of_isSeparable
13 declarations indexed from sourceView source ↗

Module documentation

Place ord diff Coeff D nonneg of is Separable

Imports13
Imported by5

Declarations

theorem

diffCoeff_smul_D_eq_of_isSeparable

L48 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.diffCoeff_smul_D_eq_of_isSeparable
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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem diffCoeff_smul_D_eq_of_isSeparable {K F : Type*} [Field K] [Field F]
    [Algebra K F] (v : Place K F) {t : F} (ht : v.ord t ≠ 0)
    [Algebra.IsSeparable (IntermediateField.adjoin K ({t} : Set F)) F] (g : F) :
    Place.diffCoeff t (g • KaehlerDifferential.D K F t) = g
theorem

polyMem

L56 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
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

L70 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
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

L116 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
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)
theorem

isAlgebraic_residueField_of_X_mem

L128 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.isAlgebraic_residueField_of_X_mem
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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem isAlgebraic_residueField_of_X_mem {K : Type*} [Field K] (u : Place K (RatFunc K))
    [Algebra (Polynomial K) u.toValuationSubring]
    (halg : ∀ p : Polynomial K, (algebraMap (Polynomial K) u.toValuationSubring p : RatFunc K)
      = algebraMap (Polynomial K) (RatFunc K) p)
    (S : Submonoid (Polynomial K)) [IsLocalization S u.toValuationSubring]
    (hX : algebraMap (Polynomial K) u.toValuationSubring Polynomial.X
      ∈ IsLocalRing.maximalIdeal u.toValuationSubring) :
    Algebra.IsAlgebraic K (IsLocalRing.ResidueField u.toValuationSubring)
def

toValuationSubringOfRestrictEq

L181 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
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

L187 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
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

L192 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
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

L196 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
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

L200 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
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

L264 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem engine {K : Type*} [Field K] [PerfectField K] {F : Type*} [Field F] [Algebra K F]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
    [Algebra.IsSeparable (RatFunc K) 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) :
    ∃ g : F, 0 ≤ v.ord g ∧ D K F f = g • D K F (algebraMap (RatFunc K) F RatFunc.X)
theorem

ord_diffCoeff_D_nonneg_of_isSeparable

L500 ↗
AlgebraicCurves.Places.Proofs.Place_ord_diffCoeff_D_nonneg_of_isSeparable.AlgebraicCurve.FF2R4p.ord_diffCoeff_D_nonneg_of_isSeparable
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_of_isSeparable
noncomputable section
open IsDedekindDomain WithZero IsLocalRing KaehlerDifferential
open scoped TensorProduct
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4p
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem ord_diffCoeff_D_nonneg_of_isSeparable {K F : Type*} [Field K] [Field F] [Algebra K F]
    [PerfectField K] (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
    (v : AlgebraicCurve.Place K F) {t : F} (ht : v.ord t = 1)
    [Algebra.IsSeparable (IntermediateField.adjoin K ({t} : Set F)) F]
    {f : F} (hf : 0 ≤ v.ord f) :
    0 ≤ v.ord (AlgebraicCurve.Place.diffCoeff t (KaehlerDifferential.D K F f))
theorem

ord_diffCoeff_D_nonneg_of_isSeparable

L551 ↗
AlgebraicCurve.Place.ord_diffCoeff_D_nonneg_of_isSeparable
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_of_isSeparable
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_diffCoeff_D_nonneg_of_isSeparable {K F : Type*} [Field K]
  [Field F] [Algebra K F] [PerfectField K] (x : F)
    [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F] (v : AlgebraicCurve.Place K
      F) {t : F}
    (ht : v.ord t = 1)
    [Algebra.IsSeparable (IntermediateField.adjoin K ({t} : Set F)) F] {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.