Unramified extensions and residue field extensions

• Lifting irreducible residue polynomials over a DVR
• Residue-field functoriality and faithfulness for DVR extensions
• Fullness of the residue-field functor for DVR extensions
• Bijections on residue-field morphisms for local DVR extensions
• Complete-DVR wrappers for the residue-field Hom bijection

TheoremPartial residue-field equivalence for complete finite DVR extensions#✓fully proved

Let \(A\) be a discrete valuation ring, and write \(\kappa(R)\) for the residue field of a local ring \(R\). Let \(B_1\) and \(B_2\) be discrete valuation rings that are finite \(A\)-algebras with local structure maps, complete and separated for their maximal-ideal-adic topologies, such that for \(i = 1, 2\) the field \(\kappa(B_i)\) is separable over \(\kappa(A)\) and \(\operatorname{rank}_A B_i\) equals \(\dim_{\kappa(A)} \kappa(B_i)\). Then the following three statements hold. (i) Sending an \(A\)-algebra homomorphism \(B_1 \to B_2\) to the \(\kappa(A)\)-algebra homomorphism \(\kappa(B_1) \to \kappa(B_2)\) it induces is a bijection. (ii) For every finite separable field extension \(L\) of \(\kappa(A)\) there is a discrete valuation ring \(B\) that is a finite \(A\)-algebra with local structure map and whose residue field \(\kappa(B)\) is isomorphic to \(L\) as a \(\kappa(A)\)-algebra; no unramifiedness of \(B\) is claimed. (iii) Every \(\kappa(A)\)-algebra isomorphism \(e \colon \kappa(B_1) \to \kappa(B_2)\) lifts to an \(A\)-algebra isomorphism \(e' \colon B_1 \to B_2\): the map that \(e'\) induces on residue fields is \(e\), and the map that \(e'^{-1}\) induces is \(e^{-1}\).

DVRResidue.residueField_partial_equivalence_package_of_isAdicComplete · 18 lines

theorem residueField_partial_equivalence_package_of_isAdicComplete
    (hfin₁ : Module.finrank A B₁ =
      Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B₁))
    (hfin₂ : Module.finrank A B₂ =
      Module.finrank (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B₂)) :
    Function.Bijective (residueFieldMapAlgHom (A := A) (B := B₁) (C := B₂)) ∧
    (∀ (L : Type v) [Field L] [Algebra (IsLocalRing.ResidueField A) L]
      [FiniteDimensional (IsLocalRing.ResidueField A) L]
      [Algebra.IsSeparable (IsLocalRing.ResidueField A) L],
      ∃ (B : Type u) (_ : CommRing B) (_ : IsDomain B) (_ : Algebra A B)
        (_ : Module.Finite A B) (_ : IsDiscreteValuationRing B)
        (_ : IsLocalHom (algebraMap A B)),
        Nonempty (IsLocalRing.ResidueField B ≃ₐ[IsLocalRing.ResidueField A] L)) ∧
    (∀ (e : IsLocalRing.ResidueField B₁ ≃ₐ[IsLocalRing.ResidueField A]
        IsLocalRing.ResidueField B₂),
      ∃ e' : B₁ ≃ₐ[A] B₂,
        residueFieldMapAlgHom e'.toAlgHom = e.toAlgHom ∧
        residueFieldMapAlgHom e'.symm.toAlgHom = e.symm.toAlgHom)

Uses 5

Statement usesInduced map on residue fields of DVR extensions

Proof usesLifting residue-field isomorphisms between complete étale DVR extensions · Finite separable residue extensions lift to finite DVR extensions · Algebra maps from an étale DVR extension into a complete one match residue-field maps · Étale criterion for extensions of discrete valuation rings

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.