Module

HenselianFiniteIdempotent.lean

Nyll.SchemeTheory.RingTheory.HenselianFiniteIdempotent

1 declaration indexed from sourceView source ↗

Module documentation

Lifting arbitrary quotient idempotents in finite algebras

A doubled generating family gives an annihilator reducing to powers of X - 1 and X. The Henselian factorization theorem lifts these coprime factors, and evaluation of a Bézout identity gives the required idempotent.

Imports6

Nyll.SchemeTheory.RingTheory.HenselianFactorization
Nyll.SchemeTheory.RingTheory.IdempotentAnnihilator
Nyll.SchemeTheory.RingTheory.IdempotentFromCoprimeFactors
Mathlib.Algebra.Polynomial.Monic
Mathlib.RingTheory.Coprime.Lemmas
Mathlib.Tactic.Ring

Imported by2

theorem

exists_idempotent_lift_of_finite

L34 ↗

Algebra.exists_idempotent_lift_of_finite

Documentation

Every quotient idempotent of a finite algebra over a Henselian pair lifts to an idempotent of the original algebra.

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_idempotent_lift_of_finite
    {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B]
    [Module.Finite R B] (I : Ideal R) [HenselianRing R I] (b : B)
    (hb : IsIdempotentElem (Ideal.Quotient.mk (I.map (algebraMap R B)) b)) :
    ∃ e : B, IsIdempotentElem e ∧
      Ideal.Quotient.mk (I.map (algebraMap R B)) e =
        Ideal.Quotient.mk (I.map (algebraMap R B)) b

Module documentation

Lifting arbitrary quotient idempotents in finite algebras

Declarations

exists_idempotent_lift_of_finite