Module

ConstantsAreBase_of_exists_isRational.lean

Nyll.AlgebraicCurves.FunctionFields.ConstantsAreBase_of_exists_isRational

4 declarations indexed from sourceView source ↗

Module documentation

ConstantsAreBase of exists isRational

A rational place of nonzero degree identifies the constant field with the base field, using the degree of principal divisors.

Imports6

Imported by3

theorem

ord_sub_evalAt_pos_s17

L44 ↗

AlgebraicCurve.Place.ord_sub_evalAt_pos_s17

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ConstantsAreBase_of_exists_isRational
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open IsLocalRing in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_sub_evalAt_pos_s17 (hrat : v.IsRational) {f : F}
  (hf : f ∈ v.toValuationSubring)
    (hne : f - algebraMap K F (v.evalAt f) ≠ 0) :
    0 < v.ord (f - algebraMap K F (v.evalAt f))

theorem

eq_algebraMap_of_forall_ord_nonneg_s17

L72 ↗

AlgebraicCurves.FunctionFields.Proofs.ConstantsAreBase_of_exists_isRational.AlgebraicCurve.Place.eq_algebraMap_of_forall_ord_nonneg_s17

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ConstantsAreBase_of_exists_isRational
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
variable [HasPrincipalDivisors K F]

Lean source · statement

theorem eq_algebraMap_of_forall_ord_nonneg_s17 (v₀ : Place K F) (hrat : v₀.IsRational)
    (hdeg : v₀.deg ≠ 0) {g : F} (hg : g ≠ 0) (hord : ∀ v : Place K F, 0 ≤ v.ord g) :
    ∃ c : K, g = algebraMap K F c

theorem

constantsAreBase_of_exists_isRational_s17

L98 ↗

AlgebraicCurves.FunctionFields.Proofs.ConstantsAreBase_of_exists_isRational.AlgebraicCurve.constantsAreBase_of_exists_isRational_s17

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ConstantsAreBase_of_exists_isRational
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve

Lean source · statement

theorem constantsAreBase_of_exists_isRational_s17 {K F : Type*} [Field K] [Field F] [Algebra K F]
    [HasPrincipalDivisors K F]
    (v₀ : Place K F) (hrat : v₀.IsRational) (hdeg : v₀.deg ≠ 0) :
    ConstantsAreBase K F

theorem

constantsAreBase_of_exists_isRational

L113 ↗

AlgebraicCurve.constantsAreBase_of_exists_isRational

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ConstantsAreBase_of_exists_isRational
open _root_.AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.constantsAreBase_of_exists_isRational {K F : Type*} [Field K]
  [Field F] [Algebra K F]
    [AlgebraicCurve.HasPrincipalDivisors K F]
    (v₀ : AlgebraicCurve.Place K F) (hrat : v₀.IsRational) (hdeg : v₀.deg ≠ 0) :
    AlgebraicCurve.ConstantsAreBase K F

Module documentation

ConstantsAreBase of exists isRational

Declarations

ord_sub_evalAt_pos_s17

eq_algebraMap_of_forall_ord_nonneg_s17

constantsAreBase_of_exists_isRational_s17

constantsAreBase_of_exists_isRational