Mathlib.RingTheory.Localization.FractionRing

IsFractionRing abbrev

[CommRing K] [Algebra R K]

Full source

/-- `IsFractionRing R K` states `K` is the ring of fractions of a commutative ring `R`. -/
abbrev IsFractionRing [CommRing K] [Algebra R K] :=
  IsLocalization (nonZeroDivisors R) K

Fraction Ring Characterization

Informal description

Given a commutative ring $R$ and a commutative ring $K$ with an algebra structure from $R$ to $K$, the abbreviation `IsFractionRing R K` asserts that $K$ is the fraction ring (or field of fractions when $R$ is an integral domain) of $R$. This means $K$ is obtained by localizing $R$ at its non-zero divisors.

instIsFractionRing instance

{R : Type*} [Field R] : IsFractionRing R R

Full source

instance {R : Type*} [Field R] : IsFractionRing R R :=
  IsLocalization.at_units _ (fun _ ↦ isUnit_of_mem_nonZeroDivisors)

A Field is its Own Fraction Field

Informal description

For any field $R$, the localization of $R$ at its non-zero divisors is $R$ itself. In other words, $R$ is its own fraction field.

Rat.isFractionRing instance

: IsFractionRing ℤ ℚ

Full source

/-- The cast from `Int` to `Rat` as a `FractionRing`. -/
instance Rat.isFractionRing : IsFractionRing ℤ ℚ where
  map_units' := by
    rintro ⟨x, hx⟩
    rw [mem_nonZeroDivisors_iff_ne_zero] at hx
    simpa only [eq_intCast, isUnit_iff_ne_zero, Int.cast_eq_zero, Ne, Subtype.coe_mk] using hx
  surj' := by
    rintro ⟨n, d, hd, h⟩
    refine ⟨⟨n, ⟨d, ?_⟩⟩, Rat.mul_den_eq_num _⟩
    rw [mem_nonZeroDivisors_iff_ne_zero, Int.natCast_ne_zero_iff_pos]
    exact Nat.zero_lt_of_ne_zero hd
  exists_of_eq {x y} := by
    rw [eq_intCast, eq_intCast, Int.cast_inj]
    rintro rfl
    use 1

$\mathbb{Q}$ as the Fraction Field of $\mathbb{Z}$

Informal description

The field of rational numbers $\mathbb{Q}$ is the fraction field of the integers $\mathbb{Z}$. This means that $\mathbb{Q}$ is obtained by localizing $\mathbb{Z}$ at its non-zero divisors, and every element of $\mathbb{Q}$ can be expressed as a fraction of two integers with non-zero denominator.

IsFractionRing.of_field theorem

 [Field K] [Algebra R K] [FaithfulSMul R K] (surj : ∀ z : K, ∃ x y, z = algebraMap R K x / algebraMap R K y) :
  IsFractionRing R K

Full source

theorem of_field [Field K] [Algebra R K] [FaithfulSMul R K]
    (surj : ∀ z : K, ∃ x y, z = algebraMap R K x / algebraMap R K y) :
    IsFractionRing R K :=
  have inj := FaithfulSMul.algebraMap_injective R K
  have := inj.noZeroDivisors _ (map_zero _) (map_mul _)
  have := Module.nontrivial R K
{ map_units' x :=
    .mk0 _ <| (map_ne_zero_iff _ inj).mpr <| mem_nonZeroDivisors_iff_ne_zero.mp x.2
  surj' z := by
    have ⟨x, y, eq⟩ := surj z
    obtain rfl | hy := eq_or_ne y 0
    · obtain rfl : z = 0 := by simpa using eq
      exact ⟨(0, 1), by simp⟩
    exact ⟨⟨x, y, mem_nonZeroDivisors_iff_ne_zero.mpr hy⟩,
      (eq_div_iff_mul_eq <| (map_ne_zero_iff _ inj).mpr hy).mp eq⟩
  exists_of_eq eq := ⟨1, by simpa using inj eq⟩ }

Field Characterization as Fraction Ring via Surjective Fraction Representation

Informal description

Let $R$ be a commutative ring and $K$ a field equipped with an algebra structure from $R$ to $K$. Suppose the scalar multiplication action of $R$ on $K$ is faithful (i.e., distinct elements of $R$ act differently on $K$). If for every element $z \in K$ there exist $x, y \in R$ such that $z = \frac{\text{algebraMap}_R^K(x)}{\text{algebraMap}_R^K(y)}$, then $K$ is the fraction ring of $R$.

IsFractionRing.to_map_eq_zero_iff theorem

{x : R} : algebraMap R K x = 0 ↔ x = 0

Full source

theorem to_map_eq_zero_iff {x : R} : algebraMapalgebraMap R K x = 0 ↔ x = 0 :=
  IsLocalization.to_map_eq_zero_iff _ le_rfl

Vanishing Criterion for Algebra Maps in Fraction Rings

Informal description

For any element $x$ in a commutative ring $R$ and a fraction ring $K$ of $R$, the algebra map $\text{algebraMap}_R^K(x)$ equals zero in $K$ if and only if $x$ equals zero in $R$.

IsFractionRing.injective theorem

: Function.Injective (algebraMap R K)

Full source

protected theorem injective : Function.Injective (algebraMap R K) :=
  IsLocalization.injective _ (le_of_eq rfl)

Injectivity of the Fraction Ring Embedding

Informal description

The algebra map $\text{algebraMap} : R \to K$ is injective when $K$ is a fraction ring of $R$.

IsFractionRing.instFaithfulSMul instance

: FaithfulSMul R K

Full source

instance (priority := 100) : FaithfulSMul R K :=
  (faithfulSMul_iff_algebraMap_injective R K).mpr <| IsFractionRing.injective R K

Faithful Scalar Multiplication in Fraction Rings

Informal description

For any commutative ring $R$ and its fraction ring $K$, the scalar multiplication action of $R$ on $K$ is faithful. That is, distinct elements of $R$ act differently on $K$ via scalar multiplication.

IsFractionRing.coe_inj theorem

{a b : R} : (Algebra.cast a : K) = Algebra.cast b ↔ a = b

Full source

@[norm_cast, simp]
-- Porting note: using `↑` didn't work, so I needed to explicitly put in the cast myself
theorem coe_inj {a b : R} : (Algebra.cast a : K) = Algebra.cast b ↔ a = b :=
  (IsFractionRing.injective R K).eq_iff

Injectivity of the Canonical Map to Fraction Ring

Informal description

For any elements $a, b$ in a commutative ring $R$, the images of $a$ and $b$ under the canonical algebra map $R \to K$ are equal in the fraction ring $K$ if and only if $a = b$ in $R$.

IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors theorem

[Nontrivial R] {x : R} (hx : x ∈ nonZeroDivisors R) : algebraMap R K x ≠ 0

Full source

protected theorem to_map_ne_zero_of_mem_nonZeroDivisors [Nontrivial R] {x : R}
    (hx : x ∈ nonZeroDivisors R) : algebraMapalgebraMap R K x ≠ 0 :=
  IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors _ le_rfl hx

Non-zero divisors map to non-zero elements in fraction ring

Informal description

Let $R$ be a nontrivial commutative ring and $K$ be a commutative ring with an algebra structure from $R$ to $K$ such that $K$ is the fraction ring of $R$. For any element $x \in R$ that is a non-zero divisor, the image of $x$ under the canonical algebra map $\text{algebraMap} \ R \ K$ is non-zero in $K$.

IsFractionRing.isDomain theorem

: IsDomain K

Full source

/-- A `CommRing` `K` which is the localization of an integral domain `R` at `R - {0}` is an
integral domain. -/
protected theorem isDomain : IsDomain K :=
  isDomain_of_le_nonZeroDivisors _ (le_refl (nonZeroDivisors A))

Fraction Ring of Integral Domain is Integral Domain

Informal description

If $K$ is the fraction ring of an integral domain $R$, then $K$ is an integral domain.

IsFractionRing.inv definition

Full source

/-- The inverse of an element in the field of fractions of an integral domain. -/
protected noncomputable irreducible_def inv (z : K) : K := open scoped Classical in
  if h : z = 0 then 0
  else
    mk' K ↑(sec (nonZeroDivisors A) z).2
      ⟨(sec _ z).1,
        mem_nonZeroDivisors_iff_ne_zero.2 fun h0 =>
          h <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) z) h0⟩

Inverse in field of fractions

Informal description

The inverse of a nonzero element $z$ in the field of fractions $K$ of an integral domain $R$ is defined as follows: if $z = 0$, then the inverse is $0$; otherwise, it is constructed as the fraction $\frac{a}{b}$ where $(a, b)$ is a pair obtained from the localization of $R$ at its non-zero divisors, ensuring $b$ is a non-zero divisor in $R$.

IsFractionRing.inv_def theorem

: eta_helper Eq✝ @inv.{} @(delta% @definition✝)

Full source

/-- The inverse of an element in the field of fractions of an integral domain. -/
protected noncomputable irreducible_def inv (z : K) : K := open scoped Classical in
  if h : z = 0 then 0
  else
    mk' K ↑(sec (nonZeroDivisors A) z).2
      ⟨(sec _ z).1,
        mem_nonZeroDivisors_iff_ne_zero.2 fun h0 =>
          h <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) z) h0⟩

Definition of Inverse in Field of Fractions

Informal description

Let $R$ be an integral domain with field of fractions $K$. For any nonzero element $x \in K$, the inverse $x^{-1}$ is defined as the fraction $\frac{a}{b}$ where $(a, b)$ is obtained from the localization of $R$ at its non-zero divisors, with $b$ being a non-zero divisor in $R$.

IsFractionRing.mul_inv_cancel theorem

(x : K) (hx : x ≠ 0) : x * IsFractionRing.inv A x = 1

Full source

protected theorem mul_inv_cancel (x : K) (hx : x ≠ 0) : x * IsFractionRing.inv A x = 1 := by
  rw [IsFractionRing.inv, dif_neg hx, ←
    IsUnit.mul_left_inj
      (map_units K
        ⟨(sec _ x).1,
          mem_nonZeroDivisors_iff_ne_zero.2 fun h0 =>
            hx <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) x) h0⟩),
    one_mul, mul_assoc]
  rw [mk'_spec, ← eq_mk'_iff_mul_eq]
  exact (mk'_sec _ x).symm

Multiplicative Inverse Property in Field of Fractions: $x \cdot x^{-1} = 1$ for $x \neq 0$

Informal description

For any nonzero element $x$ in the field of fractions $K$ of an integral domain $R$, the product of $x$ and its multiplicative inverse $x^{-1}$ is equal to $1$, i.e., $x \cdot x^{-1} = 1$.

IsFractionRing.toField abbrev

: Field K

Full source

/-- A `CommRing` `K` which is the localization of an integral domain `R` at `R - {0}` is a field.
See note [reducible non-instances]. -/
@[stacks 09FJ]
noncomputable abbrev toField : Field K where
  __ := IsFractionRing.isDomain A
  inv := IsFractionRing.inv A
  mul_inv_cancel := IsFractionRing.mul_inv_cancel A
  inv_zero := show IsFractionRing.inv A (0 : K) = 0 by rw [IsFractionRing.inv]; exact dif_pos rfl
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl

Fraction Ring of Integral Domain is a Field

Informal description

If $K$ is the fraction ring (or field of fractions) of an integral domain $R$, then $K$ is a field.

IsFractionRing.surjective_iff_isField theorem

[IsDomain R] : Function.Surjective (algebraMap R K) ↔ IsField R

Full source

lemma surjective_iff_isField [IsDomain R] : Function.SurjectiveFunction.Surjective (algebraMap R K) ↔ IsField R where
  mp h := (RingEquiv.ofBijective (algebraMap R K)
      ⟨IsFractionRing.injective R K, h⟩).toMulEquiv.isField _ (IsFractionRing.toField R).toIsField
  mpr h :=
    letI := h.toField
    (IsLocalization.atUnits R _ (S := K)
      (fun _ hx ↦ Ne.isUnit (mem_nonZeroDivisors_iff_ne_zero.mp hx))).surjective

Surjectivity of Fraction Ring Embedding Characterizes Fields

Informal description

Let $R$ be an integral domain and $K$ be a fraction ring of $R$. The algebra map $\text{algebraMap} : R \to K$ is surjective if and only if $R$ is a field.

IsFractionRing.mk'_mk_eq_div theorem

{r s} (hs : s ∈ nonZeroDivisors A) : mk' K r ⟨s, hs⟩ = algebraMap A K r / algebraMap A K s

Full source

theorem mk'_mk_eq_div {r s} (hs : s ∈ nonZeroDivisors A) :
    mk' K r ⟨s, hs⟩ = algebraMap A K r / algebraMap A K s :=
  haveI := (algebraMap A K).domain_nontrivial
  mk'_eq_iff_eq_mul.2 <|
    (div_mul_cancel₀ (algebraMap A K r)
        (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hs)).symm

Fraction Construction as Quotient of Canonical Images

Informal description

Let $A$ be a commutative ring and $K$ its fraction ring. For any elements $r, s \in A$ with $s$ a non-zero divisor, the fraction ring element $\text{mk'}\ K\ r\ \langle s, hs \rangle$ is equal to the quotient of the images of $r$ and $s$ under the canonical algebra map from $A$ to $K$, i.e., \[ \text{mk'}\ K\ r\ \langle s, hs \rangle = \frac{\text{algebraMap}\ A\ K\ r}{\text{algebraMap}\ A\ K\ s}. \]

IsFractionRing.mk'_eq_div theorem

{r} (s : nonZeroDivisors A) : mk' K r s = algebraMap A K r / algebraMap A K s

Full source

@[simp]
theorem mk'_eq_div {r} (s : nonZeroDivisors A) : mk' K r s = algebraMap A K r / algebraMap A K s :=
  mk'_mk_eq_div s.2

Fraction Construction as Quotient in Fraction Ring

Informal description

Let $A$ be a commutative ring and $K$ its fraction ring. For any element $r \in A$ and any non-zero divisor $s \in A$, the fraction ring element $\text{mk'}\ K\ r\ s$ is equal to the quotient of the images of $r$ and $s$ under the canonical algebra map from $A$ to $K$, i.e., \[ \text{mk'}\ K\ r\ s = \frac{\text{algebraMap}\ A\ K\ r}{\text{algebraMap}\ A\ K\ s}. \]

IsFractionRing.div_surjective theorem

(z : K) : ∃ x y : A, y ∈ nonZeroDivisors A ∧ algebraMap _ _ x / algebraMap _ _ y = z

Full source

theorem div_surjective (z : K) :
    ∃ x y : A, y ∈ nonZeroDivisors A ∧ algebraMap _ _ x / algebraMap _ _ y = z :=
  let ⟨x, ⟨y, hy⟩, h⟩ := mk'_surjective (nonZeroDivisors A) z
  ⟨x, y, hy, by rwa [mk'_eq_div] at h⟩

Surjectivity of Fraction Representation in Fraction Ring

Informal description

Let $A$ be a commutative ring and $K$ its fraction ring. For every element $z \in K$, there exist elements $x, y \in A$ with $y$ a non-zero divisor, such that $z$ can be expressed as the quotient of the images of $x$ and $y$ under the canonical algebra map from $A$ to $K$, i.e., \[ z = \frac{\text{algebraMap}\ A\ K\ x}{\text{algebraMap}\ A\ K\ y}. \]

IsFractionRing.isUnit_map_of_injective theorem

(hg : Function.Injective g) (y : nonZeroDivisors A) : IsUnit (g y)

Full source

theorem isUnit_map_of_injective (hg : Function.Injective g) (y : nonZeroDivisors A) :
    IsUnit (g y) :=
  haveI := g.domain_nontrivial
  IsUnit.mk0 (g y) <|
    show g.toMonoidWithZeroHom y ≠ 0 from map_ne_zero_of_mem_nonZeroDivisors g hg y.2

Injective Homomorphism Maps Non-Zero Divisors to Units in Fraction Field

Informal description

Let $A$ be a commutative ring and $K$ its field of fractions. If $g : A \to K$ is an injective ring homomorphism, then for any non-zero divisor $y \in A$, the image $g(y)$ is a unit in $K$.

IsFractionRing.mk'_eq_zero_iff_eq_zero theorem

[Algebra R K] [IsFractionRing R K] {x : R} {y : nonZeroDivisors R} : mk' K x y = 0 ↔ x = 0

Full source

theorem mk'_eq_zero_iff_eq_zero [Algebra R K] [IsFractionRing R K] {x : R} {y : nonZeroDivisors R} :
    mk'mk' K x y = 0 ↔ x = 0 := by
  haveI := (algebraMap R K).domain_nontrivial
  simp [nonZeroDivisors.ne_zero]

Vanishing Condition for Fractions in Fraction Rings

Informal description

Let $R$ be a commutative ring and $K$ its fraction ring. For any $x \in R$ and any non-zero divisor $y \in R$, the fraction $\text{mk'}_K(x, y)$ equals zero if and only if $x = 0$. In other words, $\frac{x}{y} = 0$ in $K$ if and only if $x = 0$ in $R$.

IsFractionRing.mk'_eq_one_iff_eq theorem

{x : A} {y : nonZeroDivisors A} : mk' K x y = 1 ↔ x = y

Full source

theorem mk'_eq_one_iff_eq {x : A} {y : nonZeroDivisors A} : mk'mk' K x y = 1 ↔ x = y := by
  haveI := (algebraMap A K).domain_nontrivial
  refine ⟨?_, fun hxy => by rw [hxy, mk'_self']⟩
  intro hxy
  have hy : (algebraMap A K) ↑y ≠ (0 : K) :=
    IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors y.property
  rw [IsFractionRing.mk'_eq_div, div_eq_one_iff_eq hy] at hxy
  exact IsFractionRing.injective A K hxy

Fraction Ring Element Equals One if and only if Numerator Equals Denominator

Informal description

Let $A$ be a commutative ring and $K$ its fraction ring. For any element $x \in A$ and any non-zero divisor $y \in A$, the fraction ring element $\text{mk'}\ K\ x\ y$ equals $1$ if and only if $x = y$.

IsFractionRing.closure_range_algebraMap theorem

: Subfield.closure (Set.range (algebraMap A K)) = ⊤

Full source

/-- If `A` is a commutative ring with fraction field `K`, then the subfield of `K` generated by
the image of `algebraMap A K` is equal to the whole field `K`. -/
theorem closure_range_algebraMap : Subfield.closure (Set.range (algebraMap A K)) = ⊤ :=
  top_unique fun z _ ↦ by
    obtain ⟨_, _, -, rfl⟩ := div_surjective (A := A) z
    apply div_mem <;> exact Subfield.subset_closure ⟨_, rfl⟩

Subfield Generated by Fraction Ring Embedding Equals Whole Field

Informal description

Let $A$ be a commutative ring with fraction field $K$. The subfield of $K$ generated by the image of the canonical algebra map $\text{algebraMap}\ A\ K$ is equal to the entire field $K$.

IsFractionRing.ringHom_fieldRange_eq_of_comp_eq theorem

(h : RingHom.comp f (algebraMap A K) = g) : f.fieldRange = Subfield.closure g.range

Full source

/-- If `A` is a commutative ring with fraction field `K`, `L` is a field, `g : A →+* L` lifts to
`f : K →+* L`, then the image of `f` is the subfield generated by the image of `g`. -/
theorem ringHom_fieldRange_eq_of_comp_eq (h : RingHom.comp f (algebraMap A K) = g) :
    f.fieldRange = Subfield.closure g.range := by
  rw [f.fieldRange_eq_map, ← closure_range_algebraMap A K,
    f.map_field_closure, ← Set.range_comp, ← f.coe_comp, h, g.coe_range]

Image of Fraction Field Homomorphism Equals Subfield Generated by Base Ring Homomorphism

Informal description

Let $A$ be a commutative ring with fraction field $K$, and let $L$ be a field. Given a ring homomorphism $g : A \to L$ and a ring homomorphism $f : K \to L$ such that $f \circ \text{algebraMap}\ A\ K = g$, the image of $f$ is equal to the subfield of $L$ generated by the image of $g$. In other words, $f(K) = \text{Subfield.closure}(g(A))$.

IsFractionRing.ringHom_fieldRange_eq_of_comp_eq_of_range_eq theorem

 (h : RingHom.comp f (algebraMap A K) = g) {s : Set L} (hs : g.range = Subring.closure s) :
  f.fieldRange = Subfield.closure s

Full source

/-- If `A` is a commutative ring with fraction field `K`, `L` is a field, `g : A →+* L` lifts to
`f : K →+* L`, `s` is a set such that the image of `g` is the subring generated by `s`,
then the image of `f` is the subfield generated by `s`. -/
theorem ringHom_fieldRange_eq_of_comp_eq_of_range_eq (h : RingHom.comp f (algebraMap A K) = g)
    {s : Set L} (hs : g.range = Subring.closure s) : f.fieldRange = Subfield.closure s := by
  rw [ringHom_fieldRange_eq_of_comp_eq h, hs]
  ext
  simp_rw [Subfield.mem_closure_iff, Subring.closure_eq]

Image of Fraction Field Homomorphism Equals Subfield Generated by Prescribed Set

Informal description

Let $A$ be a commutative ring with fraction field $K$, and let $L$ be a field. Given ring homomorphisms $g \colon A \to L$ and $f \colon K \to L$ such that $f \circ \text{algebraMap}_A^K = g$, and a subset $s \subseteq L$ such that the image of $g$ is equal to the subring generated by $s$, then the image of $f$ is equal to the subfield generated by $s$. In other words, $f(K) = \text{Subfield.closure}(s)$.

IsFractionRing.lift definition

(hg : Injective g) : K →+* L

Full source

/-- Given a commutative ring `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)⁻¹`. -/
noncomputable def lift (hg : Injective g) : K →+* L :=
  IsLocalization.lift fun y : nonZeroDivisors A => isUnit_map_of_injective hg y

Lift of an injective ring homomorphism to the fraction field

Informal description

Given a commutative ring $ A $ with field of fractions $ K $, and an injective ring homomorphism $ g : A \to L $ where $ L $ is a field, the function `IsFractionRing.lift hg` constructs a ring homomorphism from $ K $ to $ L $. For any $ z \in K $, this homomorphism maps $ z $ to $ g(x) \cdot (g(y))^{-1} $, where $ (x, y) \in A \times \text{NonZeroDivisors}(A) $ is such that $ z = x \cdot y^{-1} $.

IsFractionRing.lift_unique theorem

(hg : Function.Injective g) {f : K →+* L} (hf1 : ∀ x, f (algebraMap A K x) = g x) : IsFractionRing.lift hg = f

Full source

theorem lift_unique (hg : Function.Injective g) {f : K →+* L}
    (hf1 : ∀ x, f (algebraMap A K x) = g x) : IsFractionRing.lift hg = f :=
  IsLocalization.lift_unique _ hf1

Uniqueness of Fraction Field Lift for Injective Homomorphisms

Informal description

Let $A$ be a commutative ring with field of fractions $K$, and let $g : A \to L$ be an injective ring homomorphism where $L$ is a field. If $f : K \to L$ is a ring homomorphism such that $f \circ \text{algebraMap}_A^K = g$, then $f$ must be equal to the lift $\text{IsFractionRing.lift}\ hg$.

IsFractionRing.ringHom_ext theorem

{f1 f2 : K →+* L} (hf : ∀ x : A, f1 (algebraMap A K x) = f2 (algebraMap A K x)) : f1 = f2

Full source

/-- Another version of unique to give two lift maps should be equal -/
theorem ringHom_ext {f1 f2 : K →+* L}
    (hf : ∀ x : A, f1 (algebraMap A K x) = f2 (algebraMap A K x)) : f1 = f2 := by
  ext z
  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := A) z
  rw [map_div₀, map_div₀, hf, hf]

Uniqueness of Ring Homomorphisms from Fraction Ring via Agreement on Base Ring

Informal description

Let $A$ be a commutative ring with fraction ring $K$, and let $L$ be a commutative ring. For any two ring homomorphisms $f_1, f_2 : K \to L$, if $f_1$ and $f_2$ agree on the image of $A$ in $K$ (i.e., $f_1 \circ \text{algebraMap}_A^K = f_2 \circ \text{algebraMap}_A^K$), then $f_1 = f_2$.

IsFractionRing.injective_comp_algebraMap theorem

: Function.Injective fun (f : K →+* L) => f.comp (algebraMap A K)

Full source

theorem injective_comp_algebraMap :
    Function.Injective fun (f : K →+* L) => f.comp (algebraMap A K) :=
  fun _ _ h => ringHom_ext (fun x => RingHom.congr_fun h x)

Injectivity of Ring Homomorphism Composition with Fraction Ring Algebra Map

Informal description

The map sending a ring homomorphism $f : K \to L$ to its composition with the algebra map $\text{algebraMap}_A^K : A \to K$ is injective. In other words, if two ring homomorphisms $f_1, f_2 : K \to L$ satisfy $f_1 \circ \text{algebraMap}_A^K = f_2 \circ \text{algebraMap}_A^K$, then $f_1 = f_2$.

IsFractionRing.liftAlgHom definition

: K →ₐ[R] L

Full source

/-- `AlgHom` version of `IsFractionRing.lift`. -/
noncomputable def liftAlgHom : K →ₐ[R] L :=
  IsLocalization.liftAlgHom fun y : nonZeroDivisors A => isUnit_map_of_injective hg y

Algebra homomorphism lift for fraction rings

Informal description

The algebra homomorphism version of the lifting construction for fraction rings. Given an injective algebra homomorphism $ g : R \to L $ from a commutative ring $ R $ to a commutative ring $ L $, this defines the unique algebra homomorphism $ K \to L $ extending $ g $, where $ K $ is the fraction ring of $ R $.

IsFractionRing.liftAlgHom_toRingHom theorem

: (liftAlgHom hg : K →ₐ[R] L).toRingHom = lift hg

Full source

theorem liftAlgHom_toRingHom : (liftAlgHom hg : K →ₐ[R] L).toRingHom = lift hg := rfl

Equality of Underlying Ring Homomorphisms in Fraction Ring Lift Construction

Informal description

The ring homomorphism obtained from the algebra homomorphism lift $\operatorname{liftAlgHom} hg$ is equal to the ring homomorphism lift $\operatorname{lift} hg$. In other words, the underlying ring homomorphism of $\operatorname{liftAlgHom} hg$ coincides with $\operatorname{lift} hg$.

IsFractionRing.coe_liftAlgHom theorem

: ⇑(liftAlgHom hg : K →ₐ[R] L) = lift hg

Full source

@[simp]
theorem coe_liftAlgHom : ⇑(liftAlgHom hg : K →ₐ[R] L) = lift hg := rfl

Equality of Underlying Functions for Algebra and Ring Homomorphism Lifts on Fraction Rings

Informal description

The underlying function of the algebra homomorphism $\operatorname{liftAlgHom} hg : K \toₐ[R] L$ is equal to the ring homomorphism $\operatorname{lift} hg : K \to+* L$, where $K$ is the fraction ring of $R$ and $hg$ is the proof that $g : R \to L$ is injective.

IsFractionRing.liftAlgHom_apply theorem

: liftAlgHom hg x = lift hg x

Full source

theorem liftAlgHom_apply : liftAlgHom hg x = lift hg x := rfl

Equality of Algebra and Ring Homomorphism Lifts on Fraction Rings

Informal description

For any element $x$ in the fraction ring $K$ of a commutative ring $R$, the algebra homomorphism lift $\operatorname{liftAlgHom} hg$ applied to $x$ equals the ring homomorphism lift $\operatorname{lift} hg$ applied to $x$, i.e., $\operatorname{liftAlgHom} hg (x) = \operatorname{lift} hg (x)$.

IsFractionRing.lift_algebraMap theorem

(hg : Injective g) (x) : lift hg (algebraMap A K x) = g x

Full source

/-- Given a commutative ring `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`. -/
@[simp]
theorem lift_algebraMap (hg : Injective g) (x) : lift hg (algebraMap A K x) = g x :=
  lift_eq _ _

Lift of Injective Homomorphism Preserves Algebra Map on Fraction Field

Informal description

Let $A$ be a commutative ring with field of fractions $K$, and let $g : A \to L$ be an injective ring homomorphism into a field $L$. Then for any $x \in A$, the lift of $g$ to $K$ (denoted $\operatorname{lift} hg$) satisfies $\operatorname{lift} hg (\operatorname{algebraMap} A K x) = g(x)$, where $\operatorname{algebraMap} A K$ is the canonical inclusion of $A$ into $K$.

IsFractionRing.lift_fieldRange theorem

(hg : Injective g) : (lift hg : K →+* L).fieldRange = Subfield.closure g.range

Full source

/-- The image of `IsFractionRing.lift` is the subfield generated by the image
of the ring hom. -/
theorem lift_fieldRange (hg : Injective g) :
    (lift hg : K →+* L).fieldRange = Subfield.closure g.range :=
  ringHom_fieldRange_eq_of_comp_eq (by ext; simp)

Image of Fraction Field Lift Equals Subfield Generated by Base Ring Homomorphism

Informal description

Let $A$ be a commutative ring with field of fractions $K$, and let $g : A \to L$ be an injective ring homomorphism into a field $L$. Then the image of the lifted homomorphism $\operatorname{lift} hg : K \to L$ is equal to the subfield of $L$ generated by the image of $g$, i.e., \[ \operatorname{fieldRange}(\operatorname{lift} hg) = \operatorname{Subfield.closure}(g(A)). \]

IsFractionRing.lift_fieldRange_eq_of_range_eq theorem

 (hg : Injective g) {s : Set L} (hs : g.range = Subring.closure s) : (lift hg : K →+* L).fieldRange = Subfield.closure s

Full source

/-- The image of `IsFractionRing.lift` is the subfield generated by `s`, if the image
of the ring hom is the subring generated by `s`. -/
theorem lift_fieldRange_eq_of_range_eq (hg : Injective g)
    {s : Set L} (hs : g.range = Subring.closure s) :
    (lift hg : K →+* L).fieldRange = Subfield.closure s :=
  ringHom_fieldRange_eq_of_comp_eq_of_range_eq (by ext; simp) hs

Image of Fraction Field Lift Equals Subfield Generated by Prescribed Set

Informal description

Let $A$ be a commutative ring with field of fractions $K$, and let $g \colon A \to L$ be an injective ring homomorphism into a field $L$. Given a subset $s \subseteq L$ such that the image of $g$ equals the subring generated by $s$, then the image of the lifted homomorphism $\operatorname{lift} hg \colon K \to L$ equals the subfield generated by $s$, i.e., \[ \operatorname{fieldRange}(\operatorname{lift} hg) = \operatorname{Subfield.closure}(s). \]

IsFractionRing.lift_mk' theorem

(hg : Injective g) (x) (y : nonZeroDivisors A) : lift hg (mk' K x y) = g x / g y

Full source

/-- Given a commutative ring `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`. -/
theorem lift_mk' (hg : Injective g) (x) (y : nonZeroDivisors A) :
    lift hg (mk' K x y) = g x / g y := by simp only [mk'_eq_div, map_div₀, lift_algebraMap]

Lift of Fraction to Field Preserves Division: $\operatorname{lift} hg \left( \frac{x}{y} \right) = \frac{g(x)}{g(y)}$

Informal description

Let $A$ be a commutative ring with field of fractions $K$, and let $g : A \to L$ be an injective ring homomorphism into a field $L$. For any $x \in A$ and any non-zero divisor $y \in A$, the lift of $g$ to $K$ satisfies \[ \operatorname{lift} hg \left( \frac{x}{y} \right) = \frac{g(x)}{g(y)}, \] where $\frac{x}{y}$ denotes the fraction ring element $\text{mk'}\ K\ x\ y$.

IsFractionRing.map definition

 {A B K L : Type*} [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 : Injective j) : K →+* L

Full source

/-- Given commutative rings `A, B` where `B` is an integral domain, with fraction rings `K`, `L`
and an injective ring hom `j : A →+* B`, we get a ring 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)⁻¹`. -/
noncomputable def map {A B K L : Type*} [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 : Injective j) : K →+* L :=
  IsLocalization.map L j
    (show nonZeroDivisors A ≤ (nonZeroDivisors B).comap j from
      nonZeroDivisors_le_comap_nonZeroDivisors_of_injective j hj)

Extension of injective ring homomorphism to fraction rings

Informal description

Given commutative rings $A$, $B$ where $B$ is an integral domain, with fraction rings $K$, $L$ respectively, and an injective ring homomorphism $j : A \to B$, the function `IsFractionRing.map` constructs a ring homomorphism from $K$ to $L$ that extends $j$ to the fraction rings. Specifically, for any $z \in K$ expressed as $z = f(x) \cdot (f(y))^{-1}$ where $(x, y) \in A \times (\text{nonZeroDivisors } A)$, the homomorphism maps $z$ to $g(j(x)) \cdot (g(j(y)))^{-1}$ in $L$.

IsFractionRing.ringEquivOfRingEquiv definition

: K ≃+* L

Full source

/-- Given rings `A, B` and localization maps to their fraction rings
`f : A →+* K, g : B →+* L`, an isomorphism `h : A ≃+* B` induces an isomorphism of
fraction rings `K ≃+* L`. -/
noncomputable def ringEquivOfRingEquiv : K ≃+* L :=
  IsLocalization.ringEquivOfRingEquiv K L h (MulEquivClass.map_nonZeroDivisors h)

Ring isomorphism of fraction rings induced by a ring isomorphism

Informal description

Given commutative rings $ A $ and $ B $ with fraction rings $ K $ and $ L $ respectively, and given a ring isomorphism $ h : A \simeq+* B $, the function `IsFractionRing.ringEquivOfRingEquiv` constructs a ring isomorphism $ K \simeq+* L $ between the fraction rings induced by $ h $.

IsFractionRing.ringEquivOfRingEquiv_algebraMap theorem

(a : A) : ringEquivOfRingEquiv h (algebraMap A K a) = algebraMap B L (h a)

Full source

@[simp]
lemma ringEquivOfRingEquiv_algebraMap
    (a : A) : ringEquivOfRingEquiv h (algebraMap A K a) = algebraMap B L (h a) := by
  simp [ringEquivOfRingEquiv]

Compatibility of Fraction Ring Isomorphism with Algebra Maps

Informal description

For any element $a$ in a commutative ring $A$, the ring isomorphism $\text{ringEquivOfRingEquiv}\, h$ between the fraction rings $K$ and $L$ maps the image of $a$ under the algebra map $A \to K$ to the image of $h(a)$ under the algebra map $B \to L$. In other words, the following diagram commutes: $$\text{ringEquivOfRingEquiv}\, h \circ \text{algebraMap}\, A\, K = \text{algebraMap}\, B\, L \circ h.$$

IsFractionRing.ringEquivOfRingEquiv_symm theorem

: (ringEquivOfRingEquiv h : K ≃+* L).symm = ringEquivOfRingEquiv h.symm

Full source

@[simp]
lemma ringEquivOfRingEquiv_symm :
    (ringEquivOfRingEquiv h : K ≃+* L).symm = ringEquivOfRingEquiv h.symm := rfl

Inverse of Induced Fraction Ring Isomorphism Equals Induced Inverse Isomorphism

Informal description

Given commutative rings $A$ and $B$ with fraction rings $K$ and $L$ respectively, and a ring isomorphism $h : A \simeq+* B$, the inverse of the induced ring isomorphism $\text{ringEquivOfRingEquiv}\, h : K \simeq+* L$ is equal to the ring isomorphism $\text{ringEquivOfRingEquiv}\, h^{-1}$ induced by the inverse isomorphism $h^{-1} : B \simeq+* A$.

IsFractionRing.algEquivOfAlgEquiv definition

: K ≃ₐ[R] L

Full source

/-- Given `R`-algebras `A, B` and localization maps to their fraction rings
`f : A →ₐ[R] K, g : B →ₐ[R] L`, an isomorphism `h : A ≃ₐ[R] B` induces an isomorphism of
fraction rings `K ≃ₐ[R] L`. -/
noncomputable def algEquivOfAlgEquiv : K ≃ₐ[R] L :=
  IsLocalization.algEquivOfAlgEquiv K L h (MulEquivClass.map_nonZeroDivisors h)

Fraction ring isomorphism induced by algebra isomorphism

Informal description

Given $R$-algebras $A$, $B$ with fraction rings $K$ and $L$ respectively, and an $R$-algebra isomorphism $h : A \simeq B$, this constructs an $R$-algebra isomorphism between the fraction rings $K \simeq L$ that is compatible with the localization maps.

IsFractionRing.algEquivOfAlgEquiv_algebraMap theorem

(a : A) : algEquivOfAlgEquiv h (algebraMap A K a) = algebraMap B L (h a)

Full source

@[simp]
lemma algEquivOfAlgEquiv_algebraMap
    (a : A) : algEquivOfAlgEquiv h (algebraMap A K a) = algebraMap B L (h a) := by
  simp [algEquivOfAlgEquiv]

Compatibility of Fraction Ring Isomorphism with Canonical Maps

Informal description

For any element $a$ in the commutative ring $A$, the algebra isomorphism $\text{algEquivOfAlgEquiv}\, h$ between the fraction rings $K$ and $L$ maps the canonical image of $a$ in $K$ to the canonical image of $h(a)$ in $L$. In other words, the following diagram commutes: \[ \text{algEquivOfAlgEquiv}\, h \circ \text{algebraMap}\, A\, K = \text{algebraMap}\, B\, L \circ h. \]

IsFractionRing.algEquivOfAlgEquiv_symm theorem

: (algEquivOfAlgEquiv h : K ≃ₐ[R] L).symm = algEquivOfAlgEquiv h.symm

Full source

@[simp]
lemma algEquivOfAlgEquiv_symm :
    (algEquivOfAlgEquiv h : K ≃ₐ[R] L).symm = algEquivOfAlgEquiv h.symm := rfl

Inverse of Fraction Ring Isomorphism Induced by Algebra Isomorphism

Informal description

The inverse of the algebra isomorphism $\text{algEquivOfAlgEquiv}\, h : K \simeq_{\text{Alg}[R]} L$ is equal to the algebra isomorphism $\text{algEquivOfAlgEquiv}\, h^{-1}$.

IsFractionRing.fieldEquivOfAlgEquiv definition

(f : B ≃ₐ[A] C) : FB ≃ₐ[FA] FC

Full source

/-- An algebra isomorphism of rings induces an algebra isomorphism of fraction fields. -/
noncomputable def fieldEquivOfAlgEquiv (f : B ≃ₐ[A] C) : FB ≃ₐ[FA] FC where
  __ := IsFractionRing.ringEquivOfRingEquiv f.toRingEquiv
  commutes' x := by
    obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := A) x
    simp_rw [map_div₀, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B FB]
    simp [← IsScalarTower.algebraMap_apply A C FC]

Fraction field isomorphism induced by an algebra isomorphism

Informal description

Given an algebra isomorphism $ f : B \simeq_{\text{Alg}[A]} C $ between $ A $-algebras $ B $ and $ C $, and given fraction fields $ FB $ and $ FC $ of $ B $ and $ C $ respectively (as $ A $-algebras), the function `IsFractionRing.fieldEquivOfAlgEquiv` constructs an algebra isomorphism $ FB \simeq_{\text{Alg}[FA]} FC $ between the fraction fields, where $ FA $ is the fraction field of $ A $. This isomorphism is induced by $ f $ and preserves the algebraic structure over $ FA $.

IsFractionRing.restrictScalars_fieldEquivOfAlgEquiv theorem

(f : B ≃ₐ[A] C) : (fieldEquivOfAlgEquiv FA FB FC f).restrictScalars A = algEquivOfAlgEquiv f

Full source

lemma restrictScalars_fieldEquivOfAlgEquiv (f : B ≃ₐ[A] C) :
    (fieldEquivOfAlgEquiv FA FB FC f).restrictScalars A = algEquivOfAlgEquiv f := by
  ext; rfl

Restriction of Fraction Field Isomorphism to Base Ring Equals Fraction Ring Isomorphism

Informal description

Given an $A$-algebra isomorphism $f : B \simeq_{\text{Alg}[A]} C$ and fraction fields $FB$ and $FC$ of $B$ and $C$ respectively (as $A$-algebras), the restriction of the fraction field isomorphism $\text{fieldEquivOfAlgEquiv}\, FA\, FB\, FC\, f$ to scalars in $A$ is equal to the fraction ring isomorphism $\text{algEquivOfAlgEquiv}\, f$.

IsFractionRing.fieldEquivOfAlgEquiv_algebraMap theorem

(f : B ≃ₐ[A] C) (b : B) : fieldEquivOfAlgEquiv FA FB FC f (algebraMap B FB b) = algebraMap C FC (f b)

Full source

/-- This says that `fieldEquivOfAlgEquiv f` is an extension of `f` (i.e., it agrees with `f` on
`B`). Whereas `(fieldEquivOfAlgEquiv f).commutes` says that `fieldEquivOfAlgEquiv f` fixes `K`. -/
@[simp]
lemma fieldEquivOfAlgEquiv_algebraMap (f : B ≃ₐ[A] C) (b : B) :
    fieldEquivOfAlgEquiv FA FB FC f (algebraMap B FB b) = algebraMap C FC (f b) :=
  ringEquivOfRingEquiv_algebraMap f.toRingEquiv b

Compatibility of Fraction Field Isomorphism with Algebra Maps

Informal description

Given an $A$-algebra isomorphism $f \colon B \simeq_{\text{Alg}[A]} C$ and fraction fields $FB$ and $FC$ of $B$ and $C$ respectively (as $A$-algebras), the fraction field isomorphism $\text{fieldEquivOfAlgEquiv}\, FA\, FB\, FC\, f$ satisfies \[ \text{fieldEquivOfAlgEquiv}\, f\, (\text{algebraMap}\, B\, FB\, b) = \text{algebraMap}\, C\, FC\, (f\, b) \] for any $b \in B$.

IsFractionRing.fieldEquivOfAlgEquiv_refl theorem

: fieldEquivOfAlgEquiv FA FB FB (AlgEquiv.refl : B ≃ₐ[A] B) = AlgEquiv.refl

Full source

@[simp]
lemma fieldEquivOfAlgEquiv_refl :
    fieldEquivOfAlgEquiv FA FB FB (AlgEquiv.refl : B ≃ₐ[A] B) = AlgEquiv.refl := by
  ext x
  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := B) x
  simp

Fraction Field Isomorphism Induced by Identity is Identity

Informal description

The fraction field isomorphism induced by the identity algebra isomorphism $\text{id} \colon B \simeq_{\text{Alg}[A]} B$ is equal to the identity isomorphism on the fraction field $FB$ of $B$.

IsFractionRing.fieldEquivOfAlgEquiv_trans theorem

 (f : B ≃ₐ[A] C) (g : C ≃ₐ[A] D) :
  fieldEquivOfAlgEquiv FA FB FD (f.trans g) = (fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g)

Full source

lemma fieldEquivOfAlgEquiv_trans (f : B ≃ₐ[A] C) (g : C ≃ₐ[A] D) :
    fieldEquivOfAlgEquiv FA FB FD (f.trans g) =
      (fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g) := by
  ext x
  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := B) x
  simp

Transitivity of Fraction Field Isomorphism under Composition of Algebra Isomorphisms

Informal description

Let $A$ be a commutative ring with fraction field $FA$, and let $B$, $C$, and $D$ be $A$-algebras with fraction fields $FB$, $FC$, and $FD$ respectively. Given $A$-algebra isomorphisms $f \colon B \simeq_{\text{Alg}[A]} C$ and $g \colon C \simeq_{\text{Alg}[A]} D$, the composition of the induced fraction field isomorphisms satisfies \[ \text{fieldEquivOfAlgEquiv}\, FA\, FB\, FD\, (f \circ g) = (\text{fieldEquivOfAlgEquiv}\, FA\, FB\, FC\, f) \circ (\text{fieldEquivOfAlgEquiv}\, FA\, FC\, FD\, g). \]

IsFractionRing.fieldEquivOfAlgEquivHom definition

: (B ≃ₐ[A] B) →* (L ≃ₐ[K] L)

Full source

/-- An algebra automorphism of a ring induces an algebra automorphism of its fraction field.

This is a bundled version of `fieldEquivOfAlgEquiv`. -/
noncomputable def fieldEquivOfAlgEquivHom : (B ≃ₐ[A] B) →* (L ≃ₐ[K] L) where
  toFun := fieldEquivOfAlgEquiv K L L
  map_one' := fieldEquivOfAlgEquiv_refl A B K L
  map_mul' f g := fieldEquivOfAlgEquiv_trans K L L L g f

Induced automorphism homomorphism on fraction fields

Informal description

The function `IsFractionRing.fieldEquivOfAlgEquivHom` constructs a monoid homomorphism from the group of algebra automorphisms of $B$ (as an $A$-algebra) to the group of algebra automorphisms of its fraction field $L$ (as a $K$-algebra), where $K$ is the fraction field of $A$. This homomorphism is defined by mapping each algebra automorphism $f \colon B \simeq_{\text{Alg}[A]} B$ to the induced automorphism `fieldEquivOfAlgEquiv K L L f` of the fraction field $L$.

IsFractionRing.fieldEquivOfAlgEquivHom_apply theorem

(f : B ≃ₐ[A] B) : fieldEquivOfAlgEquivHom K L f = fieldEquivOfAlgEquiv K L L f

Full source

@[simp]
lemma fieldEquivOfAlgEquivHom_apply (f : B ≃ₐ[A] B) :
    fieldEquivOfAlgEquivHom K L f = fieldEquivOfAlgEquiv K L L f :=
  rfl

Equality of Induced Fraction Field Automorphisms via Algebra Automorphism

Informal description

For any algebra automorphism $f \colon B \simeq_{\text{Alg}[A]} B$ of an $A$-algebra $B$, the induced automorphism on the fraction fields via `fieldEquivOfAlgEquivHom` is equal to the automorphism obtained by applying `fieldEquivOfAlgEquiv` to $f$, i.e., \[ \text{fieldEquivOfAlgEquivHom}\, K\, L\, f = \text{fieldEquivOfAlgEquiv}\, K\, L\, L\, f. \] Here, $K$ is the fraction field of $A$ and $L$ is the fraction field of $B$.

IsFractionRing.fieldEquivOfAlgEquivHom_injective theorem

: Function.Injective (fieldEquivOfAlgEquivHom K L : (B ≃ₐ[A] B) →* (L ≃ₐ[K] L))

Full source

lemma fieldEquivOfAlgEquivHom_injective :
    Function.Injective (fieldEquivOfAlgEquivHom K L : (B ≃ₐ[A] B) →* (L ≃ₐ[K] L)) := by
  intro f g h
  ext b
  simpa using AlgEquiv.ext_iff.mp h (algebraMap B L b)

Injectivity of Fraction Field Automorphism Induction

Informal description

The homomorphism `fieldEquivOfAlgEquivHom K L` from the group of $A$-algebra automorphisms of $B$ to the group of $K$-algebra automorphisms of its fraction field $L$ is injective. In other words, if two $A$-algebra automorphisms of $B$ induce the same automorphism on $L$ via this homomorphism, then they must be equal.

IsFractionRing.isFractionRing_iff_of_base_ringEquiv theorem

(h : R ≃+* P) : IsFractionRing R S ↔ @IsFractionRing P _ S _ ((algebraMap R S).comp h.symm.toRingHom).toAlgebra

Full source

theorem isFractionRing_iff_of_base_ringEquiv (h : R ≃+* P) :
    IsFractionRingIsFractionRing R S ↔
      @IsFractionRing P _ S _ ((algebraMap R S).comp h.symm.toRingHom).toAlgebra := by
  delta IsFractionRing
  convert isLocalization_iff_of_base_ringEquiv (nonZeroDivisors R) S h
  exact (MulEquivClass.map_nonZeroDivisors h).symm

Fraction Ring Characterization under Base Ring Isomorphism

Informal description

Let $R$ and $P$ be commutative rings, and let $S$ be a commutative ring with an algebra structure from $R$ to $S$. Given a ring isomorphism $h \colon R \to P$, the following are equivalent: 1. $S$ is the fraction ring of $R$ (i.e., $\text{IsFractionRing}\, R\, S$ holds). 2. $S$ is the fraction ring of $P$ with the algebra structure induced by composing the algebra map from $R$ to $S$ with the inverse of $h$. In other words, being a fraction ring is preserved under base change by a ring isomorphism.

IsFractionRing.nontrivial theorem

(R S : Type*) [CommRing R] [Nontrivial R] [CommRing S] [Algebra R S] [IsFractionRing R S] : Nontrivial S

Full source

protected theorem nontrivial (R S : Type*) [CommRing R] [Nontrivial R] [CommRing S] [Algebra R S]
    [IsFractionRing R S] : Nontrivial S := by
  apply nontrivial_of_ne
  · intro h
    apply @zero_ne_one R
    exact
      IsLocalization.injective S (le_of_eq rfl)
        (((algebraMap R S).map_zero.trans h).trans (algebraMap R S).map_one.symm)

Nontriviality of Fraction Ring: $R$ nontrivial $\implies$ $S$ nontrivial

Informal description

Let $R$ be a nontrivial commutative ring and $S$ a commutative ring with an algebra structure from $R$ to $S$. If $S$ is the fraction ring of $R$, then $S$ is also nontrivial.

algebraMap_injective_of_field_isFractionRing theorem

 (K L : Type*) [Field K] [Semiring L] [Nontrivial L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L]
  [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] : Function.Injective (algebraMap R S)

Full source

theorem algebraMap_injective_of_field_isFractionRing (K L : Type*) [Field K] [Semiring L]
    [Nontrivial L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L] [Algebra R L]
    [IsScalarTower R S L] [IsScalarTower R K L] : Function.Injective (algebraMap R S) := by
  refine Function.Injective.of_comp (f := algebraMap S L) ?_
  rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective R K)

Injectivity of Algebra Map in Fraction Ring Context

Informal description

Let $R$ be a commutative ring, $K$ a field, and $L$ a nontrivial semiring. Suppose $K$ is the fraction ring of $R$ (i.e., $\text{IsFractionRing}\, R\, K$ holds), and there are compatible algebra structures $R \to K \to L$ and $R \to S \to L$ forming scalar towers. Then the algebra map $\text{algebraMap} \colon R \to S$ is injective.

FaithfulSMul.of_field_isFractionRing theorem

 (K L : Type*) [Field K] [Semiring L] [Nontrivial L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L]
  [Algebra R L] [IsScalarTower R S L] [IsScalarTower R K L] : FaithfulSMul R S

Full source

theorem FaithfulSMul.of_field_isFractionRing (K L : Type*) [Field K] [Semiring L]
    [Nontrivial L] [Algebra R K] [IsFractionRing R K] [Algebra S L] [Algebra K L] [Algebra R L]
    [IsScalarTower R S L] [IsScalarTower R K L] : FaithfulSMul R S :=
  (faithfulSMul_iff_algebraMap_injective R S).mpr <|
    algebraMap_injective_of_field_isFractionRing R S K L

Faithfulness of Scalar Multiplication in Fraction Ring Context

Informal description

Let $R$ be a commutative ring, $K$ a field, and $L$ a nontrivial semiring. Suppose $K$ is the fraction ring of $R$ (i.e., $K$ is obtained by localizing $R$ at its non-zero divisors), and there are compatible algebra structures $R \to K \to L$ and $R \to S \to L$ forming scalar towers. Then the scalar multiplication action of $R$ on $S$ is faithful, meaning that distinct elements of $R$ act differently on $S$.

FractionRing abbrev

Full source

/-- 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`.
-/
abbrev FractionRing :=
  Localization (nonZeroDivisors R)

Fraction Ring Construction

Informal description

The fraction ring (or field of fractions) of a commutative ring $R$, denoted $\mathrm{Frac}(R)$, is constructed as a quotient type. This construction is also known as the *total fraction ring* of $R$. When $R$ is an integral domain, this yields a field of fractions.

FractionRing.unique instance

[Subsingleton R] : Unique (FractionRing R)

Full source

instance unique [Subsingleton R] : Unique (FractionRing R) := inferInstance

Uniqueness of the Fraction Ring for Subsingleton Base Ring

Informal description

If $R$ is a subsingleton (i.e., has at most one element), then the fraction ring $\mathrm{Frac}(R)$ has exactly one element.

FractionRing.instNontrivial instance

[Nontrivial R] : Nontrivial (FractionRing R)

Full source

instance [Nontrivial R] : Nontrivial (FractionRing R) := inferInstance

Nontriviality of the Fraction Ring

Informal description

For any nontrivial commutative ring $R$, the fraction ring $\mathrm{Frac}(R)$ is also nontrivial.

FractionRing.field instance

: Field (FractionRing A)

Full source

/-- 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 -/
noncomputable instance field : Field (FractionRing A) := inferInstance

Fraction Ring is a Field

Informal description

The fraction ring $\mathrm{Frac}(A)$ of a commutative ring $A$ is a field.

FractionRing.mk_eq_div theorem

{r s} : (Localization.mk r s : FractionRing A) = (algebraMap _ _ r / algebraMap A _ s : FractionRing A)

Full source

@[simp]
theorem mk_eq_div {r s} :
    (Localization.mk r s : FractionRing A) =
      (algebraMap _ _ r / algebraMap A _ s : FractionRing A) := by
  rw [Localization.mk_eq_mk', IsFractionRing.mk'_eq_div]

Fraction Construction as Quotient in Fraction Ring

Informal description

For any elements $r$ and $s$ in a commutative ring $A$, the element $\mathrm{mk}\ r\ s$ in the fraction ring $\mathrm{Frac}(A)$ is equal to the quotient of the images of $r$ and $s$ under the canonical algebra map from $A$ to $\mathrm{Frac}(A)$, i.e., \[ \mathrm{mk}\ r\ s = \frac{\mathrm{algebraMap}\ A\ \mathrm{Frac}(A)\ r}{\mathrm{algebraMap}\ A\ \mathrm{Frac}(A)\ s}. \]

FractionRing.liftAlgebra abbrev

: Algebra (FractionRing R) K

Full source

/-- 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]. -/
noncomputable abbrev liftAlgebra : Algebra (FractionRing R) K :=
  have := (FaithfulSMul.algebraMap_injective R K).isDomain
  RingHom.toAlgebra (IsFractionRing.lift (FaithfulSMul.algebraMap_injective R K))

Algebra Structure from Fraction Ring to Field Extension

Informal description

Given a commutative ring $R$ and its field of fractions $\mathrm{Frac}(R)$, there exists an algebra structure $\mathrm{Frac}(R) \to K$ for any field $K$ that extends the canonical map $R \to K$.

FractionRing.isScalarTower_liftAlgebra instance

: IsScalarTower R (FractionRing R) K

Full source

instance isScalarTower_liftAlgebra : IsScalarTower R (FractionRing R) K :=
  have := (FaithfulSMul.algebraMap_injective R K).isDomain
  .of_algebraMap_eq fun x ↦
    (IsFractionRing.lift_algebraMap (FaithfulSMul.algebraMap_injective R K) x).symm

Scalar Tower Structure for Fraction Ring and Field Extension

Informal description

For a commutative ring $R$ with field of fractions $\mathrm{Frac}(R)$ and any field $K$, the scalar multiplication action of $R$ on $K$ factors through $\mathrm{Frac}(R)$, forming a scalar tower structure. In other words, the composition of the canonical map $R \to \mathrm{Frac}(R)$ with the algebra map $\mathrm{Frac}(R) \to K$ is compatible with the scalar multiplication action of $R$ on $K$.

FractionRing.algebraMap_liftAlgebra theorem

 :
  have := (FaithfulSMul.algebraMap_injective R K).isDomain
  algebraMap (FractionRing R) K = IsFractionRing.lift (FaithfulSMul.algebraMap_injective R _)

Full source

lemma algebraMap_liftAlgebra :
    have := (FaithfulSMul.algebraMap_injective R K).isDomain
    algebraMap (FractionRing R) K = IsFractionRing.lift (FaithfulSMul.algebraMap_injective R _) :=
  rfl

Equality of Fraction Ring Algebra Map and Lift of Injective Map

Informal description

Let $R$ be a commutative ring and $K$ a field with an $R$-algebra structure such that the scalar multiplication action of $R$ on $K$ is faithful. Then the algebra map from the fraction ring $\mathrm{Frac}(R)$ to $K$ is equal to the lift of the injective algebra map from $R$ to $K$, i.e., \[ \mathrm{algebraMap}_{\mathrm{Frac}(R) \to K} = \mathrm{IsFractionRing.lift}(\mathrm{FaithfulSMul.algebraMap\_injective}_{R \to K}). \]

FractionRing.instIsScalarTower instance

 {R₀} [SMul R₀ R] [IsScalarTower R₀ R R] [SMul R₀ K] [IsScalarTower R₀ R K] : IsScalarTower R₀ (FractionRing R) K

Full source

instance {R₀} [SMul R₀ R] [IsScalarTower R₀ R R] [SMul R₀ K] [IsScalarTower R₀ R K] :
    IsScalarTower R₀ (FractionRing R) K where
  smul_assoc r₀ r k := r.ind fun ⟨r, s⟩ ↦ by
    simp_rw [Localization.smul_mk, Algebra.smul_def, Localization.mk_eq_mk',
      algebraMap_liftAlgebra, IsFractionRing.lift_mk', mul_comm_div, ← Algebra.smul_def, smul_assoc]

Scalar Tower Property for Fraction Rings

Informal description

For any commutative ring $R$ with fraction ring $\mathrm{Frac}(R)$, and any scalar action of $R_0$ on $R$ and $K$ such that $R_0$ acts compatibly with $R$ and $K$, the scalar action of $R_0$ on $\mathrm{Frac}(R)$ is compatible with its action on $K$. In other words, the following diagram commutes for all $r_0 \in R_0$, $x \in \mathrm{Frac}(R)$, and $k \in K$: \[ r_0 \cdot (x \cdot k) = (r_0 \cdot x) \cdot k. \]

FractionRing.algEquiv definition

(K : Type*) [CommRing K] [Algebra A K] [IsFractionRing A K] : FractionRing A ≃ₐ[A] K

Full source

/-- Given a ring `A` and a localization map to a fraction ring
`f : A →+* K`, we get an `A`-isomorphism between the fraction ring of `A` as a quotient
type and `K`. -/
noncomputable def algEquiv (K : Type*) [CommRing K] [Algebra A K] [IsFractionRing A K] :
    FractionRingFractionRing A ≃ₐ[A] K :=
  Localization.algEquiv (nonZeroDivisors A) K

Isomorphism between fraction ring and its localization

Informal description

Given a commutative ring $A$ and a commutative ring $K$ with an $A$-algebra structure, if $K$ is the fraction ring of $A$ (i.e., $K$ is obtained by localizing $A$ at its non-zero divisors), then there exists an $A$-algebra isomorphism between the fraction ring of $A$ (as a quotient type) and $K$.

FractionRing.instFaithfulSMul instance

[Algebra R A] [FaithfulSMul R A] : FaithfulSMul R (FractionRing A)

Full source

instance [Algebra R A] [FaithfulSMul R A] : FaithfulSMul R (FractionRing A) := by
  rw [faithfulSMul_iff_algebraMap_injective, IsScalarTower.algebraMap_eq R A]
  exact (FaithfulSMul.algebraMap_injective A (FractionRing A)).comp
    (FaithfulSMul.algebraMap_injective R A)

Faithful Scalar Multiplication in Fraction Rings

Informal description

For any commutative ring $R$ and its fraction ring $\mathrm{Frac}(R)$, if the scalar multiplication action of $R$ on $A$ is faithful, then the scalar multiplication action of $R$ on $\mathrm{Frac}(A)$ is also faithful. This means that distinct elements of $R$ act differently on $\mathrm{Frac}(A)$ via scalar multiplication.

Mathlib.RingTheory.Localization.FractionRing

Main definitions

Main results

Implementation notes

Tags