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
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} :
x ∈ is_localization.coe_submodule S I ↔ ∃ (y : R), y ∈ I ∧ ⇑(algebra_map R S) y = x
@[simp]
theorem
is_localization.coe_submodule_bot
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S] :
@[simp]
theorem
is_localization.coe_submodule_top
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S] :
@[simp]
theorem
is_localization.coe_submodule_sup
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S]
(I J : ideal R) :
@[simp]
theorem
is_localization.coe_submodule_mul
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S]
(I J : ideal R) :
is_localization.coe_submodule S (I * J) = (is_localization.coe_submodule S I) * is_localization.coe_submodule S J
theorem
is_localization.coe_submodule_fg
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S]
(hS : function.injective ⇑(algebra_map R S))
(I : ideal R) :
(is_localization.coe_submodule S I).fg ↔ submodule.fg I
@[simp]
theorem
is_localization.coe_submodule_span
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S]
(s : set R) :
is_localization.coe_submodule S (ideal.span s) = submodule.span R (⇑(algebra_map R S) '' s)
@[simp]
theorem
is_localization.coe_submodule_span_singleton
{R : Type u_1}
[comm_ring R]
(S : Type u_2)
[comm_ring S]
[algebra R S]
(x : R) :
is_localization.coe_submodule S (ideal.span {x}) = submodule.span R {⇑(algebra_map R S) x}
theorem
is_localization.is_noetherian_ring
{R : Type u_1}
[comm_ring R]
(M : submonoid R)
(S : Type u_2)
[comm_ring S]
[algebra R S]
[is_localization M S]
(h : is_noetherian_ring R) :
theorem
is_localization.coe_submodule_le_coe_submodule
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
(h : M ≤ R⁰)
{I J : ideal R} :
is_localization.coe_submodule S I ≤ is_localization.coe_submodule S J ↔ I ≤ J
theorem
is_localization.coe_submodule_strict_mono
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
{S : Type u_2}
[comm_ring S]
[algebra R S]
[is_localization M S]
(h : M ≤ R⁰) :
theorem
is_localization.coe_submodule_injective
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
(S : Type u_2)
[comm_ring S]
[algebra R S]
[is_localization M S]
(h : M ≤ R⁰) :
theorem
is_localization.coe_submodule_is_principal
{R : Type u_1}
[comm_ring R]
{M : submonoid R}
(S : Type u_2)
[comm_ring S]
[algebra R S]
[is_localization M S]
{I : ideal R}
(h : M ≤ R⁰) :
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
@[simp]
theorem
is_fraction_ring.coe_submodule_le_coe_submodule
{R : Type u_1}
[comm_ring R]
{K : Type u_5}
[comm_ring K]
[algebra R K]
[is_fraction_ring R K]
{I J : ideal R} :
is_localization.coe_submodule K I ≤ is_localization.coe_submodule K J ↔ I ≤ J
theorem
is_fraction_ring.coe_submodule_strict_mono
{R : Type u_1}
[comm_ring R]
{K : Type u_5}
[comm_ring K]
[algebra R K]
[is_fraction_ring R K] :
theorem
is_fraction_ring.coe_submodule_injective
(R : Type u_1)
[comm_ring R]
(K : Type u_5)
[comm_ring K]
[algebra R K]
[is_fraction_ring R K] :
@[simp]
theorem
is_fraction_ring.coe_submodule_is_principal
(R : Type u_1)
[comm_ring R]
(K : Type u_5)
[comm_ring K]
[algebra R K]
[is_fraction_ring R K]
{I : ideal R} :