Fullness of the residue-field functor for DVR extensions

TheoremLifting residue-field images to roots of a minimal polynomial#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with \(B\) a finite étale \(A\)-algebra whose structure map is local, and let \(C\) be a Henselian local ring that is an \(A\)-algebra whose structure map is local. Write \(k_A\), \(k_B\), \(k_C\) for the residue fields. Let \(\beta \in B\) generate \(B\) as an \(A\)-algebra, and let \(\bar\beta \in k_B\) be its residue class. Then for every \(k_A\)-algebra homomorphism \(f : k_B \to k_C\) there is \(\gamma \in C\) that is a root of the minimal polynomial of \(\beta\) over \(A\) and whose residue class in \(k_C\) is \(f(\bar\beta)\).

theorem exists_root_lift_of_adjoin_eq_top
    {beta : B} (hbeta : Algebra.adjoin A {beta} = ⊤)
    (f : IsLocalRing.ResidueField B →ₐ[IsLocalRing.ResidueField A]
      IsLocalRing.ResidueField C) :
    exists gamma : C, Polynomial.aeval gamma (minpoly A beta) = 0 /\
      IsLocalRing.residue C gamma = f (IsLocalRing.residue B beta)

Used by 1

Used byLifting residue-field homomorphisms of finite étale DVR extensions

TheoremLifting residue-field homomorphisms of finite étale DVR extensions#✓fully proved

Let \(A\), \(B\), \(C\) be discrete valuation rings, with \(B\) and \(C\) finite \(A\)-algebras whose structure maps are local, \(B\) étale over \(A\) and \(C\) Henselian. Write \(k_A\), \(k_B\), \(k_C\) for the residue fields. Then every \(k_A\)-algebra homomorphism \(k_B \to k_C\) is induced by an \(A\)-algebra homomorphism: the map sending an \(A\)-algebra homomorphism \(\varphi : B \to C\) to the induced homomorphism of residue fields \(k_B \to k_C\), \(\bar b \mapsto \overline{\varphi(b)}\), is surjective.

theorem residueFieldMapAlgHom_surjective :
    Function.Surjective
      (residueFieldMapAlgHom (A := A) (B := B) (C := C))

Uses 3 · Used by 2

Statement usesInduced map on residue fields of DVR extensions

Proof usesAlgebra maps from a DVR into a finite local DVR extension are local · Lifting residue-field images to roots of a minimal polynomial

Used byLifting residue-field isomorphisms between Henselian étale DVR extensions · Algebra maps from an étale DVR extension into a Henselian one match residue-field maps

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.