Skip to content

Residue-field functoriality and faithfulness for DVR extensions

3 fully proved

Algebra maps

TheoremAlgebra maps from a DVR into a finite local DVR extension are local#✓fully proved

Let \(A\), \(B\), \(C\) be discrete valuation rings, with \(B\) and \(C\) algebras over \(A\), where \(C\) is finite as an \(A\)-module and the structure map \(A \to C\) is a local homomorphism. Then every \(A\)-algebra homomorphism \(B \to C\) is a local homomorphism.

theorem isLocalHom_of_isDiscreteValuationRing (f : B →ₐ[A] C) :
    IsLocalHom f
Used by 4
Used byLifting residue-field isomorphisms between Henselian étale DVR extensions · Lifting residue-field homomorphisms of finite étale DVR extensions · Induced map on residue fields of DVR extensions · Residue-field maps determine algebra maps out of a formally unramified DVR extension

Residue fields of DVR extensions

DefinitionInduced map on residue fields of DVR extensions#✓fully proved

Let \(A\), \(B\), \(C\) be discrete valuation rings, with \(B\) and \(C\) algebras over \(A\) whose structure maps are local homomorphisms, where \(C\) is finite as an \(A\)-module. Write \(\kappa(R)\) for the residue field of a local ring \(R\). An \(A\)-algebra homomorphism \(f \colon B \to C\) induces the \(\kappa(A)\)-algebra homomorphism \(\kappa(B) \to \kappa(C)\) that sends the residue class of \(b \in B\) to the residue class of \(f(b)\).

noncomputable def residueFieldMapAlgHom (f : B →ₐ[A] C) :
    IsLocalRing.ResidueField B →ₐ[IsLocalRing.ResidueField A]
      IsLocalRing.ResidueField C :=
  haveI := AlgHom.isLocalHom_of_isDiscreteValuationRing f
  IsLocalRing.ResidueField.mapAlgHom' f
Uses 1 · Used by 7
Statement usesAlgebra maps from a DVR into a finite local DVR extension are local
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 · Lifting residue-field isomorphisms between complete étale DVR extensions · Algebra maps from an étale DVR extension into a complete one match residue-field maps · Lifting residue-field homomorphisms of finite étale DVR extensions · Residue-field maps determine algebra maps out of a formally unramified DVR extension · Partial residue-field equivalence for complete finite DVR extensions

TheoremResidue-field maps determine algebra maps out of a formally unramified DVR extension#✓fully proved

Let \(A\), \(B\), \(C\) be discrete valuation rings, with \(B\) and \(C\) algebras over \(A\) whose structure maps are local homomorphisms, where \(C\) is finite as an \(A\)-module and \(B\) is formally unramified over \(A\). Write \(\kappa(R)\) for the residue field of a local ring \(R\). Then two \(A\)-algebra homomorphisms \(B \to C\) that induce the same \(\kappa(A)\)-algebra homomorphism \(\kappa(B) \to \kappa(C)\) are equal.

theorem residueFieldMapAlgHom_injective
    [Algebra.FormallyUnramified A B] :
    Function.Injective
      (residueFieldMapAlgHom (A := A) (B := B) (C := C))
Uses 2 · 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
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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.