FractionalIdeal.coeIdeal_injective'
theorem FractionalIdeal.coeIdeal_injective' :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
[loc : IsLocalization S P], S ≤ nonZeroDivisors R → Function.Injective fun I => ↑I
The theorem `FractionalIdeal.coeIdeal_injective'` states that for any commutative ring `R`, submonoid `S` of `R`, type `P` which also has a commutative ring structure, and that `P` is an algebra over `R` and a localization of `R` at `S`, if `S` is a subset of the non-zero divisors of `R`, then the function that maps an ideal `I` to its type-cast version is injective. In simpler words, no two distinct ideals will map to the same output under this function, provided `S` contains no zero divisors of `R`.
More concisely: Given a commutative ring `R`, a submonoid `S` of non-zero divisors in `R`, a commutative ring `P` that is an algebra and localization of `R` over `S`, the type-cast function from ideals of `R` to ideals of `P` is injective.
|
FractionalIdeal.mem_coe
theorem FractionalIdeal.mem_coe :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
{I : FractionalIdeal S P} {x : P}, x ∈ ↑I ↔ x ∈ I
This theorem states that for any commutative ring `R`, a submonoid `S` of `R`, a commutative ring `P` that is an `R`-algebra, a fractional ideal `I` of `P` over `S`, and an element `x` of `P`, `x` is an element of the coercive version of `I` (i.e., `I` viewed as a subset of `P`) if and only if `x` is an element of `I`. Essentially, this theorem confirms that the membership of an element `x` in the fractional ideal `I` is preserved when `I` is coerced to a subset of `P`.
More concisely: For any commutative ring `R`, submonoid `S` of `R`, commutative `R`-algebra `P`, fractional ideal `I` of `P` over `S`, and element `x` in `P`, `x` belongs to `I` if and only if `x` belongs to the coercion of `I` to a subset of `P`.
|
FractionalIdeal.coe_one_eq_coeSubmodule_top
theorem FractionalIdeal.coe_one_eq_coeSubmodule_top :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
↑1 = IsLocalization.coeSubmodule P ⊤
This theorem, `FractionalIdeal.coe_one_eq_coeSubmodule_top`, states that for any type `R` with a commutative ring structure, any submonoid `S` of `R`, and any type `P` with a commutative ring structure and an algebra structure over `R`, the fraction 1 as an element of the fractional ideals in `P` is defined as the `R`-submodule generated by `f(R)` that is less than or equal to `P`. However, this is not the same as `1` in the submodule of `R` in `P`, which is a result proven in the lemma `coe_one`. Instead, the fraction `1` of the fractional ideals in `P` is equal to the top element `⊤` when viewed as the image under the localizing map from ideals of `R` to submodules of `P`.
More concisely: The theorem asserts that the image of the multiplicative identity under the localizing map from ideals of a commutative ring `R` to submodules of a commutative ring `P` with an algebra structure over `R`, is equal to the submodule of `P` generated by the image of `R` under the given algebra structure.
|
FractionalIdeal.coe_one
theorem FractionalIdeal.coe_one :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
↑1 = 1
This theorem states that for any commutative ring `R`, submonoid `S` of `R`, another type `P` which is also a commutative ring, and an algebra structure over `R` and `P`, the coercion of the multiplicative identity `1` (seen as a fractional ideal) is equal to the multiplicative identity in the ring. In other words, when we view `1` as a fractional ideal and then convert it back into the ring, it remains as the identity element.
More concisely: For any commutative rings R and P, a submonoid S of R, and an algebra structure over R and P, the coercion of the multiplicative identity 1 as a fractional ideal in R equals the multiplicative identity in R.
|
FractionalIdeal.ext
theorem FractionalIdeal.ext :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
{I J : FractionalIdeal S P}, (∀ (x : P), x ∈ I ↔ x ∈ J) → I = J
The theorem `FractionalIdeal.ext` states that for any commutative ring `R`, a submonoid `S` of `R`, a type `P` with a commutative ring structure and an `R`-algebra structure, and any two fractional ideals `I` and `J` of `S` in `P`, if every element `x` in `P` belongs to `I` if and only if it belongs to `J`, then `I` and `J` are equal. In other words, two fractional ideals are equal if they contain exactly the same elements.
More concisely: Two fractional ideals of a commutative ring `R` in a commutative `R`-algebra `P` are equal if and only if they contain the same elements.
|
FractionalIdeal.coe_zero
theorem FractionalIdeal.coe_zero :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
↑0 = ⊥
This theorem states that for any commutative ring `R` and any submonoid `S` of `R`, and for any commutative ring `P` with an algebra structure over `R`, the Fractional Ideal of `0` in `R` is equivalent to the bottom element (`⊥`) in the lattice structure of Fractional Ideals. In simpler terms, the ideal generated by `0` is the smallest possible ideal in the lattice of fractional ideals under these conditions.
More concisely: For any commutative ring R, submonoid S of R, and commutative R-algebra P, the ideal (0) in R equals the bottom element in the lattice of fractional ideals of R over P.
|
FractionalIdeal.mem_one_iff
theorem FractionalIdeal.mem_one_iff :
∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
{x : P}, x ∈ 1 ↔ ∃ x', (algebraMap R P) x' = x
The theorem `FractionalIdeal.mem_one_iff` states that for any given commutative rings `R` and `P` with an algebra structure, and for any submonoid `S` of `R` and any element `x` of `P`, `x` is an element of the unit ideal in the ring `P` if and only if there exists an element `x'` in `R` such that `x'` mapped into `P` using the algebra structure is equal to `x`. Here, `FractionalIdeal` is a concept in commutative algebra used to generalize the idea of an ideal in a ring, and `algebraMap` is a function embedding `R` into `A` given by the algebra structure.
More concisely: For a commutative ring `R` with algebra structure over a commutative ring `P`, an element `x` of `P` belongs to the unit ideal of `P` if and only if there exists an element `x'` in `R` such that `x'` maps to `x` under the algebra map from `R` to `P`.
|
FractionalIdeal.coeIdeal_le_one
theorem FractionalIdeal.coeIdeal_le_one :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
{I : Ideal R}, ↑I ≤ 1
This theorem states that for any commutative ring `R`, any submonoid `S` of `R`, any commutative ring `P`, any algebra `R P`, and any ideal `I` of `R`, the fractional ideal generated by `I` in the ring of fractions `P` is less than or equal to one. This essentially means that any element of `I` when seen as a fraction in `P` always has a value that's less than or equal to one.
More concisely: For any commutative ring `R`, submonoid `S` of `R`, commutative ring `P`, algebra `RP`, and ideal `I` of `R`, the fractional ideal of `I` in `RP` is contained in the multiplicative monoid of `RP` consisting of elements less than or equal to one.
|
FractionalIdeal.mem_zero_iff
theorem FractionalIdeal.mem_zero_iff :
∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
{x : P}, x ∈ 0 ↔ x = 0
This theorem states that for any commutative ring `R`, given a submonoid `S` of `R`, and a commutative ring `P` with an algebra structure over `R`, an element `x` of `P` belongs to the zero fractional ideal if and only if `x` is equal to zero. In more mathematical terms, it asserts that a member of the zero fractional ideal in a commutative ring is zero.
More concisely: In a commutative ring, an element belongs to the zero fractional ideal if and only if it is zero.
|
FractionalIdeal.coeToSubmodule_injective
theorem FractionalIdeal.coeToSubmodule_injective :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
Function.Injective fun I => ↑I
The theorem `FractionalIdeal.coeToSubmodule_injective` states that for any commutative ring `R`, any submonoid `S` of `R`, and any type `P` that is also a commutative ring and an algebra over `R`, the function that maps a fractional ideal `I` to its underlying submodule (denoted by `↑I`) is injective. In other words, if two fractional ideals of `R` give rise to the same submodule when considered as submodules of `P`, then the two fractional ideals were originally the same.
More concisely: The map from fractional ideals of a commutative ring `R` to their underlying submodules in a commutative ring `P` is an injection.
|
FractionalIdeal.mul_le
theorem FractionalIdeal.mul_le :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
{I J K : FractionalIdeal S P}, I * J ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K
The theorem `FractionalIdeal.mul_le` states that for any commutative ring `R` with a submonoid `S`, and any type `P` that is also a commutative ring and an `R`-algebra, for any fractional ideals `I`, `J`, and `K` of `S` in `P`, the product of `I` and `J` is less than or equal to `K` if and only if for every element `i` in `I` and every element `j` in `J`, the product of `i` and `j` is an element of `K`. In other words, the product of two fractional ideals is contained within another fractional ideal if and only if every product of an element from each of the two fractional ideals is contained within the third fractional ideal.
More concisely: For commutative rings R with submonoid S, and R-algebras P containing S, two fractional ideals I and J of S in P have the property that I * J ≤ K if and only if i * j ∈ K for all i ∈ I and j ∈ J.
|
FractionalIdeal.coe_mul
theorem FractionalIdeal.coe_mul :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
(I J : FractionalIdeal S P), ↑(I * J) = ↑I * ↑J
This theorem states that for any commutative ring `R`, a submonoid `S` of `R`, and a type `P` that is also a commutative ring and an `R`-algebra, if `I` and `J` are fractional ideals of `S` in `P`, then the product of `I` and `J` as fractional ideals is equal to the product of `I` and `J` in the underlying structure of `P`. In other words, the operation of multiplication on fractional ideals is consistent with the multiplication on the underlying structure.
More concisely: For any commutative rings `R`, `P` with `R` a subring of `P`, a commutative submonoid `S` of `R`, and fractional ideals `I` and `J` of `S` in `P`, the product of `I` and `J` as fractional ideals equals their product as ideals in `P`.
|
FractionalIdeal.mul_mem_mul
theorem FractionalIdeal.mul_mem_mul :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
{I J : FractionalIdeal S P} {i j : P}, i ∈ I → j ∈ J → i * j ∈ I * J
The theorem `FractionalIdeal.mul_mem_mul` states that for any commutative ring `R`, submonoid `S` of `R`, commutative ring `P`, algebra structure of `P` over `R`, and fractional ideals `I` and `J` of `P` over `R` with respect to `S`, if an element `i` is in `I` and another element `j` is in `J`, then the product `i * j` is in the product of the fractional ideals `I * J`. In mathematical terms, this means if $i \in I$ and $j \in J$, then $i*j \in I*J$ where $I$ and $J$ are fractional ideals of some ring.
More concisely: If `I` and `J` are fractional ideals of a commutative ring `P` with respect to a submonoid `S` of `P`, then for all `i` in `I` and `j` in `J`, the product `i * j` is in the product `I * J`.
|
FractionalIdeal.mul_left_mono
theorem FractionalIdeal.mul_left_mono :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
(I : FractionalIdeal S P), Monotone fun x => I * x
This theorem, `FractionalIdeal.mul_left_mono`, states that for any commutative ring `R`, submonoid `S` of `R`, commutative ring `P`, and algebra structure on `R` and `P`, and for any fractional ideal `I` of `S` in `P`, the function that multiplies `I` to the left is monotone. In other words, if we have two elements `x` and `y` in the ring such that `x ≤ y`, then `I * x ≤ I * y`, where the multiplication and comparison are done in the ring.
More concisely: For any commutative rings R and P, submonoid S of R, algebra structure on R and P, and fractional ideal I of S in P, the multiplication of I by any element x in R (left multiplication) is monotone, that is, I * x ≤ I * y whenever x ≤ y in R.
|
FractionalIdeal.mul_def
theorem FractionalIdeal.mul_def :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
(I J : FractionalIdeal S P), I * J = ⟨↑I * ↑J, ⋯⟩
The theorem `FractionalIdeal.mul_def` states that for any commutative ring `R`, any submonoid `S` of `R`, any type `P` that is also a commutative ring and an `R`-algebra, and any two fractional ideals `I` and `J` of the localization of `R` at `S`, the multiplication of `I` and `J` is defined to be the fractional ideal whose value is the product of the values of `I` and `J`, and whose proof of being a fractional ideal is suppressed for brevity. In other words, this theorem provides the definition of multiplication for fractional ideals.
More concisely: Given commutative rings R and S, an R-algebra P, and fractional ideals I and J of the localization of R at S, their product I \* J is the fractional ideal whose value is the product of I and J as ideals in the localization.
|
FractionalIdeal.isFractional
theorem FractionalIdeal.isFractional :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
(I : FractionalIdeal S P), IsFractional S ↑I
This theorem states that for any commutative ring `R`, any submonoid `S` of `R`, any type `P` with a commutative ring structure such that `P` is an `R`-algebra, and any fractional ideal `I` of `P` with respect to `S`, `I` satisfies the property of being a fractional ideal. In other words, there exists a non-zero element `a` in `S` such that the product of `a` and any element of `I` is an integer in the localization of `R` at `S`.
More concisely: Given a commutative ring `R`, a submonoid `S` of `R`, an `R`-algebra `P`, and a fractional ideal `I` of `P` with respect to `S`, there exists an element `a` in `S` such that `aI` is an ideal in the localization `R_S`.
|
FractionalIdeal.coe_le_coe
theorem FractionalIdeal.coe_le_coe :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
{I J : FractionalIdeal S P}, ↑I ≤ ↑J ↔ I ≤ J
The theorem `FractionalIdeal.coe_le_coe` states that for any commutative ring `R`, any submonoid `S` of `R`, any type `P` equipped with a commutative ring structure and an `R`-algebra structure, and any two fractional ideals `I` and `J` of `S` on `P`, the relation that `I` is a subset of or equal to `J` in the set of fractional ideals is equivalent to the relation that `I` is a subset of or equal to `J` as subsets in the algebra `P`. In other words, the inclusion relationship between `I` and `J` remains the same whether we view them as fractional ideals or as subsets of the algebra `P`.
More concisely: For any commutative ring `R`, submonoid `S` of `R`, type `P` with commutative ring and `R`-algebra structures, and fractional ideals `I` and `J` of `S` on `P`, `I ⊆ J` as fractional ideals if and only if `I ⊆ J` as subsets of `P`.
|