IsCyclotomicExtension.discr_prime_pow
theorem IsCyclotomicExtension.discr_prime_pow :
∀ {p : ℕ+} {k : ℕ} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (↑p).Prime] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)),
Irreducible (Polynomial.cyclotomic (↑(p ^ k)) K) →
Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
(-1) ^ ((↑p ^ k).totient / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
The theorem `IsCyclotomicExtension.discr_prime_pow` states that for a given prime number `p` and a positive integer `k`, if `K` is a field and `L` is a cyclotomic extension of `K` of order `p ^ k`, then the discriminant of the power basis given by a primitive root `ζ` of `L` is `(-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))`, provided that the `p^k`-th cyclotomic polynomial over `K` is irreducible. Note that for the cases `p ^ k = 1` and `p ^ k = 2`, the formula takes advantage of the integer division `1 / 2 = 0` and the fact that `0 - 1 = 0`, these cases are only handled this way to have a uniform result. This theorem complements the `IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow` theorem.
More concisely: If `p` is a prime number, `k` is a positive integer, `K` is a field, `L` is a cyclotomic extension of `K` of order `p^k`, and the `p^k`-th cyclotomomic polynomial over `K` is irreducible, then the discriminant of the power basis of `L` in terms of a primitive root `ζ` is `(-1) ^ ((p^k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))`.
|
IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one
theorem IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one :
∀ {n : ℕ+} {K : Type u} [inst : Field K] [inst_1 : CharZero K] {ζ : K} [ce : IsCyclotomicExtension {n} ℚ K]
(hζ : IsPrimitiveRoot ζ ↑n),
Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis =
Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis
The theorem `IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one` states that, for any positive natural number `n`, any type `K` with a field structure and character zero, and any `ζ` of type `K` that is a primitive root of unity and forms a cyclotomic extension with the field of rational numbers, the discriminant of the power basis given by `ζ` is equal to the discriminant of the power basis given by `ζ - 1`. This theorem connects the discriminant, which measures the dependency between the basis elements, of two different power bases related to a primitive root of unity.
More concisely: For any positive natural number `n`, any field `K` with character zero, and any primitive root of unity `ζ` in `K` generating a cyclotomic extension, the discriminant of the power basis of `ζ` is equal to the discriminant of the power basis of `ζ - 1`.
|
IsCyclotomicExtension.discr_odd_prime
theorem IsCyclotomicExtension.discr_odd_prime :
∀ {p : ℕ+} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : IsCyclotomicExtension {p} K L] [hp : Fact (↑p).Prime] (hζ : IsPrimitiveRoot ζ ↑p),
Irreducible (Polynomial.cyclotomic (↑p) K) →
p ≠ 2 → Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
This theorem states that if `p` is an odd prime number and `K` is a cyclotomic extension of `L` with respect to `{p}`, then the discriminant of the power basis given by a primitive root `ζ` of `p` in `K` is equal to `(-1) ^ ((p - 1) / 2) * p ^ (p - 2)`, provided that the `p`-th cyclotomic polynomial over `K` is irreducible and `p` is not equal to `2`. This discriminant is a key invariant that characterizes the structure of the extension field.
More concisely: If `p` is an odd prime number and `K` is a cyclotomic extension of `L` with respect to a primitive root of `p` in `K`, then the discriminant of the power basis is equal to `(-1) ^ ((p - 1) / 2) * p ^ (p - 2)` provided `p`-th cyclotomic polynomial over `K` is irreducible and `p` is not 2.
|
IsCyclotomicExtension.discr_prime_pow_ne_two'
theorem IsCyclotomicExtension.discr_prime_pow_ne_two' :
∀ {p : ℕ+} {k : ℕ} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact (↑p).Prime] (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))),
Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K) →
p ^ (k + 1) ≠ 2 →
Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
(-1) ^ (↑p ^ k * (↑p - 1) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
This theorem states that if `p` is a prime number and there is a cyclotomic extension of order `p^(k+1)` from a field `K` to a field `L`, then the discriminant of the power basis generated by a primitive root `ζ` of this extension is equal to `(-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`, given that the cyclotomic polynomial of order `p^(k+1)` in field `K` is irreducible and `p ^ (k + 1)` is different from 2.
Here, a cyclotomic extension is an extension generated by the roots of a cyclotomic polynomial, which is a polynomial whose roots are the `n`-th roots of unity. A primitive root is an element whose powers generate all the elements of the field extension. The discriminant is a certain attribute of a basis in a field extension, calculated as the determinant of a matrix called the trace matrix, that provides information about the algebraic properties of the field extension.
More concisely: Given a prime number `p` and a cyclotomic extension of order `p^(k+1)` from field `K` to field `L`, the discriminant of the power basis generated by a primitive root of this extension equals `(-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))` if the cyclotomic polynomial of order `p^(k+1)` in field `K` is irreducible and `p ^ (k + 1)` is distinct from 2.
|
IsCyclotomicExtension.discr_prime_pow_ne_two
theorem IsCyclotomicExtension.discr_prime_pow_ne_two :
∀ {p : ℕ+} {k : ℕ} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact (↑p).Prime] (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))),
Irreducible (Polynomial.cyclotomic (↑(p ^ (k + 1))) K) →
p ^ (k + 1) ≠ 2 →
Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
(-1) ^ ((↑p ^ (k + 1)).totient / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
The theorem `IsCyclotomicExtension.discr_prime_pow_ne_two` states that if `p` is a prime number and `L` is a cyclotomic extension of a field `K` where the extension is constructed through the `p` raised to the power of `k + 1`, then the discriminant of the power basis given by a primitive root `ζ` is equal to `(-1)` raised to the power equal to half of the totient of `p` raised to the power of `k + 1`, times `p` raised to the power of `p` raised to the power of `k` times `p - 1` times `k + 1`, minus `1`. This holds under the conditions that the `p` raised to the power of `k + 1`th cyclotomic polynomial is irreducible and `p` raised to the power of `k + 1` is not equal to `2`.
More concisely: If `p` is a prime number, `L` is the cyclotomic extension of degree `p^(k+1)` over a field `K` with a primitive root `ζ`, and `p^(k+1)`th cyclotomatic polynomial is irreducible and `p^(k+1) ≠ 2`, then the discriminant of the power basis given by `ζ` is equal to `(-1)^{(p-1)(k+1)/2} * p^(p^k*(k+1) - 1)`.
|
IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow
theorem IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow :
∀ {p : ℕ+} {k : ℕ} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (↑p).Prime] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)),
Irreducible (Polynomial.cyclotomic (↑(p ^ k)) K) →
∃ u n, Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑↑u * ↑↑p ^ n
The theorem `IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow` states that if `p` is a prime number and we have a cyclotomic extension of degree `p^k` from a field `K` to a field `L`, then there exist a unit integer `u` and a non-negative integer `n` such that the discriminant of the power basis generated by a primitive root `ζ` of the extension is equal to `u * p^n`. This is often a more convenient statement to use than the more general result `IsCyclotomicExtension.discr_prime_pow`, as it avoids the need to directly handle the cyclotomic polynomial. The condition that the `p^k`-th cyclotomic polynomial is irreducible in `K` is necessary for this statement.
More concisely: In a cyclotomic extension of degree $p^k$ over a field $K$, where $p$ is a prime number and the $p^k$-th cyclotomic polynomial is irreducible in $K$, there exist a unit $u$ and a non-negative integer $n$ such that the discriminant of the power basis is equal to $u \cdot p^n$.
|