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

Main definitions #

is_fraction_ring R K expresses that K is a field of fractions of R, as an abbreviation of is_localization (non_zero_divisors R) K

Main results #

is_fraction_ring.field: a definition (not an instance) stating the localization of an integral domain R at R \ {0} is a field
rat.is_fraction_ring is an instance stating ℚ is the field of fractions of ℤ

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

source

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.

source

@[protected, instance]

def rat.is_fraction_ring :

is_fraction_ring ℤ ℚ

The cast from int to rat as a fraction_ring.

source

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

source

@[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] :

function.injective ⇑(algebra_map R K)

source

@[protected, instance]

def is_fraction_ring.no_zero_smul_divisors {R : Type u_1} [comm_ring R] {K : Type u_5} [comm_ring K] [algebra R K] [is_fraction_ring R K] [no_zero_divisors K] :

no_zero_smul_divisors R K

source

@[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 ∈ R⁰) :

⇑(algebra_map R K) x ≠ 0

source

@[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] :

is_domain K

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

source

@[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) :

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

Equations

is_fraction_ring.inv A z = dite (z = 0) (λ (h : z = 0), 0) (λ (h : ¬z = 0), is_localization.mk' K ↑((is_localization.sec A⁰ z).snd) ⟨(is_localization.sec A⁰ z).fst, _⟩)

source

@[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) :

x * is_fraction_ring.inv A x = 1

source

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] :

field 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

is_fraction_ring.to_field A = {add := comm_ring.add (show comm_ring K, from _inst_7), add_assoc := _, zero := comm_ring.zero (show comm_ring K, from _inst_7), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul (show comm_ring K, from _inst_7), nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg (show comm_ring K, from _inst_7), sub := comm_ring.sub (show comm_ring K, from _inst_7), sub_eq_add_neg := _, zsmul := comm_ring.zsmul (show comm_ring K, from _inst_7), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul (show comm_ring K, from _inst_7), mul_assoc := _, one := comm_ring.one (show comm_ring K, from _inst_7), one_mul := _, mul_one := _, npow := comm_ring.npow (show comm_ring K, from _inst_7), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := is_fraction_ring.inv A _inst_11, div := div_inv_monoid.div._default comm_ring.mul is_fraction_ring.to_field._proof_20 comm_ring.one is_fraction_ring.to_field._proof_21 is_fraction_ring.to_field._proof_22 comm_ring.npow is_fraction_ring.to_field._proof_23 is_fraction_ring.to_field._proof_24 (is_fraction_ring.inv A), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default comm_ring.mul is_fraction_ring.to_field._proof_26 comm_ring.one is_fraction_ring.to_field._proof_27 is_fraction_ring.to_field._proof_28 comm_ring.npow is_fraction_ring.to_field._proof_29 is_fraction_ring.to_field._proof_30 (is_fraction_ring.inv A), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

source

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 ∈ A⁰) :

is_localization.mk' K r ⟨s, hs⟩ = ⇑(algebra_map A K) r / ⇑(algebra_map A K) s

source

@[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 : ↥A⁰) :

is_localization.mk' K r s = ⇑(algebra_map A K) r / ⇑(algebra_map A K) ↑s

source

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 ∈ A⁰), ⇑(algebra_map A K) x / ⇑(algebra_map A K) y = z

source

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 : ↥A⁰) :

is_unit (⇑g ↑y)

source

@[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 : ↥R⁰} :

is_localization.mk' K x y = 0 ↔ x = 0

source

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 : ↥A⁰} :

is_localization.mk' K x y = 1 ↔ x = ↑y

source

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

is_fraction_ring.lift hg = is_localization.lift _

source

@[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) :

⇑(is_fraction_ring.lift hg) (⇑(algebra_map 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.

source

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 : ↥A⁰) :

⇑(is_fraction_ring.lift hg) (is_localization.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 ∈ non_zero_divisors A.

source

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

is_fraction_ring.map hj = is_localization.map L j _

source

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

is_fraction_ring.field_equiv_of_ring_equiv h = is_localization.ring_equiv_of_ring_equiv K L h _

source

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) :

is_fraction_ring R S ↔ is_fraction_ring P S

source

@[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] :

nontrivial S

source

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

fraction_ring R = localization R⁰

source

@[protected, instance]

def fraction_ring.unique (R : Type u_1) [comm_ring R] [subsingleton R] :

unique (fraction_ring R)

Equations

fraction_ring.unique R = localization.unique

source

@[protected, instance]

def fraction_ring.nontrivial (R : Type u_1) [comm_ring R] [nontrivial R] :

nontrivial (fraction_ring R)

source

@[protected, instance]

noncomputable def fraction_ring.field {A : Type u_4} [comm_ring A] [is_domain A] :

field (fraction_ring A)

Equations

fraction_ring.field = {add := has_add.add localization.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (sub_neg_monoid.to_add_monoid (fraction_ring A)), nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg localization.has_neg, sub := has_sub.sub (sub_neg_monoid.to_has_sub (fraction_ring A)), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul (add_group.to_sub_neg_monoid (fraction_ring A)), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul (localization.has_mul A⁰), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := localization.npow A⁰, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := field.inv (is_fraction_ring.to_field A), div := field.div (is_fraction_ring.to_field A), div_eq_mul_inv := _, zpow := field.zpow (is_fraction_ring.to_field A), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

source

@[simp]

theorem fraction_ring.mk_eq_div {A : Type u_4} [comm_ring A] [is_domain A] {r : A} {s : ↥A⁰} :

localization.mk r s = ⇑(algebra_map A (fraction_ring A)) r / ⇑(algebra_map A (fraction_ring A)) ↑s

source

@[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] :

algebra (fraction_ring R) K

Equations

fraction_ring.algebra R K = (is_fraction_ring.lift _).to_algebra

source

@[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] :

is_scalar_tower R (fraction_ring R) K

source

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] :

fraction_ring A ≃ₐ[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

fraction_ring.alg_equiv A K = localization.alg_equiv A⁰ K

source

@[protected, instance]

def fraction_ring.no_zero_smul_divisors (R : Type u_1) [comm_ring R] (A : Type u_4) [comm_ring A] [is_domain A] [algebra R A] [no_zero_smul_divisors R A] :

no_zero_smul_divisors R (fraction_ring A)