IsFractionRing.isAlgebraic_iff'
theorem IsFractionRing.isAlgebraic_iff' :
∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S] (K : Type u_5)
[inst_3 : Field K] [inst_4 : IsDomain R] [inst_5 : IsDomain S] [inst_6 : Algebra R K] [inst_7 : Algebra S K]
[inst_8 : NoZeroSMulDivisors R K] [inst_9 : IsFractionRing S K] [inst_10 : IsScalarTower R S K],
Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K
The theorem `IsFractionRing.isAlgebraic_iff'` states that for all types `R`, `S`, and `K`, where `R` and `S` have the structure of commutative rings, `R` and `S` have an algebra structure, `K` is a field, `R` and `S` are integral domains, and `K` is an algebra over `R` and `S`, `S` is algebraic over `R` if and only if a fraction ring of `S` is algebraic over `R`. Here, being algebraic means that every element of the algebra is a root of some nonzero polynomial with coefficients in the base ring. Also, `K` being a fraction ring of `S` refers to `K` being a field of fractions of `S`, where every element of `K` can be expressed as a quotient of two elements from `S`. The condition of `NoZeroSMulDivisors R K` ensures that the product of non-zero scalars from `R` and non-zero elements from `K` is never zero, while `IsScalarTower R S K` ensures that the scalar multiplications in `R`, `S`, and `K` are compatible.
More concisely: For commutative rings R, S with algebra structures, integrated domains, and R, S being an algebra over a field K with no zero divisors, S is algebraic over R if and only if the fraction ring of S is algebraic over R.
|
is_integral_localization_at_leadingCoeff
theorem is_integral_localization_at_leadingCoeff :
∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
{Rₘ : Type u_4} {Sₘ : Type u_5} [inst_3 : CommRing Rₘ] [inst_4 : CommRing Sₘ] [inst_5 : Algebra R Rₘ]
[inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ]
[inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] {x : S} (p : Polynomial R),
(Polynomial.aeval x) p = 0 →
p.leadingCoeff ∈ M → (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
This theorem states that, given an element `x` in an algebra `S` over a commutative ring `R` that is algebraic, meaning that there exists a non-zero polynomial `p` over `R` such that `p(x) = 0`, we can further restrict our attention to a submonoid `M` of `R` that contains the leading coefficient of `p`. In this case, the map from the localization of `R` at `M` to the localization of `S` at the image of `M` under the algebra map, becomes an integral ring morphism at the image of `x` under the algebra map. In other words, `x` becomes an integral element over the localized ring, which means that there exists a monic polynomial with coefficients in the localization that annihilates `x`. This theorem thus provides a method of localizing at a certain set to simplify the study of algebraic elements.
More concisely: Given an algebraic element `x` in an algebra `S` over a commutative ring `R`, the localization map from `R` to the localization of `S` at the image of the submonoid of `R` containing the leading coefficient of the polynomial defining `x` as root becomes an integral ring morphism at `x`.
|
integralClosure.isFractionRing_of_finite_extension
theorem integralClosure.isFractionRing_of_finite_extension :
∀ {A : Type u_4} (K : Type u_5) [inst : CommRing A] [inst_1 : IsDomain A] (L : Type u_6) [inst_2 : Field K]
[inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] [inst_6 : Algebra A L]
[inst_7 : Algebra K L] [inst_8 : IsScalarTower A K L] [inst_9 : FiniteDimensional K L],
IsFractionRing (↥(integralClosure A L)) L
The theorem `integralClosure.isFractionRing_of_finite_extension` states that for a given integral domain `A` and a field `L`, if `L` is a finite extension of the field of fractions of the integral domain `A`, then `L` is also the field of fractions of the integral closure of `A` in `L`. In other words, this theorem establishes a connection between the concept of integral closure and the property of being a fraction field in the context of finite field extensions.
More concisely: For a finite extension field `L` of the field of fractions of an integral domain `A`, `L` is the field of fractions of the integral closure of `A` in `L`.
|
IsIntegralClosure.isFractionRing_of_algebraic
theorem IsIntegralClosure.isFractionRing_of_algebraic :
∀ (A : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A] {L : Type u_6} [inst_2 : Field L] [inst_3 : Algebra A L]
(C : Type u_7) [inst_4 : CommRing C] [inst_5 : IsDomain C] [inst_6 : Algebra C L]
[inst_7 : IsIntegralClosure C A L] [inst_8 : Algebra A C] [inst_9 : IsScalarTower A C L],
Algebra.IsAlgebraic A L → (∀ (x : A), (algebraMap A L) x = 0 → x = 0) → IsFractionRing C L
The theorem `IsIntegralClosure.isFractionRing_of_algebraic` states that, for an integral domain `A` and a field `L` such that `L` is an algebraic extension of `A`, if `C` is the integral closure of `A` in `L`, then `L` serves as the field of fractions for `C`. This is subject to the following conditions: all elements in `L` are algebraic over `A`, and for every element `x` in `A`, if its image under the algebra structure from `A` to `L` is zero, then `x` must be zero. Essentially, this theorem links the concepts of algebraic extensions, integral closures, and fields of fractions.
More concisely: If `A` is an integral domain, `L` is a field that is an algebraic extension of `A` where every element is algebraic over `A` and `C` is the integral closure of `A` in `L`, then `L` is the field of fractions of `C`.
|
IsFractionRing.comap_isAlgebraic_iff
theorem IsFractionRing.comap_isAlgebraic_iff :
∀ {A : Type u_4} {K : Type u_5} {C : Type u_6} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Field K]
[inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] [inst_5 : CommRing C] [inst_6 : Algebra A C]
[inst_7 : Algebra K C] [inst_8 : IsScalarTower A K C], Algebra.IsAlgebraic A C ↔ Algebra.IsAlgebraic K C
The theorem `IsFractionRing.comap_isAlgebraic_iff` states that for any given types A, K, and C, where A is a commutative ring, A is an integral domain, K is a field, A is a K-algebra, K is the field of fractions of A, C is a commutative ring, C is an A-algebra, C is a K-algebra, and A, K, and C form a scalar tower, a ring C is algebraic over the ring A if and only if it is algebraic over the field of fractions K of A. In other words, all elements of C can be expressed as roots of non-zero polynomials with coefficients in A or K respectively.
More concisely: For a commutative ring A that is an integral domain and a field K its field of fractions, a commutative ring C is algebraic over A if and only if it is algebraic over K as A-algebras and K-algebras, forming a scalar tower.
|
integralClosure.isFractionRing_of_algebraic
theorem integralClosure.isFractionRing_of_algebraic :
∀ {A : Type u_4} [inst : CommRing A] [inst_1 : IsDomain A] {L : Type u_6} [inst_2 : Field L] [inst_3 : Algebra A L],
Algebra.IsAlgebraic A L →
(∀ (x : A), (algebraMap A L) x = 0 → x = 0) → IsFractionRing (↥(integralClosure A L)) L
This theorem states that, given an integral domain `A` and a field `L` where `L` is an algebraic extension of `A`, if all elements of the algebra from `A` to `L` are algebraic, then the fraction field of the integral closure of `A` in `L` is `L` itself. Furthermore, this holds when the function that embeds `A` into `L` preserves the property that only the zero element of `A` is mapped to the zero of `L`.
In another perspective, this theorem is about algebraic field extensions. It states that if `L` is an algebraic extension of the ring `A` (which is an integral domain), then the field of fractions of the integral closure of `A` in `L` is `L`. This is under the condition that the map from `A` to `L` (given by the algebra structure) maps only the zero of `A` to the zero of `L`.
More concisely: If `A` is an integral domain, `L` is a field and an algebraic extension of `A`, and the embedding of `A` into `L` maps only the zero element to the zero element, then the fraction field of the integral closure of `A` in `L` equals `L`.
|
IsFractionRing.ideal_span_singleton_map_subset
theorem IsFractionRing.ideal_span_singleton_map_subset :
∀ (R : Type u_1) [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {K : Type u_5}
{L : Type u_6} [inst_3 : IsDomain R] [inst_4 : IsDomain S] [inst_5 : Field K] [inst_6 : Field L]
[inst_7 : Algebra R K] [inst_8 : Algebra R L] [inst_9 : Algebra S L] [inst_10 : IsIntegralClosure S R L]
[inst_11 : IsFractionRing S L] [inst_12 : Algebra K L] [inst_13 : IsScalarTower R S L]
[inst_14 : IsScalarTower R K L] {a : S} {b : Set S},
Algebra.IsAlgebraic R L →
Function.Injective ⇑(algebraMap R L) →
↑(Ideal.span {a}) ⊆ ↑(Submodule.span R b) →
↑(Ideal.span {(algebraMap S L) a}) ⊆ ↑(Submodule.span K (⇑(algebraMap S L) '' b))
This theorem states that for any commutative rings `R` and `S`, with `S` being an algebra over `R`, and any fields `K` and `L` with `L` being an algebra over both `R`, `S`, `K`, and `S` being integral closure of `R` in `L`, and `L` being the field of fractions of `S`, if every element of `L` is algebraic over `R` and the mapping from `R` to `L` is injective, then if the `S`-multiples of an element `a` of `S` are contained in the `R`-span of a set `b` in `S`, it follows that the `L`-multiples of the image of `a` under `algebraMap S L` are contained in the `K`-span of the images under `algebraMap S L` of the set `b`. In simpler terms, if certain multiples of an element are contained in a span, then the corresponding multiples of the image of that element under a certain mapping are contained in the corresponding span of the image of the set.
More concisely: If `R` is a commutative ring, `S` is an algebra over `R` with integral closure `L` in it being the field of fractions of `S`, `K` is a field and an algebra over both `R`, `S`, and `L`, every element of `L` is algebraic over `R`, and the mapping from `R` to `L` is injective, then the `R`-span of a set in `S` contains the `S`-multiples of an element in `S`, implying that the `K`-span of their images under `algebraMap S L` contains the `L`-multiples of the image of that element under `algebraMap S L`.
|
IsFractionRing.isAlgebraic_iff
theorem IsFractionRing.isAlgebraic_iff :
∀ (A : Type u_4) (K : Type u_5) (C : Type u_6) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Field K]
[inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] [inst_5 : CommRing C] [inst_6 : Algebra A C]
[inst_7 : Algebra K C] [inst_8 : IsScalarTower A K C] {x : C}, IsAlgebraic A x ↔ IsAlgebraic K x
This theorem states that for any element of a ring, it is algebraic over the ring `A` if and only if it is algebraic over the field of fractions of `A`. More formally, given types `A`, `K`, and `C` where `A` is a commutative ring and integral domain, `K` is a field and `C` is a commutative ring, `K` is the field of fractions of `A`, and `C` is an `A`-algebra and `K`-algebra with `A` being scalar over `K` and `C`, an element `x` of `C` is algebraic over `A` (i.e., `x` is a root of a nonzero polynomial with coefficients in `A`) if and only if `x` is algebraic over `K` (i.e., `x` is a root of a nonzero polynomial with coefficients in `K`).
More concisely: An element of a commutative ring `C` that is both an `A`-algebra and `K`-algebra, where `A` is a commutative ring and integral domain, `K` is its field of fractions, and `A` is scalar over `K`, is algebraic over `A` if and only if it is algebraic over `K`.
|
isIntegral_localization
theorem isIntegral_localization :
∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
{Rₘ : Type u_4} {Sₘ : Type u_5} [inst_3 : CommRing Rₘ] [inst_4 : CommRing Sₘ] [inst_5 : Algebra R Rₘ]
[inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ]
[inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ],
Algebra.IsIntegral R S → (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegral
The theorem `isIntegral_localization` states that given an integral extension from a commutative ring `R` to another ring `S`, and a submonoid `M` of `R`. If `Rₘ` is the localization of `R` at `M`, and `Sₘ` is the localization of `S` at the image of `M` under the extension map, then the induced map from `Rₘ` to `Sₘ` is also an integral extension. An integral extension is a situation where every element of the ring extension is integral over the base ring. An element is said to be integral if it is a root of some monic polynomial with coefficients in the base ring.
More concisely: The localization of an integral extension of commutative rings preserves integral extensions.
|
IsIntegralClosure.isFractionRing_of_finite_extension
theorem IsIntegralClosure.isFractionRing_of_finite_extension :
∀ (A : Type u_4) (K : Type u_5) [inst : CommRing A] [inst_1 : IsDomain A] (L : Type u_6) [inst_2 : Field K]
[inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra A L] [inst_6 : IsFractionRing A K] (C : Type u_7)
[inst_7 : CommRing C] [inst_8 : IsDomain C] [inst_9 : Algebra C L] [inst_10 : IsIntegralClosure C A L]
[inst_11 : Algebra A C] [inst_12 : IsScalarTower A C L] [inst_13 : Algebra K L] [inst : IsScalarTower A K L]
[inst : FiniteDimensional K L], IsFractionRing C L
The theorem states that if the field `L` is a finite extension of the field of fractions `K` of an integral domain `A`, then the integral closure `C` of `A` in `L` also has `L` as its field of fractions. The integral domain `A` is a commutative ring and `K` is its field of fractions. This theorem is under the condition that `C` is an integral closure of `A` in `L`, `C` is a commutative ring, `L` is a field and `C` is an algebra over `L`. Also, `A`, `C`, and `L` form a scalar tower, as do `A`, `K`, and `L`.
More concisely: If `A` is a commutative integral domain with field of fractions `K`, `L` is a field that is a finite extension of `K`, and `C` is the integral closure of `A` in `L` (which is itself a commutative ring and an algebra over `L`), then `C` is the integral closure of `A` in `L` with `L` as its field of fractions. (In other words, `L` is the field of fractions of `C`.)
|