Bijections on residue-field morphisms for local DVR extensions

TheoremAlgebra maps from an étale DVR extension into a Henselian one match residue-field maps#✓fully proved

Let \(A\), \(B\), \(C\) be discrete valuation rings, with \(B\) and \(C\) finite \(A\)-algebras whose structure maps are local homomorphisms, \(B\) étale over \(A\), and \(C\) a Henselian local ring. Write \(\kappa(R)\) for the residue field of a local ring \(R\). Then sending an \(A\)-algebra homomorphism \(B \to C\) to the \(\kappa(A)\)-algebra homomorphism \(\kappa(B) \to \kappa(C)\) it induces is a bijection.

theorem residueFieldMapAlgHom_bijective
    [Algebra.Etale A B] [HenselianLocalRing C] :
    Function.Bijective
      (residueFieldMapAlgHom (A := A) (B := B) (C := C))

Uses 3 · Used by 1

Statement usesInduced map on residue fields of DVR extensions

Proof usesResidue-field maps determine algebra maps out of a formally unramified DVR extension · Lifting residue-field homomorphisms of finite étale DVR extensions

Used byAlgebra maps from an étale DVR extension into a complete one match residue-field maps

TheoremLifting residue-field isomorphisms between Henselian é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 homomorphisms, both étale over \(A\) and both Henselian local rings. Write \(\kappa(R)\) for the residue field of a local ring \(R\). Then every \(\kappa(A)\)-algebra isomorphism \(e \colon \kappa(B) \to \kappa(C)\) lifts to an \(A\)-algebra isomorphism \(e' \colon B \to C\): the map that \(e'\) induces on residue fields is \(e\), and the map that \(e'^{-1}\) induces is \(e^{-1}\).

theorem exists_algEquiv_lift_residueField
    [Algebra.Etale A B] [Algebra.Etale A C]
    [HenselianLocalRing B] [HenselianLocalRing C]
    (e : IsLocalRing.ResidueField B ≃ₐ[IsLocalRing.ResidueField A]
      IsLocalRing.ResidueField C) :
    ∃ e' : B ≃ₐ[A] C,
      residueFieldMapAlgHom e'.toAlgHom = e.toAlgHom ∧
      residueFieldMapAlgHom e'.symm.toAlgHom = e.symm.toAlgHom

Uses 4 · Used by 1

Statement usesInduced map on residue fields of DVR extensions

Proof usesAlgebra maps from a DVR into a finite local DVR extension are local · Residue-field maps determine algebra maps out of a formally unramified DVR extension · Lifting residue-field homomorphisms of finite étale DVR extensions

Used byLifting residue-field isomorphisms between complete étale DVR extensions

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.