English
If B.gen is integral and coordinates of x are integral, then for every n, the coordinates of x^n are integral provided minpoly alignment holds.
Русский
Если B.gen интегрирован и координаты x интегральны, то для любого n координаты x^n интегральны при условии согласования минимального многочлена.
LaTeX
$$$\\text{repr\\_pow\\_isIntegral} \\ hB \\ hx \\ hmin \\ n : ∀ i, IsIntegral R (B.basis.repr (x^n) i)$$$
Lean4
/-- 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. -/
theorem toMatrix_isIntegral {B B' : PowerBasis K S} {P : R[X]} (h : aeval B.gen P = B'.gen) (hB : IsIntegral R B.gen)
(hmin : minpoly K B.gen = (minpoly R B.gen).map (algebraMap R K)) :
∀ i j, IsIntegral R (B.basis.toMatrix B'.basis i j) :=
by
intro i j
rw [B.basis.toMatrix_apply, B'.coe_basis]
refine repr_pow_isIntegral hB (fun i => ?_) hmin _ _
rw [← h, aeval_eq_sum_range, map_sum, Finset.sum_apply']
refine IsIntegral.sum _ fun n _ => ?_
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R K S, ← Algebra.smul_def, LinearEquiv.map_smul, algebraMap_smul]
exact (repr_gen_pow_isIntegral hB hmin _ _).smul _
