Theorems · Theorem · commutative algebra

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] [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)

Let B B' : PowerBasis K S be such that IsIntegral R B.gen, and let P : R[X] be such that aeval B.gen P = B'.gen. Then IsIntegral R (B.basis.to_matrix B'.basis i j) for all i and j if minpoly K B.gen = (minpoly R B.gen).map (algebraMap R L). This is the case if R is a GCD domain and K is its fraction ring.

Defined in

Mathlib.RingTheory.Adjoin.PowerBasis

Cited by

1 results in Mathlib

Foundations

Depth 140 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldCommRingAlgebraCommRingAlgebraAlgebraIsScalarTower