EtaleFundamentalGroups.exists_completeOrthogonalIdempotents_lift_of_surjective_henselianRing_ker
A finite complete family of orthogonal idempotents lifts along a surjective ring homomorphism whose kernel is a Henselian ideal.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroupsLean source · statement
theorem exists_completeOrthogonalIdempotents_lift_of_surjective_henselianRing_ker
{R S ι : Type*} [CommRing R] [CommRing S] [Fintype ι]
(f : R →+* S) (hf : Function.Surjective f)
[HenselianRing R (RingHom.ker f)]
(e : ι → S) (he : CompleteOrthogonalIdempotents e) :
∃ e' : ι → R, CompleteOrthogonalIdempotents e' ∧ f ∘ e' = e