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

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

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

Instances
    source
    theorem Int.not_isField :
    Β¬IsField β„€

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

    source
    theorem NumberField.isAlgebraic (K : Type u_1) [Field K] [nf : NumberField K] :
    Algebra.IsAlgebraic β„š K
    source
    instance NumberField.instFiniteDimensionalToDivisionRingToAddCommGroupToRingToDivisionRingToModuleToCommSemiringToSemifieldToSemiringToDivisionSemiringToSemifield (K : Type u_1) (L : Type u_2) [Field K] [Field L] [nf : NumberField K] [NumberField L] [Algebra K L] :
    FiniteDimensional K L
    Equations
    • β‹― = β‹―
    source
    def NumberField.ringOfIntegers (K : Type u_1) [Field K] :
    Subalgebra β„€ K

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

    Equations
    Instances For
      source
      def NumberField.termπ“ž :
      Lean.ParserDescr

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

      Equations
      Instances For
        source
        theorem NumberField.mem_ringOfIntegers (K : Type u_1) [Field K] (x : K) :
        x ∈ NumberField.ringOfIntegers K ↔ IsIntegral β„€ x
        source
        theorem NumberField.isIntegral_of_mem_ringOfIntegers {K : Type u_3} [Field K] {x : K} (hx : x ∈ NumberField.ringOfIntegers K) :
        IsIntegral β„€ { val := x, property := hx }
        source
        instance NumberField.inst_ringOfIntegersAlgebra (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] :
        Algebra β†₯(NumberField.ringOfIntegers K) β†₯(NumberField.ringOfIntegers L)

        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.
        source
        instance NumberField.RingOfIntegers.instIsFractionRingSubtypeMemSubalgebraIntToCommSemiringInstCommRingToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRingToAlgebraToCommSemiringToSemifieldId {K : Type u_1} [Field K] [NumberField K] :
        IsFractionRing (β†₯(NumberField.ringOfIntegers K)) K
        Equations
        • β‹― = β‹―
        source
        instance NumberField.RingOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraIntToCommSemiringInstCommRingToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommSemiringToCommSemiringToSemifieldToAlgebraId {K : Type u_1} [Field K] :
        IsIntegralClosure β†₯(NumberField.ringOfIntegers K) β„€ K
        Equations
        • β‹― = β‹―
        source
        instance NumberField.RingOfIntegers.instIsIntegrallyClosedSubtypeMemSubalgebraIntToCommSemiringInstCommRingToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRing {K : Type u_1} [Field K] [NumberField K] :
        IsIntegrallyClosed β†₯(NumberField.ringOfIntegers K)
        Equations
        • β‹― = β‹―
        source
        theorem NumberField.RingOfIntegers.isIntegral_coe {K : Type u_1} [Field K] (x : β†₯(NumberField.ringOfIntegers K)) :
        IsIntegral β„€ ↑x
        source
        theorem NumberField.RingOfIntegers.map_mem {K : Type u_1} [Field K] {F : Type u_3} {L : Type u_4} [Field L] [CharZero K] [CharZero L] [FunLike F K L] [AlgHomClass F β„š K L] (f : F) (x : β†₯(NumberField.ringOfIntegers K)) :
        f ↑x ∈ NumberField.ringOfIntegers L
        source
        noncomputable def NumberField.RingOfIntegers.equiv {K : Type u_1} [Field K] (R : Type u_3) [CommRing R] [Algebra R K] [IsIntegralClosure R β„€ K] :
        β†₯(NumberField.ringOfIntegers K) ≃+* R

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

        Equations
        Instances For
          source
          instance NumberField.RingOfIntegers.instCharZeroSubtypeMemSubalgebraIntToCommSemiringInstCommRingToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToAddMonoidWithOneToAddGroupWithOneToRing (K : Type u_1) [Field K] [nf : NumberField K] :
          CharZero β†₯(NumberField.ringOfIntegers K)
          Equations
          • β‹― = β‹―
          source
          instance NumberField.RingOfIntegers.instIsNoetherianIntSubtypeMemSubalgebraToCommSemiringInstCommRingToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersInstSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToCommRingIntModuleToAddCommGroupToRing (K : Type u_1) [Field K] [nf : NumberField K] :
          IsNoetherian β„€ β†₯(NumberField.ringOfIntegers K)
          Equations
          • β‹― = β‹―
          source
          theorem NumberField.RingOfIntegers.not_isField (K : Type u_1) [Field K] [nf : NumberField K] :
          Β¬IsField β†₯(NumberField.ringOfIntegers K)

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

          source
          instance NumberField.RingOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraIntToCommSemiringInstCommRingToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommRing (K : Type u_1) [Field K] [nf : NumberField K] :
          IsDedekindDomain β†₯(NumberField.ringOfIntegers K)
          Equations
          • β‹― = β‹―
          source
          instance NumberField.RingOfIntegers.instFreeIntSubtypeMemSubalgebraToCommSemiringInstCommRingToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersInstSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToCommRingIntModuleToAddCommGroupToRing (K : Type u_1) [Field K] [nf : NumberField K] :
          Module.Free β„€ β†₯(NumberField.ringOfIntegers K)
          Equations
          • β‹― = β‹―
          source
          instance NumberField.RingOfIntegers.instIsLocalizationSubtypeMemSubalgebraIntToCommSemiringInstCommRingToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToCommSemiringToCommSemiringToSemifieldAlgebraMapSubmonoidInstCommSemiringToSemiringAlgebraNonZeroDivisorsToMonoidWithZeroInstSemiringToAlgebraId (K : Type u_1) [Field K] [nf : NumberField K] :
          IsLocalization (Algebra.algebraMapSubmonoid (β†₯(NumberField.ringOfIntegers K)) (nonZeroDivisors β„€)) K
          Equations
          • β‹― = β‹―
          source
          noncomputable def NumberField.RingOfIntegers.basis (K : Type u_1) [Field K] [nf : NumberField K] :
          Basis (Module.Free.ChooseBasisIndex β„€ β†₯(NumberField.ringOfIntegers K)) β„€ β†₯(NumberField.ringOfIntegers K)

          A β„€-basis of the ring of integers of K.

          Equations
          Instances For
            source
            noncomputable def NumberField.integralBasis (K : Type u_1) [Field K] [nf : NumberField K] :
            Basis (Module.Free.ChooseBasisIndex β„€ β†₯(NumberField.ringOfIntegers K)) β„š K

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

            Equations
            Instances For
              source
              @[simp]
              theorem NumberField.integralBasis_apply (K : Type u_1) [Field K] [nf : NumberField K] (i : Module.Free.ChooseBasisIndex β„€ β†₯(NumberField.ringOfIntegers K)) :
              (NumberField.integralBasis K) i = (algebraMap (β†₯(NumberField.ringOfIntegers K)) K) ((NumberField.RingOfIntegers.basis K) i)
              source
              @[simp]
              theorem NumberField.integralBasis_repr_apply (K : Type u_1) [Field K] [nf : NumberField K] (x : β†₯(NumberField.ringOfIntegers K)) (i : Module.Free.ChooseBasisIndex β„€ β†₯(NumberField.ringOfIntegers K)) :
              ((NumberField.integralBasis K).repr ↑x) i = (algebraMap β„€ β„š) (((NumberField.RingOfIntegers.basis K).repr x) i)
              source
              theorem NumberField.mem_span_integralBasis (K : Type u_1) [Field K] [nf : NumberField K] {x : K} :
              x ∈ Submodule.span β„€ (Set.range ⇑(NumberField.integralBasis K)) ↔ x ∈ NumberField.ringOfIntegers K
              source
              theorem NumberField.RingOfIntegers.rank (K : Type u_1) [Field K] [nf : NumberField K] :
              FiniteDimensional.finrank β„€ β†₯(NumberField.ringOfIntegers K) = FiniteDimensional.finrank β„š K
              source
              instance Rat.numberField :
              NumberField β„š
              Equations
              source
              noncomputable def Rat.ringOfIntegersEquiv :
              β†₯(NumberField.ringOfIntegers β„š) ≃+* β„€

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

              Equations
              Instances For
                source
                instance AdjoinRoot.instNumberFieldAdjoinRootRatCommRingInstFieldInstField {f : Polynomial β„š} [hf : Fact (Irreducible f)] :
                NumberField (AdjoinRoot f)

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

                Equations
                • β‹― = β‹―