CommAlgCat.FiniteEtale.baseChange_isEquivalence_of_henselian
Finite étale algebras over a Henselian pair are equivalent to finite étale algebras over its quotient.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory
universe u
namespace CommAlgCat.FiniteEtaleLean source · full declaration
theorem baseChange_isEquivalence_of_henselian
{R : Type u} [CommRing R] (I : Ideal R) [HenselianRing R I] :
(baseChange R (R ⧸ I) : CommAlgCat.FiniteEtale.{u} R ⥤
CommAlgCat.FiniteEtale.{u} (R ⧸ I)).IsEquivalence where
faithful := baseChange_faithful_of_le_jacobson I (HenselianRing.jac (R := R) (I := I))
full := baseChange_full_of_henselian I
essSurj := {
mem_essImage A := by
obtain ⟨B, hfinite, hetale, ⟨e⟩⟩ :=
Algebra.FiniteEtale.exists_lift_of_quotient_of_henselian (A := A) I
let : Module.Finite R B := hfinite
let : Algebra.Etale R B := hetale
exact ⟨FiniteEtale.of R B, ⟨FiniteEtale.isoMk e⟩⟩
}