A nil ideal with a nonnilpotent two-by-two matrix

A fixed vector for a₀ + t a₁ + t² a₂ yields a companion matrix with a nonzero eigenvalue after inverting 1 - a₀. Squaring puts every entry in the nil ideal. No matrix-nilness principle is used.

def KoetheCounterexample.ShiftWitness.matrixAction {K : Type u} [Field K] {M : Type v} [AddCommGroup M] [Module K M] {R : Type w} [Ring R] (φ : R →+* Module.End K M) : Matrix (Fin 2) (Fin 2) R →+* Module.End K (Fin 2 → M)

The action of a matrix of represented ring elements on two copies of the representation space.

Equations

• KoetheCounterexample.ShiftWitness.matrixAction φ = (endVecRingEquivMatrixEnd (Fin 2) K M).symm.toRingHom.comp φ.mapMatrix

@[simp]

theorem KoetheCounterexample.ShiftWitness.matrixAction_apply {K : Type u} [Field K] {M : Type v} [AddCommGroup M] [Module K M] {R : Type w} [Ring R] (φ : R →+* Module.End K M) (H : Matrix (Fin 2) (Fin 2) R) (z : Fin 2 → M) (i : Fin 2) : ((matrixAction φ) H) z i = ∑ j : Fin 2, (φ (H i j)) (z j)

theorem KoetheCounterexample.ShiftWitness.not_nilpotent_of_eigenvector {K : Type u} [Field K] {M : Type v} [AddCommGroup M] [Module K M] (f : Module.End K M) (t : K) (z : M) (ht : t ≠ 0) (hz : z ≠ 0) (he : f z = t • z) : ¬IsNilpotent f

A nonzero eigenvalue on a nonzero vector excludes nilpotence, without finite-dimensionality assumptions.

theorem KoetheCounterexample.ShiftWitness.nonnil_matrix_of_fixed_vector {K : Type u} [Field K] {M : Type v} [AddCommGroup M] [Module K M] {R : Type w} [Ring R] (I : TwoSidedIdeal R) (hI : ∀ x ∈ I, IsNilpotent x) (φ : R →+* Module.End K M) (a : Fin 3 → R) (ha : ∀ (i : Fin 3), a i ∈ I) (t : K) (ht : t ≠ 0) (z : M) (hz : z ≠ 0) (he : (φ (a 0) + t • φ (a 1) + t ^ 2 • φ (a 2)) z = z) : ∃ W ∈ TwoSidedIdeal.matrix (Fin 2) I, ¬IsNilpotent W

General companion-matrix endpoint. The scalar t lives in the representation field, not necessarily in the ground field of the nil ideal.

def KoetheCounterexample.ShiftWitness.augmentationIdeal {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (A : NonUnitalSubalgebra k B) : TwoSidedIdeal (Unitization k ↥A)

The canonical augmentation ideal in the unitization of a positive algebra.

Equations

• KoetheCounterexample.ShiftWitness.augmentationIdeal A = TwoSidedIdeal.ker (Unitization.fstHom k ↥A)

@[simp]

theorem KoetheCounterexample.ShiftWitness.mem_augmentationIdeal {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (A : NonUnitalSubalgebra k B) (x : Unitization k ↥A) : x ∈ augmentationIdeal A ↔ x.toProd.1 = 0

theorem KoetheCounterexample.ShiftWitness.one_not_mem_of_nil {k : Type u} [Field k] {B : Type v} [Ring B] [Nontrivial B] [Algebra k B] (A : NonUnitalSubalgebra k B) (hA : ∀ x ∈ A, IsNilpotent x) : 1 ∉ A

A nil positive algebra omits the ambient identity.

theorem KoetheCounterexample.ShiftWitness.augmentationIdeal_nil {k : Type u} [Field k] {B : Type v} [Ring B] [Nontrivial B] [Algebra k B] (A : NonUnitalSubalgebra k B) (hA : ∀ x ∈ A, IsNilpotent x) (x : Unitization k ↥A) : x ∈ augmentationIdeal A → IsNilpotent x

The augmentation ideal is nil. We reflect nilpotence along the faithful unitization map instead of treating a nonunital algebra as if it had a unit.

theorem KoetheCounterexample.ShiftWitness.exists_witness_of_nil_subalgebra {k : Type u} [Field k] {B : Type v} [Ring B] [Nontrivial B] [Algebra k B] {K : Type w} [Field K] {M : Type u_1} [AddCommGroup M] [Module K M] (A : NonUnitalSubalgebra k B) (hA : ∀ x ∈ A, IsNilpotent x) (φ : B →+* Module.End K M) (a : Fin 3 → B) (ha : ∀ (i : Fin 3), a i ∈ A) (t : K) (ht : t ≠ 0) (z : M) (hz : z ≠ 0) (he : (φ (a 0) + t • φ (a 1) + t ^ 2 • φ (a 2)) z = z) : ∃ (R : Type (max u v)) (x : Ring R) (I : TwoSidedIdeal R), (∀ x_1 ∈ I, IsNilpotent x_1) ∧ ∃ W ∈ TwoSidedIdeal.matrix (Fin 2) I, ¬IsNilpotent W

A nil nonunital subalgebra with a transcendental-scalar fixed vector gives an actual nil ideal in a unital ring. The ring is its unitization; its action need not be faithful, although nilness is reflected using the faithful natural unitization map into the ambient algebra.