Nyll.SchemeTheory.RingTheory.HenselianIntegralCyclicIdempotent

Module documentation

Cyclic quotient idempotents in integral algebras over a Henselian pair

A finite subalgebra can retain a quotient idempotent and its principal localization. Cyclicity descends through that localization comparison, so the finite-algebra lifting theorem applies. Mapping the resulting idempotent back gives a lift in the original integral algebra.

theorem

exists_idempotent_lift_of_integral_of_cyclic_quotient

L31 ↗

Algebra.exists_idempotent_lift_of_integral_of_cyclic_quotient

Documentation

A cyclic quotient idempotent in an integral algebra lifts whenever its principal localization is of finite type over the base.

Source context 3 commands

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

@[expose] public section
universe u v
namespace Algebra

Lean source · statement

theorem exists_idempotent_lift_of_integral_of_cyclic_quotient
    {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
    [Algebra.IsIntegral R C] (I : Ideal R) [HenselianRing R I] (b : C)
    [Algebra.FiniteType R (Localization.Away b)]
    (hb : IsIdempotentElem (Ideal.Quotient.mk (I.map (algebraMap R C)) b))
    (hcyc : ∀ x : C ⧸ I.map (algebraMap R C), ∃ r : R,
      Ideal.Quotient.mk (I.map (algebraMap R C)) b * x =
        r • Ideal.Quotient.mk (I.map (algebraMap R C)) b) :
    ∃ e : C, IsIdempotentElem e ∧
      Ideal.Quotient.mk (I.map (algebraMap R C)) e =
        Ideal.Quotient.mk (I.map (algebraMap R C)) b

Module documentation

Cyclic quotient idempotents in integral algebras over a Henselian pair

Declarations

exists_idempotent_lift_of_integral_of_cyclic_quotient