PowerBasis.lift_gen
theorem PowerBasis.lift_gen :
∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
[inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (y : S')
(hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0), (pb.lift y hy) pb.gen = y
The theorem `PowerBasis.lift_gen` states that for any type `S`, which is a ring, any type `A`, which is a commutative ring and an algebra over `A`, any type `S'`, which is also a ring and an algebra over `A`, a power basis `pb` of `A` over `S`, and an element `y` of `S'`, if the polynomial obtained by evaluating the minimal polynomial of the generator of the power basis at `y` is zero (`hy`), then evaluating the generator of the power basis under the lift of `pb` to `y` (given by `PowerBasis.lift pb y hy`) gives back `y`. In simpler terms, this means that if `y` is a root of the minimal polynomial of the generator of the power basis, then the lift of the power basis to `y` sends the generator back to `y`.
More concisely: If `pb` is a power basis of a commutative `A` over a ring `S`, and `y` is a root of the minimal polynomial of the generator of `pb` in a ring `S'`, then `PowerBasis.lift pb y (minimal polynomial of generator at y) = y`.
|
PowerBasis.isIntegral_gen
theorem PowerBasis.isIntegral_gen :
∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] (pb : PowerBasis A S),
IsIntegral A pb.gen
This theorem states that, for any type `S` with a ring structure, type `A` with a commutative ring structure, and an algebra structure over `A` and `S`, given a power basis `pb` of `S` over `A`, the generator `pb.gen` of the power basis is integral over `A`. In other words, this generator is a root of some monic polynomial with coefficients in `A`.
More concisely: For any ring `S` with a commutative ring `A` as an algebra, every generator `pb.gen` of a power basis of `S` over `A` is integral over `A`.
|
linearIndependent_pow
theorem linearIndependent_pow :
∀ {S : Type u_2} [inst : Ring S] {K : Type u_6} [inst_1 : Field K] [inst_2 : Algebra K S] (x : S),
LinearIndependent K fun i => x ^ ↑i
This theorem states that for a given element `x` of a Ring `S` which is an algebra over a Field `K`, the set of powers of `x` less than the degree of `x`'s minimal polynomial are linearly independent over `K`. In other words, no power of `x` can be represented as a linear combination of the other powers of `x`, which is a critical property for showing that `x` generates a power basis.
More concisely: The set of powers of an algebra element `x` over a field `K` in a ring `S`, up to the degree of `x`'s minimal polynomial, is linearly independent over `K`.
|
PowerBasis.finiteDimensional
theorem PowerBasis.finiteDimensional :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S],
PowerBasis R S → Module.Finite R S
The theorem `PowerBasis.finiteDimensional` states that for any types `R` and `S`, where `R` is a commutative ring, `S` is a ring, and an algebra structure over `R` and `S` exists, if a power basis over `R` and `S` is given, then `S` is a finite-dimensional `R`-module. In simpler terms, this theorem says that if we have a power basis for an algebra over a commutative ring, then that algebra is finite-dimensional as a module over the ring.
More concisely: If `R` is a commutative ring, `S` is a ring, `A` is an algebra over `R` and `S`, and `X` is a power basis of `A` over `R` and `S`, then `A` is a finite-dimensional `R`-module.
|
PowerBasis.minpolyGen_eq
theorem PowerBasis.minpolyGen_eq :
∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] (pb : PowerBasis A S),
pb.minpolyGen = minpoly A pb.gen
This theorem states that for any power basis 'pb' of type `PowerBasis A S`, where 'A' is a commutative ring and 'S' is a ring with an algebra structure over 'A', the minimal polynomial of the power basis generator, `pb.gen`, is equal to the result of the function `PowerBasis.minpolyGen` applied to 'pb'. In other words, the minimal polynomial of the power basis generator can be computed as the difference between `Polynomial.X` raised to the power of the dimension of the power basis and the sum (over all elements in the universe) of the product of the coefficient at index 'i' in the representation (under `pb.basis.repr`) of `pb.gen` to the power of the power basis dimension and `Polynomial.X` raised to the power of 'i'.
More concisely: The minimal polynomial of a power basis generator equals the polynomial generated by applying `PowerBasis.minpolyGen` to the power basis.
|
PowerBasis.degree_minpolyGen
theorem PowerBasis.degree_minpolyGen :
∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] [inst_3 : Nontrivial A]
(pb : PowerBasis A S), pb.minpolyGen.degree = ↑pb.dim
The theorem `PowerBasis.degree_minpolyGen` states that for any power basis `pb` over a commutative ring `A` and a ring `S`, where `A` has an algebra structure over `S` and `A` is nontrivial, the degree of the minimal polynomial of the generator of the power basis `pb` is equal to the dimension of the power basis `pb`. In other words, the highest power of `X` that appears in the minimal polynomial of the generator of the power basis is exactly the dimension of the power basis.
More concisely: For any power basis `pb` over a commutative ring `A` with an algebra structure over a nontrivial ring `S`, the degree of the minimal polynomial of `pb`'s generator equals the dimension of `pb`.
|
PowerBasis.equivOfMinpoly.proof_2
theorem PowerBasis.equivOfMinpoly.proof_2 :
∀ {S : Type u_3} [inst : Ring S] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_1}
[inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S'),
minpoly A pb.gen = minpoly A pb'.gen → (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0
This theorem states that for any two power bases `pb` and `pb'` over the same commutative ring `A` and rings `S` and `S'` respectively, if the minimal polynomial of the generator of `pb` is equal to the minimal polynomial of the generator of `pb'`, then the polynomial obtained by evaluating the minimal polynomial of `pb.gen` at `pb'.gen` equals zero. In other words, if two power bases have the same minimal polynomial for their generators, then one generator is a root of the other's minimal polynomial.
More concisely: If power bases `pb` and `pb'` over commutative ring `A` have generators with equal minimal polynomials, then evaluating the minimal polynomial of `pb.gen` at `pb'.gen` yields zero.
|
PowerBasis.equivOfMinpoly.proof_1
theorem PowerBasis.equivOfMinpoly.proof_1 :
∀ {S : Type u_1} [inst : Ring S] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_3}
[inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S'),
minpoly A pb.gen = minpoly A pb'.gen → (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0
The theorem `PowerBasis.equivOfMinpoly.proof_1` states that for any given rings `S` and `S'` with `A` as a common commutative ring and algebra over them, and given two power bases `pb` and `pb'` over `A` on `S` and `S'` respectively, if the minimal polynomial of the generator of `pb` is equal to the minimal polynomial of the generator of `pb'`, then applying the algebra homomorphism that maps a polynomial to an element of the algebra induced by the generator of the power basis `pb` to the minimal polynomial of the generator of `pb'` results in the zero element of the algebra. In other words, the minimal polynomial of the generator of `pb'` is annihilated by the algebra homomorphism induced by the generator of `pb` when these minimal polynomials coincide.
More concisely: If two power bases over a commutative ring have generators with equal minimal polynomials, then the algebra homomorphism induced by one generator annihilates the minimal polynomial of the other generator.
|
PowerBasis.lift_aeval
theorem PowerBasis.lift_aeval :
∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
[inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (y : S')
(hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0) (f : Polynomial A),
(pb.lift y hy) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval y) f
The theorem `PowerBasis.lift_aeval` states that for any given type `S` with a ring structure, type `A` with a commutative ring structure and an algebra structure over `A` and `S`, and any other type `S'` with a ring structure and an algebra structure over `A` and `S'`, given a power basis `pb` of `A` over `S`, and any element `y` of `S'` such that the minimal polynomial of the generator of the power basis `pb` evaluated at `y` is zero, then for any polynomial `f` with coefficients in `A`, the lifting of the power basis `pb` to `S'` evaluated at the polynomial `f` evaluated at the generator of the power basis is equal to the evaluation of the polynomial `f` at `y`.
In other words, the lifting of the power basis `pb` to `S'` respects the evaluation of polynomials in the sense that evaluating a polynomial first and then lifting is the same as lifting first and then evaluating the polynomial.
More concisely: Given a power basis `pb` of a commutative `A` over a ring `S`, and `y` in a ring `S'` with minimal polynomial of `pb`'s generator evaluating to zero at `y`, for all polynomials `f` in `A[X]`, the lifted evaluation of `pb` at `f(pb.gen)` equals the evaluation of `f` at `y`.
|
PowerBasis.finrank
theorem PowerBasis.finrank :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S]
[inst_3 : StrongRankCondition R] (pb : PowerBasis R S), FiniteDimensional.finrank R S = pb.dim
The theorem `PowerBasis.finrank` states that for any commutative ring `R`, any ring `S`, given `S` is an algebra over `R`, and `R` has the strong rank condition, the rank of the module `S` over `R`, defined to be the finite dimension of `S` over `R`, is equal to the dimension of a power basis `pb` of `S` over `R`. The strong rank condition ensures that every increasing chain of left ideals in `R` stabilizes.
More concisely: For a commutative ring `R` with the strong rank condition and an algebra `S` over `R`, the rank of `S` as an `R`-module equals the dimension of a power basis of `S`.
|