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
🔸 coverage
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 }.

Instances For
    source
    📐 coverage
    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
    🔸 coverage
    @[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.

    Instances For
      source
      🔸 coverage
      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.

      Instances For
        source
        📐 coverage
        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
        📐 coverage
        @[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
        📐 coverage
        @[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
        📐 coverage
        @[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
        📐 coverage
        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
        📐 coverage
        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
        📐 coverage
        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
        📐 coverage
        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
        📐 coverage
        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
        source
        📐 coverage
        instance IsLocalization.instFiniteTypeLocalizationOfFGSubtypeMemSubmonoid {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FiniteType R S] (M : Submonoid S) [Monoid.FG ↥M] :
        Algebra.FiniteType R (Localization M)