Theorems · Theorem · commutative algebra

Algebra.HasGoingDown.of_comap_localRingHom_surjective

• 1000+ list: Going-up and going-down theorems

∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (∀ (P : Ideal S) [inst_3 : P.IsPrime],
      Function.Surjective (PrimeSpectrum.comap (Localization.localRingHom (Ideal.under R P) P (algebraMap R S) ⋯))) →
    Algebra.HasGoingDown R S

If for every prime of S, the map Spec Sₚ → Spec Rₚ is surjective, the algebra satisfies going down.

Defined in

Mathlib.RingTheory.Ideal.GoingDown

Cited by

0 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra