# mathlibdocumentation

ring_theory.localization.inv_submonoid

# Submonoid of inverses #

## Main definitions #

• is_localization.inv_submonoid M S is the submonoid of S = M⁻¹R consisting of inverses of each element x ∈ M

## 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.inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] :

The submonoid of S = M⁻¹R consisting of { 1 / x | x ∈ M }.

Equations
theorem is_localization.submonoid_map_le_is_unit {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] :
M
noncomputable def is_localization.equiv_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] :

There is an equivalence of monoids between the image of M and inv_submonoid.

noncomputable def is_localization.to_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] :

There is a canonical map from M to inv_submonoid sending x to 1 / x.

Equations
theorem is_localization.to_inv_submonoid_surjective {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] :
@[simp]
theorem is_localization.to_inv_submonoid_mul {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] (m : M) :
m) * S) m = 1
@[simp]
theorem is_localization.mul_to_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] (m : M) :
S) m * m) = 1
@[simp]
theorem is_localization.smul_to_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] (m : M) :
m m) = 1
theorem is_localization.surj' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (z : S) :
∃ (r : R) (m : M), z = r m)
theorem is_localization.to_inv_submonoid_eq_mk' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (x : M) :
x) = x
theorem is_localization.mem_inv_submonoid_iff_exists_mk' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [ S] [ S] (x : S) :
∃ (m : M), m = x
theorem is_localization.span_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] :
theorem is_localization.finite_type_of_monoid_fg {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [ S] [ S] [monoid.fg M] :