Theorems · Theorem · commutative algebra

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

Let B : PowerBasis S A be such that IsIntegral R B.gen, and let x : A be an element with integral coordinates in the base B.basis. Then IsIntegral R ((B.basis.repr (x ^ n) i) for all i and all n 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 139 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebraIsScalarTower