PrimeSpectrum.range_comap_eq_zeroLocus_ker_of_isIntegral
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace PrimeSpectrum_range_comap_eq_zeroLocus_ker_of_isIntegral
universe u v
open PrimeSpectrumLean source · statement
theorem _root_.PrimeSpectrum.range_comap_eq_zeroLocus_ker_of_isIntegral
{R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : f.IsIntegral) :
Set.range (PrimeSpectrum.comap f) = PrimeSpectrum.zeroLocus (RingHom.ker f)