₀0 ₁1 ₂2 ₃3 ∉$\notin$ ≤$\leq$ ⊆$\subseteq$ ∪$\cup$ ∈$\in$ ∩$\cap$ ⟨$\langle$
⟩$\rangle$ ℤ$\mathbb{Z}$ ∀$\forall$ ∃$\exists$ ≅$\cong$

# Towards solid abelian groups:
A formal proof of Nöbeling’s theorem

Dagur Asgeirsson

###### Abstract.

Condensed mathematics, developed by Clausen and Scholze over the last few
years, is a new way of studying the interplay between algebra and geometry. It
replaces the concept of a topological space by a more sophisticated but
better-behaved idea, namely that of a condensed set. Central to the theory are
solid abelian groups and liquid vector spaces, analogues of complete
topological groups.

Nöbeling’s theorem, a surprising result from the 1960s about the structure of
the abelian group of continuous maps from a profinite space to the integers,
is a crucial ingredient in the theory of solid abelian groups; without it one
cannot give any nonzero examples of solid abelian groups. We discuss a
recently completed formalisation of this result in the Lean theorem prover,
and give a more detailed proof than those previously available in the
literature. The proof is somewhat unusual in that it requires induction over
ordinals – a technique which has not previously been used to a great extent in
formalised mathematics.

##  1\. Introduction

Nöbeling’s theorem says that the abelian group $C(S,\mathbb{Z})$ of continuous
maps from a profinite space $S$ to the integers, is a free abelian group. In
fact, the original statement [13, Satz 1] is the more general result that
bounded maps from any set to the integers form a free abelian group, but this
special case has recently been applied [15, Theorem 5.4] in the new field of
condensed mathematics (see also [14, 5, 3]).

We report on a recently completed formalisation of this theorem using the Lean
4 theorem prover [10], building on its _Mathlib_ library of formalised
mathematics (which was recently ported from Lean 3, see [11, 9]). The proof
uses the well-ordering principle and a tricky induction over ordinals. Once
integrated into Mathlib, this will be the first use of the induction principle
for ordinals in the library outside the folder containing the theory of
ordinals.

When formalising a nontrivial proof, one inevitably makes an effort to
organise the argument carefully. One purpose of this paper is to give a well-
organised and detailed proof of Nöbeling’s theorem, written in conventional
mathematical language, which is essentially a by-product of the formalisation
effort. This will hopefully be a more accessible proof than those that already
exist in the literature; the one in [13] is in German, while the proofs of the
result in [7, 15] are the same argument as the one presented here, but in
significantly less detail. This is the content of section 4; some mathematical
prerequisites are found in section 3.

In section 2 we give more details about the connection to condensed
mathematics and in sections 5, 6, and 7 we discuss the formalisation process
and the integration into Mathlib.

Throughout the text, we use the symbol “” for external links, either to the
documentation for definitions and theorems in Mathlib where the reader can
easily access the source code of Mathlib, or directly to source code on
development branches of Mathlib.

Mathlib is a growing library of mathematics formalised in Lean. All material
is maintained continuously by a team of experts. There is a big emphasis on
unity, meaning that there is _one_ official definition of every concept, and
it is the job of contributors to provide proofs that alternative definitions
are equivalent. This project is in the process of being integrated into
Mathlib. Naturally, that process takes some time, as high standards are
demanded of code that enters the library. However, it is an important part of
formalisation to get the code into Mathlib, because doing so means that it
stays usable to others in the future.

### Acknowledgements

First and foremost, I would like to thank Johan Commelin for encouraging me to
start seriously working on this project when we were both in Banff attending
the workshop on formalisation of cohomology theories earlier this year. I had
useful discussions related to this work with Johan, Kevin Buzzard, Adam Topaz,
and Dustin Clausen. I am indebted to all four of them for providing helpful
feedback on earlier drafts of this paper.

Any project formalising serious mathematics in Lean depends on Mathlib, and
this one is no exception. I am grateful to the Lean community as a whole for
building and maintaining such a useful mathematical library, as well as
providing an excellent forum for Lean-related discussions through the Zulip
chat.

The author was supported by the Danish National Research Foundation (DNRF)
through the “Copenhagen Center for Geometry and Topology” under grant no.
DNRF151.

##  2\. Motivation

Condensed mathematics [15, 14, 5] is a new theory developed by Clausen and
Scholze (and independently by Barwick and Haine, who called the theory
_pyknotic sets_ [3]). It has the purpose of generalising topology in a way
that gives better categorical properties, which is desirable e.g. when the
objects have both a topological and an algebraic structure. Condensed objects
can be described as sheaves on a certain site of profinite spaces. A
topological abelian group $A$ can be regarded as a condensed abelian group
with $S$-valued points $C(S,A)$ for profinite spaces $S$. Discrete abelian
groups such as $\mathbb{Z}$ are important examples of topological abelian
groups. There is a useful characterisation of discrete condensed sets (which
leads to the same characterisation for more general condensed objects such as
condensed abelian groups), which has been formalised in Lean 3 by the author
in [1].

The discreteness characterisation can be stated somewhat informally as
follows: A condensed set $X$ is discrete if and only if for every profinite
space $S=\varprojlim_{i}S_{i}$ (written as a cofiltered limit of finite
discrete spaces), the natural map

$\varinjlim_{i}X(S_{i})\to X(S)$

is an isomorphism.

There is a notion of completeness of condensed abelian groups, called being
_solid_ [15, Definition 5.1]. For the convenience of the reader, we give the
informal definition here in Definition 2.1. First, we need to recall two facts
about condensed abelian groups:

  * •

The category of condensed abelian groups has all limits.

  * •

The forgetful functor from condensed abelian groups to condensed sets has a
left adjoint, denoted by $\mathbb{Z}[-]$ (adopted from the analogous
relationship between the category of sets and the category of abelian groups).

######  Definition 2.1.

Let $S=\varprojlim_{i}S_{i}$ be a profinite space and define a condensed
abelian group as follows:

$\mathbb{Z}[S]^{\rule[0.36pt]{3.5pt}{3.5pt}}:=\varprojlim_{i}\mathbb{Z}[S_{i}]$

There is a natural map
$\mathbb{Z}[S]\to\mathbb{Z}[S]^{\rule[0.36pt]{3.5pt}{3.5pt}}$, and we say that
a condensed abelian group $A$ is _solid_ if for every profinite space $S$ and
every morphism $f:\mathbb{Z}[S]\to A$ of condensed abelian groups, there is a
unique morphism $g:\mathbb{Z}[S]^{\rule[0.36pt]{3.5pt}{3.5pt}}\to A$ making
the obvious triangle commute111This definition has also been formalised by the
author in Lean 3 in [2].

Using the discreteness characterisation and Nöbeling’s theorem, one can prove
that for every profinite space $S$, there is a set $I$ and an isomorphism of
condensed abelian groups

$\mathbb{Z}[S]^{\rule[0.36pt]{3.5pt}{3.5pt}}\cong\prod_{i\in I}\mathbb{Z}.$

This structural result is essential to developing the theory of solid abelian
groups. Without it one cannot even prove the existence of a nontrivial solid
abelian group.

Since the proof of Nöbeling’s theorem has nothing to do with condensed
mathematics, people studying the theory might be tempted to skip the proof and
use Nöbeling’s theorem as a black box. Now that it has been formalised, they
can do this with a better conscience. On the other hand, people interested in
understanding the proof might want to turn to sections 3 and 4 of this paper
for a more detailed account.

##  3\. Preliminaries

###  3.1. Order theory

######  Definition 3.1.

Let $I$ and $X$ be sets and let $r$ be a binary relation on $X$. An
$I$-indexed family $(x_{i})$ in $X$ is _directed_ if for all $i,j\in I$, there
exists $k\in I$ such that $r(x_{i},x_{k})$ and $r(x_{j},x_{k})$.

######  Lemma 3.2.

A monotone map on a poset with a join operation (i.e. a least upper bound of
two elements) is directed.

######  Remark 3.3.

Taking the union of two sets is an example of a join operation.

######  Definition 3.4.

A category $\mathcal{C}$ is _filtered_ if it satisfies the following three
conditions

  1. (i)

$\mathcal{C}$ is nonempty.

  2. (ii)

For all objects $X,Y$, there exists an object $Z$ and morphisms $f:X\to Z$ and
$g:Y\to Z$.

  3. (iii)

For all objects $X,Y$ and all morphisms $f,g:X\to Y$, there exists an object
$Z$ and a morphism $h:Y\to Z$ such that $h\circ f=h\circ g$.

A category is _cofiltered_ if the opposite category is filtered.

######  Remark 3.5.

A poset is filtered if and only if it is nonempty and directed.

######  Remark 3.6.

The poset of finite subsets of a given set is filtered.

###  3.2. Linear Independence

######  Lemma 3.7.

If $(X_{i})$ is a family of linearly independent subsets of a module over a
ring $R$, which is directed with respect to the subset relation, then its
union is linearly independent.

######  Lemma 3.8.

Suppose we have a commutative diagram

${0}$${N}$${M}$${P}$${I}$${{I\sqcup
J}}$${J}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{v}$$\scriptstyle{u}$$\scriptstyle{w}$

where $N,M,P$ are modules over a ring $R$, the top row is exact, and the
bottom maps are the inclusion maps. If $v$ and $w$ are linearly independent,
then $u$ is linearly independent.

###  3.3. Cantor’s intersection theorem

######  Theorem 3.9.

_Cantor’s intersection theorem_. If $(Z_{i})_{i\in I}$ is a nonempty family of
nonempty, closed and compact subsets of a topological space $X$, which is
directed with respect to the _superset_ relation $(V,W)\mapsto V\supseteq W$,
then the intersection $\bigcap_{i\in I}Z_{i}$ is nonempty.

######  Remark 3.10.

Cantor’s intersection theorem is often stated only for the special case of
decreasing nested sequences of nonempty compact, closed subsets. The
generalisation above can be proved by slightly modifying the standard proof of
that special case.

###  3.4. Cofiltered limits of profinite spaces

######  Definition 3.11.

A _profinite space_ is a totally disconnected compact Hausdorff space.

######  Lemma 3.12.

Every profinite space has a basis of clopen subsets.

######  Lemma 3.13.

Every profinite space is totally separated, i.e. any two distinct points can
be separated by clopen neighbourhoods.

######  Remark 3.14.

A topological space is profinite if and only if it can be written as a
cofiltered limit of finite discrete spaces. See section 7 for a further
discussion.

######  Lemma 3.15.

Any continuous map from a cofiltered limit of profinite spaces to a discrete
space factors through one of the components.

######  Remark 3.16.

In particular, a continuous map from a profinite space

$S=\varprojlim_{i}S_{i}$

to a discrete space factors through one of the finite quotients $S_{i}$.

##  4\. The theorem

######  Theorem 4.1.

(Nöbeling’s theorem). Let $S$ be a profinite space. Then the abelian group
$C(S,\mathbb{Z})$ of continuous maps from $S$ to $\mathbb{Z}$ is free.

###### Proof.

Let $I$ denote the set of clopen subsets of $S$. Then the map

$S\to\prod_{i\in I}\\{0,1\\}$

whose $i$-th projection is given by the indicator function of the clopen
subset $i$ is a closed embedding. Theorem 4.1 hence follows from Theorem 4.2.
∎

######  Theorem 4.2.

Let $I$ be a set and let $S$ be a closed subset of $\prod_{i\in I}\\{0,1\\}$.
Then $C(S,\mathbb{Z})$ is a free abelian group.

###### Proof.

Choose a well-ordering on $I$. We construct a basis as follows

  * •

Let $e_{S,i}\in C(S,\mathbb{Z})$ denote the composition

${S}$${{\prod_{i\in
I}\\{0,1\\}}}$${{\\{0,1\\}}}$${{\mathbb{Z}}}$$\scriptstyle{p_{i}}$

where $p_{i}$ denotes the $i$-th projection map, and the other two maps are
the obvious inclusions.

  * •

Let $P$ denote the set of finite, strictly decreasing sequences in $I$. Order
these lexicographically.

  * •

Let $\operatorname{ev}_{S}:P\to C(S,\mathbb{Z})$ denote the map

$(i_{1},\cdots,i_{r})\mapsto e_{S,i_{1}}\cdots e_{S,i_{r}}.$

  * •

For $p\in P$, let $\Sigma_{S}(p)$ denote the span in $C(S,\mathbb{Z})$ of the
set

$\operatorname{ev}_{S}\left(\\{q\in P\ |\ q<p\\}\right).$

  * •

Let $E(S)$ denote the subset of $P$ consisting of those elements whose
evaluation cannot be written as a linear combination of evaluations of smaller
elements of $P$, i.e.

$E(S):=\\{p\in P\ |\ \operatorname{ev}_{S}(p)\notin\Sigma_{S}(p)\\}.$

In Subsection 4.2 we prove that the set
$\operatorname{ev}_{S}\left(E(S)\right)$ spans $C(S,\mathbb{Z})$, and in
Subsection 4.3 we prove that the family

$\operatorname{ev}_{S}:E(S)\to C(S,\mathbb{Z})$

is linearly independent. Thus, $\operatorname{ev}_{S}\left(E(S)\right)$ is the
desired basis. ∎

###  4.1. Notation and generalities

For a subset $J$ of $I$ we denote by

$\pi_{J}:\prod_{i\in I}\\{0,1\\}\to\prod_{i\in I}\\{0,1\\}$

the map whose $i$-th projection is $p_{i}$ if $i\in J$, and $0$ otherwise.
These maps are continuous, and since source and target are compact Hausdorff
spaces, they are also closed. Given a subset $S\subseteq\prod_{i\in
I}\\{0,1\\}$, we let

$S_{J}:=\pi_{J}(S).$

We can regard $I$ with its well-ordering as an ordinal. Then $I$ is the set of
all strictly smaller ordinals. Given an ordinal $\mu$, we let

$\pi_{\mu}:=\pi_{\\{i\in I\ |\ i<\mu\\}}$

and

$S_{\mu}:=S_{\\{i\in I\ |\ i<\mu\\}}.$

These maps induce injective $\mathbb{Z}$-linear maps

$\pi_{J}^{*}:C(S_{J},\mathbb{Z})\to C(S,\mathbb{Z})$

by precomposition.

Recall that we have defined $P$ as the set of finite, strictly decreasing
sequences in $I$, ordered lexicographically. We will use this notation
throughout the proof of Nöbeling’s theorem.

######  Lemma 4.3.

For $p\in P$ and $x\in S$, we have

$\operatorname{ev}_{S}(p)(x)=\begin{cases}1&\text{ if }\forall i\in p,\
x_{i}=1\\\ 0&\text{ otherwise.}\end{cases}$

###### Proof.

Obvious. ∎

######  Lemma 4.4.

Let $J$ be a subset of $I$ and let $p\in P$ be such that $i\in p$ implies
$i\in J$. Then
$\pi_{J}^{*}(\operatorname{ev}_{S_{J}}(p))=\operatorname{ev}_{S}(p)$.

###### Proof.

Since $i\in p$ implies $i\in J$, we have

$x_{i}=\pi_{J}^{*}(x)_{i}$

for all $x\in S$ and $i\in p$. The result now follows from Lemma 4.3. ∎

######  Remark 4.5.

The hypothesis in Lemma 4.4 holds in particular if $p\in E(S_{J})$. Indeed,
suppose $i\in p$, then if $i\notin J$, we have
$\operatorname{ev}_{S_{J}}(p)=0$.

######  Lemma 4.6.

If $\mu^{\prime},\mu$ are ordinals satisfying $\mu^{\prime}<\mu$, then
$E(S_{\mu^{\prime}})\subseteq E(S_{\mu})$.

###### Proof.

Let $p\in E(S_{\mu^{\prime}})$. Then every entry of $p$ is $<\mu^{\prime}$,
and it suffices to show that if

$\operatorname{ev}_{S_{\mu}}(p)=\pi_{\mu^{\prime}}^{*}(\operatorname{ev}_{S_{\mu^{\prime}}}(p))$

is in the span of

$\operatorname{ev}_{S_{\mu}}\left(\\{q\in P\ |\
q<p\\}\right)=\pi_{\mu^{\prime}}^{*}\left(\operatorname{ev}_{S_{\mu^{\prime}}}\left(\\{q\in
P\ |\ q<p\\}\right)\right)$

then $\operatorname{ev}_{S_{\mu^{\prime}}}(p)$ is in the span of
$\operatorname{ev}_{S_{\mu^{\prime}}}\left(\\{q\in P\ |\ q<p\\}\right)$. This
follows by injectivity of $\pi_{\mu^{\prime}}^{*}$. ∎

###  4.2. Span

The following series of lemmas proves that
$\operatorname{ev}_{S}\left(E(S)\right)$ spans $C(S,\mathbb{Z})$.

######  Lemma 4.7.

The set $P$ is well-ordered.

###### Proof sketch.

Suppose not. Take a strictly decreasing sequence $(p_{n})$ in $P$. Let $a_{n}$
denote first term of $p_{n}$. Then $(a_{n})$ is a decreasing sequence in $I$
and hence eventually constant. Denote its limit by $a$. Let
$q_{n}=p_{n}\setminus{a_{n}}$. Then there exists an $N$ such that
$(q_{n})_{n\geq N}$ is a strictly decreasing sequence in $P$ and we can repeat
the process of taking the indices of the first factors, get a decreasing
sequence in $I$ whose limit is strictly smaller than $a$. Continuing this way,
we get a strictly decreasing sequence in $I$, a contradiction. ∎

######  Remark 4.8.

The proof sketch of Lemma 4.7 above is ill-suited for formalisation. Scott
Morrison gave a formalised proof , following similar ideas to those above,
which used close to 300 lines of code. A few days later, Junyan Xu found a
proof  that was ten times shorter, directly using the inductive datatype

    WellFounded}.
    \end

remark

######  Lemma 4.9.

If $\operatorname{ev}_{S}\left(P\right)$ spans $C(S,\mathbb{Z})$, then
$\operatorname{ev}_{S}\left(E(S)\right)$ spans $C(S,\mathbb{Z})$.

###### Proof.

It suffices to show that $\operatorname{ev}_{S}\left(P\right)$ is contained in
the span of $\operatorname{ev}_{S}\left(E(S)\right)$. Suppose it is not, and
let $p$ be the smallest element of $P$ whose evaluation is not in the span of
$\operatorname{ev}_{S}\left(E(S)\right)$ (this $p$ exists by Lemma 4.7). Write
$\operatorname{ev}_{S}(p)$ as a linear combination of evaluations of strictly
smaller elements of $P$. By minimality of $p$, each term of the linear
combination is in the span of $\operatorname{ev}_{S}\left(E(S)\right)$,
implying that $p$ is as well, a contradiction. ∎

######  Lemma 4.10.

Let $F$ denote the contravariant functor from the (filtered) poset of finite
subsets of $I$ to the category of profinite spaces, which sends $J$ to
$S_{J}$. Then $S$ is homeomorphic to the limit of $F$.

###### Proof sketch.

Since $S$ is compact and the limit is Hausdorff, it suffices to show that the
natural map from $S$ to the limit of $F$ induced by the projection maps
$\pi_{J}:S\to S_{J}$ is bijective.

For injectivity, let $a,b\in S$ such that $\pi_{J}(a)=\pi_{J}(b)$ for all
finite subsets $J$ of $I$. For all $i\in I$ we have
$a_{i}=\pi_{\\{i\\}}(a)=\pi_{\\{i\\}}(b)=b_{i}$, hence $a=b$.

For surjectivity, let $b\in\operatorname{lim}F$. Denote by

$f_{J}:\operatorname{lim}F\to S_{J}$

the projection maps. We need to construct an element $a$ of $C$ such that
$\pi_{J}(a)=f_{J}(b)$ for all $J$. In other words, we need to show that the
intersection

$\bigcap_{J}\pi_{J}^{-1}\\{f_{J}(b)\\},$

where $J$ runs over all finite subsets of $I$, is nonempty. By Cantor’s
intersection theorem 3.9, it suffices to show that this family is directed
(all the fibres are closed by continuity of the $\pi_{J}$, and closed subsets
of a compact Hausdorff space are compact). To show that it is directed, it
suffices to show that for $J\subseteq K$, we have

$\pi_{K}^{-1}\\{f_{K}(b)\\}\subseteq\pi_{J}^{-1}\\{f_{J}(b)\\}$

(by Lemma 3.2). This follows easily because the transition maps in the limits
are just restrictions of the $\pi_{J}$. ∎

######  Remark 4.11.

A pull request  to Mathlib has been opened with a precise, fully formalised
proof of a more general result implying Lemma 4.10.

######  Lemma 4.12.

Let $J$ be a finite subset of $I$. Then
$\operatorname{ev}_{S_{J}}\left(E(S_{J})\right)$ spans $C(S_{J},\mathbb{Z})$.

###### Proof.

By lemma 4.9, it suffices to show that $\operatorname{ev}_{S_{J}}(P)$ spans.
For $x\in S_{J}$, denote by $f_{x}$ the map $S_{J}\to\mathbb{Z}$ given by the
Kronecker delta $f_{x}(y)=\delta_{xy}$.

Since $S_{J}$ is finite, the set of continuous maps is actually the set of all
maps, and the maps $f_{x}$ span $C(S_{J},\mathbb{Z})$.

Now let $j_{1}>\cdots>j_{r}$ be a decreasing enumeration of the elements of
$J$. Let $x\in S_{J}$ and let $e_{i}$ denote $e_{S_{J},j_{i}}$ if
$x_{j_{i}}=1$ and $(1-e_{S_{J},j_{i}})$ if $x_{j_{i}}=0$. Then

$f_{j_{i}}=\prod_{i=1}^{r}e_{i}$

is in the span of $P(S_{J})$, as desired. ∎

######  Lemma 4.13.

$P$ spans $C(S,\mathbb{Z})$.

###### Proof.

Let $f\in C(S,\mathbb{Z})$. Then by Lemmas 4.10 and 3.15, there is a $g\in
C(S_{J},\mathbb{Z})$ such that $f=\pi_{J}^{*}(g)$. Writing this $g$ as a
linear combination of elements of $E(S_{J})$, by Lemma 4.4 we see that $f$ is
a linear combination of elements of $P$ as desired. ∎

###  4.3. Linear independence

######  Notation 4.14.

Regard $I$ with its well-ordering as an ordinal. Let $Q$ denote the following
predicate on an ordinal $\mu\leq I$:

For all closed subsets $S$ of $\prod_{i\in I}\\{0,1\\}$, such that for all
$x\in S$ and $i\in I$, $x_{i}=1$ implies $i<\mu$, $E(S)$ is linearly
independent in $C(S,\mathbb{Z})$.

We want to prove the statement $Q(I)$. We prove by induction on ordinals that
$Q(\mu)$ holds for all ordinals $\mu\leq I$.

######  Lemma 4.15.

The base case of the induction, $Q(0)$, holds.

###### Proof.

In this case, $S$ is empty or a singleton. If $S$ is empty, the result is
trivial. Suppose $S$ is a singleton. We want to show that $E(S)$ consists of
only the empty list, which evaluates to $1$ and is linearly independent in
$C(S,\mathbb{Z})\cong\mathbb{Z}$. Let $p\in P$ and suppose $p$ is nonempty.
Then it is strictly larger than the empty list. But the evaluation of the
empty list is $1$, which spans $C(S,\mathbb{Z})\cong\mathbb{Z}$, and thus
$\operatorname{ev}_{S}(p)$ is in the span of strictly smaller products, i.e.
not in $E(S)$. ∎

####  4.3.1. Limit case

Let $\mu$ be a limit ordinal, $S$ a closed subset such that for all $x\in S$
and $i\in I$, $x_{i}=1$ implies $i<\mu$. In other words, $S=S_{\mu}$. Suppose
$Q(\mu^{\prime})$ holds for all $\mu^{\prime}<\mu$. Then in particular
$E(S_{\mu^{\prime}})$ is linearly independent

######  Lemma 4.16.

Let $\mu^{\prime}<\mu$ and $p\in P$ whose entries are all $<\mu^{\prime}$.
Then

$\pi_{\mu^{\prime}}^{*}\left(\operatorname{ev}_{S_{\mu^{\prime}}}\left(\\{q\in
P\ |\ q<p\\}\right)\right)=\operatorname{ev}_{S_{\mu}}\left(\\{q\in P\ |\
q<p\\}\right).$

###### Proof.

If $q<p$, then every element of $q$ is also $<\mu^{\prime}$. Thus, by lemma
4.4,

$\pi_{\mu^{\prime}}^{*}\left(\operatorname{ev}_{S_{\mu^{\prime}}}(q)\right)=\operatorname{ev}_{S_{\mu}}(q),$

as desired. ∎

######  Lemma 4.17.

$E(S_{\mu})=\bigcup_{\mu^{\prime}<\mu}E(S_{\mu^{\prime}})$

###### Proof.

The inclusion from right to left follows from Lemma 4.6, so we only need to
show that if $p\in E(S_{\mu})$ then there exists $\mu^{\prime}<\mu$ such that
$p\in E(S_{\mu^{\prime}})$. Take $\mu^{\prime}$ to be the supremum of the set
$\\{i+1\ |\ i\in p\\}$. Then $\mu^{\prime}=0$ if $p$ is empty, and of the form
$i+1$ for an ordinal $i<\mu$ if $p$ is nonempty. In either case,
$\mu^{\prime}<\mu$.

Since every $i\in p$ satisfies $i<\mu^{\prime}<\mu$, we have

$\operatorname{ev}_{S_{\mu}}(p)=\pi_{\mu^{\prime}}^{*}(\operatorname{ev}_{S_{\mu^{\prime}}}(p))$

and

$\operatorname{ev}_{S_{\mu}}\left(\\{q\in P\ |\
q<p\\}\right)=\pi_{\mu^{\prime}}^{*}\left(\operatorname{ev}_{S_{\mu^{\prime}}}\left(\\{q\in
P\ |\ q<p\\}\right)\right)$

so if $\operatorname{ev}_{S_{\mu^{\prime}}}(p)$ is in the span of
$\operatorname{ev}_{S_{\mu^{\prime}}}\left(\\{q\in P\ |\ q<p\\}\right)$ then
$\operatorname{ev}_{S_{\mu}}(p)$ is in the span of
$\operatorname{ev}_{S_{\mu}}\left(\\{q\in P\ |\ q<p\\}\right)$, contradicting
the fact that $p\in E(S_{\mu})$. ∎

######  Lemma 4.18.

$\operatorname{ev}_{S_{\mu}}\left(E(S_{\mu})\right)=\bigcup_{\mu^{\prime}<\mu}\pi_{\mu^{\prime}}^{*}\left(\operatorname{ev}_{S_{\mu^{\prime}}}\left(E(S_{\mu^{\prime}})\right)\right)$

###### Proof.

This follows from a combination of Lemmas 4.4 and 4.17. ∎

The family of subsets in the union in Lemma 4.18 is directed with respect to
the subset relation (this follows from Lemmas 3.2, 4.6, and 4.4). The sets
$\operatorname{ev}_{S_{\mu^{\prime}}}(E(S_{\mu^{\prime}}))$ are all linearly
independent by the inductive hypothesis, and by injectivity of
$\pi_{\mu}^{*}$, their images under that map are as well. Thus, by Lemma 3.7,
the union is linearly independent, and we are done.

####  4.3.2. Successor case

Let $\mu$ be an ordinal, $S$ a closed subset such that for all $x\in S$ and
$i\in I$, $x_{i}=1$ implies $i<\mu+1$. In other words, $S=S_{\mu+1}$. Suppose
$Q(\mu)$ holds. Then in particular $\operatorname{ev}_{S_{\mu}}:E(S_{\mu})\to
C(S_{\mu},\mathbb{Z})$ is linearly independent.

To prove the inductive step in the successor case, we construct a closed
subset $S^{\prime}$ of $\prod_{i\in I}\\{0,1\\}$ such that for all $x\in
S^{\prime}$, $x_{i}=1$ implies $i<\mu$, and a commutative diagram

(1)
${0}$${{C(S_{\mu},\mathbb{Z})}}$${{C(S,\mathbb{Z})}}$${{C(S^{\prime},\mathbb{Z})}}$${{E(S_{\mu})}}$${{E(S)}}$${{E^{\prime}(S)}}$$\scriptstyle{\pi_{\mu}^{*}}$$\scriptstyle{g}$$\scriptstyle{\operatorname{ev}_{S}}$$\scriptstyle{\operatorname{ev}_{S_{\mu}}}$

where the top row is exact and $E^{\prime}(S)$ is the subset of $E(S)$
consisting if those $p$ with $\mu\in p$ (note that $p$ necessarily starts with
$\mu$). For $p\in P$, we denote by $p^{t}\in P$ the sequence obtained by
removing the first element of $p$ ($t$ stands for _tail_). The linear map $g$
has the property that
$g(\operatorname{ev}_{S}(p))=\operatorname{ev}_{S^{\prime}}(p^{t})$ and
$p^{t}\in E(S^{\prime})$. Given such a construction, the successor step in the
induction follows from lemma 3.8.

######  Construction 4.19.

Let

$S_{0}=\\{x\in S\ |\ x_{\mu}=0\\},$ $S_{1}=\\{x\in S\ |\ x_{\mu}=1\\},$

and

$S^{\prime}=S_{0}\cap\pi_{\mu}(S_{1}).$

Then $S^{\prime}$ satisfies the inductive hypothesis.

######  Construction 4.20.

Let $g_{0}:S^{\prime}\to S$ denote the inclusion map, and let
$g_{1}:S^{\prime}\to S$ denote the map that swaps the $\mu$-th coordinate to
$1$ (since $S^{\prime}\subseteq\pi_{\mu}(S_{1})$, this map lands in $S$).
These maps are both continuous, and we obtain a linear map

$g_{1}^{*}-g_{0}^{*}:C(S,\mathbb{Z})\to C(S^{\prime},\mathbb{Z}),$

which we denote by $g$.

######  Lemma 4.21.

The top row in diagram (1) is exact.

###### Proof.

We already know that $\pi_{\mu}^{*}$ is injective. Also, since

$\pi_{\mu}\circ g_{1}=\pi_{\mu}\circ g_{0},$

we have

$g\circ\pi_{\mu}^{*}=0.$

Now suppose we have

$f\in C(S,\mathbb{Z})\text{ with }g(f)=0.$

We want to find an

$f_{\mu}\in C(S_{\mu},\mathbb{Z})\text{ with }f_{\mu}\circ\pi_{\mu}=f.$

Denote by

$\pi_{\mu}^{\prime}:\pi_{\mu}(S_{1})\to S_{1}$

the map that swaps the $\mu$-th coordinate to $1$. Since $g(f)=0$, we have

$f\circ g_{1}=f\circ g_{0}$

and hence the two continuous maps $f_{|S_{0}}$ and
$f_{|S_{1}}\circ\pi_{\mu}^{\prime}$ agree on the intersection

$S^{\prime}=S_{0}\cap\pi_{\mu}(S_{1})$

Together, they define the desired continuous map $f_{\mu}$ on all of
$S_{0}\cup\pi_{\mu}(S_{1})=S_{\mu}$. ∎

######  Lemma 4.22.

If $p\in P$ starts with $\mu$, then
$g(\operatorname{ev}_{S}(p))=\operatorname{ev}_{S^{\prime}}(p^{t})$.

###### Proof.

This follows from considering all eight cases given by Lemma 4.3. We omit the
proof here and refer to the Lean proof linked above. ∎

######  Remark 4.23.

If $p\in E(S)$ and $\mu\in p$, then $p$ satisfies the hypotheses of Lemma
4.22.

######  Lemma 4.24.

If $p\in E(S)$ and $\mu\in p$, then $p^{t}\in E(S^{\prime})$.

###### Proof.

Contraposing the statement, it suffices to show that if

$\operatorname{ev}_{S^{\prime}}\left(p^{t}\right)\in\operatorname{Span}\left(\operatorname{ev}_{S^{\prime}}\left(\\{q\
|\ q<p^{t}\\}\right)\right),$

then

$\operatorname{ev}_{S}(p)\in\operatorname{Span}\left(\operatorname{ev}_{S}\left(\\{(q)\
|\ q<p\\}\right)\right).$

Given a $q\in P$ such that $i\in q$ implies $i<\mu$, we denote by $q^{\mu}\in
P$ the sequence obtained by adding $\mu$ at the front. Write

$\displaystyle g(\operatorname{ev}_{S}(p))$
$\displaystyle=\operatorname{ev}_{S^{\prime}}(p^{t})$
$\displaystyle=\sum_{q<p^{t}}n_{q}\operatorname{ev}_{S^{\prime}}(q)$
$\displaystyle=\sum_{q<p^{t}}n_{q}g(\operatorname{ev}_{S}(q^{\mu})).$

Then by Lemma 4.21, there exists an $n\in C(S_{\mu},\mathbb{Z})$ such that

$\operatorname{ev}_{S}(p)=\pi_{\mu}^{*}(n)+\sum_{q<p^{t}}n_{q}(\operatorname{ev}_{S}(q^{\mu})).$

Now it suffices to show that each of the two terms in the sum above is in the
span of $\\{\operatorname{ev}_{S}(q)\ |\ q<p\\}$. The latter term is because
$q<p^{t}$ implies $q^{\mu}<p$. The former term is because we can write $n$ as
a linear combination indexed by $E(S_{\mu})$, and for $q\in E(S_{\mu})$ we
have
$\pi_{\mu}^{*}\left(\operatorname{ev}_{S_{\mu}}(q)\right)=\operatorname{ev}_{S}(q)$
and $\mu\notin q$ so $q<p$.

∎

######  Lemma 4.25.

The set $E(S)$ is the disjoint union of $E(S_{\mu})$ and

$E^{\prime}(S)=\\{p\in E(S)\ |\ \mu\in p\\}.$

###### Proof.

We already know by Lemma 4.6 that $E(S_{\mu})\subseteq E(S)$. Also, as noted
in Remark 4.5, if $p\in E(S_{\mu})$ then all elements of $p$ are $<\mu$ and
hence $p\notin E^{\prime}(S)$. Now it suffices to show that if $p\in
E(S)\setminus E^{\prime}(S)$, then $p\in E(S_{\mu})$.

Since $p\in E(S)\setminus E^{\prime}(S)$, every $i\in p$ satisfies $i<\mu$. We
have

$\operatorname{ev}_{S}(p)=\pi_{\mu}^{*}(\operatorname{ev}_{S_{\mu}}(p))$

and

$\operatorname{ev}_{S}\left(\\{q\in P\ |\
q<p\\}\right)=\pi_{\mu}^{*}\left(\operatorname{ev}_{S_{\mu}}\left(\\{q\in P\
|\ q<p\\}\right)\right)$

so if $\operatorname{ev}_{S_{\mu}}(p)$ is in the span of
$\operatorname{ev}_{S_{\mu}}\left(\\{q\in P\ |\ q<p\\}\right)$ then
$\operatorname{ev}_{S}(p)$ is in the span of
$\operatorname{ev}_{S}\left(\\{q\in P\ |\ q<p\\}\right)$, contradicting the
fact that $p\in E(S)$. ∎

The above lemmas prove all the claims made at the beginning of this section,
concluding the inductive proof.

##  5\. The formalisation

First a note on terminology: in the mathematical exposition of the proof in
section 4, we have talked about continuous maps from $S$ to $\mathbb{Z}$.
Since $\mathbb{Z}$ is discrete, these are the same as the locally constant
maps. The statement we have formalised is

⬇

theorem Nobeling (S : Profinite.{u}) :

Module.Free ℤ (LocallyConstant S ℤ)

which says that the $\mathbb{Z}$-module of locally constant maps from $S$ to
$\mathbb{Z}$ is free. When talking about locally constant maps, one does not
have to specify a topology on the target which is slightly more convenient
when working in a proof assistant.

The actual proof is about closed subsets of the product $\prod_{i\in
I}\\{0,1\\}$, which is of course the same thing as the space of functions
$I\to\\{0,1\\}$. We implement it as the type `I → Bool}, where
\mintinline`LeanBool is the type with two elements called `true} and
\mintinline`Leanfalse. This is the canonical choice for a two-element discrete
topological space in Mathlib.

###  5.1. The implementation of $P$ and $E(S)$

We implemented the type $P$ as follows:

⬇

def Products (I : Type*) [LinearOrder I] :=

{l : List I // l.Chain’ (·>·)}

The predicate `l.Chain’ (·>·)} means that adjacent elements of the list
\mintinline`Leanl are related by “$>$”. We define the evaluation
$\operatorname{ev}_{S}$ of products as

⬇

def Products.eval (S : Set (I → Bool)) (l : Products I) :

LocallyConstant S ℤ :=

(l.val.map (e S)).prod

where `l.val.map (e S)} is the list of $e_`S,i$for$i$inthelist\verb{l.val},
and \mintinline{Lean$List.prod is the product of the elements of a list. We
define a predicate on

    Products}
    \begin

minted[mathescape, numbersep=5pt, frame=lines, framesep=2mm]Lean def
Products.isGood (S : Set (I → Bool)) (l : Products I) : Prop := l.eval C ∉
Submodule.span ℤ ((Products.eval S) ” m — m ¡ l) and then the set $E(S)$
becomes

⬇

def GoodProducts (S : Set (I → Bool)) :

Set (Products I) :=

{l : Products I | l.isGood C}

It is slightly painful to prove completely trivial lemmas like 4.3 and its
corollary 4.4 in Lean. Indeed, these results are not mentioned in the proof of
[15, Theorem 5.4]. Although trivial, they are used often in the proof of the
theorem and hence very important to making the proof work. Reading an informal
proof of this theorem, one might never realise that these trivialities are
used. This is an example of a useful by-product of formalisation; more clarity
of exposition.

###  5.2. Ordinal induction

When formalising an inductive proof of any kind, one has to be very precise
about what statement one wants to prove by induction. This is almost never the
case in traditional mathematics texts. For example, the proof of [15, Theorem
5.4] claims to be proving by induction that $E(S)$ is a basis of
$C(S,\mathbb{Z})$, not just that it is linearly independent. Furthermore, the
set $I$ is not fixed throughout the inductive proof which makes it somewhat
unclear what the inductive hypothesis actually says. Working inside the
topological space $\prod_{i\in I}\\{0,1\\}$ for a fixed set $I$ throughout the
proof was convenient in the successor step. This avoided problems that are
solved by abuse of notation in informal texts, such as regarding a set as the
same thing as its image under a continuous embedding. The statement of the
induction principle for ordinals in Mathlib is the following222We have altered
the notation slightly to match the notation in this paper.:

⬇

def Ordinal.limitRecOn {Q : Ordinal → Sort _}

(o : Ordinal) (H₁ : Q 0) (H₂ : ∀ o, Q o → Q (succ o))

(H₃ : ∀ o, IsLimit o → (∀ o’ < o, Q o’)→ Q o) :

Q o

In our setting, given a map `Q : Ordinal → Prop} (in other words, a
\emph`predicate on ordinals)333`i`s `missing`, we can prove $Q(\mu)$ for any
ordinal $\mu$ if three things hold:

  * •

The zero case: $Q(0)$ holds.

  * •

The successor case: for all ordinals $\lambda$, $Q(\lambda)$ implies
$Q(\lambda+1)$.

  * •

The limit case: for every limit ordinal $\lambda$, if $Q(\lambda^{\prime})$
holds for every $\lambda^{\prime}<\lambda$, then $Q(\lambda)$ holds.

Finding the correct predicate $Q$ on ordinals was essential to the success of
this project:

⬇

def Q (I : Type*) [LinearOrder I] [IsWellOrder I (·<·)]

(o : Ordinal) : Prop :=

o ≤ Ordinal.type (·<· : I → I → Prop) →

(∀ (S : Set (I → Bool)), IsClosed S → contained S o →

LinearIndependent ℤ (GoodProducts.eval S))

The inequality

⬇

o ≤ Ordinal.type (·<· : I → I → Prop)

means that $o\leq I$ when $I$ is considered as an ordinal, and the proposition

    contained S o} is defined as
    \begin

minted[mathescape, numbersep=5pt, frame=lines, framesep=2mm]Lean def contained
I : Type* [LinearOrder I] [IsWellOrder I (·<·)] (S : Set (I → Bool)) (o :
Ordinal) : Prop := ∀ f, f ∈ S → ∀ (i : I), f i = true → ord I i < o and

    ord I i} is an abbreviation for
    \begin

minted[mathescape, numbersep=5pt, frame=lines, framesep=2mm]Lean
Ordinal.typein (·¡· : I → I → Prop) i i.e. the element $i\in I$ considered as
an ordinal. The conclusion

⬇

LinearIndependent ℤ (GoodProducts.eval S)

means that the map $\operatorname{ev}_{S}:E(S)\to C(S,\mathbb{Z})$ is linearly
independent. As is often the case, this is quite an involved statement that we
are proving by induction, and when writing informally, mathematicians wouldn’t
bother to specify the map

    Q : Ordinal → Prop} explicitly.
    \subsection

Piecewise defined locally constant maps In the proof of Lemma 4.21, we defined
a locally constant map $S_{\mu}\to\mathbb{Z}$ by giving locally constant maps
from $S_{0}$ and $\pi_{\mu}(S_{1})$ that agreed on the intersection, and
noting that this gives a locally constant map from the union which is equal to
$S_{\mu}$. To do this in Lean, the following definition was added to Mathlib :

⬇

def LocallyConstant.piecewise {X Z : Type*} [TopologicalSpace X]

{C₁ C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂)

(h : C₁ ∪ C₂ = Set.univ)

(f : LocallyConstant C₁ Z) (g : LocallyConstant C₂ Z)

(hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, hx.1⟩ = g ⟨x, hx.2⟩)

[∀ j, Decidable (j ∈ C₁)] :

LocallyConstant X Z where

toFun i := if hi : i ∈ C₁ then f ⟨i, hi⟩

else g ⟨i, (compl_subset_iff_union.mpr h) hi⟩

isLocallyConstant := omitted

It says that given locally constant maps $f$ and $g$ defined respectively on
closed subsets $C_{1}$ and $C_{2}$ which together cover the space $X$, such
that $f$ and $g$ agree on $C_{1}\cap C_{2}$, we get a locally constant map
defined on all of $X$. This seems like exactly what we need in the above-
mentioned proof. However, there is a subtlety, in that because of how the rest
of the inductive proof is structured, we want the sets $S_{0}$,
$\pi_{\mu}(S_{1})$ and $S_{\mu}$ all to be considered as subsets of the
underlying topological space $\prod_{i\in I}\\{0,1\\}$. To use
`LocallyConstant.piecewise}, we would have to consider $S_\mu$ as the
underlying topological space and $S_0$ and $\pi_\mu(S_1)$ as subsets of it.
This is possible and is what was done initially, but a cleaner solution is to
define a variant of \mintinline`LeanLocallyConstant.piecewise:

⬇

def LocallyConstant.piecewise’ {X Z : Type*} [TopologicalSpace X]

{C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂)

(h₁ : IsClosed C₁) (h₂ : IsClosed C₂)

(f₁ : LocallyConstant C₁ Z) (f₂ : LocallyConstant C₂ Z)

[DecidablePred (· ∈ C₁)]

(hf : ∀ x (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, hx.1⟩ = f₂ ⟨x, hx.2⟩) :

LocallyConstant C₀ Z

which satisfies the equality

⬇

lemma LocallyConstant.piecewise’_apply {X Z : Type*}

[TopologicalSpace X]

{C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂)

(h₁ : IsClosed C₁) (h₂ : IsClosed C₂)

(f₁ : LocallyConstant C₁ Z) (f₂ : LocallyConstant C₂ Z)

[DecidablePred (· ∈ C₁)]

(hf : ∀ x (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, hx.1⟩ = f₂ ⟨x, hx.2⟩)

(x : C₀) :

LocallyConstant.piecewise’ h₀ h₁ h₂ f₁ f₂ hf x =

if hx : x.val ∈ C₁ then f₁ ⟨x.val, hx⟩

else f₂ ⟨x.val, (or_iff_not_imp_left.mp (h₀ x.prop)) hx⟩

Here $C_{0},C_{1},$ and $C_{2}$ are subsets of the same underlying topological
space $X$; $C_{1}$ and $C_{2}$ are closed sets covering $C_{0}$, and $f_{1}$
and $f_{2}$ are locally constant maps defined on $C_{1}$ and $C_{2}$
respectively, such that $f_{1}$ and $f_{2}$ agree on the intersection. This
fits the application perfectly and shortened the proof of Lemma 4.21
considerably. Subtleties like this come up frequently, and can stall the
formalisation process, especially when formalising general topology. When
formalising Gleason’s theorem  (another result in general topology relevant to
condensed mathematics, see [15, Definition 2.4] and [8]), similar subtleties
arose about changing the “underlying topological space” to a subset of the
previous underlying topological space.

###  5.3. Reflections on the proof

The informal proof in [15] is about half a page; 21 lines of text. Depending
on how one counts (i.e. what parts of the code count as part of the proof and
not just prerequisites), the formalised proof is somewhere between 1500 and
3000 lines of Lean code. A big part of the difference is because of omissions
in the proof in [15]. A more fair comparison would be with the entirety of
section 4 in this paper, which is an account of all the mathematical contents
of the formalised proof. Still, there is quite a big difference, which is
mostly explained by the pedantry of proof assistants, as discussed in
subsections 5.2, 5.1, and 5.2.

##  6\. Mathlib integration

The development of this project took place on a branch of Mathlib, all code
being written in new files. This was a good workflow to get the formalisation
done as quickly as possible, because if new code is put in the “correct
places” immediately, one has to refresh file dependencies to be able to use
that code in other places. This means that part of Mathlib is rebuilt, which
can be a slow process if changes are made deep in the import hierarchy. As
this paper is being written, the project is in the process of integration into
Mathlib. A big pull request was opened, with all the code in one file. Then
code of independent interest outside the proof of Nöbeling’s theorem was moved
to the top of the file, split into sections where each section became a
smaller pull request. As those pull requests are merged into the master branch
of Mathlib, the code at the top of the file is removed. When there is nothing
left in the file but code relevant only to the proof, the original pull
request will be ready for review and eventually being integrated into Mathlib.
As discussed in recent papers by Nash [12] and Best et al. [4], when
formalising mathematics in Lean, it is desirable to develop as much as
possible directly against Mathlib. Otherwise, the code risks going stale and
unusable, while if integrated into Mathlib it becomes part of a library that
is continuously maintained. The workflow described above, which means not
making any pull requests to Mathlib until the formalisation is done, works
well for small to medium-sized projects like this one. Especially in cases
like ours, where most ingredients in the proof will probably not be usable
elsewhere in the library. However, once the projects get much bigger, it
becomes very difficult to find a good workflow. Integrating everything
continuously into Mathlib while developing the project is en extremely slow
process. On the other hand, moving a huge, complete project into Mathlib is
not an ideal solution either.

##  7\. Towards condensed mathematics in Mathlib

The history of condensed mathematics in Lean started with the _Liquid Tensor
Experiment_ (LTE) [6, 16]. This is an example of a formalisation project that
was in some sense too big to be integrated into Mathlib. Nevertheless, it was
a big success in that it demonstrated the capabilities of Lean and its
community by fully formalising the complicated proof of a highly nontrivial
theorem about so-called liquid modules. Moreover, it provided a setting in
which to experiment with condensed mathematics and find the best way to do
homological algebra in Lean. As mentioned above, the goal of LTE was to
formalise one specialised theorem. This is somewhat orthogonal to the goal of
Mathlib which is to build a coherent, unified library of formalised
mathematics. It is thus understandable that the contributors of LTE chose to
focus on completing the task at hand instead of spending time on moving some
parts of the code to Mathlib. Now that both LTE and the port of Mathlib to
Lean 4 have been completed, we are seeing some important parts of LTE being
integrated into Mathlib. The definition  of a condensed object was recently
added to Mathlib. During a masterclass on formalisation of condensed
mathematics organised in Copenhagen in June 2023, participants collaborated,
under the guidance of Kevin Buzzard and Adam Topaz, on formalising as much
condensed mathematics as possible in one week (all development took place in
Lean 4 and the goal was to write material for Mathlib). The code can be found
in the masterclass GitHub repository  and some of it (mostly material about
the category of extremally disconnected compact Hausdorff spaces, an important
part of the basic theory of condensed mathematics) has already made it into
Mathlib. Profinite spaces form a rich category of topological spaces and there
is more work other than Nöbeling’s theorem to be done in Mathlib. Being the
building blocks of condensed sets, it is important to develop a good API for
profinite spaces in Mathlib. There, profinite spaces are defined as totally
disconnected compact Hausdorff spaces. It is proved  that every profinite
space can be expressed as a cofiltered limit (more precisely, over the poset
of its discrete quotients). It is also proved  that the category of profinite
spaces has all limits and that the forgetful functor to topological spaces
preserves them . From this we can extract the following useful theorem:

######  Theorem 7.1.

A topological space is profinite if and only if it can be written as a
cofiltered limit of finite discrete spaces.

The story about profinite spaces as limits does not end there, though.
Sometimes it is not enough to know just that some profinite space _can_ be
written as _a_ limit, but rather that there is a specific limit formula for
it. Lemma 4.10 gives one specific way of writing a compact subset of a product
as a cofiltered limit, which can be useful. Another example can be extracted
from [1]. This is the fact that the identity functor on the category of
profinite spaces is right Kan extended from the inclusion functor from finite
sets to profinite spaces along itself. This gives another limit formula for
profinite spaces, coming from the limit formula for right Kan extensions, and
is useful when formalising the definition of solid abelian groups [2].

##  8\. Conclusion and future work

By formalising Nöbeling’s theorem, we have illustrated that the induction
principle for ordinals in Mathlib can be used to prove nontrivial theorems
outside the theory ordinals themselves. Another contribution is the detailed
proof given in section 4, and of course as mentioned before, it is an
important step for the formalisation of condensed mathematics to continue. A
natural next step in the formalisation of the theory of solid abelian groups
is to port the code in [1, 2] to Lean 4 and get it into Mathlib. Then one can
put together the discreteness characterisation and Nöbeling’s theorem to prove
the structural results about $\mathbb{Z}[S]^{\rule[0.36pt]{3.5pt}{3.5pt}}$,
which would lead us one step closer to an example of a nontrivial solid
abelian group in Mathlib. More broadly, it is important to continue moving as
much as possible of the existing Lean code about condensed mathematics (from
the LTE and the Copenhagen masterclass) into Mathlib.

## References

  * Asgeirsson [2023a] Dagur Asgeirsson.  Formalising discrete condensed sets.  https://github.com/dagurtomas/lean-solid/tree/discrete, 2023a.
  * Asgeirsson [2023b] Dagur Asgeirsson.  Formalising solid abelian groups.  https://github.com/dagurtomas/lean-solid/, 2023b.
  * Barwick and Haine [2019] Clark Barwick and Peter Haine.  Pyknotic objects, i. basic notions, 2019.
  * Best et al. [2023] Alex J. Best, Christopher Birkbeck, Riccardo Brasca, and Eric Rodriguez Boidi.  Fermat’s Last Theorem for Regular Primes.  In Adam Naumowicz and René Thiemann, editors, _14th International Conference on Interactive Theorem Proving (ITP 2023)_ , volume 268 of _Leibniz International Proceedings in Informatics (LIPIcs)_ , pages 36:1–36:8, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  ISBN 978-3-95977-284-6.  doi: 10.4230/LIPIcs.ITP.2023.36.  URL https://drops.dagstuhl.de/opus/volltexte/2023/18411.
  * Clausen and Scholze [2022] Dustin Clausen and Peter Scholze.  Condensed mathematics and complex geometry.  https://people.mpim-bonn.mpg.de/scholze/Complex.pdf, 2022.
  * et al. [2022] Johan Commelin, Adam Topaz et al.  Liquid tensor experiment.  https://github.com/leanprover-community/lean-liquid, 2022.
  * Fuchs [1970] László Fuchs.  _Infinite Abelian Groups_.  ISSN. Elsevier Science, 1970.  ISBN 9780080873480.
  * Gleason [1958] Andrew M. Gleason.  Projective topological spaces.  _Illinois Journal of Mathematics_ , 2(4A):482 – 489, 1958.  doi: 10.1215/ijm/1255454110.  URL https://doi.org/10.1215/ijm/1255454110.
  * mathlib Community [2020] The mathlib Community.  The lean mathematical library.  In _Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs_ , CPP 2020, page 367–381, New York, NY, USA, 2020. Association for Computing Machinery.  ISBN 9781450370974.  doi: 10.1145/3372885.3373824.  URL https://doi.org/10.1145/3372885.3373824.
  * Moura and Ullrich [2021] Leonardo de Moura and Sebastian Ullrich.  The lean 4 theorem prover and programming language.  In André Platzer and Geoff Sutcliffe, editors, _Automated Deduction – CADE 28_ , pages 625–635, Cham, 2021. Springer International Publishing.  ISBN 978-3-030-79876-5.
  * Moura et al. [2015] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer.  The lean theorem prover (system description).  In Amy P. Felty and Aart Middeldorp, editors, _Automated Deduction - CADE-25_ , pages 378–388, Cham, 2015. Springer International Publishing.  ISBN 978-3-319-21401-6.
  * Nash [2023] Oliver Nash.  A Formalisation of Gallagher’s Ergodic Theorem.  In Adam Naumowicz and René Thiemann, editors, _14th International Conference on Interactive Theorem Proving (ITP 2023)_ , volume 268 of _Leibniz International Proceedings in Informatics (LIPIcs)_ , pages 23:1–23:16, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.  ISBN 978-3-95977-284-6.  doi: 10.4230/LIPIcs.ITP.2023.23.  URL https://drops.dagstuhl.de/opus/volltexte/2023/18398.
  * Nöbeling [1968] Georg Nöbeling.  Verallgemeinerung eines Satzes von Herrn E. Specker.  _Invent. Math._ , 6:41–55, 1968.  ISSN 0020-9910,1432-1297.  doi: 10.1007/BF01389832.  URL https://doi.org/10.1007/BF01389832.
  * Scholze [2019a] Peter Scholze.  Lectures on analytic geometry.  http://www.math.uni-bonn.de/people/scholze/Analytic.pdf, 2019a.
  * Scholze [2019b] Peter Scholze.  Lectures on condensed mathematics.  https://www.math.uni-bonn.de/people/scholze/Condensed.pdf, 2019b.
  * Scholze [2022] Peter Scholze.  Liquid tensor experiment.  _Experimental Mathematics_ , 31(2):349–354, 2022\.  doi: 10.1080/10586458.2021.1926016.  URL https://doi.org/10.1080/10586458.2021.1926016.


# Proportion of blocking curves in a pencil

Shamil Asgarli  Department of Mathematics and Computer Science
Santa Clara University
500 El Camino Real
USA 95053<EMAIL_ADDRESS>,  Dragos Ghioca  Department of Mathematics
University of British Columbia
1984 Mathematics Road
Canada V6T 1Z2<EMAIL_ADDRESS>and  Chi Hoi Yip  Department of
Mathematics
University of British Columbia
1984 Mathematics Road
Canada V6T 1Z2<EMAIL_ADDRESS>
###### Abstract.

Let $\mathcal{L}$ be a pencil of plane curves defined over $\mathbb{F}_{q}$
with no $\mathbb{F}_{q}$-points in its base locus. We investigate the number
of curves in $\mathcal{L}$ whose $\mathbb{F}_{q}$-points form a blocking set.
When the degree of the pencil is allowed to grow with respect to $q$, we show
that the geometric problem can be translated into a purely combinatorial
problem about disjoint blocking sets. We also study the same problem when the
degree of the pencil is fixed.

###### Key words and phrases:

Pencil, plane curves, blocking sets, finite field

###### 2020 Mathematics Subject Classification:

Primary: 14H50, 51E21; Secondary: 14C21, 14N05, 14G15, 51E20

##  1\. Introduction

Throughout the paper, $p$ denotes a prime, $q$ denotes a power of $p$, and
$\mathbb{F}_{q}$ denotes the finite field with $q$ elements. Recall that a set
of points $B\subseteq\mathbb{P}^{2}(\mathbb{F}_{q})$ is a _blocking set_ if
every $\mathbb{F}_{q}$-line meets $B$. For example, a union of $q+1$ distinct
$\mathbb{F}_{q}$-points on a line forms a blocking set. A blocking set $B$ is
_trivial_ if it contains all the $q+1$ points of a line, and is _nontrivial_
if it is not a trivial blocking set. Blocking sets have been studied
extensively in finite geometry and design theory.

Inspired by the rich interaction between finite geometry and algebraic curves
[SS98], the concept of blocking curves was formally introduced in [AGY22].
Given a projective plane curve $C\subset\mathbb{P}^{2}$ defined over
$\mathbb{F}_{q}$, recall that $C(\mathbb{F}_{q})$ denotes the set of
$\mathbb{F}_{q}$-rational points on $C$. We say that $C$ is a _blocking curve_
if $C(\mathbb{F}_{q})$ is a blocking set; otherwise, it is _nonblocking_.
Moreover, $C$ is _nontrivially blocking_ if $C(\mathbb{F}_{q})$ is a
nontrivial blocking set.

In our previous papers [AGY22] and [AGY22b], we showed that irreducible
blocking curves of low degree $d$ (namely, satisfying $d^{6}<q$) do not exist,
and that blocking curves of high degree are rare. In other words, our past
results suggest that a random curve over $\mathbb{F}_{q}$ is very likely to be
nonblocking. These results rely on combinatorial properties of blocking sets
as well as tools from algebraic geometry and arithmetic statistics. The main
purpose of this paper is to understand a refined distribution of nonblocking
curves by asking the following question:

######  Question 1.1.

Let $\mathcal{L}=\langle F,G\rangle$ be a pencil of plane curves such that
$\\{F=0\\}$ and $\\{G=0\\}$ have no common $\mathbb{F}_{q}$-points. Is there a
quantitative lower bound for the number of curves in $\mathcal{L}$ defined
over $\mathbb{F}_{q}$ which are nonblocking?

To elaborate further, let $\mathcal{L}=\langle F,G\rangle$ be a pencil that
has no $\mathbb{F}_{q}$-points in its base locus. We refer to Example 3.1
which illustrates that the condition on the base locus is natural and
necessary. Given such a pencil, consider the $q+1$ curves

$C_{[s:t]}=\\{sF+tG=0\\}$

where $[s:t]$ ranges in $\mathbb{P}^{1}(\mathbb{F}_{q})$. These curves will be
called _$\mathbb{F}_{q}$ -members_ of $\mathcal{L}=\langle F,G\rangle$. Since
$\mathcal{L}$ has no $\mathbb{F}_{q}$-points in its base locus, the sets of
$\mathbb{F}_{q}$-rational points on these $q+1$ curves are pairwise disjoint
and cover all the $\mathbb{F}_{q}$-points of the plane. Indeed, if
$P\in\mathbb{P}^{2}(\mathbb{F}_{q})$ is any $\mathbb{F}_{q}$-point, it belongs
to a unique member $C_{[s:t]}$ with $[s:t]=[-G(P):F(P)]$. In summary, the
collection of sets
$\\{C_{[s:t]}(\mathbb{F}_{q})\\}_{[s:t]\in\mathbb{P}^{1}(\mathbb{F}_{q})}$
forms a partition of $\mathbb{P}^{2}(\mathbb{F}_{q})$ into $q+1$ parts, with
the understanding that some of the parts may be empty. We will say that the
pencil $\mathcal{L}$ _induces_ the partition
$\\{C_{[s:t]}(\mathbb{F}_{q})\\}_{[s:t]\in\mathbb{P}^{1}(\mathbb{F}_{q})}$.

Let us explain a heuristic that suggests a plausible answer to Question 1.1.
Since there are $q+1$ distinct $\mathbb{F}_{q}$-members of $\mathcal{L}$, and
together they cover $q^{2}+q+1$ points, it follows that the average number of
$\mathbb{F}_{q}$-points on a given $\mathbb{F}_{q}$-member of $\mathcal{L}$ is
exactly:

$\frac{q^{2}+q+1}{q+1}<q+1.$

Since there does not exist a blocking set with less than $q+1$ points, it is
immediate that $\mathcal{L}$ contains at least one nonblocking curve. Note
that the averaging argument does not tell us whether or not the “median”
number of points on a random $\mathbb{F}_{q}$-member in $\mathcal{L}$ is less
than $q+1$. Nevertheless, it is natural to ask whether at least half of the
$\mathbb{F}_{q}$-members in the pencil must be nonblocking. Making this last
question slightly weaker, we may instead ask the following.

######  Question 1.2.

Let $\mathcal{L}=\langle F,G\rangle$ be a pencil of plane curves such that
$\\{F=0\\}$ and $\\{G=0\\}$ have no common $\mathbb{F}_{q}$-points. Does there
exist a universal constant $c_{0}>0$ such that at least $c_{0}q$ distinct
$\mathbb{F}_{q}$-members of $\mathcal{L}$ are nonblocking?

Using Blokhuis’ theorem [B94] that a nontrivial blocking set over
$\mathbb{F}_{p}$ has at least $\frac{3}{2}(p+1)$, it can be shown that
Question 1.2 has a positive answer when $p$ is prime, and in fact, $c_{0}=1/3$
works in this case. See Remark 3.4 for further details.

However, Question 1.2 turns out to have a negative answer in general.

######  Theorem 1.3.

Let $q=p^{n}$ be a prime power with $n$ even. There exists a pencil of plane
curves over $\mathbb{F}_{q}$ with no $\mathbb{F}_{q}$-points in its base locus
which contains only $\sqrt{q}$ many nonblocking curves.

The key ingredient in the proof of Theorem 1.3 is to establish the connection
between Question 1.2 and the question of determining the maximum number of
disjoint blocking sets in $\mathbb{P}^{2}(\mathbb{F}_{q})$, first studied by
Beutelspacher and Eugeni [BE86]. The latter question can be formulated more
generally and abstractly in the setting of hypergraph coloring; see [BMPS06]
for related discussions. We will prove in Proposition 3.2 that every pencil
with no $\mathbb{F}_{q}$-points in its base locus has at least $\sqrt{q}$ many
nonblocking curves, so Theorem 1.3 is sharp.

In Question 1.2, the constant $c_{0}>0$ is required to be universal. If we
allow the constant to depend on the degree of the curves, then Question 1.2
has a positive answer. More precisely, we will prove the following effective
result.

######  Theorem 1.4.

Given a pencil of plane curves of degree $d\leq q$ in $\mathbb{P}^{2}$ defined
over $\mathbb{F}_{q}$ with no $\mathbb{F}_{q}$-points in its base locus, at
least $\frac{q+1}{d+1}$ distinct $\mathbb{F}_{q}$-members of the pencil are
nonblocking curves.

The inequality $d\leq q$ in the hypothesis is natural. Indeed, if $d>q$, then
$0<\frac{q+1}{d+1}<1$, and the conclusion still holds, because we have already
seen above that the pencil must have at least one nonblocking
$\mathbb{F}_{q}$-member.

### Outline of the paper.

In Section 2, we show that every partition of the $q^{2}+q+1$ points of
$\mathbb{P}^{2}(\mathbb{F}_{q})$ into $q+1$ sets can be realized by a pencil
of plane curves. This key result Proposition 2.1 allows us to prove our main
Theorem 1.3 in Section 3. We discuss the case of fixed degree pencils and
prove Theorem 1.4 in Section 4.

##  2\. Realizing partitions by pencils of curves

The goal of this section is to prove the following result, which shows that
any partition of $\mathbb{P}^{2}(\mathbb{F}_{q})$ into $q+1$ sets (where some
sets could be empty) is induced by a pencil of plane curves.

######  Proposition 2.1.

Suppose $U_{1},U_{2},\dots,U_{q+1}$ form a partition of
$\mathbb{P}^{2}(\mathbb{F}_{q})$. Then there exists a pencil of curves
$\mathcal{L}=\langle F,G\rangle$ whose base locus has no
$\mathbb{F}_{q}$-points such that $\mathcal{L}$ induces the partition
$\\{U_{i}\\}_{i=1}^{q+1}$.

The proof of Proposition 2.1 relies on two lemmas.

######  Lemma 2.2.

Given any $Q\in\mathbb{P}^{2}(\mathbb{F}_{q})$, there exists a homogeneous
polynomial $S_{Q}\in\mathbb{F}_{q}[x,y,z]$ of degree $3(q-1)$ such that
$S_{Q}(Q)=1$, while $S_{Q}(P)=0$ for each point $P\neq Q$ in
$\mathbb{P}^{2}(\mathbb{F}_{q})$.

###### Proof.

Suppose $Q:=[a_{0}:b_{0}:c_{0}]\in\mathbb{P}^{2}(\mathbb{F}_{q})$. Without
loss of generality, we may assume that $c_{0}\neq 0$. Let $L_{1}$ and $L_{2}$
be two (distinct) $\mathbb{F}_{q}$-lines passing through the point $Q$; we let
their equations be $\alpha_{1}x+\beta_{1}+\gamma_{1}z=0$ and
$\alpha_{2}x+\beta_{2}y+\gamma_{2}z=0$ for some
$\alpha_{i},\beta_{i},\gamma_{i}\in\mathbb{F}_{q}$. Consider the homogeneous
polynomial $S_{Q}$ of degree $3(q-1)$ given by

$S_{Q}(x,y,z)=z^{q-1}\cdot\left(z^{q-1}-(\alpha_{1}x+\beta_{1}y+\gamma_{1}z)^{q-1}\right)\cdot\left(z^{q-1}-(\alpha_{2}x+\beta_{2}y+\gamma_{2}z)^{q-1}\right).$

Since $z$-coordinate of $Q$ is nonzero by assumption, we get $S_{Q}(Q)=1$. On
the other hand, $S_{Q}(P)=0$ for each point $P\neq Q$ in
$\mathbb{P}^{2}(\mathbb{F}_{q})$. Indeed, given such a point
$P=[a_{1}:b_{1}:c_{1}]$, we have two cases: $c_{1}=0$ and $c_{1}\neq 0$. If
$c_{1}=0$, then $S_{Q}(P)=0$ is immediate. If $c_{1}\neq 0$, then $P$ cannot
be on both $L_{1}$ and $L_{2}$, and we again obtain $S_{Q}(P)=0$. ∎

######  Remark 2.3.

In Lemma 2.2, we arranged $S_{Q}$ to have degree divisible by $q-1$. This
allows us to view $S_{Q}$ as a well-defined function
$\mathbb{P}^{2}(\mathbb{F}_{q})\longrightarrow\mathbb{F}_{q}$. Indeed, if
$[x_{0}:y_{0}:z_{0}]$ and $[x_{1}:y_{1}:z_{1}]$ represent the same point in
$\mathbb{P}^{2}(\mathbb{F}_{q})$, then $(x_{1},y_{1},z_{1})=(\lambda
x_{0},\lambda y_{0},\lambda z_{0})$ for some
$\lambda\in\mathbb{F}_{q}^{\ast}$. As a result,
$S_{Q}(x_{1},y_{1},z_{1})=\lambda^{3(q-1)}S_{Q}(x_{0},y_{0},z_{0})=S_{Q}(x_{0},y_{0},z_{0})$,
confirming that $S_{Q}$ is a well-defined function on
$\mathbb{P}^{2}(\mathbb{F}_{q})$.

######  Lemma 2.4.

For any function
$f\colon\mathbb{P}^{2}(\mathbb{F}_{q})\longrightarrow\mathbb{F}_{q}$ which is
not identically zero, there exists a homogeneous polynomial
$R_{f}\in\mathbb{F}_{q}[x,y,z]$ of degree $3(q-1)$ such that
$R_{f}(a,b,c)=f([a:b:c])$ for each $[a:b:c]\in\mathbb{P}^{2}(\mathbb{F}_{q})$.

###### Proof.

Borrowing the notation from Lemma 2.2, we set

$R_{f}\colonequals\sum_{Q\in\mathbb{P}^{2}(\mathbb{F}_{q})}f(Q)\cdot S_{Q}$

which satisfies the desired condition. ∎

We have now gathered the tools to prove Proposition 2.1.

###### Proof of Proposition 2.1.

Given a partition of $\mathbb{P}^{2}(\mathbb{F}_{q})$ into $q+1$ sets
$U_{1},\ldots,U_{q+1}$, there exists a function
$\varphi:\mathbb{P}^{2}(\mathbb{F}_{q})\longrightarrow\mathbb{P}^{1}(\mathbb{F}_{q})$
with the property that the preimages $\varphi^{-1}(Q)$ for the $q+1$ points
$Q\in\mathbb{P}^{1}(\mathbb{F}_{q})$ provide exactly the same partition of
$\mathbb{P}^{2}(\mathbb{F}_{q})$ as $U_{1},\ldots U_{q+1}$. We can find two
functions $f\colon\mathbb{P}^{2}(\mathbb{F}_{q})\longrightarrow\mathbb{F}_{q}$
and $g\colon\mathbb{P}^{2}(\mathbb{F}_{q})\longrightarrow\mathbb{F}_{q}$ such
that for each $P\in\mathbb{P}^{2}(\mathbb{F}_{q})$,

$\varphi(P)=[f(P):g(P)].$ (1)

By Lemma 2.4, we have two homogeneous polynomials $R_{f}$ and $R_{g}$ both of
degree $3(q-1)$ which induce $f$ and $g$, respectively.

Let $F=-R_{g}$ and $G=R_{f}$. We claim that the pencil $\mathcal{L}=\langle
F,G\rangle$ induces the partition $U_{1},\ldots U_{q+1}$. First, $\mathcal{L}$
has no $\mathbb{F}_{q}$-points in its base locus since $f(P)$ and $g(P)$
cannot be zero simultaneously for any $P\in\mathbb{P}^{2}(\mathbb{F}_{q})$ by
(1). Next, for any $[u:v]\in\mathbb{P}^{1}$ and a point $P\in\mathbb{P}^{2}$,
we have

$uF(P)+vG(P)=0\ \ \Longleftrightarrow\ \
[u:v]=[G(P):-F(P)]=[f(P):g(P)]=\varphi(P).$

Thus, a given $\mathbb{F}_{q}$-point $P$ belongs to the
$\mathbb{F}_{q}$-member of the pencil $\mathcal{L}$ parametrized by
$[u:v]\in\mathbb{P}^{1}(\mathbb{F}_{q})$ if and only if
$P\in\phi^{-1}([u:v])$. Consequently, the sets of $\mathbb{F}_{q}$-points
contained in the $q+1$ distinct $\mathbb{F}_{q}$-members of the pencil
$\mathcal{L}=\langle F,G\rangle$ precisely correspond to the partition
$U_{1},\ldots,U_{q+1}$. ∎

######  Remark 2.5.

It is possible to generalize Proposition 2.1 where $U_{1},U_{2},...,U_{q+1}$
together cover $\mathbb{P}^{2}(\mathbb{F}_{q})$, although they are no longer
assumed to be pairwise disjoint. In order to obtain a pencil of curves that
induces the sets $U_{1},U_{2},...,U_{q+1}$, it is necessary that the equality

$U_{i}\cap U_{j}=B\colonequals\bigcap_{k=1}^{q+1}U_{k}$

is satisfied for each $i\neq j$. Under this assumption, one can prove that
there exists a pencil $\mathcal{L}$ of plane curves with
$\mathbb{F}_{q}$-members $C_{1},C_{2},...,C_{q+1}$ such that
$C_{i}(\mathbb{F}_{q})=U_{i}$ for each $1\leq i\leq q+1$. The proof is almost
identical to the current proof of Proposition 2.1. We start by picking

$\varphi\colon\mathbb{P}^{2}(\mathbb{F}_{q})\setminus
B\longrightarrow\mathbb{P}^{1}(\mathbb{F}_{q})$

so that the preimages $\varphi^{-1}(\alpha_{i})$ of the points
$\alpha_{1},...,\alpha_{q+1}$ in $\mathbb{P}^{1}(\mathbb{F}_{q})$ coincide
with the pairwise disjoint sets $U_{i}\setminus B$ for $i=1,..,q+1$. By using
Lemma 2.4, we can find homogeneous polynomials $F$ and $G$ which both vanish
on $B$ such that the pencil $\mathcal{L}=\langle F,G\rangle$ satisfies the
desired properties.

##  3\. Lower bounds on the number of nonblocking curves

The averaging argument presented in the introduction showed that if a pencil
of plane curves has no $\mathbb{F}_{q}$-points in its base locus, there must
be at least one nonblocking curve in the pencil. We explain what happens when
the hypothesis on the base locus is dropped. If the set of
$\mathbb{F}_{q}$-points of the base locus is itself a blocking set, then
clearly all the curves in the pencil are blocking. Additional examples of
pencils whose $\mathbb{F}_{q}$-members are all blocking can be constructed
using the explicit families of blocking curves in [AGY22]*Proposition 6.1; in
such pencils, the base locus may have a large number of
$\mathbb{F}_{q}$-points. It may be tempting to believe that there should be at
least some nonblocking curves if the base locus is small. However, we will now
exhibit a pencil $\mathcal{L}$ of plane curves of degree $d\geq 2$ over
$\mathbb{F}_{q}$ containing _exactly one_ $\mathbb{F}_{q}$-point in its base
locus such that every $\mathbb{F}_{q}$-member of $\mathcal{L}$ is a blocking
curve. This example shows that the hypothesis that the base locus has no
$\mathbb{F}_{q}$-points cannot be relaxed.

######  Example 3.1.

Let $m=\max\\{0,q-3\\}$ and consider the polynomial $H(x,y,z)$ of degree
$q^{2}+q+1$ which is the product of all linear polynomials $ax+by+cz$, where
$[a:b:c]\in\mathbb{P}^{2}(\mathbb{F}_{q})$. Let

$\displaystyle F(x,y,z)=x^{m}H(x,y,z)+y^{q^{2}+q+1+m}$

and

$\displaystyle G(x,y,z)=x^{m}H(x,y,z)+z^{q^{2}+q+1+m}.$

Then the only $\mathbb{F}_{q}$-point in the intersection of $\\{F=0\\}$ and
$\\{G=0\\}$ is $[1:0:0]$. Thus, $\mathcal{L}=\langle F,G\rangle$ is a pencil
of plane curves with exactly one $\mathbb{F}_{q}$-point in its base locus.
However, for each $[a:b]\in\mathbb{P}^{1}(\mathbb{F}_{q})$, the curve
$C_{[a:b]}=\\{aF+bG=0\\}$ intersects any given $\mathbb{F}_{q}$-line $L$ at
some $\mathbb{F}_{q}$-point. Indeed, specializing $aF+bG=0$ along the line $L$
yields to

$ay^{q^{2}+q+1+m}+bz^{q^{2}+q+1+m}=0.$ (2)

Since $m$ was chosen so that $\gcd(q-1,q^{2}+q+1+m)=1$, the map $t\mapsto
t^{q^{2}+q+1+m}$ is an automorphism of the cyclic group
$(\mathbb{F}_{q}^{*},\cdot)$. Thus, regardless of the line $L$ along which we
specialize, the equation (2) has a nonzero solution (that is, not both $y$ and
$z$ are zero) in $\mathbb{F}_{q}$ for each
$[a:b]\in\mathbb{P}^{1}(\mathbb{F}_{q})$. Consequently, every
$\mathbb{F}_{q}$-member of $\mathcal{L}$ is a blocking curve.

An alternative construction can be carried out by using the generalized
version of Proposition 2.1 (see Remark 2.5) where $U_{1},U_{2},...,U_{q+1}$
consist of $\mathbb{F}_{q}$-points of $q+1$ distinct lines passing through a
common point. The pencil produced using that method will have degree $3(q-1)$.

We have seen that having even a single $\mathbb{F}_{q}$-point in the base
locus may result in all of the $\mathbb{F}_{q}$-members to be blocking curves.
Thus, for the remainder of the paper, we will work under the hypothesis that
there are no $\mathbb{F}_{q}$-points in the base locus of a given pencil. Our
first quantitative lower bound on the number of nonblocking curves is implicit
in the finite geometry literature [BE86]*Theorem 2.2. We include a simple
proof for a sake of completeness; the ideas and notation used in this proof
will also be needed in the remarks that follow.

######  Proposition 3.2.

Every pencil of plane curves over $\mathbb{F}_{q}$ with no $\mathbb{F}_{q}$
points in its base locus has at least $\sqrt{q}$ many $\mathbb{F}_{q}$-members
which are nonblocking.

###### Proof.

Let $\mathcal{L}=\langle F,G\rangle$ be a pencil of plane curves with no
$\mathbb{F}_{q}$-members in its base locus. If $\mathcal{L}$ has an
$\mathbb{F}_{q}$-member $C$ whose $\mathbb{F}_{q}$-rational points which is a
trivial blocking set, then there exists an $\mathbb{F}_{q}$-line $L$ such that
$L(\mathbb{F}_{q})\subseteq C(\mathbb{F}_{q})$. In this case, the other $q$
members of $\mathcal{L}$ will be nonblocking by virtue of being disjoint from
$L(\mathbb{F}_{q})$. Thus, we may assume that each $\mathbb{F}_{q}$-member of
the pencil is not trivially blocking.

Suppose we have $m$ blocking and $q+1-m$ nonblocking $\mathbb{F}_{q}$-members
of $\mathcal{L}$. Since a nontrivial blocking set has at least $q+\sqrt{q}+1$
points [B71], the following inequality holds:

$m(q+\sqrt{q}+1)\leq\sum_{\begin{subarray}{c}C\text{ is
}\mathbb{F}_{q}\text{-member of }\mathcal{L}\\\ C\text{ is
blocking}\end{subarray}}\\#C(\mathbb{F}_{q})\leq\sum_{C\text{ is
}\mathbb{F}_{q}\text{-member of }\mathcal{L}}\\#C(\mathbb{F}_{q})=q^{2}+q+1.$

It follows that,

$m\leq\frac{q^{2}+q+1}{q+\sqrt{q}+1}=q-\sqrt{q}+1$

Thus, the number of nonblocking $\mathbb{F}_{q}$-members is
$q+1-m\geq\sqrt{q}$, as desired. ∎

As a complement to the previous proposition, we now present a quick proof of
Theorem 1.3 which guarantees the existence of a pencil which has exactly
$\sqrt{q}$ many nonblocking members. Recall that if $q$ is a square, a Baer
subplane in $\mathbb{P}^{2}(\mathbb{F}_{q})$ is a subplane with size
$q+\sqrt{q}+1$. It is well-known that Baer subplanes are blocking sets.

###### Proof of Theorem 1.3.

Since $q$ is a square, it is known that that $\mathbb{P}^{2}(\mathbb{F}_{q})$
can be partitioned into

$\frac{q^{2}+q+1}{q+\sqrt{q}+1}=q-\sqrt{q}+1$

Baer subplanes [H79]*Theorem 4.3.6. Now, Proposition 2.1 implies that we can
find a pencil of curves which has exactly $\sqrt{q}$ many
$\mathbb{F}_{q}$-members which are nonblocking. ∎

######  Remark 3.3.

When $q$ is a square, we have seen that the number of nonblocking curves in a
pencil must be at least $\sqrt{q}$, and this lower bound is sharp. When $q$ is
not a square, we know each nontrivial blocking set has size at least
$q+1+cq^{2/3}$ [BSS99], so the same argument in Proposition 3.2 can be adapted
to show that there are at least $c^{\prime}q^{2/3}$ many nonblocking
$\mathbb{F}_{q}$-members in any pencil with no $\mathbb{F}_{q}$-points in its
base locus. This can be seen by mimicking the same proof as in Proposition 3.2
to get the following upper bound on the number of blocking curves in the given
pencil:

$\frac{q^{2}+q+1}{q+1+q^{2/3}}=\frac{q^{2}+q-q^{4/3}}{q+1+q^{2/3}}+\frac{q^{4/3}}{q+1+q^{2/3}}\approx
q+1-q^{2/3}+\frac{q^{4/3}}{q+1+q^{2/3}}\approx q+1-q^{2/3}+q^{1/3}.$

######  Remark 3.4.

When $q=p$ is prime, we can improve the lower bound in Proposition 3.2
significantly by relying on Blokhuis’ theorem that a nontrivial blocking set
in $\mathbb{P}^{2}(\mathbb{F}_{p})$ has at least $\frac{3}{2}(p+1)$ points
[B94]. By imitating the proof of Proposition 3.2, we see that the number of
blocking curves satisfies
$m\leq\frac{p^{2}+p+1}{\frac{3}{2}(p+1)}<\frac{2}{3}(p+1)$. It follows that
the number of nonblocking curves is $p+1-m\geq\frac{1}{3}(p+1)$, thereby
answering Question 1.2 affirmatively in the case when $q=p$ is a prime. On the
other hand, it is possible to construct $(1/3-o(1))p$ disjoint blocking sets
in $\mathbb{P}^{2}(\mathbb{F}_{p})$ [BMPS06]. Thus, Proposition 2.1 implies
the existence of a pencil with at least $1/3$ members being blocking, or
equivalently, at most $2/3$ members are nonblocking. It is conjectured by
Kriesell that $\mathbb{P}^{2}(\mathbb{F}_{q})$ can be partitioned into
$\lfloor q/2\rfloor$ blocking sets (he verified the conjecture for $q\leq 8$)
[BMPS06]*Page 150, so the best possible constant in Question 1.2 is
conjecturally $1/2$ (when $q=p$ is prime).

######  Remark 3.5.

Szőnyi [S97]*Theorem 5.7 showed if $q=p^{2}$ with $p$ prime, a nontrivial
blocking set in $\mathbb{P}^{2}(\mathbb{F}_{q})$ that avoids Baer subplanes
has size at least $3(q+1)/2$. Note that this result is analogous to Blokhuis’
result over $\mathbb{F}_{p}$ with $p$ prime. Let us explain how this
observation helps us answer Question 1.2 affirmatively in the case $q=p^{2}$
for certain pencils.

We say that a pencil of curves over $\mathbb{F}_{q}$ is _generic_ if the
number of singular members (defined over the algebraic closure
$\overline{\mathbb{F}_{q}}$) is finite. The terminology is justified by the
fact that a generic line (over $\overline{\mathbb{F}_{q}}$) in the parameter
space of plane curves of degree $d$ meets the discriminant hypersurface in
finitely many points. It follows that a given pencil $\mathcal{L}$ is either
generic or every $\overline{\mathbb{F}_{q}}$-member of $\mathcal{L}$ is a
singular curve. Thus, non-generic pencils are extremely special. When
$d=o(\sqrt{q})$, we can show that for any generic pencil, at least
$(1/3-o(1))q$ members that are not blocking. We may assume that no curve in
the pencil is trivially blocking, for otherwise, $q$ of the curves are
nonblocking. For each generic pencil there are at most $3(d-1)^{2}=o(q)$ many
singular curves by [EH16]*Proposition 7.4. Note for each smooth curve in the
pencil, by Bézout’s theorem, it does not contain a Baer subplane (otherwise,
there is a line that intersects at the curve with at least $\sqrt{q}+1>d$
points). Thus, if a smooth member in the pencil is blocking, then it has size
at least $3(q+1)/2$; therefore, there are at most $2q/3$ smooth blocking
curves in our pencils. Hence, we have more than $q/3-3(d-1)^{2}=(1/3-o(1))q$
nonblocking curves in our pencil.

##  4\. Proof of Theorem 1.4

In this section, we will show that Question 1.2 has a positive answer if the
constant $c_{0}$ is allowed to depend on $d$. More precisely, we will prove
Theorem 1.4, which guarantees that at least $\frac{1}{d+1}$ fraction of the
$\mathbb{F}_{q}$-members of a given pencil are nonblocking.

As a preparation, we start by proving a lower bound on the number of
$\mathbb{F}_{q}$-rational points on a blocking plane curve. The following
lemma is implicitly contained in [AGY22]*Section 2.5. For the sake of
completeness, we present a self-contained proof.

######  Lemma 4.1.

Suppose $C$ is a plane curve of degree $d$ defined over $\mathbb{F}_{q}$. If
$C(\mathbb{F}_{q})$ is a nontrivial blocking set, then
$\\#C(\mathbb{F}_{q})>q+\frac{q+\sqrt{q}}{d}$.

###### Proof.

Let $t_{i}$ denote the number of $\mathbb{F}_{q}$-lines $L$ such that $C\cap
L$ has exactly $i$ distinct $\mathbb{F}_{q}$-points. Let
$N=\\#C(\mathbb{F}_{q})$ denote the number of $\mathbb{F}_{q}$-points of $C$.
Since $C$ is nontrivially blocking, it cannot contain any
$\mathbb{F}_{q}$-line as a component. Thus, $t_{0}=0$, and $t_{i}=0$ for $i>d$
by Bézout’s theorem. Moreover, a standard double counting argument on point-
line incidences (see for example [AGY22]*Lemma 2.9) leads to the following
three identities:

$\displaystyle\sum_{i=1}^{d}t_{i}=q^{2}+q+1,\quad\quad\sum_{i=1}^{d}i\cdot
t_{i}=(q+1)N,\quad\quad\sum_{i=2}^{d}\binom{i}{2}\cdot t_{i}=\binom{N}{2}.$

By combining the first two identities, we obtain

$q^{2}+q+1=(q+1)N-\sum_{i=2}^{d}(i-1)t_{i},$ (3)

while the third identity implies

$\sum_{i=2}^{d}(i-1)t_{i}\geq\frac{N(N-1)}{d}.$ (4)

The inequalities (3) and (4) together yield,

$q^{2}+q+1\leq(q+1)N-\frac{N(N-1)}{d}.$ (5)

Since $C(\mathbb{F}_{q})$ is a _nontrivial_ blocking set, we have $N\geq
q+\sqrt{q}+1$ by [B71]. Now, the inequality (5) implies,

$\displaystyle(q+1)N$ $\displaystyle\geq
q^{2}+q+1+\frac{(q+\sqrt{q}+1)(q+\sqrt{q})}{d}>(q+1)q+\frac{(q+1)(q+\sqrt{q})}{d}.$

It follows that $N>q+\frac{q+\sqrt{q}}{d}$, as desired. ∎

######  Remark 4.2.

One can obtain a slightly stronger conclusion
$N>\left(\frac{d}{d-1}\right)q\cdot\left(1+o(1)\right)$ by analyzing the
inequality (5) more carefully.

We now proceed with the proof of Theorem 1.4 on the number of nonblocking
curves in a pencil of fixed degree.

###### Proof of Theorem 1.4.

Given a pencil $\mathcal{L}$ with no $\mathbb{F}_{q}$-points in its base
locus, suppose $m$ of the $\mathbb{F}_{q}$-members are blocking and $q+1-m$ of
the $\mathbb{F}_{q}$-members are nonblocking. If any $\mathbb{F}_{q}$-member
of $\mathcal{L}$ is trivially blocking, then applying the same argument as at
the beginning of Proposition 3.2, we see that the other $q$ members of the
pencil are nonblocking. So, we may assume that all the blocking
$\mathbb{F}_{q}$-members are nontrivially blocking.

By applying Lemma 4.1, we obtain the following inequality:

$m\left(\frac{qd+q+\sqrt{q}}{d}\right)<\sum_{\begin{subarray}{c}C\text{ is
}\mathbb{F}_{q}\text{-member of }\mathcal{L}\\\ C\text{ is
blocking}\end{subarray}}\\#C(\mathbb{F}_{q})\leq\sum_{C\text{ is
}\mathbb{F}_{q}\text{-member of }\mathcal{L}}\\#C(\mathbb{F}_{q})=q^{2}+q+1.$

Therefore, using the hypothesis $d\leq q$, we obtain

$m\leq\frac{(q^{2}+q+1)d}{qd+q+\sqrt{q}}=\frac{(q+1)(q+\frac{1}{q+1})d}{(d+1)(q+\frac{\sqrt{q}}{d+1})}\leq\frac{d}{d+1}(q+1).$

We conclude that the number of nonblocking $\mathbb{F}_{q}$-members of the
pencil $\mathcal{L}$ is $q+1-m\geq\frac{q+1}{d+1}$. ∎

######  Remark 4.3.

The hypothesis $d\leq q$ in Theorem 1.4 is natural. However, when
$\sqrt{q}\leq d\leq q$, Theorem 1.4 only guarantees
$\frac{q+1}{\sqrt{q}+1}=\sqrt{q}-1$ many nonblocking curves, which was already
proved in Proposition 3.2. For Theorem 1.4 to yield more refined results, we
would need to assume $d<\sqrt{q}$.

On the other hand, if $d$ gets too small compared to $q$, namely, $d<q^{1/6}$
then we can refine Theorem 1.4 for generic pencils (as defined in Remark 3.5).
More precisely, when $q>d^{6}$, then the lower bound in Theorem 1.4 can be
improved significantly so that the answer to Question 1.2 would be positive
with $c_{0}=1-o(1)$. This follows from the observation that the number of
singular members in a generic pencil is at most $3(d-1)^{2}=o(q)$ as stated in
Remark 3.5, and our earlier result that a smooth member in the pencil is not
blocking whenever $q>d^{6}$ [AGY22]*Theorem 1.2. We also mention that there
are other refined sufficient conditions on nonblocking smooth curves in
[AGY22].

## Acknowledgements

The second author is supported by an NSERC Discovery grant. The third author
is supported by a doctoral fellowship from the University of British Columbia.

## References