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

source
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
    Instances For
      source
      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
      source
      @[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] :
      ↥(Submonoid.map (algebraMap R S) M) ≃* ↥(invSubmonoid M S)

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

      Equations
        Instances For
          source
          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] :
          ↥M →* ↥(invSubmonoid M S)

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

          Equations
            Instances For
              source
              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 ⇑(toInvSubmonoid M S)
              source
              @[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 : ↥M) :
              ↑((toInvSubmonoid M S) m) * (algebraMap R S) ↑m = 1
              source
              @[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 : ↥M) :
              (algebraMap R S) ↑m * ↑((toInvSubmonoid M S) m) = 1
              source
              @[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 : ↥M) :
              m • ↑((toInvSubmonoid M S) m) = 1
              source
              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 : ↥M), z = r • ↑((toInvSubmonoid M S) m)
              source
              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 : ↥M) :
              ↑((toInvSubmonoid M S) x) = mk' S 1 x
              source
              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 ∈ invSubmonoid M S ↔ ∃ (m : ↥M), mk' S 1 m = x
              source
              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 ↑(invSubmonoid M S) = ⊤
              source
              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 ↥M] :
              Algebra.FiniteType R S