mathlib documentation

ring_theory.localization.fraction_ring

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

Main definitions #

Main results #

Implementation notes #

See src/ring_theory/localization/basic.lean for a design overview.

Tags #

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

def is_fraction_ring (R : Type u_1) [comm_ring R] (K : Type u_5) [comm_ring K] [algebra R K] :
Prop

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

@[protected, instance]

The cast from int to rat as a fraction_ring.

theorem is_fraction_ring.to_map_eq_zero_iff {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [algebra R K] [is_fraction_ring R K] {x : R} :
(algebra_map R K) x = 0 x = 0
@[protected]
theorem is_fraction_ring.injective (R : Type u_1) [comm_ring R] (K : Type u_5) [comm_ring K] [algebra R K] [is_fraction_ring R K] :
@[protected, instance]
@[protected]
theorem is_fraction_ring.to_map_ne_zero_of_mem_non_zero_divisors {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [algebra R K] [is_fraction_ring R K] [nontrivial R] {x : R} (hx : x non_zero_divisors R) :
@[protected]
theorem is_fraction_ring.is_domain (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] :

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

@[protected]
noncomputable def is_fraction_ring.inv (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] (z : K) :
K

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

Equations
@[protected]
theorem is_fraction_ring.mul_inv_cancel (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] (x : K) (hx : x 0) :
noncomputable def is_fraction_ring.to_field (A : Type u_4) [comm_ring A] [is_domain A] {K : Type u_5} [comm_ring K] [algebra A K] [is_fraction_ring A K] :

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

Equations
theorem is_fraction_ring.mk'_mk_eq_div {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] {r s : A} (hs : s non_zero_divisors A) :
@[simp]
theorem is_fraction_ring.mk'_eq_div {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] {r : A} (s : (non_zero_divisors A)) :
theorem is_fraction_ring.div_surjective {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] (z : K) :
∃ (x y : A) (hy : y non_zero_divisors A), (algebra_map A K) x / (algebra_map A K) y = z
theorem is_fraction_ring.is_unit_map_of_injective {A : Type u_4} [comm_ring A] [is_domain A] {L : Type u_7} [field L] {g : A →+* L} (hg : function.injective g) (y : (non_zero_divisors A)) :
@[simp]
theorem is_fraction_ring.mk'_eq_zero_iff_eq_zero {R : Type u_1} [comm_ring R] {K : Type u_5} [field K] [algebra R K] [is_fraction_ring R K] {x : R} {y : (non_zero_divisors R)} :
theorem is_fraction_ring.mk'_eq_one_iff_eq {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] [algebra A K] [is_fraction_ring A K] {x : A} {y : (non_zero_divisors A)} :
noncomputable def is_fraction_ring.lift {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring 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 × (non_zero_divisors A) are such that z = f x * (f y)⁻¹.

Equations
@[simp]
theorem is_fraction_ring.lift_algebra_map {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] {g : A →+* L} (hg : function.injective g) (x : A) :

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 is_fraction_ring.lift_mk' {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] {g : A →+* L} (hg : function.injective g) (x : A) (y : (non_zero_divisors A)) :

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 ∈ non_zero_divisors A.

noncomputable def is_fraction_ring.map {A : Type u_1} {B : Type u_2} {K : Type u_3} {L : Type u_4} [comm_ring A] [comm_ring B] [is_domain B] [comm_ring K] [algebra A K] [is_fraction_ring A K] [comm_ring L] [algebra B L] [is_fraction_ring 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 × (non_zero_divisors A) are such that z = f x * (f y)⁻¹.

Equations
noncomputable def is_fraction_ring.field_equiv_of_ring_equiv {A : Type u_4} [comm_ring A] [is_domain A] {K : Type u_5} {B : Type u_6} [comm_ring B] [is_domain B] [field K] {L : Type u_7} [field L] [algebra A K] [is_fraction_ring A K] [algebra B L] [is_fraction_ring 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
theorem is_fraction_ring.is_fraction_ring_iff_of_base_ring_equiv {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] {P : Type u_3} [comm_ring P] (h : R ≃+* P) :
@[protected]
theorem is_fraction_ring.nontrivial (R : Type u_1) (S : Type u_2) [comm_ring R] [nontrivial R] [comm_ring S] [algebra R S] [is_fraction_ring R S] :
def fraction_ring (R : Type u_1) [comm_ring 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.

Equations
@[protected, instance]
def fraction_ring.unique (R : Type u_1) [comm_ring R] [subsingleton R] :
Equations
@[protected, instance]
@[simp]
@[protected, instance]
noncomputable def fraction_ring.algebra (R : Type u_1) [comm_ring R] (K : Type u_5) [is_domain R] [field K] [algebra R K] [no_zero_smul_divisors R K] :
Equations
@[protected, instance]
def fraction_ring.is_scalar_tower (R : Type u_1) [comm_ring R] (K : Type u_5) [is_domain R] [field K] [algebra R K] [no_zero_smul_divisors R K] :
noncomputable def fraction_ring.alg_equiv (A : Type u_4) [comm_ring A] [is_domain A] (K : Type u_1) [field K] [algebra A K] [is_fraction_ring 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
@[protected, instance]