IsCyclotomicExtension.empty
theorem IsCyclotomicExtension.empty :
∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
[h : IsCyclotomicExtension ∅ A B], ⊥ = ⊤
This theorem states that if there is an empty cyclotomic extension from a type `A` to a type `B` (both of which are commutative rings and there is an algebra structure from `A` to `B`), then the bottom element of the lattice structure equals the top element. In mathematical terms, if `A` and `B` are commutative rings and `A` is an algebra over `B` with an empty set of cyclotomic polynomials, then the image of `A` in `B` equals `B`.
More concisely: If `A` is a commutative ring algebra over the commutative ring `B` with an empty set of cyclotomic polynomials, then `A` and `B` are equal as sets.
|
IsCyclotomicExtension.isSplittingField_X_pow_sub_one
theorem IsCyclotomicExtension.isSplittingField_X_pow_sub_one :
∀ (n : ℕ+) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : IsCyclotomicExtension {n} K L], Polynomial.IsSplittingField K L (Polynomial.X ^ ↑n - 1)
The theorem `IsCyclotomicExtension.isSplittingField_X_pow_sub_one` states that for any positive natural number `n`, any two types `K` and `L` (representing mathematical fields), given instances of `K` and `L` as fields, an instance of `L` as a `K`-algebra, and an instance proving that `L` is a cyclotomic extension of `K` at `n`, then `L` is the splitting field of the polynomial `X^n - 1` over `K`. In more mathematical terms, if `L` is a cyclotomic extension of `K` at `n`, then the polynomial `X^n - 1` splits completely over `L`, that is, it can be factored into linear factors in `L`.
More concisely: If `L` is a cyclotomic extension of field `K` at degree `n`, then `X^n - 1` splits completely in `L` as a product of linear factors.
|
IsCyclotomicExtension.numberField
theorem IsCyclotomicExtension.numberField :
∀ (S : Set ℕ+) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[h : NumberField K] [inst_3 : Finite ↑S] [inst : IsCyclotomicExtension S K L], NumberField L
The theorem states that for any set `S` of positive natural numbers and for any two types `K` and `L` where `K` and `L` are fields and `K` is a number field with a structure of an algebra over `K`, and if `S` is finite and `L` is a cyclotomic extension of `K` with respect to `S`, then `L` is also a number field. In other words, a cyclotomic finite extension of a number field is still a number field.
More concisely: If `S` is a finite set of positive natural numbers, `K` is a number field, and `L` is a cyclotomic extension of `K` with respect to `S`, then `L` is a number field.
|
IsCyclotomicExtension.splits_cyclotomic
theorem IsCyclotomicExtension.splits_cyclotomic :
∀ {n : ℕ+} {S : Set ℕ+} (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : IsCyclotomicExtension S K L],
n ∈ S → Polynomial.Splits (algebraMap K L) (Polynomial.cyclotomic (↑n) K)
The theorem `IsCyclotomicExtension.splits_cyclotomic` states that for any positive natural number `n` and a set `S` of positive natural numbers, along with two types `K` and `L` that have field and algebra structures respectively, and assuming that `L` extends `K` cyclotomically over the set `S`, if `n` is an element of `S`, then the `n`-th cyclotomic polynomial with coefficients in `K` splits when being regarded as a polynomial over `L`. Here, a polynomial 'splits' if it is either zero or all of its irreducible factors have degree 1, as defined by `Polynomial.Splits`. The mapping from `K` to `L` is given by the algebra embedding `algebraMap K L`.
More concisely: If `K` is a field, `L` is a field extension of `K` cyclotomically over a set `S` of positive natural numbers, and `n` is an element of `S`, then the `n`-th cyclotomic polynomial over `K` splits into linear factors when considered as a polynomial over `L`.
|
IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots
theorem IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots :
∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
{ζ : B} {n : ℕ+},
IsPrimitiveRoot ζ ↑n →
Algebra.adjoin A ((Polynomial.cyclotomic (↑n) A).rootSet B) = Algebra.adjoin A {b | ∃ a ∈ {n}, b ^ ↑a = 1}
This theorem states that for any given types `A` and `B` which are commutative rings with an algebra structure from `A` to `B`, and where `B` is a domain, for a given element `ζ` of `B` and a positive integer `n`, if `ζ` is a primitive `n`-th root of unity, then the minimal subalgebra of `B` over `A` that includes all the roots of the `n`-th cyclotomic polynomial in `A` is equal to the minimal subalgebra of `B` over `A` that includes all the `n`-th roots of unity.
More concisely: For any commutative rings with algebra structures `A` to `B` with `B` being a domain, if `ζ` is a primitive `n`-th root of unity in `B`, then the minimal subalgebras of `B` over `A` containing all `n`-th cyclotomic polynomials and all `n`-th roots of unity are equal.
|
IsCyclotomicExtension.iff_union_singleton_one
theorem IsCyclotomicExtension.iff_union_singleton_one :
∀ (S : Set ℕ+) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
This theorem states that for any set `S` of positive natural numbers, and any two types `A` and `B` with commutative ring structures `A` and `B` where `B` is an `A`-algebra, the property of being a cyclotomic extension of `A` to `B` for `S` is equivalent to the property of being a cyclotomic extension for the union of `S` and the singleton set containing `1`. In other words, adding `1` to the set `S` does not change whether or not `B` is a cyclotomic extension of `A`.
More concisely: For any set S of positive natural numbers, and commutative rings with unity A and B such that B is an A-algebra, the sets S and S∪{1} have isomorphic cyclotomic extensions in A if and only if B is a cyclotomic extension of A.
|
IsCyclotomicExtension.of_union_of_dvd
theorem IsCyclotomicExtension.of_union_of_dvd :
∀ {n : ℕ+} {S : Set ℕ+} (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
(∀ s ∈ S, n ∣ s) → S.Nonempty → ∀ [H : IsCyclotomicExtension S A B], IsCyclotomicExtension (S ∪ {n}) A B
The theorem `IsCyclotomicExtension.of_union_of_dvd` states that for any positive natural number `n`, any set `S` of positive natural numbers, and any types `A` and `B` with commutative ring structures where `B` is an `A`-algebra, if every element of `S` is divisible by `n` and `S` is not empty, then whenever `B` is a cyclotomic extension of `A` with respect to `S`, it is also a cyclotomic extension with respect to the union of `S` and the set containing `n`.
In other words, adding a divisor of all elements of `S` to `S` does not prevent `B` from being a cyclotomic extension of `A`.
More concisely: If `B` is a cyclotomic extension of `A` with respect to a set `S` of positive natural numbers dividing `n` in `A`, then `B` is also a cyclotomic extension of `A` with respect to the set `S ∪ {n}`.
|
IsCyclotomicExtension.trans
theorem IsCyclotomicExtension.trans :
∀ (S T : Set ℕ+) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
(C : Type w) [inst_3 : CommRing C] [inst_4 : Algebra A C] [inst_5 : Algebra B C] [inst_6 : IsScalarTower A B C]
[hS : IsCyclotomicExtension S A B] [hT : IsCyclotomicExtension T B C],
Function.Injective ⇑(algebraMap B C) → IsCyclotomicExtension (S ∪ T) A C
The theorem `IsCyclotomicExtension.trans` expresses the transitivity of cyclotomic extensions. In particular, it asserts that for all sets `S` and `T` of positive natural numbers, and for all commutative rings `A`, `B`, and `C`, if `A` is a cyclotomic extension of `B` with respect to `S`, and `B` is a cyclotomic extension of `C` with respect to `T`, and the algebra map from `B` to `C` is injective, then `A` is a cyclotomic extension of `C` with respect to the union of `S` and `T`. Here, commutative rings and cyclotomic extensions are algebraic structures, algebra maps are special kinds of ring homomorphisms, and injectivity ensures that different elements of the domain map to different elements of the codomain.
More concisely: If `A` is a cyclotomic extension of `B` with respect to `S` and `B` is a cyclotomic extension of `C` with respect to `T`, and the algebra map from `B` to `C` is injective, then `A` is a cyclotomic extension of `C` with respect to `S ∪ T`.
|
IsCyclotomicExtension.exists_prim_root
theorem IsCyclotomicExtension.exists_prim_root :
∀ {S : Set ℕ+} (A : Type u) {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
[self : IsCyclotomicExtension S A B] {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
This theorem states that for any set `S` of positive natural numbers and for any types `A` and `B` such that `A` and `B` are commutative rings and `B` is an algebra over `A`, if `B` is a cyclotomic extension of `A` with respect to `S`, then for every positive natural number `n` in `S`, there exists a primitive `n`-th root of unity in `B`. Here, a primitive `n`-th root of unity is an element `r` which generates the cyclic group of `n`-th roots of unity.
More concisely: For any set `S` of positive natural numbers, any commutative rings `A` and `B` with `B` an algebra over `A`, and `B` a cyclotomic extension of `A` with respect to `S`, there exists in `B` a primitive `n`-th root of unity for every positive natural number `n` in `S`.
|
IsCyclotomicExtension.splits_X_pow_sub_one
theorem IsCyclotomicExtension.splits_X_pow_sub_one :
∀ {n : ℕ+} {S : Set ℕ+} (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[H : IsCyclotomicExtension S K L], n ∈ S → Polynomial.Splits (algebraMap K L) (Polynomial.X ^ ↑n - 1)
This theorem states that for any positive natural number `n` and any set `S` of positive natural numbers, given any two fields `K` and `L` with an algebra structure on `L` over `K`, if `L` is a cyclotomic extension of `K` with respect to the set `S`, then if `n` is an element of `S`, the polynomial `X^n - 1` splits over `L` when considered as a polynomial with coefficients in `K`. In other words, the polynomial `X^n - 1`, when its coefficients are mapped from `K` to `L` using the algebra structure, is either the zero polynomial or all of its irreducible factors have degree 1.
More concisely: For any positive natural number `n` in a set `S` of positive natural numbers, in a cyclotomic extension `L` over field `K`, the polynomial `X^n - 1` splits completely with all irreducible factors of degree 1 when considered as a polynomial over `K`.
|
IsCyclotomicExtension.equiv
theorem IsCyclotomicExtension.equiv :
∀ (S : Set ℕ+) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
{C : Type u_1} [inst_3 : CommRing C] [inst_4 : Algebra A C] [h : IsCyclotomicExtension S A B],
(B ≃ₐ[A] C) → IsCyclotomicExtension S A C
This theorem states that given a set `S` of positive natural numbers and commutative rings `A`, `B`, and `C` where `A` is an algebra over `B` and `C`, if `B` is a cyclotomic extension of `A` over the set `S` (denoted as `IsCyclotomicExtension S A B`), and `B` is algebraically equivalent to `C` (denoted as `(B ≃ₐ[A] C)`), then `C` is also a cyclotomic extension of `A` over the set `S` (denoted as `IsCyclotomicExtension S A C`). In other words, the property of being a cyclotomic extension is preserved under algebraic equivalence.
More concisely: If `B` is a cyclotomic extension of `A` over `S`, `B` is algebraically equivalent to `C`, then `C` is a cyclotomic extension of `A` over `S`.
|
IsAlgClosed.isCyclotomicExtension
theorem IsAlgClosed.isCyclotomicExtension :
∀ (S : Set ℕ+) (K : Type w) [inst : Field K] [inst_1 : IsAlgClosed K],
(∀ a ∈ S, NeZero ↑↑a) → IsCyclotomicExtension S K K
This theorem states that for any set `S` of positive natural numbers and any type `K` that forms a field which is algebraically closed, if for all elements `a` in `S` the statement `NeZero ↑↑a` holds (i.e., the elements are not zero when cast to the field `K`), then `K` is an `S`-cyclotomic extension over itself. In mathematical terms, an algebraically closed field `K` is a cyclotomic extension of itself for a given set of natural numbers, provided none of these numbers become zero when regarded as elements of `K`.
More concisely: If a set `S` of positive natural numbers does not contain any zero elements when considered as elements of an algebraically closed field `K`, then `K` is a cyclotomic extension of itself over `S`.
|
IsCyclotomicExtension.singleton_zero_of_bot_eq_top
theorem IsCyclotomicExtension.singleton_zero_of_bot_eq_top :
∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
⊥ = ⊤ → IsCyclotomicExtension ∅ A B
This theorem states that for any types `A` and `B` that are both commutative rings with `B` being an algebra over `A`, if the smallest subalgebra of `B` that contains `A` (denoted `⊥`) is equal to the largest subalgebra of `B` that contains `A` (denoted `⊤`), then the extension from `A` to `B` is a cyclotomic extension. A cyclotomic extension is one in which every element of `B` is a root of unity in `A`.
More concisely: If for commutative rings `A` and `B` with `B` being an algebra over `A`, the smallest and largest subalgebras of `B` containing `A` are equal, then the extension of `A` by `B` is a cyclotomic extension.
|
IsCyclotomicExtension.adjoin_roots
theorem IsCyclotomicExtension.adjoin_roots :
∀ {S : Set ℕ+} {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
[self : IsCyclotomicExtension S A B] (x : B), x ∈ Algebra.adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1}
This theorem states that, for any set `S` of positive natural numbers, and any types `A` and `B` which form a communication ring and an algebra, respectively, and given a cyclotomic extension of `A` to `B` defined by `S`, any element `x` of type `B` is included in the minimal subalgebra that includes the `n`-th roots of unity, where `n` is an element of `S`. Here, an `n`-th root of unity is defined as an element `b` such that `b` raised to the power of `n` equals `1`. In other words, the `n`-th roots of unity for `n` in `S`, generate `B` as an `A`-algebra.
More concisely: For any set S of positive natural numbers, any communication ring A and its algebra B with a cyclotomic extension defined by S, every element of B contains an n-th root of unity for some n in S.
|
IsCyclotomicExtension.singleton_one
theorem IsCyclotomicExtension.singleton_one :
∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
[h : IsCyclotomicExtension {1} A B], ⊥ = ⊤
This theorem states that, for any two types `A` and `B` with instances of `CommRing A`, `CommRing B`, `Algebra A B`, and `IsCyclotomicExtension {1} A B`, the image of `A` in `B` is equal to `B`. In mathematical terms, if `A` and `B` are commutative rings and `B` is an algebra over `A`, and if `B` is a cyclotomic extension of `A` generated by the first cyclotomic polynomial, then `B` is a field extension of `A`, that is, every element of `B` is an algebraic element over `A`. Here, ⊥ represents the image of `A` in `B`, and ⊤ represents `B`.
More concisely: If `A` and `B` are commutative rings, `B` is an algebra over `A`, `B` is a cyclotomic extension of `A`, then the image of `A` in `B` is equal to `B`. In other words, every element of `B` is an algebraic element over `A`.
|
IsCyclotomicExtension.union_right
theorem IsCyclotomicExtension.union_right :
∀ (S T : Set ℕ+) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
[h : IsCyclotomicExtension (S ∪ T) A B],
IsCyclotomicExtension T (↥(Algebra.adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})) B
This theorem states that if `B` is a cyclotomic extension of `A` determined by roots of unity of orders present in the union of sets `S` and `T`, then `B` can also be described as a cyclotomic extension of the algebra obtained by adjoining `A` with the set of elements `b` from `B` that satisfy the condition: there exists a positive natural number `a` in `S` such that `b` to the power `a` equals `1`. This new cyclotomic extension is given by roots of unity of order in `T`.
More concisely: If `B` is a cyclotomic extension of `A` determined by roots of unity of orders in the union of sets `S` and `T`, then `B` is also the cyclotomic extension of `A` obtained by adjoining elements from `B` whose powers belong to `S`. The new cyclotomic extension is determined by roots of unity of orders in `T`.
|
IsCyclotomicExtension.iff_adjoin_eq_top
theorem IsCyclotomicExtension.iff_adjoin_eq_top :
∀ (S : Set ℕ+) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
IsCyclotomicExtension S A B ↔
(∀ n ∈ S, ∃ r, IsPrimitiveRoot r ↑n) ∧ Algebra.adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1} = ⊤
The theorem `IsCyclotomicExtension.iff_adjoin_eq_top` states the following: For any set `S` of positive integers and any types `A` and `B` that form commutative rings with an algebraic structure, `A` and `B` form a Cyclotomic extension (denoted as `IsCyclotomicExtension S A B`) if and only if two conditions are met. The first condition is that for every element `n` in `S`, there exists a `r` that is a primitive root of `n`. The second condition is that the algebraic closure formed by adjoining all elements `b` to `A` such that there exists an `n` in `S` where `b` to the power of `n` is `1`, equals the top element of the lattice of subalgebras of `A`. Here, the top element of a lattice represents the most inclusive subalgebra, or in other words, the whole algebra.
More concisely: A commutative ring algebra pair (A,B) forms a cyclotomic extension if and only if for every positive integer n in S, there exists a primitive root r of n in A, and the algebraic closure of A adjoining all elements b with b^n = 1 is the top element of the lattice of subalgebras of A.
|
IsCyclotomicExtension.finite
theorem IsCyclotomicExtension.finite :
∀ (S : Set ℕ+) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
[inst_3 : IsDomain B] [h₁ : Finite ↑S] [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
This theorem states that if `S` is a finite set of positive integers and `B` is a cyclotomic extension of `A` with respect to `S`, then `B` is a finite `A`-algebra. Here, `A` and `B` are assumed to be commutative rings, and `B` is assumed to be a domain. Additionally, `B` is an `A`-algebra, which means that there is a ring homomorphism from `A` to the center of `B`. In the context of this theorem, a cyclotomic extension is a type of field extension that is generated by the roots of unity present in the set `S`.
More concisely: If `S` is a finite set of positive integers and `B` is the cyclotomic extension of commutative domain `A` with respect to `S`, then `B` is a finite `A`-algebra.
|
IsCyclotomicExtension.singleton_one_of_bot_eq_top
theorem IsCyclotomicExtension.singleton_one_of_bot_eq_top :
∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
⊥ = ⊤ → IsCyclotomicExtension {1} A B
The theorem `IsCyclotomicExtension.singleton_one_of_bot_eq_top` states that for any types `A` and `B` which are commutative rings with `B` being an algebra over `A`, if the smallest subalgebra of `B` over `A` equals the largest possible subalgebra, then `B` is a cyclotomic extension of `A` with a single root of unity, namely 1. In other words, all elements of `B` can be expressed as a finite sum of 1 raised to different powers, multiplied by elements of `A`.
More concisely: If `A` is a commutative ring and `B` is an algebra over `A` such that the smallest and largest subalgebras of `B` over `A` are equal, then `B` is a cyclotomic extension of `A` generated by 1.
|
IsCyclotomicExtension.iff_union_of_dvd
theorem IsCyclotomicExtension.iff_union_of_dvd :
∀ {n : ℕ+} {S : Set ℕ+} (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
(∀ s ∈ S, n ∣ s) → S.Nonempty → (IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B)
This theorem states that for any positive natural number `n`, any set `S` of positive natural numbers, and any two types `A` and `B` with commutative ring structures and an algebra structure over `A` on `B`, if `n` divides every element of `S` and `S` is not an empty set, then `A` and `B` form a cyclotomic extension with respect to `S` if and only if they form a cyclotomic extension with respect to the union of `S` and the singleton set containing `n`. A cyclotomic extension is a type of algebraic field extension related to the roots of unity, and division here refers to the divisibility relation in the natural numbers.
More concisely: For any positive natural number `n`, set `S` of positive natural numbers, commutative rings `A` and `B` with an algebra structure over `A` on `B`, if `n` divides every element of `S` and `S` is non-empty, then `A` and `B` form a cyclotomic extension with respect to `S` if and only if they form a cyclotomic extension with respect to `S ∪ {n}`.
|
IsCyclotomicExtension.singleton_one_of_algebraMap_bijective
theorem IsCyclotomicExtension.singleton_one_of_algebraMap_bijective :
∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
Function.Surjective ⇑(algebraMap A B) → IsCyclotomicExtension {1} A B
The theorem `IsCyclotomicExtension.singleton_one_of_algebraMap_bijective` states that for any two types `A` and `B` which have `CommRing` and `Algebra` structures, if the function `algebraMap A B` (which is the embedding of `A` into `B` given by the `Algebra` structure) is surjective - that is, for every element of `B` there is an element of `A` which maps to it - then `B` is a cyclotomic extension of `A` at `{1}`. In the context of field theory, this means that all roots of unity (specifically, the roots of unity that generate the group of nth roots of unity for n in `{1}`) which exist in `B` also exist in `A`.
More concisely: If `algebraMap A B` is surjective for commutative rings `A` and `B` with `Algebra` structures, then `B` is a cyclotomic extension of `A` at `{1}`, i.e., all nth roots of unity in `B` belong to `A` for all `n` in `{1}`.
|
IsCyclotomicExtension.iff_singleton
theorem IsCyclotomicExtension.iff_singleton :
∀ (n : ℕ+) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
IsCyclotomicExtension {n} A B ↔ (∃ r, IsPrimitiveRoot r ↑n) ∧ ∀ (x : B), x ∈ Algebra.adjoin A {b | b ^ ↑n = 1}
The theorem `IsCyclotomicExtension.iff_singleton` states that for any positive natural number `n` and any types `A` and `B` that have `CommRing` structures and an `Algebra` structure between them, the extension of `A` to `B` is a cyclotomic extension with a singleton set `{n}` if and only if there exists an `r` that is a primitive root of `n` and every element `x` in `B` belongs to the subalgebra generated by `A` and the set of elements whose `n`-th power equals 1 (`{b | b ^ ↑n = 1}`).
More concisely: For a positive natural number `n`, types `A` and `B` with `CommRing` structures and an `Algebra` structure between them, the extension of `A` to `B` is a cyclotomic extension with a singleton set `{n}` if and only if there exists a primitive root `r` of `n` in `B` such that the subalgebra generated by `A` and the set of `n`-th roots of unity in `B` equals `B`.
|
IsCyclotomicExtension.finiteDimensional
theorem IsCyclotomicExtension.finiteDimensional :
∀ (S : Set ℕ+) (K : Type w) [inst : Field K] (C : Type z) [inst_1 : Finite ↑S] [inst_2 : CommRing C]
[inst_3 : Algebra K C] [inst_4 : IsDomain C] [inst_5 : IsCyclotomicExtension S K C], FiniteDimensional K C
This theorem states that if `S` is a finite set of positive natural numbers and `C` is a cyclotomic extension of a field `K` with respect to `S`, then `C` is a finite-dimensional vector space over `K`. Here, a cyclotomic extension refers to a field extension generated by a cyclotomic polynomial, which is a polynomial whose roots are the `n`th roots of unity for some `n` in `S`. Finite-dimensional means that there exists a finite basis for `C` over `K`.
More concisely: A finite cyclotomic extension of a field is a finite-dimensional vector space over the base field.
|
IsCyclotomicExtension.union_left
theorem IsCyclotomicExtension.union_left :
∀ (S T : Set ℕ+) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
[h : IsCyclotomicExtension T A B],
S ⊆ T → IsCyclotomicExtension S A ↥(Algebra.adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})
The theorem `IsCyclotomicExtension.union_left` states that if `B` is a cyclotomic extension of `A` determined by roots of unity of order in a set `T`, and if there is another set `S` that is a subset of `T`, then the algebra generated by adjoining to `A` the set of elements `b` in `B` for which there exists an element `a` in `S` such that `b` raised to the power of `a` equals 1, is a cyclotomic extension of `A` determined by roots of unity of order in `S`.
In other words, it's about constructing a smaller cyclotomic extension from a given one by considering a subset of the order of roots of unity.
More concisely: If `B` is a cyclotomic extension of `A` determined by roots of unity of order in `T`, and `S` is a subset of `T`, then the subalgebra of `B` generated by elements `b` such that there exists `a` in `S` with `b^a = 1` is a cyclotomic extension of `A` determined by roots of unity of order in `S`.
|
IsCyclotomicExtension.integral
theorem IsCyclotomicExtension.integral :
∀ (S : Set ℕ+) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
[inst_3 : IsDomain B] [inst_4 : IsNoetherianRing A] [inst_5 : Finite ↑S] [inst_6 : IsCyclotomicExtension S A B],
Algebra.IsIntegral A B
This theorem states that for any set `S` of positive natural numbers, and any types `A` and `B` with `A` being a commutative ring, `B` being a commutative ring as well as a domain, and `B` being an algebra over `A`, if `A` is a Noetherian ring, `S` is finite, and `B` is a cyclotomic extension of `A` defined by `S`, then every element of the extension `B` is integral over the base ring `A`. This means that for every element in `B`, there exists a monic polynomial with coefficients in `A` such that the element is a root of the polynomial.
More concisely: If `A` is a Noetherian commutative ring, `B` is a finite cyclotomic extension of `A` as a commutative algebra and domain over `A`, then every element of `B` is integral over `A`.
|
IsCyclotomicExtension.splitting_field_cyclotomic
theorem IsCyclotomicExtension.splitting_field_cyclotomic :
∀ (n : ℕ+) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : IsCyclotomicExtension {n} K L], Polynomial.IsSplittingField K L (Polynomial.cyclotomic (↑n) K)
The theorem `IsCyclotomicExtension.splitting_field_cyclotomic` states that if `L` is a cyclotomic extension of `K` with respect to the set containing only a single element `n`, then `L` is the splitting field of the `n`-th cyclotomic polynomial with coefficients in `K`. In other words, if `L` is a field extension of `K` that contains all the `n`-th roots of unity, then every root of the `n`-th cyclotomic polynomial (which are the `n`-th roots of unity) is in `L`, and the polynomial splits into linear factors over `L`.
More concisely: If `L` is a cyclotomic extension of `K` generated by a single `n`-th root of unity, then `L` is the splitting field of the `n`-th cyclotomic polynomial over `K`.
|