English
If B is a power basis with B.gen integral, and x,y have integral coordinates in B.basis, and the minimal polynomials align via base change, then the basis coordinates of x y are all integral.
Русский
Если B – база по степеням с интегральной геной, и x,y имеют интегральные координаты в B.basis при переходе баз, и minpoly совпадает, то координаты xy по базису также интегральны.
LaTeX
$$$\\text{repr\_mul\_isIntegral} \\ hB \\ hx \\ hy \\ hmin : ∀ i, IsIntegral R (B.basis.repr (x \\cdot y) i)$$$
Lean4
/-- 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. -/
theorem repr_mul_isIntegral (hB : IsIntegral R B.gen) {x y : A} (hx : ∀ i, IsIntegral R (B.basis.repr x i))
(hy : ∀ i, IsIntegral R (B.basis.repr y i)) (hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) :
∀ i, IsIntegral R (B.basis.repr (x * y) i) := by
intro i
rw [← B.basis.sum_repr x, ← B.basis.sum_repr y, Finset.sum_mul_sum, ← Finset.sum_product', map_sum, Finset.sum_apply']
refine IsIntegral.sum _ fun I _ => ?_
simp only [Algebra.smul_mul_assoc, Algebra.mul_smul_comm, LinearEquiv.map_smulₛₗ, RingHom.id_apply, Finsupp.coe_smul,
Pi.smul_apply, id.smul_eq_mul]
refine (hy _).mul ((hx _).mul ?_)
simp only [coe_basis, ← pow_add]
exact repr_gen_pow_isIntegral hB hmin _ _
