# Documentation

Mathlib.RingTheory.Localization.Integer

# Integer elements of a localization #

## Main definitions #

• IsLocalization.IsInteger is a predicate stating that x : S is in the image of R

## 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

def IsLocalization.IsInteger (R : Type u_1) [] {S : Type u_2} [] [Algebra R S] (a : S) :

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

Instances For
theorem IsLocalization.isInteger_zero {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] :
theorem IsLocalization.isInteger_one {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] :
theorem IsLocalization.isInteger_add {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] {a : S} {b : S} (ha : ) (hb : ) :
theorem IsLocalization.isInteger_mul {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] {a : S} {b : S} (ha : ) (hb : ) :
theorem IsLocalization.isInteger_smul {R : Type u_1} [] {S : Type u_2} [] [Algebra R S] {a : R} {b : S} (hb : ) :
theorem IsLocalization.exists_integer_multiple' {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (a : S) :
b, IsLocalization.IsInteger R (a * ↑() 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 LocalizationMap.surj.

theorem IsLocalization.exists_integer_multiple {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (a : S) :
b, IsLocalization.IsInteger R (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 SMul instance.

theorem IsLocalization.exist_integer_multiples {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] {ι : Type u_4} (s : ) (f : ιS) :
b, ∀ (i : ι), i sIsLocalization.IsInteger R (b f i)

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

theorem IsLocalization.exist_integer_multiples_of_finite {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] {ι : Type u_4} [] (f : ιS) :
b, ∀ (i : ι), IsLocalization.IsInteger R (b f i)

We can clear the denominators of a finite indexed family of fractions.

theorem IsLocalization.exist_integer_multiples_of_finset {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (s : ) :
b, ∀ (a : S), a sIsLocalization.IsInteger R (b a)

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

noncomputable def IsLocalization.commonDenom {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] {ι : Type u_4} (s : ) (f : ιS) :
{ x // x M }

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

Instances For
noncomputable def IsLocalization.integerMultiple {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] {ι : Type u_4} (s : ) (f : ιS) (i : { x // x s }) :
R

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

Instances For
@[simp]
theorem IsLocalization.map_integerMultiple {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] {ι : Type u_4} (s : ) (f : ιS) (i : { x // x s }) :
↑() () = f i
noncomputable def IsLocalization.commonDenomOfFinset {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (s : ) :
{ x // x M }

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

Instances For
noncomputable def IsLocalization.finsetIntegerMultiple {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] [] (s : ) :

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

Instances For
theorem IsLocalization.finsetIntegerMultiple_image {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] [] (s : ) :
↑() '' =