Documentation

Mathlib.RingTheory.Localization.Submodule

Submodules in localizations of commutative rings #

Implementation notes #

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

Tags #

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

def IsLocalization.coeSubmodule {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] (I : Ideal R) :

Map from ideals of R to submodules of S induced by f.

Equations
Instances For
    theorem IsLocalization.mem_coeSubmodule {R : Type u_1} [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] (I : Ideal R) {x : S} :
    x IsLocalization.coeSubmodule S I yI, (algebraMap R S) y = x
    @[simp]
    theorem IsLocalization.mem_span_iff {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] {N : Type u_5} [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] {x : N} {a : Set N} :
    x Submodule.span S a ySubmodule.span R a, ∃ (z : M), x = IsLocalization.mk' S 1 z y
    theorem IsLocalization.mem_span_map {R : Type u_1} [CommRing R] (M : Submonoid R) {S : Type u_2} [CommRing S] [Algebra R S] [IsLocalization M S] {x : S} {a : Set R} :
    x Ideal.span ((algebraMap R S) '' a) yIdeal.span a, ∃ (z : M), x = IsLocalization.mk' S y z