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

source

def is_localization.is_integer (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R 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

is_localization.is_integer R a = (a ∈ (algebra_map R S).range)

source

theorem is_localization.is_integer_zero {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] :

is_localization.is_integer R 0

source

theorem is_localization.is_integer_one {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] :

is_localization.is_integer R 1

source

theorem is_localization.is_integer_add {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {a b : S} (ha : is_localization.is_integer R a) (hb : is_localization.is_integer R b) :

is_localization.is_integer R (a + b)

source

theorem is_localization.is_integer_mul {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {a b : S} (ha : is_localization.is_integer R a) (hb : is_localization.is_integer R b) :

is_localization.is_integer R (a * b)

source

theorem is_localization.is_integer_smul {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] {a : R} {b : S} (hb : is_localization.is_integer R b) :

is_localization.is_integer R (a • b)

source

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

∃ (b : ↥M), is_localization.is_integer R (a * ⇑(algebra_map 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 localization_map.surj.

source

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

∃ (b : ↥M), is_localization.is_integer 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 has_scalar instance.

source

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

∃ (b : ↥M), ∀ (i : ι), i ∈ s → is_localization.is_integer R (↑b • f i)

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

source

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] [algebra R S] [is_localization M S] {ι : Type u_3} [fintype ι] (f : ι → S) :

∃ (b : ↥M), ∀ (i : ι), is_localization.is_integer R (↑b • f i)

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

source

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] [algebra R S] [is_localization M S] (s : finset S) :

∃ (b : ↥M), ∀ (a : S), a ∈ s → is_localization.is_integer R (↑b • a)

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

source

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

↥M

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

Equations

is_localization.common_denom M s f = _.some

source

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

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

Equations

is_localization.integer_multiple M s f i = Exists.some _

source

@[simp]

theorem is_localization.map_integer_multiple {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {ι : Type u_3} (s : finset ι) (f : ι → S) (i : ↥s) :

⇑(algebra_map R S) (is_localization.integer_multiple M s f i) = is_localization.common_denom M s f • f ↑i

source

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] [algebra R S] [is_localization M S] (s : finset S) :

↥M

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

Equations

is_localization.common_denom_of_finset M s = is_localization.common_denom M s id

source

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

finset R

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

Equations

is_localization.finset_integer_multiple M s = finset.image (λ (t : {x // x ∈ s}), is_localization.integer_multiple M s id t) s.attach

source

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

⇑(algebra_map R S) '' ↑(is_localization.finset_integer_multiple M s) = is_localization.common_denom_of_finset M s • ↑s