# 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 `Mathlib/RingTheory/Localization/Basic.lean` for a design overview.

## Tags #

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

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

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`.

Equations

- IsLocalization.IsInteger R a = (a ∈ (algebraMap R S).rangeS)

Instances For

source
theorem IsLocalization.isInteger_zero {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] :
IsInteger R 0
source
theorem IsLocalization.isInteger_one {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] :
IsInteger R 1
source
theorem IsLocalization.isInteger_add {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {a b : S} (ha : IsInteger R a) (hb : IsInteger R b) :
IsInteger R (a + b)
source
theorem IsLocalization.isInteger_mul {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {a b : S} (ha : IsInteger R a) (hb : IsInteger R b) :
IsInteger R (a * b)
source
theorem IsLocalization.isInteger_smul {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {a : R} {b : S} (hb : IsInteger R b) :
IsInteger R (a • b)
source
theorem IsLocalization.exists_integer_multiple' {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (a : S) :
∃ (b : ↥M), IsInteger R (a * (algebraMap R 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 `LocalizationMap.surj`.

source
theorem IsLocalization.exists_integer_multiple {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (a : S) :
∃ (b : ↥M), 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.

source
theorem IsLocalization.exist_integer_multiples {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {ι : Type u_4} (s : Finset ι) (f : ι → S) :
∃ (b : ↥M), ∀ i ∈ s, IsInteger R (↑b • f i)

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

source
theorem IsLocalization.exist_integer_multiples_of_finite {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {ι : Type u_4} [Finite ι] (f : ι → S) :
∃ (b : ↥M), ∀ (i : ι), IsInteger R (↑b • f i)

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

source
theorem IsLocalization.exist_integer_multiples_of_finset {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (s : Finset S) :
∃ (b : ↥M), ∀ a ∈ s, IsInteger R (↑b • a)

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

source
noncomputable def IsLocalization.commonDenom {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {ι : Type u_4} (s : Finset ι) (f : ι → S) :
↥M

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

Equations

- IsLocalization.commonDenom M s f = ⋯.choose

Instances For

source
noncomputable def IsLocalization.integerMultiple {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {ι : Type u_4} (s : Finset ι) (f : ι → S) (i : ↥s) :
R

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

Equations

- IsLocalization.integerMultiple M s f i = Exists.choose ⋯

Instances For

source
@[simp]
theorem IsLocalization.map_integerMultiple {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {ι : Type u_4} (s : Finset ι) (f : ι → S) (i : ↥s) :
(algebraMap R S) (integerMultiple M s f i) = commonDenom M s f • f ↑i
source
noncomputable def IsLocalization.commonDenomOfFinset {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (s : Finset S) :
↥M

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

Equations

- IsLocalization.commonDenomOfFinset M s = IsLocalization.commonDenom M s id

Instances For

source
noncomputable def IsLocalization.finsetIntegerMultiple {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] [DecidableEq R] (s : Finset S) :
Finset R

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

Equations

- IsLocalization.finsetIntegerMultiple M s = Finset.image (fun (t : ↥s) => IsLocalization.integerMultiple M s id t) s.attach

Instances For

source
theorem IsLocalization.finsetIntegerMultiple_image {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] [DecidableEq R] (s : Finset S) :
⇑(algebraMap R S) '' ↑(finsetIntegerMultiple M s) = commonDenomOfFinset M s • ↑s