English
Let B be a power basis of S over A, with gen integral over R. If minpoly S B.gen equals the map of minpoly R B.gen, then for every n and i, the i-th coordinate of (B.gen)^n expressed in the basis is integral over R.
Русский
Пусть B — базис мощности S над A, ген B.gen интеграл над R. При условии равенства minpoly_S(B.gen) и map(minpoly_R(B.gen)), для любых n и i i-й координат в представлении B.gen^n в базисе интегральна над R.
LaTeX
$$$\forall n\in\mathbb{N}, \forall i \in \{0,\dots, \dim B-1\},\ IsIntegral_R\big( (B.basis.repr(B.gen^n))_i \big)$$$
Lean4
/-- If `B : PowerBasis S A` is such that `IsIntegral R B.gen`, then
`IsIntegral R (B.basis.repr (B.gen ^ n) 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_gen_pow_isIntegral (hB : IsIntegral R B.gen)
(hmin : minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)) (n : ℕ) :
∀ i, IsIntegral R (B.basis.repr (B.gen ^ n) i) := by
intro i
nontriviality S
let Q := X ^ n %ₘ minpoly R B.gen
have : B.gen ^ n = aeval B.gen Q :=
by
rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly.monic hB)]
simp [Q]
by_cases hQ : Q = 0
· simp [this, hQ, isIntegral_zero]
have hlt : Q.natDegree < B.dim :=
by
rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map, natDegree_lt_natDegree_iff hQ]
letI : Nontrivial R := Nontrivial.of_polynomial_ne hQ
exact degree_modByMonic_lt _ (minpoly.monic hB)
rw [this, aeval_eq_sum_range' hlt]
simp only [map_sum, Finset.sum_apply']
refine IsIntegral.sum _ fun j hj => ?_
replace hj := Finset.mem_range.1 hj
rw [← Fin.val_mk hj, ← B.basis_eq_pow, Algebra.smul_def, IsScalarTower.algebraMap_apply R S A, ← Algebra.smul_def,
LinearEquiv.map_smul]
simp only [algebraMap_smul, Finsupp.coe_smul, Pi.smul_apply, B.basis.repr_self_apply]
by_cases hij : (⟨j, hj⟩ : Fin _) = i
· simp only [hij, if_true]
rw [Algebra.smul_def, mul_one]
exact isIntegral_algebraMap
· simp [hij, isIntegral_zero]
