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) [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 ∈ RingHom.rangeS (algebraMap R S))

theorem IsLocalization.isInteger_zero {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] : IsLocalization.IsInteger R 0

theorem IsLocalization.isInteger_one {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] : IsLocalization.IsInteger R 1

theorem IsLocalization.isInteger_add {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {a : S} {b : S} (ha : IsLocalization.IsInteger R a) (hb : IsLocalization.IsInteger R b) : IsLocalization.IsInteger R (a + b)

theorem IsLocalization.isInteger_mul {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {a : S} {b : S} (ha : IsLocalization.IsInteger R a) (hb : IsLocalization.IsInteger R b) : IsLocalization.IsInteger R (a * b)

theorem IsLocalization.isInteger_smul {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {a : R} {b : S} (hb : IsLocalization.IsInteger R b) : IsLocalization.IsInteger R (a • b)

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), IsLocalization.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.

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), 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} [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, IsLocalization.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} [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 : ι), 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} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] (s : Finset S) : ∃ (b : ↥M), ∀ a ∈ s, IsLocalization.IsInteger R (↑b • a)

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

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 = Exists.choose (_ : ∃ (b : ↥M), ∀ i ∈ s, IsLocalization.IsInteger R (↑b • f i))

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 : { x : ι // x ∈ 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 (_ : IsLocalization.IsInteger R (↑(Exists.choose (_ : ∃ (b : ↥M), ∀ i ∈ s, IsLocalization.IsInteger R (↑b • f i))) • f ↑i))

@[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 : { x : ι // x ∈ s }) : (algebraMap R S) (IsLocalization.integerMultiple M s f i) = IsLocalization.commonDenom M s f • f ↑i

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

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 : { x : S // x ∈ s }) => IsLocalization.integerMultiple M s id t) (Finset.attach s)

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) '' ↑(IsLocalization.finsetIntegerMultiple M s) = IsLocalization.commonDenomOfFinset M s • ↑s