Module

Place_ordDiff_D_eq_ord_sub_one.lean

Nyll.AlgebraicCurves.Places.Place_ordDiff_D_eq_ord_sub_one

8 declarations indexed from sourceView source ↗

Module documentation

Place ord Diff D eq ord sub one

Imports9

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

ordDiff_smul

L45 ↗

AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one.AlgebraicCurve.FF2R4A.ordDiff_smul

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4A
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section R3grade
variable [CharZero K] (x : F) [Algebra.IsAlgebraic (IntermediateField.adjoin K ({x} : Set F)) F]
include x in

Lean source · statement

theorem ordDiff_smul (v : Place K F) {g : F} (hg : g ≠ 0) {ω : Ω[F⁄K]} (hω : ω ≠ 0) :
    v.ordDiff (g • ω) = v.ord g + v.ordDiff ω

theorem

ord_diffCoeff_D_eq_zero

L62 ↗

AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one.AlgebraicCurve.FF2R4A.ord_diffCoeff_D_eq_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4A
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section R4grade
variable [CharZero K] (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
include x in

Lean source · statement

theorem ord_diffCoeff_D_eq_zero (v : Place K F) {t t' : F} (ht : v.ord t = 1) (ht' : v.ord t' = 1) :
    v.ord (Place.diffCoeff t (D K F t')) = 0

theorem

ordDiff_eq_ord_diffCoeff

L81 ↗

AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one.AlgebraicCurve.FF2R4A.ordDiff_eq_ord_diffCoeff

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4A
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section R4grade
variable [CharZero K] (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
include x in

Lean source · statement

theorem ordDiff_eq_ord_diffCoeff (v : Place K F) {t : F} (ht : v.ord t = 1) (ω : Ω[F⁄K]) :
    v.ordDiff ω = v.ord (Place.diffCoeff t ω)

theorem

ordDiff_D_nonneg

L99 ↗

AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one.AlgebraicCurve.FF2R4A.ordDiff_D_nonneg

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4A
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section R4grade
variable [CharZero K] (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
include x in

Lean source · statement

theorem ordDiff_D_nonneg (v : Place K F) {f : F} (hf : 0 ≤ v.ord f) : 0 ≤ v.ordDiff (D K F f)

theorem

ordDiff_D_of_ord_pos

L104 ↗

AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one.AlgebraicCurve.FF2R4A.ordDiff_D_of_ord_pos

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4A
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section R4grade
variable [CharZero K] (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
include x in

Lean source · statement

theorem ordDiff_D_of_ord_pos (v : Place K F) {f : F} (hf : 0 < v.ord f) :
    v.ordDiff (D K F f) = v.ord f - 1

theorem

ordDiff_D_eq_ord_sub_one

L146 ↗

AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one.AlgebraicCurve.FF2R4A.ordDiff_D_eq_ord_sub_one

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4A
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section R4grade
variable [CharZero K] (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
include x in

Lean source · statement

theorem ordDiff_D_eq_ord_sub_one (v : Place K F) {f : F} (hf : v.ord f ≠ 0) :
    v.ordDiff (D K F f) = v.ord f - 1

theorem

ordDiff_D_eq_ord_sub_algebraMap_sub_one

L163 ↗

AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one.AlgebraicCurve.FF2R4A.ordDiff_D_eq_ord_sub_algebraMap_sub_one

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace FF2R4A
open _root_.AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section R4grade
variable [CharZero K] (x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
include x in

Lean source · statement

theorem ordDiff_D_eq_ord_sub_algebraMap_sub_one (v : Place K F) {f : F} {c : K}
    (hfc : v.ord (f - algebraMap K F c) ≠ 0) :
    v.ordDiff (D K F f) = v.ord (f - algebraMap K F c) - 1

theorem

ordDiff_D_eq_ord_sub_one

L176 ↗

AlgebraicCurve.Place.ordDiff_D_eq_ord_sub_one

Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ordDiff_D_eq_ord_sub_one

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ordDiff_D_eq_ord_sub_one {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)
      {f : F} (hf : v.ord f ≠ 0) :
    v.ordDiff (KaehlerDifferential.D K F f) = v.ord f - 1

Module documentation

Place ord Diff D eq ord sub one

Declarations