English
Given compatible power bases B and B' with a relating polynomial P, if B.gen is integral and minpoly relations hold, then every entry of the matrix B.basis.toMatrix B'.basis is integral.
Русский
Пусть B и B' – базы по степеням, связанные полиномом P; если B.gen интегрирован и выполняются условия минимального многочлена, все элементы матрицы B.basis.toMatrix B'.basis интегральны.
LaTeX
$$$\\forall i,j, \\ IsIntegral R (B.basis.toMatrix B'.basis i j)$$$
Lean4
/-- 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. -/
theorem repr_pow_isIntegral (hB : IsIntegral R B.gen) {x : A} (hx : ∀ i, IsIntegral R (B.basis.repr x i))
(hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) (n : ℕ) :
∀ i, IsIntegral R (B.basis.repr (x ^ n) i) :=
by
nontriviality A using Subsingleton.elim (x ^ n) 0, isIntegral_zero
revert hx
refine
Nat.case_strong_induction_on (p := fun n ↦ _ → ∀ (i : Fin B.dim), IsIntegral R (B.basis.repr (x ^ n) i)) n ?_
fun n hn => ?_
· intro _ i
rw [pow_zero, ← pow_zero B.gen, ← Fin.val_mk B.dim_pos, ← B.basis_eq_pow, B.basis.repr_self_apply]
split_ifs
· exact isIntegral_one
· exact isIntegral_zero
· intro hx
rw [pow_succ]
exact repr_mul_isIntegral hB (fun _ => hn _ le_rfl (fun _ => hx _) _) hx hmin
