isAlgebraic_algebraMap
theorem isAlgebraic_algebraMap :
∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [inst_3 : Nontrivial R]
(x : R), IsAlgebraic R ((algebraMap R A) x)
This theorem states that for any element `x` from a commutative ring `R`, when `x` is viewed as an element of an `R`-algebra `A` via the algebraic embedding `algebraMap R A`, it is considered to be algebraic over `R`. In mathematical terms, `x` is a root of a nonzero polynomial with coefficients in `R`. The theorem holds under the assumption that `R` is nontrivial, that is, `R` contains at least two distinct elements.
More concisely: For any commutative ring `R` with at least two elements and any `x` in an `R`-algebra `A` via the algebraic embedding `algebraMap R A`, `x` is algebraic over `R`.
|
Algebra.IsAlgebraic.of_injective
theorem Algebra.IsAlgebraic.of_injective :
∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u_2}
[inst_3 : Ring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
Function.Injective ⇑f → Algebra.IsAlgebraic R B → Algebra.IsAlgebraic R A
The theorem `Algebra.IsAlgebraic.of_injective` states that for any types `R` and `A`, where `R` is a commutative ring, `A` is a ring, and `A` is an `R`-algebra, if there exists another type `B` that is also a ring and an `R`-algebra, along with an algebra map `f : A →ₐ[R] B` that is injective, then if `B` is an algebraic over `R` (all elements of `B` are algebraic over `R`), it implies that `A` is also algebraic over `R`. In simpler terms, an injective algebra map from an algebra `A` to another algebra `B` preserves the property of being algebraic over a common base ring `R`.
More concisely: If `R` is a commutative ring, `A` and `B` are `R`-algebras, `f : A →ₐ[R] B` is an injective algebra map, and `B` is algebraic over `R`, then `A` is also algebraic over `R`.
|
Subalgebra.isField_of_algebraic
theorem Subalgebra.isField_of_algebraic :
∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (A : Subalgebra K L),
Algebra.IsAlgebraic K L → IsField ↥A
This theorem states that for any algebraic extension L/K, any intermediate subalgebra is a field. Specifically, given a field K and another field L, where L is an algebra over K, and given that L is an algebraic over K, then any subalgebra A of L over K is also a field. This means that every non-zero element within the subalgebra A has a multiplicative inverse.
More concisely: In a field extension L/K, any subalgebra of L that is algebraic over K is itself a field.
|
IsAlgebraic.isIntegral
theorem IsAlgebraic.isIntegral :
∀ {K : Type u} {A : Type v} [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A] {x : A},
IsAlgebraic K x → IsIntegral K x
This theorem, known as an alias of the forward direction of `isAlgebraic_iff_isIntegral`, states that for any element `x` in an algebra `A` over a field `K`, if `x` is algebraic over `K` then `x` is also integral over `K`. Here, an element being algebraic means that it is a root of a nonzero polynomial with coefficients in `K`, and being integral means that it is root of some monic polynomial with coefficients in `K`. In other words, if an element of an algebra satisfies a polynomial equation with coefficients in the field, it also satisfies a monic polynomial equation with coefficients in the field.
More concisely: If an element in an algebra over a field is algebraic, then it is integral.
|
Subalgebra.isAlgebraic_iff
theorem Subalgebra.isAlgebraic_iff :
∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
S.IsAlgebraic ↔ Algebra.IsAlgebraic R ↥S
This theorem states that for any commutative ring `R` and ring `A` where `A` is an `R`-algebra, a subalgebra `S` of `A` is algebraic if and only if it is algebraic when considered as an algebra itself. Here, a subalgebra `S` is said to be algebraic if all its elements are roots of some non-zero polynomial with coefficients in `R`, and similarly, an algebra is said to be algebraic if all its elements satisfy the same property.
More concisely: A subalgebra of an `R`-algebra `A` is algebraic if and only if it is an algebraic subset of `A` considered as an `R`-algebra itself.
|
Algebra.IsAlgebraic.trans
theorem Algebra.IsAlgebraic.trans :
∀ {K : Type u_1} {L : Type u_2} {A : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Ring A]
[inst_3 : Algebra K L] [inst_4 : Algebra L A] [inst_5 : Algebra K A] [inst_6 : IsScalarTower K L A],
Algebra.IsAlgebraic K L → Algebra.IsAlgebraic L A → Algebra.IsAlgebraic K A
The theorem `Algebra.IsAlgebraic.trans` states that if we have a field `L` that is an algebraic field extension of another field `K`, and if `A` is an algebraic algebra over `L`, then `A` is also algebraic over `K`. This is assuming that we have the appropriate algebra structures between the types, and that there exists a scalar tower between `K`, `L`, and `A`. In simpler terms, if `L` is constructed from `K` by adding elements that are roots of polynomials with coefficients in `K`, and `A` is similarly constructed from `L`, then `A` can also be seen as being constructed from `K` in a similar manner.
More concisely: If `L` is an algebraic field extension of `K`, then every algebraic element of an algebra `A` over `L` is also algebraic over `K`.
|
Algebra.IsAlgebraic.tower_top_of_injective
theorem Algebra.IsAlgebraic.tower_top_of_injective :
∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
[inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A],
Function.Injective ⇑(algebraMap R S) → Algebra.IsAlgebraic R A → Algebra.IsAlgebraic S A
The theorem `Algebra.IsAlgebraic.tower_top_of_injective` states that, given the types `R`, `S`, and `A` with the conditions that `R` and `S` are commutative rings, `A` is a ring, and `S` and `A` are algebras over `R`, and `A` is also an algebra over `S` with a scalar tower structure between `R`, `S`, and `A`. If the algebra structure `R` to `S` is injective (meaning the mapping from `R` to `S` does not assign the same value to any two different elements of `R`), and `A` is an algebraic algebra over `R` (meaning all elements in `A` are algebraic over `R`), then `A` is also algebraic over `S` (meaning all elements in `A` are also algebraic over `S`).
More concisely: If `R`, `S`, and `A` are commutative rings with `A` being a ring and an algebra over both `R` and `S`, an algebraic algebra over `R`, and the `R`-algebra structure on `S` is injective, then `A` is an algebraic algebra over `S`.
|
IsAlgebraic.algHom
theorem IsAlgebraic.algHom :
∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u_2}
[inst_3 : Ring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) {a : A}, IsAlgebraic R a → IsAlgebraic R (f a)
The theorem `IsAlgebraic.algHom` states that for any commutative ring `R` and rings `A` and `B` such that `A` and `B` are both `R`-algebras, if an element `a` from the ring `A` is algebraic over `R` (meaning that there exists a nonzero polynomial with coefficients in `R` that evaluates to zero at `a`), then the image of `a` under any `R`-algebra homomorphism `f` from `A` to `B` is also algebraic over `R`. This theorem expands on `IsAlgebraic.algebraMap` by allowing the intermediate ring `A` to be noncommutative.
More concisely: If `R` is a commutative ring, `A` and `B` are `R`-algebras, and `a` is an algebraic element in `A` over `R`, then the image of `a` under any `R`-algebra homomorphism from `A` to `B` is also an algebraic element in `B` over `R`.
|
Algebra.IsAlgebraic.algHom_bijective₂
theorem Algebra.IsAlgebraic.algHom_bijective₂ :
∀ {K : Type u_1} {L : Type u_2} {R : Type u_3} [inst : CommRing K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : NoZeroSMulDivisors K L] [inst_4 : Field R] [inst_5 : Algebra K R],
Algebra.IsAlgebraic K L → ∀ (f : L →ₐ[K] R) (g : R →ₐ[K] L), Function.Bijective ⇑f ∧ Function.Bijective ⇑g
The theorem `Algebra.IsAlgebraic.algHom_bijective₂` states that for any three types `K`, `L`, and `R` where `K` is a commutative ring, `L` and `R` are fields, and `L` and `R` are also `K`-algebras, if all elements of `L` are algebraic over `K` (i.e., `L` is an algebraic `K`-algebra), then for any two algebra homomorphisms `f` from `L` to `R` and `g` from `R` to `L` (both preserving the structure of `K`-algebras), the function `f` is bijective (i.e., both injective and surjective) and the function `g` is also bijective. In other words, if `L` is an algebraic `K`-algebra, any pair of algebra homomorphisms between `L` and `R` will always be bijections.
More concisely: If `L` is a commutative `K`-algebra, `R` is a field, `L` is algebraic over `K`, and `f: L → R` and `g: R → L` are `K`-algebra homomorphisms, then both `f` and `g` are bijective functions.
|
Subalgebra.inv_mem_of_algebraic
theorem Subalgebra.inv_mem_of_algebraic :
∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (A : Subalgebra K L)
{x : ↥A}, IsAlgebraic K ↑x → (↑x)⁻¹ ∈ A
The theorem `Subalgebra.inv_mem_of_algebraic` states that for any two types `K` and `L` that are fields, with `L` being a `K`-algebra, and for any subalgebra `A` of `L` over `K`, if an element `x` of `A` is algebraic over `K`, then the multiplicative inverse of `x` (denoted `(↑x)⁻¹`) also belongs to `A`. Here, being algebraic means that `x` is a root of some non-zero polynomial with coefficients in `K`.
In the context of algebra, this theorem guarantees that if we have an element in a subalgebra that is algebraic over the base field, then its inverse also remains in the subalgebra, ensuring that subalgebras are closed under inversion for algebraic elements.
More concisely: If `A` is a subalgebra of a `K`-algebra `L`, and `x` is an algebraic element of `A` over `K`, then `(↑x)⁻¹` is also in `A`.
|
Algebra.IsAlgebraic.of_finite
theorem Algebra.IsAlgebraic.of_finite :
∀ (K : Type u_1) (A : Type u_5) [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A]
[inst_3 : FiniteDimensional K A], Algebra.IsAlgebraic K A
This theorem states that for any field `K` and ring `A`, if `A` is a field extension of `K` (i.e., `A` is an algebra over `K`) and `A` is also a finite-dimensional vector space over `K`, then `A` is an algebraic field extension of `K`. In other words, every element of `A` is algebraic over `K`, meaning it is a root of some non-zero polynomial with coefficients in `K`.
More concisely: If `A` is a finite-dimensional field extension of `K`, then every element of `A` is algebraic over `K`.
|
Algebra.isAlgebraic_iff
theorem Algebra.isAlgebraic_iff :
∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
Algebra.IsAlgebraic R A ↔ ⊤.IsAlgebraic
This theorem states that for any given algebra over a commutative ring, it is algebraic if and only if it is algebraic as a subalgebra. More technically, given any types `R` and `A` with `R` being a commutative ring, `A` being a ring, and `A` being an algebra over `R`, we have that `A` is algebraic over `R` (that is, every element of `A` is a root of some non-zero polynomial with coefficients in `R`) if and only if the whole of `A` (denoted by `⊤`) as a subalgebra of itself is algebraic. This is a characterization of algebraicity that works at the level of the entire algebra `A`, and not just individual elements.
More concisely: A commutative ring algebra is algebraic if and only if the whole algebra is algebraic as a subalgebra.
|
IsIntegral.isAlgebraic
theorem IsIntegral.isAlgebraic :
∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [inst_3 : Nontrivial R]
{x : A}, IsIntegral R x → IsAlgebraic R x
This theorem states that if an element `x` of an algebra `A` over a commutative ring `R` is integral, then `x` is also algebraic over `R`. In other words, if `x` is a root of a monic polynomial with coefficients in `R` (the definition of being integral), then there exists a non-zero polynomial with coefficients in `R` such that `x` is a root of this polynomial (the definition of being algebraic). This is true for all nontrivial commutative rings `R` and any ring `A` where `R` acts as an algebra on `A`.
More concisely: If an element `x` of an algebra `A` over a commutative ring `R` is integral, then `x` is algebraic over `R`. (An integral element is a root of a monic polynomial with coefficients in `R`, and an algebraic element is a root of some non-zero polynomial with coefficients in `R`.)
|
Algebra.IsAlgebraic.tower_top
theorem Algebra.IsAlgebraic.tower_top :
∀ {K : Type u_1} (L : Type u_2) {A : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Ring A]
[inst_3 : Algebra K L] [inst_4 : Algebra L A] [inst_5 : Algebra K A] [inst_6 : IsScalarTower K L A],
Algebra.IsAlgebraic K A → Algebra.IsAlgebraic L A
The theorem `Algebra.IsAlgebraic.tower_top` states that for any field K, if A is an algebraic algebra over K, then A also remains algebraic over another field L whenever L is an extension of K. Here, a field extension means that K is a subfield of L. In formal notation, it asserts that: for all fields K, L and a ring A, if A is algebraic over K and there exist valid algebra structures over K, L, and A as well as a valid scalar tower structure over K, L, and A, then A is also algebraic over L.
More concisely: If A is an algebraic algebra over field K and K is a subfield of L, then A is algebraic over the field extension L.
|
Algebra.IsAlgebraic.algHom_bijective
theorem Algebra.IsAlgebraic.algHom_bijective :
∀ {K : Type u_1} {L : Type u_2} [inst : CommRing K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : NoZeroSMulDivisors K L], Algebra.IsAlgebraic K L → ∀ (f : L →ₐ[K] L), Function.Bijective ⇑f
The theorem `Algebra.IsAlgebraic.algHom_bijective` states that for any commutative ring `K` and any field `L` that is an algebra over `K` with no zero scalar multiplication divisors, if all elements of `L` are algebraic over `K` (i.e., `L` is an algebraic algebra over `K`), then for any algebra homomorphism `f` from `L` to `L` over `K`, the function `f` is bijective – that is, it is both injective (it maps distinct elements of its domain to distinct elements of its codomain) and surjective (every element of its codomain is the image of some element of its domain).
More concisely: If `K` is a commutative ring, `L` is a field algebraically closed over `K` with no zero divisors in scalar multiplication, and `f` is an algebra homomorphism from `L` to `L` over `K`, then `f` is a bijective function.
|
IsIntegralClosure.exists_smul_eq_mul
theorem IsIntegralClosure.exists_smul_eq_mul :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] {L : Type u_3}
[inst_3 : Field L] [inst_4 : Algebra R S] [inst_5 : Algebra S L] [inst_6 : Algebra R L]
[inst_7 : IsScalarTower R S L] [inst_8 : IsIntegralClosure S R L],
Algebra.IsAlgebraic R L →
Function.Injective ⇑(algebraMap R L) → ∀ (a : S) {b : S}, b ≠ 0 → ∃ c d, d ≠ 0 ∧ d • a = b * c
The theorem `IsIntegralClosure.exists_smul_eq_mul` states that for any elements `a` and `b` (with `b` not equal to zero) from a ring `S`, which is the integral closure of a commutative ring `R` in an algebraic extension `L` of `R`, we can find elements `c` from `S` and `d` from `R` (with `d` not equal to zero) such that `d` times `a` equals `b` times `c`. This is under the conditions that `L` is algebraic over `R` and the algebra map from `R` to `L` is injective.
More concisely: For any elements `a` in an integral closure `S` of a commutative ring `R` in an algebraic extension `L` of `R`, and any non-zero `b` in `L`, there exist `c` in `S` and `d` in `R` (with `d` non-zero) such that `d * a = b * c`.
|
IsAlgebraic.tower_top_of_injective
theorem IsAlgebraic.tower_top_of_injective :
∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
[inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A],
Function.Injective ⇑(algebraMap R S) → ∀ {x : A}, IsAlgebraic R x → IsAlgebraic S x
The theorem states that if an element `x` is algebraic over a commutative ring `R`, then `x` is also algebraic over a commutative ring `S` provided that `S` is an extension of `R` and the mapping from `R` to `S` is injective. Here, being algebraic means that `x` is a root of a non-zero polynomial with coefficients in the respective ring (`R` or `S`). This theorem is stated in the context of commutative rings `R` and `S`, a ring `A`, with algebraic structures defined between `R`, `S`, and `A` such that `R`, `S`, and `A` form a scalar tower, which is a sequence of scalar extensions.
More concisely: If `x` is algebraic over a commutative ring `R`, then `x` is also algebraic over an injective homomorphism's image of `R` in a commutative ring `S`, extending `R`.
|
Algebra.IsAlgebraic.isIntegral
theorem Algebra.IsAlgebraic.isIntegral :
∀ {K : Type u} {A : Type v} [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A],
Algebra.IsAlgebraic K A → Algebra.IsIntegral K A
This theorem, labeled as an alias of the forward direction of `Algebra.isAlgebraic_iff_isIntegral`, states that for any field `K` and any ring `A` with a structure of `K`-algebra, if the `K`-algebra `A` is algebraic (i.e., all its elements are algebraic), then it is integral. In other words, every element of the `K`-algebra `A` is integral over the base field `K`.
More concisely: If `K` is a field and `A` is a `K`-algebra, then `A` being algebraic implies that every element of `A` is integral over `K`.
|
AlgEquiv.isAlgebraic
theorem AlgEquiv.isAlgebraic :
∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u_2}
[inst_3 : Ring B] [inst_4 : Algebra R B], (A ≃ₐ[R] B) → Algebra.IsAlgebraic R A → Algebra.IsAlgebraic R B
The theorem `AlgEquiv.isAlgebraic` states that the property of being algebraic is preserved under an algebraic equivalence. Specifically, for any types `R`, `A` and `B` where `R` is a commutative ring, `A` and `B` are rings, `A` is an `R`-algebra and `B` is an `R`-algebra, if there exists an algebraic equivalence between `A` and `B`, and if `A` is algebraic over `R`, then `B` is also algebraic over `R`. In other words, if every element of `A` is the root of some polynomial with coefficients in `R`, then under an algebraic equivalence, every element of `B` will also be the root of some polynomial with coefficients in `R`.
More concisely: If `A` and `B` are `R`-algebras with an algebraic equivalence between them, and `A` is algebraic over `R`, then `B` is also algebraic over `R`.
|
IsAlgebraic.inv
theorem IsAlgebraic.inv :
∀ {R : Type u} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] {x : K},
IsAlgebraic R x → IsAlgebraic R x⁻¹
The theorem `IsAlgebraic.inv` states that for any commutative ring `R` and field `K`, if `x` is an element of `K` and `x` is algebraic over `R`, then the inverse of `x` is also algebraic over `R`. Here, an element is considered algebraic over `R` if it is a root of a nonzero polynomial with coefficients in `R`.
More concisely: If `x` is an algebraic element over the commutative ring `R` in the field `K`, then the multiplicative inverse of `x` (when it exists) is also an algebraic element over `R`.
|
isAlgebraic_iff_isIntegral
theorem isAlgebraic_iff_isIntegral :
∀ {K : Type u} {A : Type v} [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A] {x : A},
IsAlgebraic K x ↔ IsIntegral K x
This theorem states that for any element `x` of an algebra `A` over a field `K`, `x` is algebraic over `K` if and only if `x` is integral over `K`. Here, an element is defined as algebraic over `K` if it is a root of a non-zero polynomial with coefficients in `K`, and it is defined as integral over `K` if it is a root of a monic polynomial in `K[X]`, equivalently, the element is integral with respect to the induced `algebraMap` from `K` to `A`.
More concisely: An element `x` in an algebra `A` over a field `K` is algebraic over `K` if and only if it is integral over `K`.
|
IsAlgebraic.tower_top
theorem IsAlgebraic.tower_top :
∀ {K : Type u_1} (L : Type u_2) {A : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Ring A]
[inst_3 : Algebra K L] [inst_4 : Algebra L A] [inst_5 : Algebra K A] [inst_6 : IsScalarTower K L A] {x : A},
IsAlgebraic K x → IsAlgebraic L x
The theorem `IsAlgebraic.tower_top` states that if an element `x` from a ring `A` is algebraic over a field `K`, then `x` is also algebraic over another field `L` provided that `L` is an extension of `K`. This is understood within the context of `L` and `A` being algebras over `K`, and `A` being an algebra over `L` with `K`, `L`, and `A` forming a scalar tower. Here, being algebraic means that there exists some nonzero polynomial with coefficients in the corresponding field such that `x` is a root of this polynomial.
More concisely: If `x` is an algebraic element over a field `K`, then `x` is also algebraic over any extension field `L` of `K` within the context of `L` being a scalar extension of `K` over `A`, where `A` is an algebra over `L` containing `K` and `x`.
|