Residue maps of singly generated algebras

TheoremSurjectivity of the residue map for a singly generated algebra#✓fully proved

Let \(A\) and \(B\) be commutative rings, \(B\) an \(A\)-algebra, \(\mathfrak q\) an ideal of \(B\) and \(\mathfrak p\) its preimage under \(A \to B\). If \(B\) is generated as an \(A\)-algebra by a single element \(\pi \in \mathfrak q\), then the canonical map \(A/\mathfrak p \to B/\mathfrak q\) is surjective.

Indeed, every element of \(B\) is \(f(\pi)\) for a polynomial \(f\) with coefficients in \(A\), and modulo \(\mathfrak q\) it agrees with the image of the constant coefficient of \(f\), because \(\pi\) maps to zero.

theorem quotient_algebraMap_surjective_of_adjoin_singleton_eq_top
    (q : Ideal B) (π : B) (hπ : π ∈ q)
    (hgen : Algebra.adjoin A {π} = ⊤) :
    Function.Surjective (algebraMap (A ⧸ q.comap (algebraMap A B)) (B ⧸ q))

Used by 1

Used byInertia degree one for a singly generated algebra

TheoremInertia degree one for a singly generated algebra#✓fully proved

Let \(A\) and \(B\) be commutative rings, \(B\) an \(A\)-algebra, and \(\mathfrak q\) a maximal ideal of \(B\) whose preimage \(\mathfrak p\) under \(A \to B\) is maximal. If \(B\) is generated as an \(A\)-algebra by a single element \(\pi \in \mathfrak q\), then the inertia degree of \(\mathfrak q\) over \(\mathfrak p\) is \(1\).

The canonical map \(A/\mathfrak p \to B/\mathfrak q\) is surjective, so the residue field extension has degree one.

theorem inertiaDeg_eq_one_of_adjoin_singleton_eq_top
    {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
    (q : Ideal B) [q.IsMaximal] [(q.under A).IsMaximal]
    (π : B) (hπ : π ∈ q)
    (hgen : Algebra.adjoin A {π} = ⊤) :
    q.inertiaDeg A = 1

Uses 1 · Used by 1

Proof usesSurjectivity of the residue map for a singly generated algebra

Used byA generating uniformizer gives total ramification

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.