Documentation

Mathlib.RingTheory.Localization.FractionRing

Fraction ring / fraction field Frac(R) as localization #

Main definitions #

Main results #

Implementation notes #

See RingTheory/Localization/Basic.lean for a design overview.

Tags #

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

@[reducible, inline]
abbrev IsFractionRing (R : Type u_1) [CommRing R] (K : Type u_5) [CommRing K] [Algebra R K] :

IsFractionRing R K states K is the field of fractions of an integral domain R.

Equations
Instances For
    instance instIsFractionRing {R : Type u_6} [Field R] :
    Equations
    • =
    theorem IsFractionRing.to_map_eq_zero_iff {R : Type u_1} [CommRing R] {K : Type u_5} [CommRing K] [Algebra R K] [IsFractionRing R K] {x : R} :
    (algebraMap R K) x = 0 x = 0
    @[simp]
    theorem IsFractionRing.coe_inj {R : Type u_1} [CommRing R] {K : Type u_5} [CommRing K] [Algebra R K] [IsFractionRing R K] {a : R} {b : R} :
    a = b a = b
    @[instance 100]
    Equations
    • =
    theorem IsFractionRing.isDomain (A : Type u_4) [CommRing A] [IsDomain A] {K : Type u_5} [CommRing K] [Algebra A K] [IsFractionRing A K] :

    A CommRing K which is the localization of an integral domain R at R - {0} is an integral domain.

    @[irreducible]
    noncomputable def IsFractionRing.inv (A : Type u_6) [CommRing A] [IsDomain A] {K : Type u_7} [CommRing K] [Algebra A K] [IsFractionRing A K] (z : K) :
    K

    The inverse of an element in the field of fractions of an integral domain.

    Equations
    Instances For
      theorem IsFractionRing.inv_def (A : Type u_6) [CommRing A] [IsDomain A] {K : Type u_7} [CommRing K] [Algebra A K] [IsFractionRing A K] (z : K) :
      IsFractionRing.inv A z = if h : z = 0 then 0 else IsLocalization.mk' K (IsLocalization.sec (nonZeroDivisors A) z).2 (IsLocalization.sec (nonZeroDivisors A) z).1,
      theorem IsFractionRing.mul_inv_cancel (A : Type u_4) [CommRing A] [IsDomain A] {K : Type u_5} [CommRing K] [Algebra A K] [IsFractionRing A K] (x : K) (hx : x 0) :
      @[reducible, inline]
      noncomputable abbrev IsFractionRing.toField (A : Type u_4) [CommRing A] [IsDomain A] {K : Type u_5} [CommRing K] [Algebra A K] [IsFractionRing A K] :

      A CommRing K which is the localization of an integral domain R at R - {0} is a field. See note [reducible non-instances].

      Equations
      Instances For
        theorem IsFractionRing.mk'_mk_eq_div {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {r : A} {s : A} (hs : s nonZeroDivisors A) :
        IsLocalization.mk' K r s, hs = (algebraMap A K) r / (algebraMap A K) s
        @[simp]
        theorem IsFractionRing.mk'_eq_div {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {r : A} (s : (nonZeroDivisors A)) :
        IsLocalization.mk' K r s = (algebraMap A K) r / (algebraMap A K) s
        theorem IsFractionRing.div_surjective {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] (z : K) :
        ∃ (x : A), ynonZeroDivisors A, (algebraMap A K) x / (algebraMap A K) y = z
        theorem IsFractionRing.isUnit_map_of_injective {A : Type u_4} [CommRing A] [IsDomain A] {L : Type u_7} [Field L] {g : A →+* L} (hg : Function.Injective g) (y : (nonZeroDivisors A)) :
        IsUnit (g y)
        @[simp]
        theorem IsFractionRing.mk'_eq_zero_iff_eq_zero {R : Type u_1} [CommRing R] {K : Type u_5} [Field K] [Algebra R K] [IsFractionRing R K] {x : R} {y : (nonZeroDivisors R)} :
        theorem IsFractionRing.mk'_eq_one_iff_eq {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] [Algebra A K] [IsFractionRing A K] {x : A} {y : (nonZeroDivisors A)} :
        IsLocalization.mk' K x y = 1 x = y
        noncomputable def IsFractionRing.lift {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] {g : A →+* L} (hg : Function.Injective g) :
        K →+* L

        Given an integral domain A with field of fractions K, and an injective ring hom g : A →+* L where L is a field, we get a field hom sending z : K to g x * (g y)⁻¹, where (x, y) : A × (NonZeroDivisors A) are such that z = f x * (f y)⁻¹.

        Equations
        Instances For
          @[simp]
          theorem IsFractionRing.lift_algebraMap {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] {g : A →+* L} (hg : Function.Injective g) (x : A) :
          (IsFractionRing.lift hg) ((algebraMap A K) x) = g x

          Given an integral domain A with field of fractions K, and an injective ring hom g : A →+* L where L is a field, the field hom induced from K to L maps x to g x for all x : A.

          theorem IsFractionRing.lift_mk' {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] {g : A →+* L} (hg : Function.Injective g) (x : A) (y : (nonZeroDivisors A)) :
          (IsFractionRing.lift hg) (IsLocalization.mk' K x y) = g x / g y

          Given an integral domain A with field of fractions K, and an injective ring hom g : A →+* L where L is a field, field hom induced from K to L maps f x / f y to g x / g y for all x : A, y ∈ NonZeroDivisors A.

          noncomputable def IsFractionRing.map {A : Type u_8} {B : Type u_9} {K : Type u_10} {L : Type u_11} [CommRing A] [CommRing B] [IsDomain B] [CommRing K] [Algebra A K] [IsFractionRing A K] [CommRing L] [Algebra B L] [IsFractionRing B L] {j : A →+* B} (hj : Function.Injective j) :
          K →+* L

          Given integral domains A, B with fields of fractions K, L and an injective ring hom j : A →+* B, we get a field hom sending z : K to g (j x) * (g (j y))⁻¹, where (x, y) : A × (NonZeroDivisors A) are such that z = f x * (f y)⁻¹.

          Equations
          Instances For
            noncomputable def IsFractionRing.fieldEquivOfRingEquiv {A : Type u_4} [CommRing A] [IsDomain A] {K : Type u_5} {B : Type u_6} [CommRing B] [IsDomain B] [Field K] {L : Type u_7} [Field L] [Algebra A K] [IsFractionRing A K] [Algebra B L] [IsFractionRing B L] (h : A ≃+* B) :
            K ≃+* L

            Given integral domains A, B and localization maps to their fields of fractions f : A →+* K, g : B →+* L, an isomorphism j : A ≃+* B induces an isomorphism of fields of fractions K ≃+* L.

            Equations
            Instances For
              @[reducible, inline]
              abbrev FractionRing (R : Type u_1) [CommRing R] :
              Type u_1

              The fraction ring of a commutative ring R as a quotient type.

              We instantiate this definition as generally as possible, and assume that the commutative ring R is an integral domain only when this is needed for proving.

              In this generality, this construction is also known as the total fraction ring of R.

              Equations
              Instances For
                Equations
                Equations
                • =
                noncomputable instance FractionRing.field (A : Type u_4) [CommRing A] [IsDomain A] :

                Porting note: if the fields of this instance are explicitly defined as they were in mathlib3, the last instance in this file suffers a TC timeout

                Equations
                @[simp]
                theorem FractionRing.mk_eq_div (A : Type u_4) [CommRing A] [IsDomain A] {r : A} {s : (nonZeroDivisors A)} :
                @[reducible, inline]
                noncomputable abbrev FractionRing.liftAlgebra (R : Type u_1) [CommRing R] (K : Type u_5) [IsDomain R] [Field K] [Algebra R K] [NoZeroSMulDivisors R K] :

                This is not an instance because it creates a diamond when K = FractionRing R. Should usually be introduced locally along with isScalarTower_liftAlgebra See note [reducible non-instances].

                Equations
                Instances For
                  Equations
                  • =
                  noncomputable def FractionRing.algEquiv (A : Type u_4) [CommRing A] (K : Type u_6) [Field K] [Algebra A K] [IsFractionRing A K] :

                  Given an integral domain A and a localization map to a field of fractions f : A →+* K, we get an A-isomorphism between the field of fractions of A as a quotient type and K.

                  Equations
                  Instances For
                    Equations
                    • =