Complete-DVR wrappers for the residue-field Hom bijection

TheoremAlgebra maps from an étale DVR extension into a complete 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\) complete and separated for its maximal-ideal-adic topology. 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_of_isAdicComplete
    [Algebra.Etale A B]
    [IsAdicComplete (IsLocalRing.maximalIdeal C) 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 usesAlgebra maps from an étale DVR extension into a Henselian one match residue-field maps · Complete local rings are Henselian

Used byPartial residue-field equivalence for complete finite DVR extensions

TheoremLifting residue-field isomorphisms between complete é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 complete and separated for their maximal-ideal-adic topologies. 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_of_isAdicComplete
    [Algebra.Etale A B] [Algebra.Etale A C]
    [IsAdicComplete (IsLocalRing.maximalIdeal B) B]
    [IsAdicComplete (IsLocalRing.maximalIdeal C) 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 3 · Used by 1

Statement usesInduced map on residue fields of DVR extensions

Proof usesLifting residue-field isomorphisms between Henselian étale DVR extensions · Complete local rings are Henselian

Used byPartial residue-field equivalence for complete finite DVR extensions

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.