Algebra.exists_idempotent_lift_of_coprime_polynomial_factors
Coprime factors reducing to (X - 1) ^ n and X ^ n construct a lift of a quotient idempotent by evaluating a Bézout identity.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open Polynomial
universe u v
namespace AlgebraLean source · statement
theorem exists_idempotent_lift_of_coprime_polynomial_factors
{R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B]
(I : Ideal R) (b : B)
(hb : IsIdempotentElem (Ideal.Quotient.mk (I.map (algebraMap R B)) b))
(n : ℕ) (hn : 1 ≤ n) (g h : R[X]) (hcoprime : IsCoprime g h)
(hzero : aeval b (g * h) = 0)
(hg : g.map (Ideal.Quotient.mk I) = (X - 1) ^ n)
(hh : h.map (Ideal.Quotient.mk I) = X ^ n) :
∃ e : B, IsIdempotentElem e ∧
Ideal.Quotient.mk (I.map (algebraMap R B)) e =
Ideal.Quotient.mk (I.map (algebraMap R B)) b