Documentation

Mathlib.RingTheory.Localization.InvSubmonoid

Submonoid of inverses #

Main definitions #

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] :

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

Instances For
    @[inline, reducible]
    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] :

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

    Instances For
      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 // x M } →* { x // x IsLocalization.invSubmonoid M S }

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

      Instances For
        @[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 // 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 // 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 // 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 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 // x M }) :
        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 // x M }] :