Algebra.IsAlgebraic.perfectField
theorem Algebra.IsAlgebraic.perfectField :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : PerfectField K], Algebra.IsAlgebraic K L → PerfectField L
The theorem `Algebra.IsAlgebraic.perfectField` states that for any two types `K` and `L`, if `K` is a field, `L` is a field, `K` is a perfect field, and `L / K` is an algebraic extension (meaning all elements of `L` are algebraic over `K`), then `L` must also be a perfect field. In simpler terms, if a field `K` is perfect and we create an algebraic extension to get a new field `L`, then `L` must also be perfect.
More concisely: If `K` is a perfect field and `L` is a purely algebraic extension of `K`, then `L` is also a perfect field.
|
PerfectField.separable_of_irreducible
theorem PerfectField.separable_of_irreducible :
∀ {K : Type u_1} [inst : Field K] [self : PerfectField K] {f : Polynomial K}, Irreducible f → f.Separable := by
sorry
This theorem states that in a perfect field, any irreducible polynomial is separable. Here, a field K is deemed perfect if either its characteristic is 0, or every element of the field is a p-th power for some prime number p that is equal to the characteristic of the field. An irreducible polynomial is one that cannot be factored into polynomials of lesser degree. A polynomial is called separable if it has no repeated roots. So, in essence, the theorem is saying that in a perfect field, if a polynomial cannot be factored, then it does not have any repeated roots.
More concisely: In a perfect field, every irreducible polynomial is separable.
|
bijective_frobenius
theorem bijective_frobenius :
∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
Function.Bijective ⇑(frobenius R p)
This theorem states that for any commutative semiring `R` of a certain type, and any natural number `p`, given that the exponential characteristic of `R` is `p` and `R` is a perfect ring, the Frobenius map, which sends each element `x` of `R` to `x^p`, is a bijective function. In other words, the Frobenius map is both injective (no two different elements in `R` will be mapped to the same element in `R`) and surjective (for each element in `R`, there is an element in `R` that maps to it).
More concisely: Given a commutative semiring of characteristic `p` and being a perfect ring, the Frobenius map is a bijective function.
|
frobenius_apply_frobeniusEquiv_symm
theorem frobenius_apply_frobeniusEquiv_symm :
∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
(frobenius R p) ((frobeniusEquiv R p).symm x) = x
The theorem `frobenius_apply_frobeniusEquiv_symm` states that for any type `R`, any natural number `p`, and any element `x` of `R`, if `R` is a commutative semiring with characteristic exponent `p` and is a perfect ring, then applying the Frobenius map (which sends `x` to `x^p`) to the inverse of the Frobenius automorphism mapped to `x`, we get back `x` itself. In other words, the Frobenius map and the inverse of the Frobenius automorphism are inverse operations to each other in the sense that their composition is the identity on `R`.
More concisely: For any commutative semiring R with characteristic exponent p and perfect ring structure, the Frobenius map and the inverse of the Frobenius automorphism are inverse operations, i.e., applying the Frobenius map to the inverse of the Frobenius automorphism of an element x returns x itself.
|
PerfectRing.toPerfectField
theorem PerfectRing.toPerfectField :
∀ (K : Type u_1) (p : ℕ) [inst : Field K] [inst_1 : ExpChar K p] [inst_2 : PerfectRing K p], PerfectField K := by
sorry
This theorem states that for any type `K`, natural number `p`, and given `K` is a field with exponential characteristic `p` and is a perfect ring, `K` is also a perfect field. More intuitively, this theorem establishes that any perfect ring that is also a field (with a specific exponential characteristic) is necessarily a perfect field.
More concisely: If a field `K` of exponential characteristic `p` is a perfect ring, then `K` is a perfect field.
|
PerfectRing.ofSurjective
theorem PerfectRing.ofSurjective :
∀ (R : Type u_2) (p : ℕ) [inst : CommRing R] [inst_1 : ExpChar R p] [inst_2 : IsReduced R],
Function.Surjective ⇑(frobenius R p) → PerfectRing R p
The theorem named `PerfectRing.ofSurjective` states that for any type `R` (representing a commutative ring) with a fixed natural number `p` (representing the exponential characteristic of the ring), if `R` is a reduced ring and the Frobenius map (which sends an element `x` to `x^p`) is surjective (i.e., for each element in the ring, there exists another element such that the Frobenius map applied to the second element gives the first), then `R` is a perfect ring with respect to `p`. In other words, the surjectivity of the Frobenius map is sufficient for a reduced ring to be a perfect ring.
More concisely: If `R` is a reduced commutative ring of characteristic `p` where the Frobenius map is surjective, then `R` is a perfect ring with respect to `p`.
|
PerfectRing.bijective_frobenius
theorem PerfectRing.bijective_frobenius :
∀ {R : Type u_1} {p : ℕ} [inst : CommSemiring R] [inst_1 : ExpChar R p] [self : PerfectRing R p],
Function.Bijective ⇑(frobenius R p)
The theorem `PerfectRing.bijective_frobenius` states that for any type `R` that is a commutative semiring and has an exponential characteristic `p`, if `R` is a perfect ring, then the function `frobenius R p`, which maps any element in `R` to its `p`th power, is a bijective function. In other words, each element in `R` is uniquely associated with its `p`th power in the ring, and every `p`th power corresponds to some unique element in the ring.
More concisely: In a commutative semiring `R` of characteristic `p`, if `R` is perfect, then the `p`th power function `frobenius R p` is a bijective mapping on `R`.
|
Algebra.IsAlgebraic.isSeparable_of_perfectField
theorem Algebra.IsAlgebraic.isSeparable_of_perfectField :
∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : PerfectField K], Algebra.IsAlgebraic K L → IsSeparable K L
The theorem states that if `L / K` is an algebraic extension and `K` is a perfect field, then the field extension `L / K` is separable. In other words, for any pair of types `K` and `L` where `K` is a Field, `L` is a Field, and there is an algebra from `K` to `L`, if `K` is a perfect field and every element of `L` is algebraic over `K`, then every element of `L` is separable over `K`. A field is 'perfect' if all its elements are roots of some polynomial with coefficients in the field. An element is 'algebraic' over a field if it is a root of some non-zero polynomial with coefficients in that field. A field extension is 'separable' if every element of the extension field is a root of a separable polynomial with coefficients in the base field. A polynomial is 'separable' if it has no repeated roots.
More concisely: If `L` is an algebraic extension of the perfect field `K`, then `L/K` is a separable extension.
|
Polynomial.roots_expand_pow
theorem Polynomial.roots_expand_pow :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {p n : ℕ} [inst_2 : ExpChar R p] {f : Polynomial R}
[inst_3 : PerfectRing R p],
((Polynomial.expand R (p ^ n)) f).roots = p ^ n • Multiset.map (⇑(iterateFrobeniusEquiv R p n).symm) f.roots
This theorem states that for any commutative ring `R` that is a domain and has characteristic `p`, and for any polynomial `f` in `R` and natural numbers `p` and `n`, given `R` is a perfect ring with characteristic `p`, the roots of the expanded polynomial `f` by a factor of `p^n` are obtained by mapping the roots of `f` through the inverse of the `n`-times iterated Frobenius automorphism and multiplying it by `p^n`. The Frobenius automorphism is an endomorphism that raises elements to the `p`-th power, and its iteration is an automorphism that raises elements to the `p^n`-th power. This theorem relates the roots of a polynomial and its expanded version in the context of perfect rings.
More concisely: In a perfect commutative domain `R` of characteristic `p`, the n-th expanded root of a polynomial `f(x)` is given by the n-th iterate of the Frobenius automorphism followed by multiplication by `p^n`.
|