Algebra.exists_completeOrthogonalIdempotents_lift_of_isIntegral
A complete orthogonal family in the closed fiber of an integral algebra over a Henselian pair lifts to an actual complete orthogonal family.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Algebra
universe u v wLean source · statement
theorem exists_completeOrthogonalIdempotents_lift_of_isIntegral
{R : Type u} {B : Type v} {ι : Type w}
[CommRing R] [CommRing B] [Algebra R B] [Algebra.IsIntegral R B]
[Fintype ι] (I : Ideal R) [HenselianRing R I]
(e : ι → B ⧸ I.map (algebraMap R B)) (he : CompleteOrthogonalIdempotents e) :
∃ e' : ι → B, CompleteOrthogonalIdempotents e' ∧
∀ i, Ideal.Quotient.mk (I.map (algebraMap R B)) (e' i) = e i