Rückert's descent along polynomial-like ring maps

This file develops the abstract descent principle of Bosch, Güntzer and Remmert, §5.2.5, which transfers the noetherian, factorial and Jacobson properties from a ring A to a ring B receiving an injective map φ : A[X] →+* B that behaves like the inclusion of polynomials into restricted power series.

The hypotheses (RingHom.IsRueckert) concern a set W of monic polynomials, closed under taking monic factors, such that

• for every w ∈ W, the map φ induces an isomorphism A[X] ⧸ (w) ≃+* B ⧸ (φ w) (RingHom.IsRueckert.quotientEquiv), and
• every nonzero b : B becomes a unit multiple of some φ w after a ring automorphism of B.

For a Tate algebra A = K⟨X₁, …, Xₙ⟩ and B = A⟨Y⟩, the polynomials W are the Weierstrass polynomials: the quotient comparison is Weierstrass division, and the automorphisms are the changes of variables making a series distinguished, followed by Weierstrass preparation.

The quotient comparison descends every quotient of B by a nonzero ideal, after an automorphism, to a quotient of some A[X] ⧸ (w), which is finite over A because w is monic (RingHom.IsRueckert.exists_finite_quotient). Consequently:

• RingHom.IsRueckert.isNoetherianRing: if A is noetherian, so is B;
• RingHom.IsRueckert.uniqueFactorizationMonoid: if A is a unique factorisation domain and B is a domain, then B is a unique factorisation domain. Each φ w is a product of primes, because a monic factorisation of w in the factorial ring A[X] stays in W, and an irreducible w ∈ W generates a prime ideal whose quotient is identified with B ⧸ (φ w);
• RingHom.IsRueckert.isJacobsonRing: if A is a Jacobson ring and the Jacobson radical of B is zero, then B is a Jacobson ring. Indeed every nonzero radical ideal of B is the intersection of the maximal ideals containing it (RingHom.IsRueckert.jacobson_eq_self): it contains some nonzero b, and B ⧸ (b) is isomorphic to the Jacobson ring A[X] ⧸ (w). The condition on the Jacobson radical cannot be dropped: for a reduced ring B it is necessary (RingHom.IsRueckert.isJacobsonRing_iff_jacobson_eq_bot).

Main definitions

• RingHom.IsRueckert φ W: the Rückert hypotheses for φ : A[X] →+* B and W ⊆ A[X].
• RingHom.IsRueckert.quotientEquiv: the ring isomorphism A[X] ⧸ (w) ≃+* B ⧸ (φ w) induced by φ, for w ∈ W.

References

• S. Bosch, U. Güntzer and R. Remmert, Non-Archimedean Analysis, §5.2.5.

structure RingHom.IsRueckert {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (φ : Polynomial A →+* B) (W : Set (Polynomial A)) : Prop

The Rückert hypotheses for an injective ring map φ : A[X] →+* B and a set W of monic polynomials closed under taking monic factors: for each w ∈ W, the map φ induces an isomorphism A[X] ⧸ (w) ≃+* B ⧸ (φ w) (the divisibility and remainder conditions below), and every nonzero element of B is mapped by some ring automorphism of B to a unit multiple of φ w for some w ∈ W.

• injective : Function.Injective ⇑φ

  The map φ is injective.

• monic {w : Polynomial A} (hw : w ∈ W) : w.Monic

  Every member of W is monic.

• mem_of_dvd {w p : Polynomial A} (hw : w ∈ W) (hp : p.Monic) (hpw : p ∣ w) : p ∈ W

  Monic factors of members of W belong to W.

• dvd_iff {w : Polynomial A} (hw : w ∈ W) (p : Polynomial A) : φ w ∣ φ p ↔ w ∣ p

  Divisibility by w ∈ W is detected after applying φ: the induced map A[X] ⧸ (w) → B ⧸ (φ w) is injective.

• exists_dvd_sub {w : Polynomial A} (hw : w ∈ W) (b : B) : ∃ (p : Polynomial A), φ w ∣ b - φ p

  Every element of B is congruent to an element of the image of φ modulo φ w for w ∈ W: the induced map A[X] ⧸ (w) → B ⧸ (φ w) is surjective.

• exists_mul_eq {b : B} (hb : b ≠ 0) : ∃ (α : B ≃+* B) (u : Bˣ), ∃ w ∈ W, ↑u * α b = φ w

  Every nonzero element of B is, after a ring automorphism, a unit multiple of φ w for some w ∈ W.

noncomputable def RingHom.IsRueckert.quotientEquiv {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) {w : Polynomial A} (hw : w ∈ W) : Polynomial A ⧸ Ideal.span {w} ≃+* B ⧸ Ideal.span {φ w}

For w ∈ W, the map φ induces a ring isomorphism A[X] ⧸ (w) ≃+* B ⧸ (φ w).

@[simp]

theorem RingHom.IsRueckert.quotientEquiv_mk {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) {w : Polynomial A} (hw : w ∈ W) (p : Polynomial A) : (h.quotientEquiv hw) ((Ideal.Quotient.mk (Ideal.span {w})) p) = (Ideal.Quotient.mk (Ideal.span {φ w})) (φ p)

The quotient comparison sends the class of a polynomial to the class of its image.

theorem RingHom.IsRueckert.exists_nonempty_ringEquiv_quotient_span_singleton {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) {b : B} (hb : b ≠ 0) : ∃ w ∈ W, Nonempty (Polynomial A ⧸ Ideal.span {w} ≃+* B ⧸ Ideal.span {b})

The quotient of B by a nonzero principal ideal is isomorphic to A[X] ⧸ (w) for some w ∈ W.

theorem RingHom.IsRueckert.exists_finite_quotient {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) {I : Ideal B} (hI : I ≠ ⊥) : ∃ (α : B ≃+* B), ((Ideal.Quotient.mk (Ideal.map α I)).comp (φ.comp Polynomial.C)).Finite

Finite-quotient descent. For every nonzero ideal I of B there is a ring automorphism α of B such that B ⧸ α(I) is finite over A, through A → A[X] → B.

theorem RingHom.IsRueckert.isNoetherianRing {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) [IsNoetherianRing A] : IsNoetherianRing B

Rückert's noetherian descent. If A is noetherian, so is B.

theorem RingHom.IsRueckert.prime_apply {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) {w : Polynomial A} (hw : w ∈ W) (hp : Prime w) : Prime (φ w)

The image of a prime member of W is prime.

theorem RingHom.IsRueckert.exists_prime_factors_apply {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) [IsDomain A] [UniqueFactorizationMonoid A] {w : Polynomial A} (hw : w ∈ W) : ∃ (f : Multiset B), (∀ b ∈ f, Prime b) ∧ Associated f.prod (φ w)

Over a unique factorisation domain A, the image of every member of W is associated to a product of primes.

theorem RingHom.IsRueckert.uniqueFactorizationMonoid {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) [IsDomain A] [UniqueFactorizationMonoid A] [IsDomain B] : UniqueFactorizationMonoid B

Rückert's factorial descent. If A is a unique factorisation domain and B is a domain, then B is a unique factorisation domain.

theorem RingHom.IsRueckert.jacobson_eq_self {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) [IsJacobsonRing A] {P : Ideal B} (hP : P.IsRadical) (hP0 : P ≠ ⊥) : P.jacobson = P

Over a Jacobson ring A, every nonzero radical ideal of B is the intersection of the maximal ideals containing it.

theorem RingHom.IsRueckert.isJacobsonRing {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) [IsJacobsonRing A] (hB : Ring.jacobson B = ⊥) : IsJacobsonRing B

Rückert's Jacobson descent. If A is a Jacobson ring and the Jacobson radical of B is zero, then B is a Jacobson ring.

theorem RingHom.IsRueckert.isJacobsonRing_iff_jacobson_eq_bot {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] {φ : Polynomial A →+* B} {W : Set (Polynomial A)} (h : φ.IsRueckert W) [IsJacobsonRing A] [IsReduced B] : IsJacobsonRing B ↔ Ring.jacobson B = ⊥

For a reduced ring B over a Jacobson ring A, the ring B is Jacobson exactly when its Jacobson radical is zero.