Nyll.SchemeTheory.RingTheory.CyclicIdempotentAnnihilator

Module documentation

Annihilators for cyclic idempotent factors modulo a Jacobson ideal

Suppose an element of a finite algebra reduces to an idempotent whose factor is generated by that idempotent over the base. A finite generating family beginning with this element makes its multiplication matrix diagonal modulo the ideal, with diagonal entries 1, 0, ..., 0. Nakayama and the determinant trick then give a monic annihilator reducing to (X - 1) * X ^ d, with d ≥ 1.

theorem

exists_monic_annihilator_of_cyclic_quotient_idempotent

L39 ↗

Algebra.exists_monic_annihilator_of_cyclic_quotient_idempotent

Documentation

A quotient idempotent with a cyclic factor has a monic annihilator reducing to (X - 1) * X ^ d for a positive d.

The cyclicity hypothesis says that every element of the quotient factor is a scalar multiple of its unit. Scalars from R suffice because R → R ⧸ I is surjective.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open Polynomial
universe u v
namespace Algebra

Lean source · statement

theorem exists_monic_annihilator_of_cyclic_quotient_idempotent
    {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B]
    [Module.Finite R B] (I : Ideal R) (hI : I ≤ Ideal.jacobson ⊥) (b : B)
    (hb : IsIdempotentElem (Ideal.Quotient.mk (I.map (algebraMap R B)) b))
    (hcyc : ∀ x : B ⧸ I.map (algebraMap R B), ∃ r : R,
      Ideal.Quotient.mk (I.map (algebraMap R B)) b * x =
        r • Ideal.Quotient.mk (I.map (algebraMap R B)) b) :
    ∃ d ≥ 1, ∃ p : R[X], p.Monic ∧ aeval b p = 0 ∧
      p.map (Ideal.Quotient.mk I) = (X - 1) * X ^ d

Module documentation

Annihilators for cyclic idempotent factors modulo a Jacobson ideal

Declarations

exists_monic_annihilator_of_cyclic_quotient_idempotent