traceForm_dualBasis_powerBasis_eq
theorem traceForm_dualBasis_powerBasis_eq :
∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : FiniteDimensional K L] [inst_4 : IsSeparable K L] (pb : PowerBasis K L) (i : Fin pb.dim),
((Algebra.traceForm K L).dualBasis ⋯ pb.basis) i =
(minpolyDiv K pb.gen).coeff ↑i / (Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen))
The theorem `traceForm_dualBasis_powerBasis_eq` states that for any field `K` and `L` where `L` is a `K`-algebra, and `L` is a finite dimensional and a separable `K`-algebra, given a power basis `pb` over `K` and `L`, and an integer `i` within the dimension of the power basis, the `i`th element of the dual basis of the power basis under the trace form is the `i`th coefficient of the polynomial obtained by dividing the minimal polynomial of the generator of the power basis by `(X - pb.gen)`, divided by the derivative of the minimal polynomial evaluated at the generator of the power basis.
In simpler terms, this theorem describes the relationship between a power basis, its dual basis under the trace form, and the minimal polynomial of the generator. It shows that each element of the dual basis can be computed from the coefficients of a certain polynomial related to the minimal polynomial of the basis generator and the derivative of the minimal polynomial.
More concisely: For any finite dimensional and separable `K`-algebra `L` over a field `K`, the `i`th element of the dual basis of a power basis `pb` under the trace form is equal to the `i`th coefficient of the polynomial obtained by dividing the minimal polynomial of `pb.gen` by `(X - pb.gen)` and then dividing by the derivative of the minimal polynomial evaluated at `pb.gen`.
|
Algebra.trace_algebraMap
theorem Algebra.trace_algebraMap :
∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x : K),
(Algebra.trace K L) ((algebraMap K L) x) = FiniteDimensional.finrank K L • x
The theorem `Algebra.trace_algebraMap` states that if `x` is an element of a base field `K`, then the trace of the algebra map from `K` to a field extension `L` applied to `x` is equal to the scalar multiple of `x` by the rank of `L` as a vector space over `K`. Here, the rank is defined to be `0` if `L` is not finite-dimensional over `K`, and in this case, the trace and rank functions also return `0`. The trace of an element `s` of an `R`-algebra is defined as the trace of `(s * ·)`, interpreted as an `R`-linear map. The algebra map is the embedding from `R` to `A` given by the algebra structure.
More concisely: For any base field extension `L/K`, the trace of an element `x` in `K` under the algebra map is equal to the scalar multiple of `x` by the finite-dimensionality (or rank) of `L` over `K`. If `L` is not finite-dimensional, both the trace and rank are zero.
|
Algebra.trace_algebraMap_of_basis
theorem Algebra.trace_algebraMap_of_basis :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
[inst_3 : Fintype ι], Basis ι R S → ∀ (x : R), (Algebra.trace R S) ((algebraMap R S) x) = Fintype.card ι • x
This theorem states that for every commutative ring `R` and `S`, where `S` is an `R`-algebra and for every finite type `ι` which serves as a basis for `S` over `R`, the trace of an element `x` from `R` (when it's embedded into `S` using the `algebraMap`) is equal to the product of the size of the basis (number of elements in `ι`) and `x`. In other words, if `x` is an element of the base field `R`, then the trace of `x` under this setup is equal to the product of the dimension of `S` over `R` (denoted `[S : R]` and represented as `Fintype.card ι` in the code) and `x`.
More concisely: For every commutative ring `R`, `R-алгебра` `S` with finite basis `ι`, and `x` in `R`, the trace of `x` in `S` equals the product of the cardinality of `ι` and `x`.
|
PowerBasis.trace_gen_eq_nextCoeff_minpoly
theorem PowerBasis.trace_gen_eq_nextCoeff_minpoly :
∀ {S : Type u_2} [inst : CommRing S] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra K S]
[inst_3 : Nontrivial S] (pb : PowerBasis K S), (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff
The theorem `PowerBasis.trace_gen_eq_nextCoeff_minpoly` states that for any power basis `pb` of an algebra `S` over a field `K`, the trace of the generator of the power basis `pb.gen` is the negative of the next coefficient of the minimal polynomial of `pb.gen` over `K`.
Here, the trace of an element in an `R`-algebra is defined as the trace of the `R`-linear map `(s * ·)`, where `·` is a placeholder for multiplication. The minimal polynomial of an element in a field extension is the monic polynomial of smallest degree that has the element as a root. The next coefficient of a polynomial is the coefficient of the second-highest degree term.
More concisely: For any power basis `pb` of an algebra `S` over a field `K`, the trace of `pb.gen` in `S` equals the negative of the coefficient of the second-highest term in the minimal polynomial of `pb.gen` over `K`.
|
PowerBasis.trace_gen_eq_sum_roots
theorem PowerBasis.trace_gen_eq_sum_roots :
∀ {S : Type u_2} [inst : CommRing S] {K : Type u_4} [inst_1 : Field K] {F : Type u_6} [inst_2 : Field F]
[inst_3 : Algebra K S] [inst_4 : Algebra K F] [inst_5 : Nontrivial S] (pb : PowerBasis K S),
Polynomial.Splits (algebraMap K F) (minpoly K pb.gen) →
(algebraMap K F) ((Algebra.trace K S) pb.gen) = ((minpoly K pb.gen).aroots F).sum
This theorem states that for any power basis `pb` of a commutative ring `S` over a field `K`, with another field `F` having algebra structures over `K`, if the minimal polynomial of `pb.gen` over `K` splits over `F`, then the trace of `pb.gen` (when mapped from `K` to `F`) is equal to the sum of the roots of the minimal polynomial of `pb.gen` in `F`. Note that the trace of an element in an algebra is defined as the trace of the linear map multiplying by that element, and a polynomial is said to split if it is zero or all of its irreducible factors have degree 1.
More concisely: For a power basis `pb` of a commutative `K`-algebra `S` over a field `K`, if the minimal polynomial of `pb.gen` over `K` splits in `F` as a product of linear factors, then the trace of `pb.gen` from `K` to `F` equals the sum of its roots in `F`.
|