Theorems · Theorem · algebraic geometry

isNilpotent_tensor_residueField_iff

∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : Module.Free R A] [inst_4 : Module.Finite R A] (f : A) (I : Ideal R) [inst_5 : I.IsPrime],
  IsNilpotent ((algebraMap A (TensorProduct R A I.ResidueField)) f) ↔
    ∀ i < Module.finrank R A, (LinearMap.charpoly ((Algebra.lmul R A) f)).coeff i ∈ I

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 𝔭.

Defined in

Mathlib.RingTheory.Spectrum.Prime.Polynomial

Cited by

1 results in Mathlib

Foundations

Depth 128 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraModule.FreeModule.FiniteIdeal.IsPrime