noncomputable def globalSections_spec_iso (R : CommRingCat) : (AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤) ≅ R

Theorem 2.1: the global sections of Spec R recover R, i.e. Γ(Spec R, O) ≅ R.

theorem specQuasiCompact (R : Type u_1) [CommRing R] : CompactSpace (PrimeSpectrum R)

Spec R is quasi-compact: the prime spectrum of any commutative ring is compact.

theorem closedSubspace_isClosedEmbedding (A : Type u_1) [CommRing A] (I : Ideal A) : Topology.IsClosedEmbedding (PrimeSpectrum.comap (Ideal.Quotient.mk I))

The closed subspace Spec(A/I) → Spec A arising from a quotient ring is a closed topological embedding.

theorem closedSubspace_range_eq_zeroLocus (A : Type u_1) [CommRing A] (I : Ideal A) : Set.range (PrimeSpectrum.comap (Ideal.Quotient.mk I)) = PrimeSpectrum.zeroLocus ↑I

The image of Spec(A/I) → Spec A is the zero locus V(I) of the ideal I.

theorem hilbertBasisTheorem_mv (k : Type u_1) [CommRing k] [IsNoetherianRing k] (n : ℕ) : IsNoetherianRing (MvPolynomial (Fin n) k)

Hilbert basis theorem: polynomials over a Noetherian ring in finitely many variables form a Noetherian ring.

theorem hilbertBasisTheorem_field (k : Type u_1) [Field k] (n : ℕ) : IsNoetherianRing (MvPolynomial (Fin n) k)

Hilbert basis theorem specialized to a field: k[x_1, …, x_n] is Noetherian.