IsFractionRing.coeSubmodule_le_coeSubmodule
theorem IsFractionRing.coeSubmodule_le_coeSubmodule :
∀ {R : Type u_1} [inst : CommRing R] {K : Type u_5} [inst_1 : CommRing K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] {I J : Ideal R},
IsLocalization.coeSubmodule K I ≤ IsLocalization.coeSubmodule K J ↔ I ≤ J
The theorem `IsFractionRing.coeSubmodule_le_coeSubmodule` states that for any commutative ring `R`, and any field of fractions `K` of this ring, and for any two ideals `I` and `J` of the ring `R`, the submodule of `K` induced by `I` is less than or equal to the submodule of `K` induced by `J` if and only if `I` is less than or equal to `J`. Here, less than or equal to for ideals or submodules means that every element of the first ideal or submodule is also an element of the second one. Basically, this theorem is comparing ideals in the ring `R` and their corresponding submodules in the field of fractions `K`.
More concisely: For any commutative ring R, ideal I <= J in R if and only if the submodule of the field of fractions of R induced by I is less than or equal to the submodule induced by J.
|
IsLocalization.coeSubmodule_le_coeSubmodule
theorem IsLocalization.coeSubmodule_le_coeSubmodule :
∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
[inst_3 : IsLocalization M S],
M ≤ nonZeroDivisors R →
∀ {I J : Ideal R}, IsLocalization.coeSubmodule S I ≤ IsLocalization.coeSubmodule S J ↔ I ≤ J
This theorem states that for any commutative ring `R`, any submonoid `M` of `R`, any type `S` which is also a commutative ring and an `R`-algebra, and for any `S` which is a localization of `M`, if `M` is a subset of non-zero divisors of `R`, then for any two ideals `I` and `J` of `R`, the image of `I` under the submodule construction induced by the localization is a submodule of the image of `J` if and only if `I` is a submodule of `J`. Essentially, the ordering of ideals in `R` is preserved under the localization map. The proof is not displayed here.
More concisely: For any commutative rings `R` and `S` with `S` being a localization of a submonoid `M` of `R` consisting of non-zero divisors, the submodule relationship between ideals of `R` is preserved under the submodule construction induced by the localization map.
|