mathlib documentation

ring_theory.localization.inv_submonoid

Submonoid of inverses #

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

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

Equations
@[reducible]
noncomputable def is_localization.equiv_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M 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] [algebra R S] [is_localization M S] :

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

Equations
@[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] [algebra R S] [is_localization M S] (m : M) :
@[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] [algebra R S] [is_localization M S] (m : M) :
@[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] [algebra R S] [is_localization M S] (m : M) :
theorem is_localization.surj' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (z : S) :
∃ (r : R) (m : M), z = r ((is_localization.to_inv_submonoid M S) 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] [algebra R S] [is_localization M S] (x : M) :
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] [algebra R S] [is_localization M S] (x : 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] [algebra R S] [is_localization M S] [monoid.fg M] :