# mathlibdocumentation

ring_theory.localization.integer

# Integer elements of a localization #

## Main definitions #

• is_localization.is_integer is a predicate stating that x : S is in the image of R

## 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_localization.is_integer (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [ S] (a : S) :
Prop

Given a : S, S a localization of R, is_integer R a iff a is in the image of the localization map from R to S.

Equations
theorem is_localization.is_integer_zero {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] :
theorem is_localization.is_integer_one {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] :
theorem is_localization.is_integer_add {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {a b : S} (ha : a) (hb : b) :
(a + b)
theorem is_localization.is_integer_mul {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {a b : S} (ha : a) (hb : b) :
(a * b)
theorem is_localization.is_integer_smul {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] {a : R} {b : S} (hb : b) :
(a b)
theorem is_localization.exists_integer_multiple' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (a : S) :
∃ (b : M), (a * S) b)

Each element a : S has an M-multiple which is an integer.

This version multiplies a on the right, matching the argument order in localization_map.surj.

theorem is_localization.exists_integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (a : S) :
∃ (b : M), (b a)

Each element a : S has an M-multiple which is an integer.

This version multiplies a on the left, matching the argument order in the has_scalar instance.

theorem is_localization.exist_integer_multiples {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} (s : finset ι) (f : ι → S) :
∃ (b : M), ∀ (i : ι), i s (b f i)

We can clear the denominators of a finset-indexed family of fractions.

theorem is_localization.exist_integer_multiples_of_fintype {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} [fintype ι] (f : ι → S) :
∃ (b : M), ∀ (i : ι), (b f i)

We can clear the denominators of a fintype-indexed family of fractions.

theorem is_localization.exist_integer_multiples_of_finset {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (s : finset S) :
∃ (b : M), ∀ (a : S), a s (b a)

We can clear the denominators of a finite set of fractions.

noncomputable def is_localization.common_denom {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} (s : finset ι) (f : ι → S) :

A choice of a common multiple of the denominators of a finset-indexed family of fractions.

Equations
noncomputable def is_localization.integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} (s : finset ι) (f : ι → S) (i : s) :
R

The numerator of a fraction after clearing the denominators of a finset-indexed family of fractions.

Equations
@[simp]
theorem is_localization.map_integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] {ι : Type u_3} (s : finset ι) (f : ι → S) (i : s) :
S) i) = f i
noncomputable def is_localization.common_denom_of_finset {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (s : finset S) :

A choice of a common multiple of the denominators of a finite set of fractions.

Equations
noncomputable def is_localization.finset_integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] [decidable_eq R] (s : finset S) :

The finset of numerators after clearing the denominators of a finite set of fractions.

Equations
theorem is_localization.finset_integer_multiple_image {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] [decidable_eq R] (s : finset S) :