Submodules in localizations of commutative rings #
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
def
IsLocalization.coeSubmodule
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
:
Submodule R S
Map from ideals of R to submodules of S induced by f.
Equations
- IsLocalization.coeSubmodule S I = Submodule.map (Algebra.linearMap R S) I
Instances For
theorem
IsLocalization.mem_coeSubmodule
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I : Ideal R)
{x : S}
:
x ∈ IsLocalization.coeSubmodule S I ↔ ∃ y ∈ I, (algebraMap R S) y = x
theorem
IsLocalization.coeSubmodule_mono
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
{I J : Ideal R}
(h : I ≤ J)
:
@[simp]
theorem
IsLocalization.coeSubmodule_bot
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
:
@[simp]
theorem
IsLocalization.coeSubmodule_top
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
:
@[simp]
theorem
IsLocalization.coeSubmodule_sup
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I J : Ideal R)
:
IsLocalization.coeSubmodule S (I ⊔ J) = IsLocalization.coeSubmodule S I ⊔ IsLocalization.coeSubmodule S J
@[simp]
theorem
IsLocalization.coeSubmodule_mul
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(I J : Ideal R)
:
IsLocalization.coeSubmodule S (I * J) = IsLocalization.coeSubmodule S I * IsLocalization.coeSubmodule S J
theorem
IsLocalization.coeSubmodule_fg
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(hS : Function.Injective ⇑(algebraMap R S))
(I : Ideal R)
:
(IsLocalization.coeSubmodule S I).FG ↔ Submodule.FG I
@[simp]
theorem
IsLocalization.coeSubmodule_span
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(s : Set R)
:
IsLocalization.coeSubmodule S (Ideal.span s) = Submodule.span R (⇑(algebraMap R S) '' s)
theorem
IsLocalization.coeSubmodule_span_singleton
{R : Type u_1}
[CommSemiring R]
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
(x : R)
:
IsLocalization.coeSubmodule S (Ideal.span {x}) = Submodule.span R {(algebraMap R S) x}
theorem
IsLocalization.isNoetherianRing
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
(h : IsNoetherianRing R)
:
theorem
IsLocalization.coeSubmodule_le_coeSubmodule
{R : Type u_3}
[CommRing R]
{M : Submonoid R}
{S : Type u_4}
[CommRing S]
[Algebra R S]
[IsLocalization M S]
(h : M ≤ nonZeroDivisors R)
{I J : Ideal R}
:
IsLocalization.coeSubmodule S I ≤ IsLocalization.coeSubmodule S J ↔ I ≤ J
theorem
IsLocalization.coeSubmodule_strictMono
{R : Type u_3}
[CommRing R]
{M : Submonoid R}
{S : Type u_4}
[CommRing S]
[Algebra R S]
[IsLocalization M S]
(h : M ≤ nonZeroDivisors R)
:
theorem
IsLocalization.coeSubmodule_injective
{R : Type u_3}
[CommRing R]
{M : Submonoid R}
(S : Type u_4)
[CommRing S]
[Algebra R S]
[IsLocalization M S]
(h : M ≤ nonZeroDivisors R)
:
theorem
IsLocalization.coeSubmodule_isPrincipal
{R : Type u_3}
[CommRing R]
{M : Submonoid R}
(S : Type u_4)
[CommRing S]
[Algebra R S]
[IsLocalization M S]
{I : Ideal R}
(h : M ≤ nonZeroDivisors R)
:
(IsLocalization.coeSubmodule S I).IsPrincipal ↔ Submodule.IsPrincipal I
theorem
IsLocalization.mem_span_iff
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
{S : Type u_2}
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
{N : Type u_3}
[AddCommMonoid N]
[Module R N]
[Module S N]
[IsScalarTower R S N]
{x : N}
{a : Set N}
:
x ∈ Submodule.span S a ↔ ∃ y ∈ Submodule.span R a, ∃ (z : ↥M), x = IsLocalization.mk' S 1 z • y
theorem
IsLocalization.mem_span_map
{R : Type u_1}
[CommSemiring R]
(M : Submonoid R)
{S : Type u_2}
[CommSemiring S]
[Algebra R S]
[IsLocalization M S]
{x : S}
{a : Set R}
:
x ∈ Ideal.span (⇑(algebraMap R S) '' a) ↔ ∃ y ∈ Ideal.span a, ∃ (z : ↥M), x = IsLocalization.mk' S y z
@[simp]
theorem
IsFractionRing.coeSubmodule_le_coeSubmodule
{R : Type u_3}
{K : Type u_4}
[CommRing R]
[CommRing K]
[Algebra R K]
[IsFractionRing R K]
{I J : Ideal R}
:
IsLocalization.coeSubmodule K I ≤ IsLocalization.coeSubmodule K J ↔ I ≤ J
theorem
IsFractionRing.coeSubmodule_strictMono
{R : Type u_3}
{K : Type u_4}
[CommRing R]
[CommRing K]
[Algebra R K]
[IsFractionRing R K]
:
theorem
IsFractionRing.coeSubmodule_injective
(R : Type u_3)
(K : Type u_4)
[CommRing R]
[CommRing K]
[Algebra R K]
[IsFractionRing R K]
:
@[simp]
theorem
IsFractionRing.coeSubmodule_isPrincipal
(R : Type u_3)
(K : Type u_4)
[CommRing R]
[CommRing K]
[Algebra R K]
[IsFractionRing R K]
{I : Ideal R}
:
(IsLocalization.coeSubmodule K I).IsPrincipal ↔ Submodule.IsPrincipal I