IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two
theorem IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two :
∀ {p : ℕ+} {k : ℕ} {K : Type u} [inst : Field K] [inst_1 : CharZero K] {ζ : K} [hp : Fact (↑p).Prime]
[inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))),
p ≠ 2 → Prime (hζ.toInteger - 1)
The theorem `IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two` states that if `p` is a prime number not equal to 2 and `ζ` is a primitive `(p ^ (k + 1))`-th root of unity in a field `K` (which has characteristic zero and is a cyclotomic extension of the rationals by `{p ^ (k + 1)}`), then `ζ - 1` is a prime element in the ring of integers of `K`. This is a special case of a more general theorem `zeta_sub_one_prime`.
More concisely: If `p` is a prime number not equal to 2 in a field `K` of characteristic zero that is a cyclotomic extension, then a primitive `(p ^ (k + 1))`-th root of unity `ζ` in `K` implies that `ζ - 1` is a prime element in the ring of integers of `K`.
|
IsCyclotomicExtension.Rat.discr_prime_pow'
theorem IsCyclotomicExtension.Rat.discr_prime_pow' :
∀ {p : ℕ+} {k : ℕ} {K : Type u} [inst : Field K] [inst_1 : CharZero K] {ζ : K} [hp : Fact (↑p).Prime]
[inst_2 : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)),
Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
(-1) ^ ((↑p ^ k).totient / 2) * ↑↑p ^ (↑p ^ (k - 1) * ((↑p - 1) * k - 1))
The theorem `IsCyclotomicExtension.Rat.discr_prime_pow'` is about the discriminant of a certain type of power basis in algebra. Specifically, it says that for a fixed prime number `p` and natural number `k`, with `ζ` being a primitive root of `p^k`, the discriminant of the power basis given by `ζ - 1` is equal to `(-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))`. This holds in any field `K` of characteristic zero and the field of rational numbers `ℚ`. Note that the formula uses `1 / 2 = 0` and `0 - 1 = 0` when `p ^ k = 1` and `p ^ k = 2`, respectively.
More concisely: In characteristic zero fields, the discriminant of the power basis given by a primitive root of prime power `p^k` is equal to `(-1) ^ (p^k.totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))`.
|
IsPrimitiveRoot.zeta_sub_one_prime'
theorem IsPrimitiveRoot.zeta_sub_one_prime' :
∀ {p : ℕ+} {K : Type u} [inst : Field K] [inst_1 : CharZero K] {ζ : K} [hp : Fact (↑p).Prime]
[h : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ ↑p), Prime (hζ.toInteger - 1)
The theorem asserts that if `ζ` is a primitive `p`-th root of unity in a field `K` that is a cyclotomic extension of the rational numbers ℚ, where `p` is a positive integer and `K` has characteristic zero, then `ζ - 1` is a prime element. Here, a prime element is defined in the commutative monoid with zero sense: it is nonzero, not a unit, and if it divides the product of two elements, it must divide at least one of them.
More concisely: In a cyclotomic extension of characteristic zero rational numbers, a primitive p-th root of unity minus one is a prime element.
|
IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow
theorem IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow :
∀ {k : ℕ} {K : Type u} [inst : Field K] [inst_1 : CharZero K] {ζ : K}
[inst_2 : IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(2 ^ (k + 1))),
Prime (hζ.toInteger - 1)
The theorem `IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow` states that if `ζ` is a primitive `2^(k+1)`-th root of unity in a field `K` that is a cyclotomic extension of the rationals `ℚ` with characteristic zero, then `ζ - 1` is a prime element. Here, a prime element in a commutative monoid with zero (such as a field) is an element that is not zero, not a unit, and has the property that if it divides the product of two elements, then it must divide at least one of the factors.
More concisely: In a cyclotomic extension of the rationals with characteristic zero, a primitive root of unity `ζ` of order `2^(k+1)` has `ζ - 1` as a prime element.
|
IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow'
theorem IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow' :
∀ {p : ℕ+} {k : ℕ} {K : Type u} [inst : Field K] [inst_1 : CharZero K] {ζ : K} [hp : Fact (↑p).Prime]
[inst_2 : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ k)),
∃ u n, Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑↑p ^ n
The theorem states that given a prime number `p`, and a cyclotomic extension of order `p ^ k`, there exist an integer unit `u` and a natural number `n` such that the discriminant of the power basis defined by `ζ - 1` is equal to the product of `u` and `p` raised to the power `n`. This is often more convenient to use than the variant `IsCyclotomicExtension.Rat.discr_prime_pow'`. Here, `IsCyclotomicExtension` refers to a type of field extension in which the minimal polynomial of an element is a cyclotomic polynomial, and `IsPrimitiveRoot` refers to an element whose powers generate a cyclic group.
More concisely: Given a prime number `p` and a cyclotomic extension of order `p^k`, there exists a unit `u` and a natural number `n` such that the discriminant of the power basis defined by a primitive root `ζ` of unity is `u * p^n`.
|
IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow
theorem IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow :
∀ {p : ℕ+} {k : ℕ} {K : Type u} [inst : Field K] [inst_1 : CharZero K] {ζ : K} [hp : Fact (↑p).Prime]
[hcycl : IsCyclotomicExtension {p ^ k} ℚ K],
IsPrimitiveRoot ζ ↑(p ^ k) → IsIntegralClosure ↥(Algebra.adjoin ℤ {ζ}) ℤ K
This theorem states that for any prime `p` and natural number `k`, and for any field `K` of characteristic zero, if `K` is a cyclotomic extension of the rational numbers `ℚ` generated by the `p ^ k`-th roots of unity, and `ζ` is one such `p ^ k`-th root of unity, then the smallest subalgebra that contains `ζ` is also the integral closure of the integers `ℤ` in `K`. In other words, every element of this subalgebra is a root of a polynomial with integer coefficients. This shows the important property that such cyclotomic extensions are well-behaved in terms of arithmetic, as they contain no "extra" elements beyond those required by the roots of unity.
More concisely: In a field of characteristic zero, the subalgebra generated by a prime power root of unity is equal to the integral closure of the integers in that field.
|
IsPrimitiveRoot.zeta_sub_one_prime
theorem IsPrimitiveRoot.zeta_sub_one_prime :
∀ {p : ℕ+} {k : ℕ} {K : Type u} [inst : Field K] [inst_1 : CharZero K] {ζ : K} [hp : Fact (↑p).Prime]
[inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))),
Prime (hζ.toInteger - 1)
The theorem `IsPrimitiveRoot.zeta_sub_one_prime` states that for any positive natural number `p`, and any natural number `k`, in a field `K` with zero characteristic, if `ζ` is a primitive `(p ^ (k + 1))`-th root of unity in `K`, and `K` is a cyclotomic extension of the rationals ℚ with respect to `{p ^ (k + 1)}` and `p` is a prime number, then the element `ζ - 1` is a prime element in the field. A prime element in this context is an element that is not zero, not a unit, and if it divides the product of two elements, it must divide at least one of them.
More concisely: If `ζ` is a primitive `(p ^ (k + 1))`-th root of unity in a field `K` of characteristic zero, which is a cyclotomic extension of the rationals with respect to `{p ^ (k + 1)}`, and `p` is a prime number, then `ζ - 1` is a prime element in `K`.
|
IsCyclotomicExtension.Rat.discr_prime_pow_ne_two'
theorem IsCyclotomicExtension.Rat.discr_prime_pow_ne_two' :
∀ {p : ℕ+} {k : ℕ} {K : Type u} [inst : Field K] [inst_1 : CharZero K] {ζ : K} [hp : Fact (↑p).Prime]
[inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))),
p ^ (k + 1) ≠ 2 →
Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
(-1) ^ ((↑p ^ (k + 1)).totient / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))
This theorem proves that for a given `ζ`, which is a primitive root of unity of order `p ^ (k + 1)` in a field `K` of characteristic zero and is part of a cyclotomic extension of the rational numbers `ℚ`, the discriminant of the power basis given by `ζ - 1` equals `(-1) ^ ((p ^ (k + 1)).totient / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`, provided `p ^ (k + 1)` is not equal to 2. Here, `p` is a prime number and `k` is a natural number. The `totient` function is the Euler's totient function which gives the count of integers that are relatively prime to a given integer. In this case, `p ^ (k + 1).totient` gives the count of integers that are relatively prime to `p ^ (k + 1)`.
More concisely: Given a prime number `p` and a natural number `k`, if `ζ` is a primitive root of unity of order `p^(k+1)` in a field `K` of characteristic zero that is part of a cyclotomic extension of the rational numbers `ℚ`, then the discriminant of the power basis given by `ζ - 1` equals `(-1) ^ ((p^(k+1)).totient / 2) * p ^ (p^k * ((p-1) * (k+1) - 1))`. This holds only when `p^(k+1)` is not equal to 2.
|
IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow
theorem IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow :
∀ {p : ℕ+} {k : ℕ} [hp : Fact (↑p).Prime],
IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ)
The theorem `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow` states that for any positive prime number `p` and any natural number `k`, the integral closure of the integers (`ℤ`) in the cyclotomic field of `p` to the power of `k` over the rationals (`ℚ`) is the cyclotomic ring of `p` to the power of `k` over `ℤ` and `ℚ`. In other words, every integer in the cyclotomic field of `p^k` over `ℚ` that is a root of a monic polynomial with coefficients in `ℤ` lies within the cyclotomic ring of `p^k` over `ℤ` and `ℚ`.
More concisely: The integral closure of the integers in the cyclotomic field of a prime power over the rationals equals the cyclotomic ring of that prime power over the integers and rationals.
|