Documentation

Mathlib.NumberTheory.NumberField.Basic

Number fields #

This file defines a number 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.

References #

Tags #

number field, ring of integers

class NumberField (K : Type u_1) [Field K] :

A number field is a field which has characteristic zero and is finite dimensional over β„š.

Instances
    theorem NumberField.to_charZero {K : Type u_1} [Field K] [self : NumberField K] :

    β„€ with its usual ring structure is not a field.

    instance NumberField.instFiniteDimensional (K : Type u_1) (L : Type u_2) [Field K] [Field L] [nf : NumberField K] [NumberField L] [Algebra K L] :
    Equations
    • β‹― = β‹―
    def NumberField.RingOfIntegers (K : Type u_1) [Field K] :
    Type u_1

    The ring of integers (or number ring) corresponding to a number field is the integral closure of β„€ in the number field.

    This is defined as its own type, rather than a Subalgebra, for performance reasons: looking for instances of the form SMul (RingOfIntegers _) (RingOfIntegers _) makes much more effective use of the discrimination tree than instances of the form SMul (Subtype _) (Subtype _). The drawback is we have to copy over instances manually.

    Equations
    Instances For

      The ring of integers (or number ring) corresponding to a number field is the integral closure of β„€ in the number field.

      This is defined as its own type, rather than a Subalgebra, for performance reasons: looking for instances of the form SMul (RingOfIntegers _) (RingOfIntegers _) makes much more effective use of the discrimination tree than instances of the form SMul (Subtype _) (Subtype _). The drawback is we have to copy over instances manually.

      Equations
      Instances For
        Equations
        • β‹― = β‹―
        Equations
        • β‹― = β‹―
        @[reducible, inline]

        The canonical coercion from π“ž K to K.

        Equations
        Instances For

          This instance has to be CoeHead because we only want to apply it from π“ž K to K.

          Equations
          • NumberField.RingOfIntegers.instCoeHead = { coe := NumberField.RingOfIntegers.val }
          theorem NumberField.RingOfIntegers.ext {K : Type u_1} [Field K] {x : NumberField.RingOfIntegers K} {y : NumberField.RingOfIntegers K} (h : ↑x = ↑y) :
          x = y
          @[simp]
          theorem NumberField.RingOfIntegers.map_mk {K : Type u_1} [Field K] (x : K) (hx : x ∈ integralClosure β„€ K) :
          (algebraMap (NumberField.RingOfIntegers K) K) ⟨x, hx⟩ = x
          theorem NumberField.RingOfIntegers.coe_mk {K : Type u_1} [Field K] {x : K} (hx : x ∈ integralClosure β„€ K) :
          β†‘βŸ¨x, hx⟩ = x
          theorem NumberField.RingOfIntegers.mk_eq_mk {K : Type u_1} [Field K] (x : K) (y : K) (hx : x ∈ integralClosure β„€ K) (hy : y ∈ integralClosure β„€ K) :
          ⟨x, hx⟩ = ⟨y, hy⟩ ↔ x = y
          @[simp]
          theorem NumberField.RingOfIntegers.mk_one {K : Type u_1} [Field K] :
          ⟨1, β‹―βŸ© = 1
          @[simp]
          theorem NumberField.RingOfIntegers.mk_zero {K : Type u_1} [Field K] :
          ⟨0, β‹―βŸ© = 0
          @[simp]
          theorem NumberField.RingOfIntegers.mk_add_mk {K : Type u_1} [Field K] (x : K) (y : K) (hx : x ∈ integralClosure β„€ K) (hy : y ∈ integralClosure β„€ K) :
          ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, β‹―βŸ©
          @[simp]
          theorem NumberField.RingOfIntegers.mk_mul_mk {K : Type u_1} [Field K] (x : K) (y : K) (hx : x ∈ integralClosure β„€ K) (hy : y ∈ integralClosure β„€ K) :
          ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, β‹―βŸ©
          @[simp]
          theorem NumberField.RingOfIntegers.mk_sub_mk {K : Type u_1} [Field K] (x : K) (y : K) (hx : x ∈ integralClosure β„€ K) (hy : y ∈ integralClosure β„€ K) :
          ⟨x, hx⟩ - ⟨y, hy⟩ = ⟨x - y, β‹―βŸ©
          @[simp]
          theorem NumberField.RingOfIntegers.neg_mk {K : Type u_1} [Field K] (x : K) (hx : x ∈ integralClosure β„€ K) :
          -⟨x, hx⟩ = ⟨-x, β‹―βŸ©

          Given an algebra between two fields, create an algebra between their two rings of integers.

          Equations
          • One or more equations did not get rendered due to their size.

          The canonical map from π“ž K to K is injective.

          This is a convenient abbreviation for NoZeroSMulDivisors.algebraMap_injective.

          @[simp]

          The canonical map from π“ž K to K is injective.

          This is a convenient abbreviation for map_eq_zero_iff applied to NoZeroSMulDivisors.algebraMap_injective.

          The canonical map from π“ž K to K is injective.

          This is a convenient abbreviation for map_ne_zero_iff applied to NoZeroSMulDivisors.algebraMap_injective.

          The ring of integers of K are equivalent to any integral closure of β„€ in K

          Equations
          Instances For

            The ring of integers of a number field is not a field.

            def NumberField.RingOfIntegers.restrict {K : Type u_1} [Field K] {M : Type u_3} (f : M β†’ K) (h : βˆ€ (x : M), IsIntegral β„€ (f x)) (x : M) :

            Given f : M β†’ K such that βˆ€ x, IsIntegral β„€ (f x), the corresponding function M β†’ π“ž K.

            Equations
            Instances For

              Given f : M β†’+ K such that βˆ€ x, IsIntegral β„€ (f x), the corresponding function M β†’+ π“ž K.

              Equations
              Instances For
                def NumberField.RingOfIntegers.restrict_monoidHom {K : Type u_1} [Field K] {M : Type u_3} [MulOneClass M] (f : M β†’* K) (h : βˆ€ (x : M), IsIntegral β„€ (f x)) :

                Given f : M β†’* K such that βˆ€ x, IsIntegral β„€ (f x), the corresponding function M β†’* π“ž K.

                Equations
                Instances For

                  A basis of K over β„š that is also a basis of π“ž K over β„€.

                  Equations
                  Instances For

                    The ring of integers of β„š as a number field is just β„€.

                    Equations
                    Instances For

                      The quotient of β„š[X] by the ideal generated by an irreducible polynomial of β„š[X] is a number field.

                      Equations
                      • β‹― = β‹―