Theorems · Theorem · algebraic geometry

PrimeSpectrum.range_comap_snd

∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S],
  Set.range (PrimeSpectrum.comap (RingHom.snd R S)) = PrimeSpectrum.zeroLocus ↑(RingHom.ker (RingHom.snd R S))

Defined in

Mathlib.RingTheory.Spectrum.Prime.Topology

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiring