Theorems · Theorem · commutative algebra

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] [IsScalarTower R S A] {B : PowerBasis S A},
  IsIntegral R B.gen →
    ∀ {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)

Let B : PowerBasis S A be such that IsIntegral R B.gen, and let x y : A be elements with integral coordinates in the base B.basis. Then IsIntegral R ((B.basis.repr (x * y) i) for all i if minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S). This is the case if R is a GCD domain and S is its fraction ring.

Defined in

Mathlib.RingTheory.Adjoin.PowerBasis

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTower