theorem
L25 ↗exists_etale_lift
ValuationTheory.Henselian.exists_etale_lift
A residue point of an etale algebra over a Henselian local pair lifts to an actual point over the base ring.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.Henselian
variable {R S : Type*} [CommRing R] [CommRing S] [Algebra R S]
{I : Ideal R} [I.IsMaximal] [HenselianRing R I] [Algebra.Etale R S]Lean source · statement
theorem exists_etale_lift (σ : S →ₐ[R] R ⧸ I) :
∃ τ : S →ₐ[R] R, (Ideal.Quotient.mkₐ R I).comp τ = σ