# 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} [] (S : Type u_2) [] [Algebra R S] (I : ) :

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

Equations
Instances For
theorem IsLocalization.mem_coeSubmodule {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) {x : S} :
yI, () y = x
theorem IsLocalization.coeSubmodule_mono {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] {I : } {J : } (h : I J) :
@[simp]
theorem IsLocalization.coeSubmodule_bot {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] :
@[simp]
theorem IsLocalization.coeSubmodule_top {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] :
@[simp]
theorem IsLocalization.coeSubmodule_sup {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) (J : ) :
@[simp]
theorem IsLocalization.coeSubmodule_mul {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (I : ) (J : ) :
theorem IsLocalization.coeSubmodule_fg {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (hS : Function.Injective ()) (I : ) :
.FG
@[simp]
theorem IsLocalization.coeSubmodule_span {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (s : Set R) :
= Submodule.span R (() '' s)
theorem IsLocalization.coeSubmodule_span_singleton {R : Type u_1} [] (S : Type u_2) [] [Algebra R S] (x : R) :
= Submodule.span R {() x}
theorem IsLocalization.isNoetherianRing {R : Type u_1} [] (M : ) (S : Type u_2) [] [Algebra R S] [] (h : ) :
theorem IsLocalization.coeSubmodule_le_coeSubmodule {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (h : ) {I : } {J : } :
theorem IsLocalization.coeSubmodule_strictMono {R : Type u_1} [] {M : } {S : Type u_2} [] [Algebra R S] [] (h : ) :
theorem IsLocalization.coeSubmodule_injective {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] (h : ) :
theorem IsLocalization.coeSubmodule_isPrincipal {R : Type u_1} [] {M : } (S : Type u_2) [] [Algebra R S] [] {I : } (h : ) :
.IsPrincipal
theorem IsLocalization.mem_span_iff {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] {N : Type u_5} [] [Module R N] [Module S N] [] {x : N} {a : Set N} :
x y, ∃ (z : M), x = y
theorem IsLocalization.mem_span_map {R : Type u_1} [] (M : ) {S : Type u_2} [] [Algebra R S] [] {x : S} {a : Set R} :
x Ideal.span (() '' a) y, ∃ (z : M), x =
@[simp]
theorem IsFractionRing.coeSubmodule_le_coeSubmodule {R : Type u_1} [] {K : Type u_5} [] [Algebra R K] [] {I : } {J : } :
theorem IsFractionRing.coeSubmodule_strictMono {R : Type u_1} [] {K : Type u_5} [] [Algebra R K] [] :
theorem IsFractionRing.coeSubmodule_injective (R : Type u_1) [] (K : Type u_5) [] [Algebra R K] [] :
@[simp]
theorem IsFractionRing.coeSubmodule_isPrincipal (R : Type u_1) [] (K : Type u_5) [] [Algebra R K] [] {I : } :
.IsPrincipal