mathlib3 documentation

ring_theory.localization.inv_submonoid

Submonoid of inverses #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

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]
@[simp]
@[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)