mathlib documentation

ring_theory.localization.submodule

Submodules in localizations of commutative rings #

Implementation notes #

See src/ring_theory/localization/basic.lean for a design overview.

Tags #

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

def is_localization.coe_submodule {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (I : ideal R) :

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

Equations
theorem is_localization.mem_coe_submodule {R : Type u_1} [comm_ring R] (S : Type u_2) [comm_ring S] [algebra R S] (I : ideal R) {x : S} :
theorem is_localization.mem_span_iff {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {N : Type u_3} [add_comm_group N] [module R N] [module S N] [is_scalar_tower R S N] {x : N} {a : set N} :
x submodule.span S a (y : N) (H : y submodule.span R a) (z : M), x = is_localization.mk' S 1 z y
theorem is_localization.mem_span_map {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] {x : S} {a : set R} :
x ideal.span ((algebra_map R S) '' a) (y : R) (H : y ideal.span a) (z : M), x = is_localization.mk' S y z