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

source
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
Instances For
    source
    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
    source
    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
    source
    @[simp]
    theorem IsLocalization.coeSubmodule_bot {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] :
    coeSubmodule S ⊥ = ⊥
    source
    @[simp]
    theorem IsLocalization.coeSubmodule_top {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] :
    coeSubmodule S ⊤ = 1
    source
    @[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
    source
    @[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
    source
    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
    source
    @[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)
    source
    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}) = R ∙ (algebraMap R S) x
    source
    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
    source
    instance IsLocalization.instIsNoetherianRingLocalization {R : Type u_3} [CommRing R] [IsNoetherianRing R] (S : Submonoid R) :
    IsNoetherianRing (Localization S)
    source
    theorem Algebra.EssFiniteType.isNoetherianRing (R : Type u_3) (S : Type u_4) [CommRing R] [CommRing S] [Algebra R S] [EssFiniteType R S] [IsNoetherianRing R] :
    IsNoetherianRing S
    source
    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
    source
    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)
    source
    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)
    source
    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
    source
    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
    source
    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
    source
    @[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
    source
    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)
    source
    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)
    source
    @[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