Documentation

Mathlib.RingTheory.Localization.Submodule

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) :

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 ∈ 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) :

coeSubmodule S I ≤ coeSubmodule S J

@[simp]

theorem IsLocalization.coeSubmodule_bot {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] :

coeSubmodule S ⊥ = ⊥

@[simp]

theorem IsLocalization.coeSubmodule_top {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] :

coeSubmodule S ⊤ = 1

@[simp]

theorem IsLocalization.coeSubmodule_sup {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (I J : Ideal R) :

coeSubmodule S (I ⊔ J) = coeSubmodule S I ⊔ 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) :

coeSubmodule S (I * J) = coeSubmodule S I * 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) :

(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) :

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) :

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) :

IsNoetherianRing S

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} :

coeSubmodule S I ≤ 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) :

StrictMono (coeSubmodule S)

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) :

Function.Injective (coeSubmodule S)

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) :

(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 = 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 = 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] :

StrictMono (IsLocalization.coeSubmodule K)

theorem IsFractionRing.coeSubmodule_injective (R : Type u_3) (K : Type u_4) [CommRing R] [CommRing K] [Algebra R K] [IsFractionRing R K] :

Function.Injective (IsLocalization.coeSubmodule 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