Submonoid of inverses #

Main definitions #

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

Implementation notes #

See Mathlib/RingTheory/Localization/Basic.lean for a design overview.

Tags #

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

def IsLocalization.invSubmonoid {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] :

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

Equations
Instances For
theorem IsLocalization.submonoid_map_le_is_unit {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :
@[reducible, inline]
noncomputable abbrev IsLocalization.equivInvSubmonoid {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :
(Submonoid.map () M) ≃*

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

Equations
Instances For
noncomputable def IsLocalization.toInvSubmonoid {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :
M →*

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

Equations
• = .toMonoidHom.comp ((()).submonoidMap M)
Instances For
theorem IsLocalization.toInvSubmonoid_surjective {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :
@[simp]
theorem IsLocalization.toInvSubmonoid_mul {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (m : M) :
() * () m = 1
@[simp]
theorem IsLocalization.mul_toInvSubmonoid {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (m : M) :
() m * () = 1
@[simp]
theorem IsLocalization.smul_toInvSubmonoid {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (m : M) :
m () = 1
theorem IsLocalization.surj'' {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (z : S) :
∃ (r : R) (m : M), z = r ()
theorem IsLocalization.toInvSubmonoid_eq_mk' {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (x : M) :
() =
theorem IsLocalization.mem_invSubmonoid_iff_exists_mk' {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] (x : S) :
∃ (m : M), = x
theorem IsLocalization.span_invSubmonoid {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] :
theorem IsLocalization.finiteType_of_monoid_fg {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] [] :