Hilbert's Nullstellensatz

Title:	Hilbert's Nullstellensatz
Author:	Alexander Maletzky
Submission date:	2019-06-16
Abstract:	This entry formalizes Hilbert's Nullstellensatz, an important theorem in algebraic geometry that can be viewed as the generalization of the Fundamental Theorem of Algebra to multivariate polynomials: If a set of (multivariate) polynomials over an algebraically closed field has no common zero, then the ideal it generates is the entire polynomial ring. The formalization proves several equivalent versions of this celebrated theorem: the weak Nullstellensatz, the strong Nullstellensatz (connecting algebraic varieties and radical ideals), and the field-theoretic Nullstellensatz. The formalization follows Chapter 4.1. of Ideals, Varieties, and Algorithms by Cox, Little and O'Shea.
BibTeX:	@article{Nullstellensatz-AFP, author = {Alexander Maletzky}, title = {Hilbert's Nullstellensatz}, journal = {Archive of Formal Proofs}, month = jun, year = 2019, note = {\url{https://isa-afp.org/entries/Nullstellensatz.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Groebner_Bases
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.