Module

IdempotentAnnihilator.lean

Nyll.SchemeTheory.RingTheory.IdempotentAnnihilator

1 declaration indexed from sourceView source ↗

Module documentation

Annihilators of idempotents modulo an ideal

An element of a finite algebra that becomes idempotent modulo an extended ideal admits a monic annihilator reducing to (X - 1) ^ n * X ^ n, with positive n. Splitting a finite generating family into its multiples by b and 1 - b gives a diagonal multiplication action modulo the ideal. No freeness, Jacobson condition, or cyclicity hypothesis is needed.

Imports7

Nyll.SchemeTheory.RingTheory.DeterminantTrickCongruence
Mathlib.Algebra.Algebra.Bilinear
Mathlib.Algebra.Polynomial.Monic
Mathlib.Data.Fintype.BigOperators
Mathlib.RingTheory.Finiteness.Defs
Mathlib.RingTheory.Ideal.Maps
Mathlib.Tactic.Ring

Imported by2

theorem

exists_monic_annihilator_of_quotient_idempotent

L38 ↗

Algebra.exists_monic_annihilator_of_quotient_idempotent

Documentation

An element that is idempotent modulo an extended ideal has a monic annihilator whose reduction is a product of equal positive powers of X - 1 and X.

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_quotient_idempotent
    {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B]
    [Module.Finite R B] (I : Ideal R) (b : B)
    (hb : IsIdempotentElem (Ideal.Quotient.mk (I.map (algebraMap R B)) b)) :
    ∃ n ≥ 1, ∃ p : R[X], p.Monic ∧ aeval b p = 0 ∧
      p.map (Ideal.Quotient.mk I) = (X - 1) ^ n * X ^ n

Module documentation

Annihilators of idempotents modulo an ideal

Declarations

exists_monic_annihilator_of_quotient_idempotent