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} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] : Submonoid S

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

Equations

• IsLocalization.invSubmonoid M S = (Submonoid.map (algebraMap R S) M).leftInv

theorem IsLocalization.submonoid_map_le_is_unit {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] : Submonoid.map (algebraMap R S) M ≤ IsUnit.submonoid S

@[reducible, inline]

noncomputable abbrev IsLocalization.equivInvSubmonoid {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] : { x : S // x ∈ Submonoid.map (algebraMap R S) M } ≃* { x : S // x ∈ IsLocalization.invSubmonoid M S }

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

Equations

• IsLocalization.equivInvSubmonoid M S = ((Submonoid.map (algebraMap R S) M).leftInvEquiv ⋯).symm

noncomputable def IsLocalization.toInvSubmonoid {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] : { x : R // x ∈ M } →* { x : S // x ∈ IsLocalization.invSubmonoid M S }

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

Equations

• IsLocalization.toInvSubmonoid M S = (IsLocalization.equivInvSubmonoid M S).toMonoidHom.comp ((↑(algebraMap R S)).submonoidMap M)

theorem IsLocalization.toInvSubmonoid_surjective {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] : Function.Surjective ⇑(IsLocalization.toInvSubmonoid M S)

@[simp]

theorem IsLocalization.toInvSubmonoid_mul {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] (m : { x : R // x ∈ M }) : ↑((IsLocalization.toInvSubmonoid M S) m) * (algebraMap R S) ↑m = 1

@[simp]

theorem IsLocalization.mul_toInvSubmonoid {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] (m : { x : R // x ∈ M }) : (algebraMap R S) ↑m * ↑((IsLocalization.toInvSubmonoid M S) m) = 1

@[simp]

theorem IsLocalization.smul_toInvSubmonoid {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] (m : { x : R // x ∈ M }) : m • ↑((IsLocalization.toInvSubmonoid M S) m) = 1

theorem IsLocalization.surj'' {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (z : S) : ∃ (r : R) (m : { x : R // x ∈ M }), z = r • ↑((IsLocalization.toInvSubmonoid M S) m)

theorem IsLocalization.toInvSubmonoid_eq_mk' {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (x : { x : R // x ∈ M }) : ↑((IsLocalization.toInvSubmonoid M S) x) = IsLocalization.mk' S 1 x

theorem IsLocalization.mem_invSubmonoid_iff_exists_mk' {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] (x : S) : x ∈ IsLocalization.invSubmonoid M S ↔ ∃ (m : { x : R // x ∈ M }), IsLocalization.mk' S 1 m = x

theorem IsLocalization.span_invSubmonoid {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] : Submodule.span R ↑(IsLocalization.invSubmonoid M S) = ⊤

theorem IsLocalization.finiteType_of_monoid_fg {R : Type u_1} [CommRing R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] [Monoid.FG { x : R // x ∈ M }] : Algebra.FiniteType R S