FractionalIdeal.coe_spanSingleton
theorem FractionalIdeal.coe_spanSingleton :
∀ {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] (x : P), ↑(FractionalIdeal.spanSingleton S x) = Submodule.span R {x}
This theorem states that for any commutative ring `R`, any submonoid `S` of `R`, any commutative ring `P`, any `R`-algebra structure on `P`, and a localization `S` at `P`, for any element `x` in `P`, the ring-coercion of the fractional ideal generated by `x` (if `0` is not in `S`) is equal to the smallest submodule of `P` that contains the set `{x}`. In other words, the fractional ideal generated by a single element `x` in a localized ring corresponds to the span of the singleton set `{x}` in the module over the commutative ring `R`.
More concisely: For any commutative ring `R`, submonoid `S` of `R`, commutative `R`-algebra `P`, and localization `S^(-1)P` of `P` at `S`, the fractional ideal generated by an element `x` in `P` equals the submodule of `P` generated by `{x}` over `R`.
|
FractionalIdeal.coeIdeal_ne_zero
theorem FractionalIdeal.coeIdeal_ne_zero :
∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] {I : Ideal R}, ↑I ≠ 0 ↔ I ≠ ⊥
The theorem `FractionalIdeal.coeIdeal_ne_zero` states the following: For any commutative ring `R`, any field `K` that is the field of fractions of `R` (i.e., `K` is the field extension of `R` where elements of `R` can be viewed as fractions), and any left ideal `I` in `R`, the coercion of `I` to a fractional ideal in `K` is not zero if and only if `I` is not the zero ideal in `R`. In other words, a non-zero ideal in the ring `R` remains non-zero when considered as a fractional ideal in its field of fractions `K`.
More concisely: For any commutative ring R, field K extending it, and non-zero left ideal I in R, the coercion of I to a fractional ideal in K is a non-zero fractional ideal.
|
FractionalIdeal.isFractional_adjoin_integral
theorem FractionalIdeal.isFractional_adjoin_integral :
∀ {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] (x : P),
IsIntegral R x → IsFractional S (Subalgebra.toSubmodule (Algebra.adjoin R {x}))
The theorem `FractionalIdeal.isFractional_adjoin_integral` states that for any commutative ring `R`, any submonoid `S` of `R`, commutative ring `P`, and an algebra `P` over `R` that is a localization at `S`, if an element `x` of `P` is integral over `R`, then the subalgebra generated by `R` and `{x}` (`A[x]`), when viewed as a submodule, is a fractional ideal. In other words, given an integral element `x` in an algebra over a commutative ring, the ring adjoined with `x` forms a fractional ideal.
More concisely: If `x` is an integral element in an algebra `P` over a commutative ring `R`, then the submodule generated by `R` and `{x}` in `P` is a fractional ideal.
|
FractionalIdeal.map_comp
theorem FractionalIdeal.map_comp :
∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
{P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] {P'' : Type u_4} [inst_5 : CommRing P'']
[inst_6 : Algebra R P''] (I : FractionalIdeal S P) (g : P →ₐ[R] P') (g' : P' →ₐ[R] P''),
FractionalIdeal.map (g'.comp g) I = FractionalIdeal.map g' (FractionalIdeal.map g I)
The theorem `FractionalIdeal.map_comp` states that for any commutative ring `R`, any submonoid `S` of `R`, any fractional ideal `I` of a localization `P` of `R` at `S`, and any two algebra homomorphisms `g: P → P'` and `g': P' → P''`, the map of `I` through the composition of `g'` and `g` is equal to the map of the map of `I` through `g` through `g'`. In simpler terms, this theorem states that pushing forward a fractional ideal through a composition of algebra morphisms is the same as pushing forward separately through each morphism, which is an application of the principle of function composition.
More concisely: For any commutative ring $R$, submonoid $S$ of $R$, fractional ideal $I$ of a localization $P$ of $R$ at $S$, and algebra homomorphisms $g: P \to P'$ and $g': P' \to P''$, the map of $I$ through the composition $g' \circ g$ is equal to the map of $I$ through $g$ composed with $g'$.
|
FractionalIdeal.mem_div_iff_of_nonzero
theorem FractionalIdeal.mem_div_iff_of_nonzero :
∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
[frac : IsFractionRing R₁ K] [inst_3 : IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K},
J ≠ 0 → ∀ {x : K}, x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I
The theorem `FractionalIdeal.mem_div_iff_of_nonzero` states that for any two fractional ideals `I` and `J` of a field `K` that is a fraction field of an integral domain `R₁` (with non-zero divisors), given that `J` is not the zero ideal, a field element `x` is in the quotient `I / J` if and only if for any element `y` in `J`, the product `x * y` is in `I`. This gives us a characterization of elements belonging to the quotient of two fractional ideals in terms of multiplication with elements of the denominator ideal.
More concisely: For fractional ideals I and J of a field K as the fraction field of an integral domain R₁ with non-zero divisors, where J is non-zero, x ∈ I / J if and only if x * y ∈ I for all y ∈ J.
|
FractionalIdeal.spanSingleton_one
theorem FractionalIdeal.spanSingleton_one :
∀ {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], FractionalIdeal.spanSingleton S 1 = 1
This theorem states that for any commutative ring `R`, submonoid `S` of `R`, and another commutative ring `P` with `R` acting as an algebra on `P` such that `P` is a localization of `R` at `S`, the fractional ideal generated by the element `1` in `P` is the unit element in the ring of fractional ideals of `P`. In other words, if you generate a fractional ideal in `P` using just the element `1`, you would end up with the unit element in the ring of fractional ideals.
More concisely: For any commutative ring `R`, submonoid `S` of `R`, and `R`-algebra `P` localized at `S`, the fractional ideal generated by `1` in `P` is the multiplicative identity in the ring of fractional ideals of `P`.
|
FractionalIdeal.spanSingleton_def
theorem FractionalIdeal.spanSingleton_def :
∀ {R : Type u_5} [inst : CommRing R] (S : Submonoid R) {P : Type u_6} [inst_1 : CommRing P] [inst_2 : Algebra R P]
[loc : IsLocalization S P] (x : P), FractionalIdeal.spanSingleton S x = ⟨Submodule.span R {x}, ⋯⟩
The theorem `FractionalIdeal.spanSingleton_def` states that for any commutative ring `R`, a submonoid `S` of `R`, a commutative ring `P`, an algebra structure on `R` and `P`, and a localization `loc` of `S` in `P`, and for any element `x` of `P`, the fractional ideal generated by `x` (denoted as `FractionalIdeal.spanSingleton S x`) is equal to the set containing the submodule of `R` spanned by `{x}`. This defines the action of `spanSingleton` on a single element of the ring `P`. The property part of the fractional ideal is omitted for brevity.
More concisely: For any commutative ring `R`, submonoid `S` of `R`, commutative ring `P`, algebra structure on `R` and `P`, localization `loc` of `S` in `P`, and element `x` of `P`, the fractional ideal generated by `x` equals the submodule of `R` spanned by `{x}`.
|
FractionalIdeal.map_id
theorem FractionalIdeal.map_id :
∀ {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), FractionalIdeal.map (AlgHom.id R P) I = I
This theorem states that for any commutative ring `R`, submonoid `S` of `R`, and any type `P` that forms a commutative ring and is an `R`-algebra, if `I` is a fractional ideal of `P` with respect to `S`, then mapping `I` via the identity algebra homomorphism leaves the fractional ideal unchanged. In mathematical terms, the mapping of a fractional ideal under the identity operation is the ideal itself.
More concisely: For any commutative ring `R`, submonoid `S` of `R`, and `R`-algebra `P`, if `I` is a fractional ideal of `P` with respect to `S`, then applying the identity algebra homomorphism to `I` results in `I` itself.
|
FractionalIdeal.spanSingleton_mul_spanSingleton
theorem FractionalIdeal.spanSingleton_mul_spanSingleton :
∀ {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] (x y : P),
FractionalIdeal.spanSingleton S x * FractionalIdeal.spanSingleton S y = FractionalIdeal.spanSingleton S (x * y)
The theorem `FractionalIdeal.spanSingleton_mul_spanSingleton` states that for any commutative ring `R`, submonoid `S` of `R`, algebra `P` over `R`, and localization of `S` to `P`; the fractional ideal generated by element `x` in `P` multiplied by the fractional ideal generated by element `y` in `P` is equal to the fractional ideal generated by `x * y`. This theorem describes a property of the operation of multiplication in the context of fractional ideals, highlighting the distributive property of multiplication over the generation of fractional ideals.
More concisely: For any commutative ring R, submonoid S of R, algebra P over R, and localization of S to P: the fractional ideal generated by x in P times the fractional ideal generated by y in P equals the fractional ideal generated by x * y in P.
|
FractionalIdeal.div_zero
theorem FractionalIdeal.div_zero :
∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
[frac : IsFractionRing R₁ K] [inst_3 : IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K}, I / 0 = 0
The theorem `FractionalIdeal.div_zero` states that for any commutative ring `R₁`, any field `K` that is the field of fractions of `R₁`, and any fractional ideal `I` of the domain `R₁` over the submonoid of non-zero divisors of `R₁` in `K`, the result of dividing `I` by zero is zero. In other words, it signifies that any fractional ideal divided by zero equals zero in the context of algebraic structures such as rings and fields.
More concisely: For any commutative ring R₁, field K as its fraction field, and fractional ideal I of R₁ over its non-zero divisors, I ∕ 0 = 0.
|
FractionalIdeal.isFractional_span_singleton
theorem FractionalIdeal.isFractional_span_singleton :
∀ {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] (x : P), IsFractional S (Submodule.span R {x})
The theorem `FractionalIdeal.isFractional_span_singleton` states that for any commutative ring `R`, a submonoid `S` of `R`, another commutative ring `P` such that there is an algebra structure over `R` on `P`, and given that `P` is a localization of `R` at `S`, and for any element `x` in `P`, the span of the singleton set `{x}` in `P` is a fractional ideal of `R` in `P`. In other words, there exists a non-zero element `a` in `R` such that multiplying `a` with any element in the span of `{x}` results in an integer in the ring `R`.
More concisely: For any commutative ring R, submonoid S of R, commutative local ring P algebraically extended from R at S, and element x in P, the singleton set {x} spans a fractional ideal in R within P.
|
FractionalIdeal.ne_zero_of_mul_eq_one
theorem FractionalIdeal.ne_zero_of_mul_eq_one :
∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
(I J : FractionalIdeal (nonZeroDivisors R₁) K), I * J = 1 → I ≠ 0
The theorem `FractionalIdeal.ne_zero_of_mul_eq_one` states that for any commutative ring `R₁` and any field `K` with `K` being a `R₁`-algebra, if `I` and `J` are fractional ideals of `R₁` in `K` with respect to the submonoid of non-zero divisors of `R₁`, and the product of `I` and `J` equals the multiplicative identity `1`, then `I` cannot be the zero ideal. This essentially means that if the multiplication of two fractional ideals results in the multiplicative identity, neither of the fractional ideals can be zero, ensuring the invertibility of non-zero fractional ideals in the ring of fractional ideals.
More concisely: If `I` and `J` are fractional ideals of a commutative ring `R₁` in a field `K` with respect to the submonoid of non-zero divisors, and `I ∘ J = 1`, then `I` is not the zero ideal.
|
FractionalIdeal.exists_ne_zero_mem_isInteger
theorem FractionalIdeal.exists_ne_zero_mem_isInteger :
∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra R K]
[inst_3 : IsFractionRing R K] {I : FractionalIdeal (nonZeroDivisors R) K} [inst_4 : Nontrivial R],
I ≠ 0 → ∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I
This theorem, titled "Nonzero fractional ideals contain a nonzero integer", states that for any commutative ring `R` and any field `K`, where `K` is the field of fractions of `R`, and for any non-zero fractional ideal `I` of the non-zero divisors of `R` in `K`, there exists a non-zero element `x` in `R` such that the image of `x` under the algebra structure map from `R` to `K` is contained in `I`. In other words, every non-zero fractional ideal in the field of fractions of an integral domain contains at least one non-zero integer.
More concisely: Every non-zero fractional ideal of the non-zero divisors of an integral domain `R` in its field of fractions `K` contains a non-zero element from `R`.
|
FractionalIdeal.den_mul_self_eq_num'
theorem FractionalIdeal.den_mul_self_eq_num' :
∀ {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] (I : FractionalIdeal S P),
FractionalIdeal.spanSingleton S ((algebraMap R P) ↑I.den) * I = ↑I.num
This theorem states that for any commutative ring `R`, submonoid `S` of `R`, type `P` with a commutative ring structure, and an algebraic structure on `P` over `R`, if `P` is a localization of `R` at `S`, then for any fractional ideal `I` of `S` in `P`, the product of the fractional ideal generated by the denominator `I.den` of `I` (mapped from `R` to `P` using the algebra structure) and `I` itself is equal to the numerator `I.num` of `I`. In other words, for any fractional ideal, the fractional ideal generated by its denominator times the fractional ideal itself equals the numerator of the fractional ideal, when the denominator is considered as an element of the ring `P` via the algebra structure.
More concisely: For any commutative ring `R`, submonoid `S` of `R`, commutative ring `P` with algebra structure over `R` as a localization of `R` at `S`, and fractional ideal `I` of `S` in `P`, we have `I.den * I = I.num`, where `den` and `num` denote the denominator and numerator of `I`, respectively, considered as elements of `P` via the algebra structure.
|
FractionalIdeal.div_nonzero
theorem FractionalIdeal.div_nonzero :
∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
[frac : IsFractionRing R₁ K] [inst_3 : IsDomain R₁] {I J : FractionalIdeal (nonZeroDivisors R₁) K} (h : J ≠ 0),
I / J = ⟨↑I / ↑J, ⋯⟩
This theorem states that for any given Commutative Ring `R₁`, Field `K` (where `K` is the field of fractions of `R₁`), along with an Algebra structure over `R₁` and `K`, and given that `R₁` is an integral domain, for any two non-zero fractional ideals `I` and `J` of `R₁` in `K` (where `J` is not equal to zero), the quotient of `I` by `J` equals a fractional ideal formed from the quotient of the carriers of `I` and `J`. In more mathematical terms, if `I` and `J` are fractional ideals of `R₁` in `K`, then `I / J = { val := ↑I / ↑J, property := ⋯ }`, where the property ensures the resulting set is a fractional ideal.
More concisely: For any commutative ring `R₁` that is an integral domain, two non-zero fractional ideals `I` and `J` of `R₁` in its field of fractions `K` have the same quotient as the fractional ideal generated by the quotient of their carrier ideals in `R₁`.
|
FractionalIdeal.isNoetherian
theorem FractionalIdeal.isNoetherian :
∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
[frac : IsFractionRing R₁ K] [inst_3 : IsDomain R₁] [inst_4 : IsNoetherianRing R₁]
(I : FractionalIdeal (nonZeroDivisors R₁) K), IsNoetherian R₁ ↥↑I
The theorem states that for any Noetherian integral domain `R₁`, if `K` is the field of fractions of `R₁` and `I` is a fractional ideal of `R₁` (i.e., an ideal of `R₁` divided by some non-zero element in `R₁`), then `I` is also a Noetherian `R₁`-module. Here, an integral domain being Noetherian means all its ideals are finitely generated. Essentially, it means that fractional ideals in Noetherian integral domains retain the property of being finitely generated, and hence are also Noetherian.
More concisely: If `R₁` is a Noetherian integral domain, then every fractional ideal of `R₁` is a finitely generated `R₁`-module.
|