NYLL
Module

Differential_correspondence_mem_regularDifferentials.lean

Nyll.AlgebraicCurves.Differentials.Differential_correspondence_mem_regularDifferentials
26 declarations indexed from sourceView source ↗

Module documentation

Differential correspondence mem regular Differentials

Imports5
Imported by1

Declarations

theorem

ord_nonneg_of_mem'

L46 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.TraceDifferentBound.ord_nonneg_of_mem'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace TraceDifferentBound
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem ord_nonneg_of_mem' {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg'

L61 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.TraceDifferentBound.mem_of_ord_nonneg'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace TraceDifferentBound
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem mem_of_ord_nonneg' {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring
theorem

mem_iff_ord_nonneg'

L69 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.TraceDifferentBound.mem_iff_ord_nonneg'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace TraceDifferentBound
section SinglePlace
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem mem_iff_ord_nonneg' {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f
theorem

eq_ord_of_addHom_of_nonneg_iff

L79 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.TraceDifferentBound.eq_ord_of_addHom_of_nonneg_iff
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace TraceDifferentBound
section Uniqueness
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (w : Place K F)
Lean source · statement
theorem eq_ord_of_addHom_of_nonneg_iff (φ : F → ℤ)
    (hmul : ∀ x y, x ≠ 0 → y ≠ 0 → φ (x * y) = φ x + φ y)
    (hone : ∃ t, t ≠ 0 ∧ φ t = 1)
    (hiff : ∀ x, x ≠ 0 → (0 ≤ φ x ↔ x ∈ w.toValuationSubring))
    {x : F} (hx : x ≠ 0) : φ x = w.ord x
theorem

neg_log_valuation_fiberCenter_eq_ord

L154 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.TraceDifferentBound.neg_log_valuation_fiberCenter_eq_ord
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace TraceDifferentBound
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']
section ValuationDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem neg_log_valuation_fiberCenter_eq_ord (hw : w.restrict F = v) {x : F'} (hx : x ≠ 0) :
    -log ((fiberCenter F' v hw).valuation F' x) = w.ord x
theorem

le_ord_iff_mem_pow_fiberCenter

L193 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.TraceDifferentBound.le_ord_iff_mem_pow_fiberCenter
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace TraceDifferentBound
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']
section ValuationDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem le_ord_iff_mem_pow_fiberCenter (hw : w.restrict F = v)
    {c : integralClosureAt F' v} (hc : c ≠ 0) (n : ℕ) :
    (n : ℤ) ≤ w.ord (algebraMap (integralClosureAt F' v) F' c) ↔
      c ∈ (fiberCenter F' v hw).asIdeal ^ n
theorem

ramificationIndex_eq_ramificationIdx_fiberCenter

L216 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.TraceDifferentBound.ramificationIndex_eq_ramificationIdx_fiberCenter
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace TraceDifferentBound
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']
section ValuationDictionary
variable {v : Place K F} {w : Place K F'}
Lean source · statement
theorem ramificationIndex_eq_ramificationIdx_fiberCenter (hw : w.restrict F = v) :
    w.ramificationIndex F =
      (IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx'
        (fiberCenter F' v hw).asIdeal
theorem

differentIdeal_le_pow

L249 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.TraceDifferentBound.differentIdeal_le_pow
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace TraceDifferentBound
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']
section Different
variable (v : Place K F)
omit [Algebra K F'] [IsScalarTower K F F'] in
Lean source · statement
theorem differentIdeal_le_pow (P : HeightOneSpectrum (integralClosureAt F' v)) :
    differentIdeal v.toValuationSubring (integralClosureAt F' v) ≤
      P.asIdeal ^ ((IsLocalRing.maximalIdeal v.toValuationSubring).ramificationIdx' P.asIdeal - 1)
theorem

trace_mem_of_le_ord

L261 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.TraceDifferentBound.trace_mem_of_le_ord
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace TraceDifferentBound
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']
section Different
variable (v : Place K F)
Lean source · statement
theorem trace_mem_of_le_ord (g : F')
    (hg : ∀ w : Place K F', w.restrict F = v → 1 - (w.ramificationIndex F : ℤ) ≤ w.ord g) :
    Algebra.trace F F' g ∈ v.toValuationSubring
theorem

exists_mem_finiteDimensional

L342 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.exists_mem_finiteDimensional
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_mem_finiteDimensional (v : Place K F)
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F) :
    ∃ y : F, y ∈ v.toValuationSubring ∧
      FiniteDimensional (IntermediateField.adjoin K ({y} : Set F)) F
theorem

essFiniteType_of_finiteType

L364 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.essFiniteType_of_finiteType
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem essFiniteType_of_finiteType (v : Place K F) {R : Type*} [CommRing R]
    [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F] [Algebra K R]
    [Algebra.FiniteType K R]
    (hRK : ∀ k : K, algebraMap R F (algebraMap K R k) = algebraMap K F k)
    (hR : ∀ r : R, algebraMap R F r ∈ v.toValuationSubring) :
    Algebra.EssFiniteType K v.toValuationSubring
theorem

adjoin_le_of_mem

L414 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.adjoin_le_of_mem
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem adjoin_le_of_mem (v : Place K F) {y : F} (hy : y ∈ v.toValuationSubring)
    {a : F} (ha : a ∈ Algebra.adjoin K ({y} : Set F)) : a ∈ v.toValuationSubring
theorem

essFiniteType_of_mem

L426 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.essFiniteType_of_mem
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
open scoped IntermediateField.algebraAdjoinAdjoin in
Lean source · statement
theorem essFiniteType_of_mem [CharZero K] (v : Place K F) {y : F}
    (hyv : y ∈ v.toValuationSubring) [FiniteDimensional K⟮y⟯ F] :
    Algebra.EssFiniteType K v.toValuationSubring
theorem

essFiniteType

L469 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.essFiniteType
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem essFiniteType [CharZero K] (v : Place K F)
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F) :
    Algebra.EssFiniteType K v.toValuationSubring
theorem

exists_eq_algebraMap_add_mul

L477 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.exists_eq_algebraMap_add_mul
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_eq_algebraMap_add_mul [IsAlgClosed K] (v : Place K F) [v.FiniteResidue]
    {ϖ : v.toValuationSubring} (hϖ : Irreducible ϖ) (a : v.toValuationSubring) :
    ∃ c : K, ∃ b : v.toValuationSubring, a = algebraMap K v.toValuationSubring c + ϖ * b
theorem

span_D_eq_top

L493 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.span_D_eq_top
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem span_D_eq_top [IsAlgClosed K] (v : Place K F) [v.FiniteResidue]
    [Algebra.EssFiniteType K v.toValuationSubring]
    {ϖ : v.toValuationSubring} (hϖ : Irreducible ϖ) :
    Submodule.span v.toValuationSubring
      {KaehlerDifferential.D K v.toValuationSubring ϖ} = ⊤
theorem

exists_irreducible_coe_eq

L516 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.exists_irreducible_coe_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_irreducible_coe_eq (v : Place K F) {π : F} (hπ : v.ord π = 1) :
    ∃ ϖ : v.toValuationSubring, Irreducible ϖ ∧ (ϖ : F) = π
theorem

exists_D_eq_smul_D

L528 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.exists_D_eq_smul_D
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_D_eq_smul_D [IsAlgClosed K] [CharZero K] (v : Place K F) [v.FiniteResidue]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    {π f : F} (hπ : v.ord π = 1) (hf : f ∈ v.toValuationSubring) :
    ∃ g ∈ v.toValuationSubring,
      KaehlerDifferential.D K F f = g • KaehlerDifferential.D K F π
theorem

D_ne_zero_of_ord_eq_one

L549 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.D_ne_zero_of_ord_eq_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem D_ne_zero_of_ord_eq_one [IsAlgClosed K] [CharZero K] [Nontrivial (Ω[F⁄K])]
    (v : Place K F) [v.FiniteResidue]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    {ϖ : F} (hϖ : v.ord ϖ = 1) : KaehlerDifferential.D K F ϖ ≠ 0
theorem

isUnit_add_of_mem_maximalIdeal

L578 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.isUnit_add_of_mem_maximalIdeal
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isUnit_add_of_mem_maximalIdeal {R : Type*} [CommRing R] [IsLocalRing R] {a b : R}
    (ha : IsUnit a) (hb : b ∈ IsLocalRing.maximalIdeal R) : IsUnit (a + b)
theorem

exists_D_eq_smul_D_of_ord_pos

L587 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation.exists_D_eq_smul_D_of_ord_pos
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
namespace LocalDerivation
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_D_eq_smul_D_of_ord_pos [IsAlgClosed K] [CharZero K] (v : Place K F)
    [v.FiniteResidue]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    {ϖ y : F} (hϖ : v.ord ϖ = 1) (hy0 : y ≠ 0) (hy : 0 < v.ord y) :
    ∃ δ : F, δ ≠ 0 ∧ v.ord δ = v.ord y - 1 ∧
      KaehlerDifferential.D K F y = δ • KaehlerDifferential.D K F ϖ
theorem

exists_restrict_eq

L644 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.exists_restrict_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section Above
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']
Lean source · statement
theorem exists_restrict_eq (v : Place K F) : ∃ w : Place K F', w.restrict F = v
theorem

hfg_along

L676 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Differential.CorrespondenceRegular.hfg_along
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Differential
open _root_.AlgebraicCurve.Differential
open _root_.AlgebraicCurve.Differential
namespace CorrespondenceRegular
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurves.Differentials.Proofs
open Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place
open TraceDifferentBound
open _root_.AlgebraicCurves.Differentials.Proofs
open Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem hfg_along (ψ : F →ₐ[K] F') (hψfin : FiniteAlong K ψ)
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F) :
    ∃ x' : F', Transcendental K x' ∧
      FiniteDimensional (IntermediateField.adjoin K ({x'} : Set F')) F'
theorem

pullbackAlong_mem

L705 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Differential.CorrespondenceRegular.pullbackAlong_mem
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Differential
open _root_.AlgebraicCurve.Differential
open _root_.AlgebraicCurve.Differential
namespace CorrespondenceRegular
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurves.Differentials.Proofs
open Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place
open TraceDifferentBound
open _root_.AlgebraicCurves.Differentials.Proofs
open Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem pullbackAlong_mem [IsAlgClosed K] [CharZero K] [IsCurveOver K F] [IsCurveOver K F']
    (ψ : F →ₐ[K] F') (hψ : ψ.toRingHom.IsIntegral) (hψfin : FiniteAlong K ψ)
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    {ω : Ω[F⁄K]} (hω : ω ∈ regularDifferentials K F) :
    pullbackAlong ψ ω ∈ regularDifferentials K F'
theorem

traceAlong_mem

L732 ↗
AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Differential.CorrespondenceRegular.traceAlong_mem
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Differential
open _root_.AlgebraicCurve.Differential
open _root_.AlgebraicCurve.Differential
namespace CorrespondenceRegular
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurves.Differentials.Proofs
open Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place
open TraceDifferentBound
open _root_.AlgebraicCurves.Differentials.Proofs
open Differential_correspondence_mem_regularDifferentials.AlgebraicCurve.Place.LocalDerivation
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem traceAlong_mem [IsAlgClosed K] [CharZero K] [IsCurveOver K F] [IsCurveOver K F']
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (hfg' : ∃ x : F', Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F')
    {η : Ω[F'⁄K]} (hη : η ∈ regularDifferentials K F') :
    traceAlong φ η ∈ regularDifferentials K F
theorem

correspondence_mem_regularDifferentials

L820 ↗
AlgebraicCurve.Differential.correspondence_mem_regularDifferentials
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs.Differential_correspondence_mem_regularDifferentials
noncomputable section
open IsDedekindDomain WithZero IsLocalRing Polynomial nonZeroDivisors
open scoped IntermediateField
open _root_.AlgebraicCurve AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Differential.correspondence_mem_regularDifferentials
    (K F F' : Type*) [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    [IsAlgClosed K] [CharZero K] [IsCurveOver K F] [IsCurveOver K F']
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
    (hψfin : FiniteAlong K ψ)
    {ω : Ω[F⁄K]} (hω : ω ∈ regularDifferentials K F) :
    Differential.correspondence φ ψ ω ∈ 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.