PowerBasis.repr_pow_isIntegral
theorem PowerBasis.repr_pow_isIntegral :
∀ {S : Type u_2} [inst : CommRing S] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Algebra R S] {A : Type u_4}
[inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A]
{B : PowerBasis S A},
IsIntegral R B.gen →
∀ [inst_7 : IsDomain S] {x : A},
(∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) →
minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen) →
∀ (n : ℕ) (i : Fin B.dim), IsIntegral R ((B.basis.repr (x ^ n)) i)
This theorem states that if there is a power basis `B` for an algebra `A` over a commutative ring `S`, and if the generator of this power basis is integral over another commutative ring `R`, then for any element `x` in `A` with integral coordinates in the basis `B.basis`, the image of each power of `x` under the linear map `B.basis.repr` is also integral over `R` for all bases and all natural powers `n`. This is assuming that the minimal polynomial of the generator of `B` over `S` equals the minimal polynomial of the generator over `R` mapped to `S` using the algebra map from `R` to `S`. The theorem further specifies that this is the case when `R` is a GCD domain and `S` is its fraction ring.
More concisely: If `A` is an algebra over commutative rings `S` and `R`, `B` is a power basis for `A` over `S` with generator integral over `R`, and `R` is a GCD domain and the minimal polynomial of `B.generator` over `S` equals its minimal polynomial over `R` mapped to `S`, then for all `x` in `A` with integral coordinates in `B.basis` and all natural numbers `n`, the image of `x^n` under `B.basis.repr` is integral over `R`.
|
PowerBasis.repr_gen_pow_isIntegral
theorem PowerBasis.repr_gen_pow_isIntegral :
∀ {S : Type u_2} [inst : CommRing S] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Algebra R S] {A : Type u_4}
[inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A]
{B : PowerBasis S A},
IsIntegral R B.gen →
∀ [inst_7 : IsDomain S],
minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen) →
∀ (n : ℕ) (i : Fin B.dim), IsIntegral R ((B.basis.repr (B.gen ^ n)) i)
This theorem states that given a power basis `B` of an algebra `A` over a commutative ring `S`, if the generator of `B` is integral over another commutative ring `R`, then for all natural numbers `n` and for all `i` in the dimension of `B`, the `i`-th component of the representation of `B.gen^n` in the basis `B.basis` is also integral over `R`. This is true if the minimal polynomial of `B.gen` over `S` is the map of the minimal polynomial of `B.gen` over `R` through the algebra map from `R` to `S`. This is the case when `R` is a GCD domain (Greatest Common Divisor domain) and `S` is the fraction ring of `R`.
More concisely: If `B` is a power basis of algebra `A` over commutative ring `S`, `B.gen` is integral over commutative ring `R`, and the minimal polynomial of `B.gen` over `S` is the image of its minimal polynomial over `R` via the algebra map from `R` to `S`, then for all natural numbers `n` and all `i`, the `i`-th component of `B.gen^n` in the basis `B.basis` is integral over `R`.
|
PowerBasis.toMatrix_isIntegral
theorem PowerBasis.toMatrix_isIntegral :
∀ {K : Type u_1} {S : Type u_2} [inst : Field K] [inst_1 : CommRing S] [inst_2 : Algebra K S] {R : Type u_3}
[inst_3 : CommRing R] [inst_4 : Algebra R S] [inst_5 : Algebra R K] [inst_6 : IsScalarTower R K S]
{B B' : PowerBasis K S} {P : Polynomial R},
(Polynomial.aeval B.gen) P = B'.gen →
IsIntegral R B.gen →
minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen) →
∀ (i : Fin B.dim) (j : Fin B'.dim), IsIntegral R (B.basis.toMatrix (⇑B'.basis) i j)
This theorem states that given two power bases `B` and `B'` over a field `K` and a commutative ring `R` such that the generator of `B` is integral over `R`, and a polynomial `P` with coefficients in `R` such that applying `P` to the generator of `B` gives the generator of `B'`, then every element of the matrix formed by taking the basis of `B` to the basis of `B'` is integral over `R`, if the minimal polynomial of the generator of `B` over `K` is equal to the image of the minimal polynomial of the generator of `B` over `R` under the algebraic map from `R` to the field `K`. This condition on the minimal polynomials is satisfied when `R` is a greatest common divisor (GCD) domain and `K` is the fraction ring of `R`.
More concisely: If `B` and `B'` are power bases over a field `K` with integral generators, `R` is a commutative ring, `P` maps the generator of `B` to that of `B'`, and the minimal polynomial of the generator of `B` over `R` equals its image under the algebraic map from `R` to `K`, then every entry in the matrix transforming `B` to `B'` is integral over `R`. (This holds when `R` is a GCD domain and `K` is the fraction ring of `R`. )
|
PowerBasis.repr_mul_isIntegral
theorem PowerBasis.repr_mul_isIntegral :
∀ {S : Type u_2} [inst : CommRing S] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Algebra R S] {A : Type u_4}
[inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A]
{B : PowerBasis S A},
IsIntegral R B.gen →
∀ [inst_7 : IsDomain S] {x y : A},
(∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) →
(∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)) →
minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen) →
∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x * y)) i)
This theorem is about integrality in an algebraic setting. It states that, given a power basis `B` of `A` over `S` such that the generator `B.gen` is integral over `R`, and two elements `x` and `y` of `A` that have integral coordinates in the base `B.basis`, then the representation of the product `x * y` in the basis `B` is also integral over `R` for each coordinate. This claim holds if the minimal polynomial of `B.gen` over `S` is the image of the minimal polynomial of `B.gen` over `R` under the map induced by the algebra structure from `R` to `S`. This is typically the case when `R` is a GCD domain and `S` is its field of fractions.
More concisely: Given a power basis `B` over `S` with integral generator `B.gen` over `R`, and elements `x` and `y` of `A` with integral coordinates in `B.basis`, if the minimal polynomial of `B.gen` over `S` is the image of its minimal polynomial over `R` under the algebra structure map, then the product `x * y` has integral coordinates in `B.basis` over `R`.
|