English
For a finite free R-algebra A and prime ideal I ⊆ R, f ∈ A is nilpotent after base change to κ(p) ⊗_R A if and only if every non-leading coefficient of charpoly(lmul_R_A f) lies in I.
Русский
Для конечного свободного R-алгебры A и идеала I ⊆ R, элемент f ∈ Anilpotent после базового изменения до κ(p) ⊗_R A тогда и только тогда, когда каждый коэффициент, кроме ведущего, характеристического полинома лямбда-подмножителя f принадлежит I.
LaTeX
$$$[\\text{Module.Free } R A] [\\text{Module.Finite } R A] \\;\\Rightarrow\\; \\text{IsNilpotent}(\\mathrm{algebraMap}_A(A \\otimes_R I^{\\mathrm{ResidueField}}) f) \\iff\\ \\forall i<\\mathrm{finrank}_R A:\\ (\\mathrm{Algebra.lmul}_{R,A} f).charpoly.coeff\,i \\in I$$
Lean4
/-- If `A` is a finite free `R`-algebra, then `f : A` is nilpotent on `κ(𝔭) ⊗ A` for some
prime `𝔭 ◃ R` if and only if every non-leading coefficient of `charpoly(f)` is in `𝔭`. -/
theorem isNilpotent_tensor_residueField_iff [Module.Free R A] [Module.Finite R A] (f : A) (I : Ideal R) [I.IsPrime] :
IsNilpotent (algebraMap A (A ⊗[R] I.ResidueField) f) ↔
∀ i < Module.finrank R A, (Algebra.lmul R A f).charpoly.coeff i ∈ I :=
by
cases subsingleton_or_nontrivial R
· have := (algebraMap R (A ⊗[R] I.ResidueField)).codomain_trivial
simp [Subsingleton.elim I ⊤, Subsingleton.elim (f ⊗ₜ[R] (1 : I.ResidueField)) 0]
have : Module.finrank I.ResidueField (I.ResidueField ⊗[R] A) = Module.finrank R A := by
rw [Module.finrank_tensorProduct, Module.finrank_self, one_mul]
rw [← IsNilpotent.map_iff (Algebra.TensorProduct.comm R A I.ResidueField).injective]
simp only [Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self, RingHom.id_apply, Algebra.coe_lmul_eq_mul,
Algebra.TensorProduct.comm_tmul]
rw [← IsNilpotent.map_iff (Algebra.lmul_injective (R := I.ResidueField)), LinearMap.isNilpotent_iff_charpoly, ←
Algebra.baseChange_lmul, LinearMap.charpoly_baseChange]
simp_rw [this, ← ((LinearMap.mul R A) f).charpoly_natDegree]
constructor
· intro e i hi
replace e := congr(($e).coeff i)
simpa only [Algebra.coe_lmul_eq_mul, coeff_map, coeff_X_pow, hi.ne, ↓reduceIte, ← RingHom.mem_ker,
Ideal.ker_algebraMap_residueField] using e
· intro H
ext i
obtain (hi | hi) := eq_or_ne i ((LinearMap.mul R A) f).charpoly.natDegree
· simp only [Algebra.coe_lmul_eq_mul, hi, coeff_map, coeff_X_pow, ↓reduceIte]
rw [← Polynomial.leadingCoeff, ((LinearMap.mul R A) f).charpoly_monic, map_one]
obtain (hi | hi) := lt_or_gt_of_ne hi
· simpa [hi.ne, ← RingHom.mem_ker, Ideal.ker_algebraMap_residueField] using H i hi
· simp [hi.ne', coeff_eq_zero_of_natDegree_lt hi]
