Skip to content

Lifting irreducible residue polynomials over a DVR

TheoremMonic lifts of irreducible residue polynomials#✓fully proved

Let \(A\) be a discrete valuation ring with residue field \(k\), and let \(\bar g \in k[X]\) be monic and irreducible. Then there is a monic polynomial \(g \in A[X]\) whose reduction modulo the maximal ideal of \(A\) is \(\bar g\), such that \(A[X]/(g)\) is an integral domain and is finitely generated as an \(A\)-module.

theorem exists_monic_lift_adjoinRoot_domain
    (gbar : (IsLocalRing.ResidueField A)[X]) (hmonic : gbar.Monic)
    (hirr : Irreducible gbar) :
    ∃ (g : A[X]) (_ : g.Monic) (_ : IsDomain (AdjoinRoot g))
      (_ : Module.Finite A (AdjoinRoot g)),
      g.map (IsLocalRing.residue A) = gbar
Used by 1
Used byFinite separable residue extensions lift to finite DVR extensions
12 fully proved

Quotient Equiv

DefinitionReducing \(R(X)/(g)\) modulo the maximal ideal of \(R\)#✓fully proved

Let \(R\) be a local ring with maximal ideal \(\mathfrak m\) and residue field \(k\), let \(g \in R[X]\), and let \(\bar g \in k[X]\) be a polynomial equal to the reduction of \(g\) modulo \(\mathfrak m\). This is the canonical ring isomorphism from the quotient of \(R[X]/(g)\) by the ideal generated by the image of \(\mathfrak m\) onto \(k[X]/(\bar g)\); it sends the class of the image of \(p \in R[X]\) to the class of the reduction \(\bar p \in k[X]\).

noncomputable def adjoinRootQuotientEquivOfMapEq
    (g : R[X]) (gbar : (IsLocalRing.ResidueField R)[X])
    (hmap : g.map (IsLocalRing.residue R) = gbar) :
    AdjoinRoot g ⧸ Ideal.map (AdjoinRoot.of g) (IsLocalRing.maximalIdeal R) ≃+*
      AdjoinRoot gbar := by
  subst gbar
  exact AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot
    (IsLocalRing.maximalIdeal R) g
Used by 2
Used byResidue field of \(A(X)/(g)\) · Residue field of \(A(X)/(g)\) on representatives

Local

TheoremThe extended maximal ideal is maximal for irreducible reduction#✓fully proved

Let \(A\) be a local ring with maximal ideal \(\mathfrak m\) and residue field \(k\), and let \(g \in A[X]\) be a polynomial whose reduction \(\bar g \in k[X]\) modulo \(\mathfrak m\) is irreducible. Then the ideal of \(A[X]/(g)\) generated by the image of \(\mathfrak m\) under the canonical map \(A \to A[X]/(g)\) is maximal.

theorem adjoinRoot_map_maximalIdeal_isMaximal
    (hirr : Irreducible (g.map (IsLocalRing.residue A))) :
    (Ideal.map (algebraMap A (AdjoinRoot g))
      (IsLocalRing.maximalIdeal A)).IsMaximal
Uses 1 · Used by 2
Proof usesResidual irreducible factors give maximal ideals of a monogenic algebra
Used byMonic polynomials with irreducible reduction give local rings · The maximal ideal of \(A(X)/(g)\) is extended from \(A\)

TheoremMonic polynomials with irreducible reduction give local rings#✓fully proved

Let \(A\) be a local ring with residue field \(k\), and let \(g \in A[X]\) be a monic polynomial whose reduction \(\bar g \in k[X]\) modulo the maximal ideal of \(A\) is irreducible. Then \(A[X]/(g)\) is a local ring.

theorem adjoinRoot_isLocalRing_of_monic_of_irreducible_map (hg : g.Monic)
    (hirr : Irreducible (g.map (IsLocalRing.residue A))) :
    IsLocalRing (AdjoinRoot g)
Uses 1 · Used by 1
Proof usesThe extended maximal ideal is maximal for irreducible reduction
Used byFinite separable residue extensions lift to finite DVR extensions

TheoremThe maximal ideal of \(A(X)/(g)\) is extended from \(A\)#✓fully proved

Let \(A\) be a local ring with maximal ideal \(\mathfrak m\) and residue field \(k\), and let \(g \in A[X]\) be a polynomial whose reduction \(\bar g \in k[X]\) modulo \(\mathfrak m\) is irreducible. If \(A[X]/(g)\) is a local ring, then its maximal ideal is the ideal generated by the image of \(\mathfrak m\) under the canonical map \(A \to A[X]/(g)\).

theorem maximalIdeal_adjoinRoot_eq_map [IsLocalRing (AdjoinRoot g)]
    (hirr : Irreducible (g.map (IsLocalRing.residue A))) :
    IsLocalRing.maximalIdeal (AdjoinRoot g) =
      Ideal.map (AdjoinRoot.of g) (IsLocalRing.maximalIdeal A)
Uses 1 · Used by 4
Proof usesThe extended maximal ideal is maximal for irreducible reduction
Used byMonic lifts of irreducible residue polynomials give DVRs · Local base map for polynomials with irreducible reduction · Residue field of \(A(X)/(g)\) · Residue field of \(A(X)/(g)\) on representatives

DefinitionResidue field of \(A(X)/(g)\)#✓fully proved

Let \(A\) be a local ring with residue field \(\kappa(A)\), let \(g \in A[X]\) be such that \(A[X]/(g)\) is a local ring, and let \(\bar g \in \kappa(A)[X]\) be the reduction of \(g\) modulo the maximal ideal of \(A\), assumed irreducible. This is the ring isomorphism from the residue field of \(A[X]/(g)\) onto \(\kappa(A)[X]/(\bar g)\) that sends the residue class of the image of each \(p \in A[X]\) to the class of \(\bar p\), the reduction of the coefficients of \(p\) modulo the maximal ideal of \(A\).

noncomputable def residueFieldEquivAdjoinRootOfMapEq
    [IsLocalRing (AdjoinRoot g)] (gbar : (IsLocalRing.ResidueField A)[X])
    (hirr : Irreducible (g.map (IsLocalRing.residue A)))
    (hmap : g.map (IsLocalRing.residue A) = gbar) :
    IsLocalRing.ResidueField (AdjoinRoot g) ≃+* AdjoinRoot gbar := by
  change (AdjoinRoot g ⧸ IsLocalRing.maximalIdeal (AdjoinRoot g)) ≃+*
    AdjoinRoot gbar
  exact (Ideal.quotEquivOfEq
    (maximalIdeal_adjoinRoot_eq_map (g := g) hirr)).trans
    (adjoinRootQuotientEquivOfMapEq g gbar hmap)
Uses 2 · Used by 2
Statement usesReducing \(R(X)/(g)\) modulo the maximal ideal of \(R\) · The maximal ideal of \(A(X)/(g)\) is extended from \(A\)
Used byThe residue field of \(A(X)/(g)\) as a \(k\)-algebra · Residue field of \(A(X)/(g)\) on representatives

TheoremResidue field of \(A(X)/(g)\) on representatives#✓fully proved

Let \(A\) be a local ring with residue field \(\kappa(A)\), let \(g \in A[X]\) be such that \(A[X]/(g)\) is a local ring, and let \(\bar g \in \kappa(A)[X]\) be the reduction of \(g\) modulo the maximal ideal of \(A\), assumed irreducible. Then for every \(p \in A[X]\), the ring isomorphism from the residue field of \(A[X]/(g)\) onto \(\kappa(A)[X]/(\bar g)\) sends the residue class of the image of \(p\) in \(A[X]/(g)\) to the class of \(\bar p\), the reduction of the coefficients of \(p\) modulo the maximal ideal of \(A\).

@[simp]
theorem residueFieldEquivAdjoinRootOfMapEq_residue_mk
    [IsLocalRing (AdjoinRoot g)] (gbar : (IsLocalRing.ResidueField A)[X])
    (hirr : Irreducible (g.map (IsLocalRing.residue A)))
    (hmap : g.map (IsLocalRing.residue A) = gbar) (p : A[X]) :
    residueFieldEquivAdjoinRootOfMapEq (g := g) gbar hirr hmap
        (IsLocalRing.residue (AdjoinRoot g) (AdjoinRoot.mk g p)) =
      AdjoinRoot.mk gbar (p.map (IsLocalRing.residue A))
Uses 3 · Used by 2
Statement usesResidue field of \(A(X)/(g)\)
Proof usesReducing \(R(X)/(g)\) modulo the maximal ideal of \(R\) · The maximal ideal of \(A(X)/(g)\) is extended from \(A\)
Used byThe residue field of \(A(X)/(g)\) as a \(k\)-algebra · The residue-field algebra isomorphism on polynomial classes

TheoremLocal base map for polynomials with irreducible reduction#✓fully proved

Let \(A\) be a local ring with residue field \(k\), and let \(g \in A[X]\) be a polynomial whose reduction \(\bar g \in k[X]\) modulo the maximal ideal of \(A\) is irreducible. If \(A[X]/(g)\) is a local ring, then the canonical map \(A \to A[X]/(g)\) is a local ring homomorphism: an element of \(A\) whose image in \(A[X]/(g)\) is a unit is itself a unit.

theorem adjoinRoot_isLocalHom_of_irreducible_map [IsLocalRing (AdjoinRoot g)]
    (hirr : Irreducible (g.map (IsLocalRing.residue A))) :
    IsLocalHom (AdjoinRoot.of g)
Uses 1 · Used by 1
Proof usesThe maximal ideal of \(A(X)/(g)\) is extended from \(A\)
Used byFinite separable residue extensions lift to finite DVR extensions

DefinitionThe residue field of \(A(X)/(g)\) as a \(k\)-algebra#✓fully proved

Let \(A\) be a local ring with maximal ideal \(\mathfrak m\) and residue field \(k\), and let \(g \in A[X]\) be a polynomial such that \(A[X]/(g)\) is a local ring, the canonical map \(A \to A[X]/(g)\) is a local homomorphism, and the reduction \(\bar g \in k[X]\) of \(g\) modulo \(\mathfrak m\) is irreducible. This is the isomorphism of \(k\)-algebras from the residue field of \(A[X]/(g)\) (a \(k\)-algebra via \(A \to A[X]/(g)\)) onto \(k[X]/(\bar g)\) that sends the residue class of the image of each \(p \in A[X]\) to the class of its reduction \(\bar p \in k[X]\).

DVRResidue.residueFieldAlgEquivAdjoinRootOfMapEq · 22 lines 
noncomputable def residueFieldAlgEquivAdjoinRootOfMapEq [IsLocalRing (AdjoinRoot g)]
    [IsLocalHom (algebraMap A (AdjoinRoot g))]
    (gbar : (IsLocalRing.ResidueField A)[X])
    (hirr : Irreducible (g.map (IsLocalRing.residue A)))
    (hmap : g.map (IsLocalRing.residue A) = gbar) :
    IsLocalRing.ResidueField (AdjoinRoot g) ≃ₐ[IsLocalRing.ResidueField A]
      AdjoinRoot gbar :=
  AlgEquiv.ofRingEquiv
    (f := residueFieldEquivAdjoinRootOfMapEq (g := g) gbar hirr hmap)
    (fun x => by
      obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective x
      have hmap_res : algebraMap (IsLocalRing.ResidueField A)
          (IsLocalRing.ResidueField (AdjoinRoot g)) (IsLocalRing.residue A a) =
          IsLocalRing.residue (AdjoinRoot g) (algebraMap A (AdjoinRoot g) a) :=
        rfl
      rw [hmap_res, AdjoinRoot.algebraMap_eq,
        AdjoinRoot.algebraMap_eq,
        show AdjoinRoot.of g a = AdjoinRoot.mk g (C a) from rfl,
        show AdjoinRoot.of gbar (IsLocalRing.residue A a) =
          AdjoinRoot.mk gbar (C (IsLocalRing.residue A a)) from rfl,
        residueFieldEquivAdjoinRootOfMapEq_residue_mk,
        Polynomial.map_C])
Uses 2 · Used by 2
Statement usesResidue field of \(A(X)/(g)\) · Residue field of \(A(X)/(g)\) on representatives
Used byFinite separable residue extensions lift to finite DVR extensions · The residue-field algebra isomorphism on polynomial classes

TheoremThe residue-field algebra isomorphism on polynomial classes#✓fully proved

Let \(A\) be a local ring with maximal ideal \(\mathfrak m\) and residue field \(k\), let \(g \in A[X]\) be a polynomial such that \(A[X]/(g)\) is a local ring, the canonical map \(A \to A[X]/(g)\) is a local homomorphism, and the reduction \(\bar g \in k[X]\) of \(g\) modulo \(\mathfrak m\) is irreducible. Then for every \(p \in A[X]\), the canonical \(k\)-algebra isomorphism from the residue field of \(A[X]/(g)\) onto \(k[X]/(\bar g)\) sends the residue class of the image of \(p\) in \(A[X]/(g)\) to the class of the reduction \(\bar p \in k[X]\) of \(p\).

@[simp]
theorem residueFieldAlgEquivAdjoinRootOfMapEq_residue_mk
    [IsLocalRing (AdjoinRoot g)] [IsLocalHom (algebraMap A (AdjoinRoot g))]
    (gbar : (IsLocalRing.ResidueField A)[X])
    (hirr : Irreducible (g.map (IsLocalRing.residue A)))
    (hmap : g.map (IsLocalRing.residue A) = gbar) (p : A[X]) :
    residueFieldAlgEquivAdjoinRootOfMapEq (g := g) gbar hirr hmap
        (IsLocalRing.residue (AdjoinRoot g) (AdjoinRoot.mk g p)) =
      AdjoinRoot.mk gbar (p.map (IsLocalRing.residue A))
Uses 2
Statement usesThe residue field of \(A(X)/(g)\) as a \(k\)-algebra
Proof usesResidue field of \(A(X)/(g)\) on representatives

DVR

TheoremMonic lifts of irreducible residue polynomials give DVRs#✓fully proved

Let \(A\) be a discrete valuation ring with residue field \(k\), and let \(g \in A[X]\) be a monic polynomial whose reduction \(\bar g \in k[X]\) modulo the maximal ideal of \(A\) is irreducible. If \(A[X]/(g)\) is an integral domain and a local ring, then \(A[X]/(g)\) is a discrete valuation ring.

theorem adjoinRoot_isDiscreteValuationRing_of_monic_of_irreducible_map
    (hg : g.Monic)
    (hirr : Irreducible (g.map (IsLocalRing.residue A))) :
    IsDiscreteValuationRing (AdjoinRoot g)
Uses 1 · Used by 1
Proof usesThe maximal ideal of \(A(X)/(g)\) is extended from \(A\)
Used byFinite separable residue extensions lift to finite DVR extensions

Essential Surjectivity

TheoremFinite separable residue extensions lift to finite DVR extensions#✓fully proved

Let \(A\) be a discrete valuation ring with residue field \(k\), and let \(L\) be a finite separable field extension of \(k\). Then there is a discrete valuation ring \(B\) with an \(A\)-algebra structure such that \(B\) is finitely generated as an \(A\)-module and the structure map \(A \to B\) is a local homomorphism, together with an isomorphism of \(k\)-algebras between the residue field of \(B\) (a \(k\)-algebra via \(A \to B\)) and \(L\).

theorem exists_finite_dvr_extension_residueField_algEquiv
    (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)
Sources
  • ATLAS NumberTheoryI N211, Theorem 10.13, essential-surjectivity object-construction stage only (a prerequisite, not the full N211 target): completeness and Henselianity of \(A\) are not assumed, and neither full faithfulness nor the categorical equivalence is proved.
Uses 5 · Used by 1
Proof usesMonic lifts of irreducible residue polynomials give DVRs · Local base map for polynomials with irreducible reduction · Monic polynomials with irreducible reduction give local rings · Monic lifts of irreducible residue polynomials · The residue field of \(A(X)/(g)\) as a \(k\)-algebra
Used byPartial residue-field equivalence for complete finite DVR extensions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.