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

@[inline, reducible]
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
    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
    theorem IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors {R : Type u_1} [CommRing R] {K : Type u_5} [CommRing K] [Algebra R K] [IsFractionRing R K] [Nontrivial R] {x : R} (hx : x nonZeroDivisors R) :
    ↑(algebraMap R K) x 0
    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.

    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).snd { val := (IsLocalization.sec (nonZeroDivisors A) z).fst, property := (_ : (IsLocalization.sec (nonZeroDivisors A) z).fst nonZeroDivisors A) }
    @[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.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]
      noncomputable def 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
      • One or more equations did not get rendered due to their size.
      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 { val := s, property := 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 : { x // x 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 y hy, ↑(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 : { x // x 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 : { x // x 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 : { x // x 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 : { x // x 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]
              def 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
                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 : { x // x nonZeroDivisors A }} :
                @[reducible]
                noncomputable def 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

                  Should be introduced locally after introducing FractionRing.liftAlgebra

                  noncomputable def FractionRing.algEquiv (A : Type u_4) [CommRing A] [IsDomain 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