Finitesatz

This project formalizes key results from "On polynomial semantics for propositional logics" by Juan C. Agudelo-Agudelo. Our main focus is the formalization of Theorem 4: The Nullstellensatz for finite fields in Lean using Mathlib.

Introduction

This section introduces the theoretical foundations required to understand the formalization of multivariate polynomials in Mathlib, which is essential for this project.

Multivariate Polynomials in Mathlib

Let $R$ be a commutative ring and $\sigma$ an indexing set (representing the variables). The ring of multivariate polynomials over $R$ with variables in $\sigma$ is denoted as $R[X_i : i \in \sigma]$. In Mathlib, this structure is implemented using the type:

$$\text{MvPolynomial}\ \sigma\ R := (\sigma \to_0 \mathbb{N}) \to_0 R$$

At first glance, this definition may seem distant from the classical notation. However, it elegantly encapsulates the structure of a polynomial ring by combining two layers of finitely supported functions.

1. Finite Support Functions

To understand the definition, we first define the concept of finite support. Let $f : A \to B$ be a function where $B$ has a zero element ($0$). The support of $f$ is defined as:

$$\text{supp}(f) := \{a \in A \mid f(a) \neq 0\}$$

A function $f$ has finite support if $\text{supp}(f)$ is finite. The type of finitely supported functions from $A$ to $B$ is denoted as $A \to_0 B$.

Finite support functions are versatile because they can represent different algebraic structures depending on how we interpret the mapping $a \mapsto b$. If $\text{supp}(f) = \{a_1, \ldots, a_n\}$ with $f(a_i) = b_i$, we can visualize $f$ in two ways:

Representation	Notation	Used in this formalization for...
Additive	$b_1 a_1 + b_2 a_2 + \cdots + b_n a_n$	The Polynomial itself (Sum of monomials weighted by coefficients)
Multiplicative	$a_1^{b_1} a_2^{b_2} \cdots a_n^{b_n}$	The Monomials (Variables raised to exponents)

This duality is why Finsupp is used twice in the definition of MvPolynomial.

Note: This table is merely pedagogical. The representation of a finitely supported function is not restricted to these two forms. Fundamentally, A →₀ B is just a function with finite non-zero values; these specific notations are simply the most common algebraic interpretations used to build polynomial structures.

2. The Type of Monomials

The inner part of the polynomial definition is $\sigma \to_0 \mathbb{N}$. Here, $\sigma$ represents the set of variables (e.g., $\sigma = \{x, y, z\}$).

A function $m : \sigma \to_0 \mathbb{N}$ assigns a natural number (an exponent) to each variable, such that only finitely many variables have a non-zero exponent. This perfectly corresponds to the definition of a monomial.

Example: Consider $\sigma = \{x, y, z\}$. The monomial $x^2 y^3 z^1$ corresponds to the function $m : \sigma \to_0 \mathbb{N}$ defined by:

• $m(x) = 2$
• $m(y) = 3$
• $m(z) = 1$
• $m(v) = 0$ for all other $v \in \sigma$.

Thus, we can identify the type of monomials $\mathcal{M}$ with $\sigma \to_0 \mathbb{N}$.

3. Polynomials as Linear Combinations

Finally, a polynomial is simply a finite linear combination of monomials with coefficients in $R$.

This brings us back to the full type:

$$(\underbrace{\sigma \to_0 \mathbb{N}}_{\text{Monomials}}) \to_0 R$$

A polynomial is a function $p: \mathcal{M} \to_0 R$ that assigns a coefficient to each monomial. Since it has finite support, a polynomial has only finitely many non-zero terms.

For example, $3x^2y - 5z$ is represented as a function that maps the monomial $x^2y$ to $3$, the monomial $z$ to $-5$, and all other monomials to $0$.

The Nullstellensatz for Finite Fields

This section outlines the main theoretical result formalized in this repository.

Definitions

Let $R$ be a commutative ring. We consider the polynomial ring in $n$ variables, denoted as $R[X_1, \dots, X_n]$.

Restricted Variety ($V^A$): Given an ideal $J \subseteq R[X_1, \dots, X_n]$, the variety defined by $J$ restricted to $A = A_1 \times \cdots \times A_n$, where each is a finset of $R$, is the set of common zeros within $A$:

$$V^A(J) = \{(a_1, \dots, a_n) \in A \mid \forall p \in J, p(a_1, \dots, a_n) = 0\}$$

Note: A similar definition can be found in MvPolynomial.zeroLocus.

Ideal of a Set ($I$): Conversely, given a subset $B \subseteq R^n$, the ideal of functions vanishing on $B$ is defined as:

$$I(B) = \{p \in R[X_1, \dots, X_n] \mid \forall \mathbf{a} \in B, p(\mathbf{a}) = 0\}$$

Note: This is exactly the definition MvPolynomial.vanishingIdeal.

Theorem 4: Weak Nullstellensatz

The main objective of this repository is the formalization of the following result, which connects the algebraic and geometric perspectives over finite fields.

Theorem: Let $K$ be a field, $A \subseteq K^n$ a finite subset, and $J \subseteq K[X_1, \dots, X_n]$ an ideal. Then:

$$I(V^A(J)) = J + I(A)$$

References

• Agudelo-Agudelo, J. C., Agudelo-González, C. A., & García-Quintero, O. E. (2016). On polynomial semantics for propositional logics. Journal of Applied Non-Classical Logics, 26(2), 103–125. https://doi.org/10.1080/11663081.2016.1198529
• Clark, P. L. (2014). The Combinatorial Nullstellensätze Revisited. The Electronic Journal of Combinatorics, 21(4), P4.15. https://doi.org/10.37236/4359