mathlib documentation

ring_theory.localization.integer

Integer elements of a localization #

Main definitions #

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] [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
theorem is_localization.is_integer_zero {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] :
theorem is_localization.is_integer_one {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [algebra R S] :
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) :
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) :
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) :
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) :

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

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_smul instance.

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 sis_localization.is_integer R (b f i)

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

theorem is_localization.exist_integer_multiples_of_finite {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} [finite ι] (f : ι → S) :
∃ (b : M), ∀ (i : ι), is_localization.is_integer R (b f i)

We can clear the denominators of a finite 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] [algebra R S] [is_localization M S] (s : finset S) :
∃ (b : M), ∀ (a : S), a sis_localization.is_integer R (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] [algebra R S] [is_localization M 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] [algebra R S] [is_localization M 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] [algebra R S] [is_localization M S] {ι : Type u_3} (s : finset ι) (f : ι → S) (i : s) :
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) :

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

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

Equations