Maximal ideals in integral extensions of local rings

TheoremKernel of reducing polynomial coefficients modulo an ideal#✓fully proved

Let \(A\) be a commutative ring and \(I\) an ideal of \(A\). The kernel of the ring homomorphism \(A[X] \to (A/I)[X]\) that reduces every coefficient modulo \(I\) is the ideal of \(A[X]\) generated by the constant polynomials \(a\) with \(a \in I\).

theorem comap_mapRingHom_bot_eq_map_C_ker (I : Ideal A) :
    Ideal.comap (Polynomial.mapRingHom (Ideal.Quotient.mk I)) ⊥ =
      Ideal.map Polynomial.C I

Used by 2

Used byMaximal ideals of a monogenic algebra over a local ring come from residual irreducible factors · Residual irreducible factors give maximal ideals of a monogenic algebra

TheoremMaximal ideals of a monogenic algebra over a local ring come from residual irreducible factors#✓fully proved

Maximal ideals of a monogenic algebra over a local ring come from residual irreducible factors. Let \(A\) be a commutative local ring with maximal ideal \(\mathfrak{m}\), and for \(f \in A[X]\) write \(\bar{f}\) for its image in \((A/\mathfrak{m})[X]\). Let \(g \in A[X]\) and suppose that \(A[X]/(g)\) is integral over \(A\). Then for every maximal ideal \(M\) of \(A[X]/(g)\) there is a polynomial \(q \in A[X]\) such that \(\bar{q}\) is irreducible in \((A/\mathfrak{m})[X]\), \(\bar{q}\) divides \(\bar{g}\), and \(M\) is the ideal of \(A[X]/(g)\) generated by the image of \(\mathfrak{m}\) and the class of \(q\).

theorem exists_irreducible_factor_of_is_maximal (g : A[X])
    [Algebra.IsIntegral A (AdjoinRoot g)] (m : Ideal (AdjoinRoot g))
    [hm : m.IsMaximal] :
    ∃ q : A[X],
      Irreducible (q.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) ∧
        (q.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) ∣
          (g.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) ∧
        m = Ideal.map (algebraMap A (AdjoinRoot g))
          (IsLocalRing.maximalIdeal A) ⊔
          Ideal.span {AdjoinRoot.mk g q}

Uses 1 · Used by 1

Proof usesKernel of reducing polynomial coefficients modulo an ideal

Used byMaximal ideals of a monogenic algebra over a local ring

TheoremResidual irreducible factors give maximal ideals of a monogenic algebra#✓fully proved

Let \(A\) be a commutative local ring with maximal ideal \(\mathfrak{m}\), and for \(f \in A[X]\) write \(\bar{f}\) for its image in \((A/\mathfrak{m})[X]\). Let \(g, q \in A[X]\) be such that \(\bar{q}\) is irreducible in \((A/\mathfrak{m})[X]\) and \(\bar{q}\) divides \(\bar{g}\). Then the ideal of \(A[X]/(g)\) generated by the image of \(\mathfrak{m}\) and the class of \(q\) is maximal.

No integrality assumption on \(A[X]/(g)\) over \(A\) is needed.

theorem is_maximal_of_irreducible_factor (g q : A[X])
    (hirr : Irreducible
      (q.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))))
    (hdvd : (q.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) ∣
      (g.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)))) :
    (Ideal.map (algebraMap A (AdjoinRoot g)) (IsLocalRing.maximalIdeal A) ⊔
      Ideal.span {AdjoinRoot.mk g q}).IsMaximal

Uses 1 · Used by 3

Proof usesKernel of reducing polynomial coefficients modulo an ideal

Used byMaximal ideals of a monogenic algebra over a local ring · The adjoined root of an Eisenstein polynomial generates a maximal ideal · The extended maximal ideal is maximal for irreducible reduction

TheoremMaximal ideals of a monogenic algebra over a local ring#✓fully proved

Let \(A\) be a commutative local ring with maximal ideal \(\mathfrak{m}\), and for \(f \in A[X]\) write \(\bar{f}\) for its image in \((A/\mathfrak{m})[X]\). Let \(g \in A[X]\) and suppose that \(A[X]/(g)\) is integral over \(A\). Then an ideal \(M\) of \(A[X]/(g)\) is maximal if and only if there is a polynomial \(q \in A[X]\) such that \(\bar{q}\) is irreducible in \((A/\mathfrak{m})[X]\), \(\bar{q}\) divides \(\bar{g}\), and \(M\) is the ideal of \(A[X]/(g)\) generated by the image of \(\mathfrak{m}\) and the class of \(q\).

theorem is_maximal_iff_irreducible_factor (g : A[X])
    [Algebra.IsIntegral A (AdjoinRoot g)] (m : Ideal (AdjoinRoot g)) :
    m.IsMaximal ↔
      ∃ q : A[X],
        Irreducible
          (q.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) ∧
          (q.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) ∣
            (g.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) ∧
          m = Ideal.map (algebraMap A (AdjoinRoot g))
            (IsLocalRing.maximalIdeal A) ⊔
            Ideal.span {AdjoinRoot.mk g q}

Uses 2 · Used by 1

Proof usesMaximal ideals of a monogenic algebra over a local ring come from residual irreducible factors · Residual irreducible factors give maximal ideals of a monogenic algebra

Used byMaximal ideals of a monogenic algebra over a local ring, monic case

TheoremMaximal ideals of a monogenic algebra over a local ring, monic case#✓fully proved

Let \(A\) be a commutative local ring with maximal ideal \(\mathfrak{m}\), and for \(f \in A[X]\) write \(\bar{f}\) for its image in \((A/\mathfrak{m})[X]\). Let \(g \in A[X]\) be monic. Then an ideal \(M\) of \(A[X]/(g)\) is maximal if and only if there is a polynomial \(q \in A[X]\) such that \(\bar{q}\) is irreducible in \((A/\mathfrak{m})[X]\), \(\bar{q}\) divides \(\bar{g}\), and \(M\) is the ideal of \(A[X]/(g)\) generated by the image of \(\mathfrak{m}\) and the class of \(q\).

theorem is_maximal_iff_irreducible_factor_of_monic (g : A[X]) (hg : g.Monic)
    (m : Ideal (AdjoinRoot g)) :
    m.IsMaximal ↔
      ∃ q : A[X],
        Irreducible
          (q.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) ∧
          (q.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) ∣
            (g.map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A))) ∧
          m = Ideal.map (algebraMap A (AdjoinRoot g))
            (IsLocalRing.maximalIdeal A) ⊔
            Ideal.span {AdjoinRoot.mk g q}

Uses 1

Proof usesMaximal ideals of a monogenic algebra over a local ring

TheoremMaximal ideals of an integral algebra over a local ring contain the base maximal ideal#✓fully proved

Let \(A\) be a commutative local ring with maximal ideal \(\mathfrak{m}\), and let \(B\) be a commutative \(A\)-algebra that is integral over \(A\). Then every maximal ideal \(M\) of \(B\) contains the ideal of \(B\) generated by the image of \(\mathfrak{m}\).

theorem IsMaximal.map_maximalIdeal_le {A B : Type*} [CommRing A] [IsLocalRing A]
    [CommRing B] [Algebra A B] [Algebra.IsIntegral A B]
    {m : Ideal B} (hm : m.IsMaximal) :
    Ideal.map (algebraMap A B) (IsLocalRing.maximalIdeal A) ≤ m

Used by 2

Used byMaximal ideals of an integral monogenic algebra over a local ring contain the base maximal ideal · Maximal ideals of a monogenic algebra over a local ring contain the base maximal ideal, monic case

TheoremMaximal ideals of an integral monogenic algebra over a local ring contain the base maximal ideal#✓fully proved

Maximal ideals of an integral monogenic algebra over a local ring contain the base maximal ideal. Let \(A\) be a commutative local ring with maximal ideal \(\mathfrak{m}\), let \(g \in A[X]\), and suppose that \(A[X]/(g)\) is integral over \(A\). Then every maximal ideal \(M\) of \(A[X]/(g)\) contains the ideal of \(A[X]/(g)\) generated by the image of \(\mathfrak{m}\).

theorem isMaximal_map_maximalIdeal_le {A : Type*} [CommRing A] [IsLocalRing A]
    {g : Polynomial A} [Algebra.IsIntegral A (AdjoinRoot g)]
    {m : Ideal (AdjoinRoot g)} (hm : m.IsMaximal) :
    Ideal.map (algebraMap A (AdjoinRoot g)) (IsLocalRing.maximalIdeal A) ≤ m

Uses 1

Proof usesMaximal ideals of an integral algebra over a local ring contain the base maximal ideal

TheoremMaximal ideals of a monogenic algebra over a local ring contain the base maximal ideal, monic case#✓fully proved

Maximal ideals of a monogenic algebra over a local ring contain the base maximal ideal, monic case. Let \(A\) be a commutative local ring with maximal ideal \(\mathfrak{m}\) and let \(g \in A[X]\) be monic. Then every maximal ideal \(M\) of \(A[X]/(g)\) contains the ideal of \(A[X]/(g)\) generated by the image of \(\mathfrak{m}\).

theorem isMaximal_map_maximalIdeal_le_of_monic {A : Type*} [CommRing A]
    [IsLocalRing A] {g : Polynomial A} (hg : g.Monic)
    {m : Ideal (AdjoinRoot g)} (hm : m.IsMaximal) :
    Ideal.map (algebraMap A (AdjoinRoot g)) (IsLocalRing.maximalIdeal A) ≤ m

Uses 1

Proof usesMaximal ideals of an integral algebra over a local ring contain the base maximal ideal

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.