Function fields #

This file defines a function field and the ring of integers corresponding to it.

Main definitions #

Implementation notes #

The definitions that involve a field of fractions choose a canonical field of fractions, but are independent of that choice. We also omit assumptions like Finite Fq or IsScalarTower Fq[X] (FractionRing Fq[X]) F in definitions, adding them back in lemmas when they are needed.

References #

Tags #

function field, ring of integers

@[inline, reducible]
abbrev FunctionField (Fq : Type) (F : Type) [Field Fq] [Field F] [Algebra (RatFunc Fq) F] :

F is a function field over the finite field Fq if it is a finite extension of the field of rational functions in one variable over Fq.

Note that F can be a function field over multiple, non-isomorphic, Fq.

Instances For
    theorem functionField_iff (Fq : Type) (F : Type) [Field Fq] [Field F] (Fqt : Type u_1) [Field Fqt] [Algebra (Polynomial Fq) Fqt] [IsFractionRing (Polynomial Fq) Fqt] [Algebra (RatFunc Fq) F] [Algebra Fqt F] [Algebra (Polynomial Fq) F] [IsScalarTower (Polynomial Fq) Fqt F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] :

    F is a function field over Fq iff it is a finite extension of Fq(t).

    The function field analogue of NumberField.ringOfIntegers: FunctionField.ringOfIntegers Fq Fqt F is the integral closure of Fq[t] in F.

    We don't actually assume F is a function field over Fq in the definition, only when proving its properties.

    Instances For

      The place at infinity on Fq(t) #

      The valuation at infinity is the nonarchimedean valuation on Fq(t) with uniformizer 1/t. Explicitly, if f/g ∈ Fq(t) is a nonzero quotient of polynomials, its valuation at infinity is Multiplicative.ofAdd(degree(f) - degree(g)).

      Instances For
        theorem FunctionField.inftyValuation_of_nonzero (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] {x : RatFunc Fq} (hx : x 0) :
        FunctionField.inftyValuationDef Fq x = ↑(Multiplicative.ofAdd (RatFunc.intDegree x))

        The valuation at infinity on Fq(t).

        Instances For
          theorem FunctionField.inftyValuation.C (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] {k : Fq} (hk : k 0) :
          FunctionField.inftyValuationDef Fq (RatFunc.C k) = ↑(Multiplicative.ofAdd 0)
          theorem FunctionField.inftyValuation.X (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] :
          FunctionField.inftyValuationDef Fq RatFunc.X = ↑(Multiplicative.ofAdd 1)
          theorem FunctionField.inftyValuation.polynomial (Fq : Type) [Field Fq] [DecidableEq (RatFunc Fq)] {p : Polynomial Fq} (hp : p 0) :
          FunctionField.inftyValuationDef Fq (↑(algebraMap (Polynomial Fq) (RatFunc Fq)) p) = ↑(Multiplicative.ofAdd ↑(Polynomial.natDegree p))

          The valued field Fq(t) with the valuation at infinity.

          Instances For

            The completion Fq((t⁻¹)) of Fq(t) with respect to the valuation at infinity.

            Instances For

              The valuation at infinity on k(t) extends to a valuation on FqtInfty.