arXiv ScienceSearch

arXiv subjects

Adam Topaz

Publications and source records attributed to Adam Topaz.

16 recordsLinked to original sources

Anatomy of a Formal Proof

Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a computer can parse them and check them against the rules of a formal axiomatic foundation. This article describes the experience of working with a proof assistant and considers the impact the technology will have on mathematics.

math.HO

Categorical Foundations of Formalized Condensed Mathematics

Condensed mathematics, developed by Clausen and Scholze over the last few years, proposes a generalization of topology with better categorical properties. It replaces the concept of a topological space by that of a condensed set, which can be defined as a sheaf for the coherent topology on a certain category of compact Hausdorff spaces. In this case, the sheaf condition has a fairly simple explicit description, which arises from studying the relationship between the coherent, regular and extensive topologies. In this paper, we establish this relationship under minimal assumptions on the category, going beyond the case of compact Hausdorff spaces. Along the way, we also provide a characterization of sheaves and covering sieves for these categories. All results in this paper have been fully formalized in the Lean proof assistant.

math.CT

Abstraction boundaries and spec driven development in pure mathematics

In this article we discuss how abstraction boundaries can help tame complexity in mathematical research, with the help of an interactive theorem prover. While many of the ideas we present here have been used implicitly by mathematicians for some time, we argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas.

math.HO

Algebraic dependence and Milnor K-theory

This paper shows that algebraic (in)dependence is encoded in Milnor K-theory of fields. As an application, we show that the isomorphism type of a field is determined by its Milnor K-theory, up to purely inseparable extensions, in most situations.

math.KT

Line and Hyperplane GT-variants

In this work, we introduce a variant of the Grothendieck-Teichm{\"u}ller group, defined in terms of complements of hyperplane arrangements and pro-$\ell$ two-step nilpotent fundamental groups, and prove that it is isomorphic to the absolute Galois group of $\Qbb$.

math.AG

Recovering function fields from their integral $\ell$-adic cohomology with the Galois action

In this note, we consider function fields of higher-dimensional algebraic varieties defined over non-local fields, and show how the Galois action on the cohomology such function fields can be used to parameterize their divisorial valuations. By applying a recent theorem of Pop, we observe that, in dimension $\geq 3$, this information is enough to completely determine the function field and the base-field in question.

math.KT

Invariant hypersurfaces

The following theorem, which includes as very special cases results of Jouanolou and Hrushovski on algebraic $D$-varieties on the one hand, and of Cantat on rational dynamics on the other, is established: Working over a field of characteristic zero, suppose $\phi_1,\phi_2: Z \to X$ are dominant rational maps from a (possibly nonreduced) irreducible scheme $Z$ of finite-type to an algebraic variety $X$, with the property that there are infinitely many hypersurfaces on $X$ whose scheme-theoretic inverse images under $\phi_1$ and $\phi_2$ agree. Then there is a nonconstant rational function $g$ on $X$ such that $g\phi_1=g\phi_2$. In the case when $Z$ is also reduced the scheme-theoretic inverse image can be replaced by the proper transform. A partial result is obtained in positive characteristic. Applications include an extension of the Jouanolou-Hrushovski theorem to generalised algebraic $\mathcal D$-varieties and of Cantat's theorem to self-correspondences.

math.AG

Four-fold Massey products in Galois cohomology

In this paper, we develop a new necessary and sufficient condition for the vanishing of 4-Massey products of elements in the mod-2 Galois cohomology of a field. This new description allows us to define a splitting variety for 4-Massey products, which is shown in the Appendix to satisfy a local-to-global principle over number fields. As a consequence, we prove that, for a number field, all such 4-Massey products vanish whenever they are defined. This provides new explicit restrictions on the structure of absolute Galois groups of number fields.

math.NT

The Galois action on geometric lattices and the mod-$\ell$ I/OM

This paper studies the Galois action on a special lattice of geometric origin, which is related to mod-$\ell$ abelian-by-central quotients of geometric fundamental groups of varieties. As a consequence, we formulate and prove the mod-$\ell$ abelian-by-central variant/strengthening of a conjecture due to Ihara/Oda-Matsumoto.

math.AG

Reconstructing function fields from rational quotients of mod-$\ell$ Galois groups

In this paper, we develop the main step in the global theory for the mod-$\ell$ analogue of Bogomolov's program in birational anabelian geometry for higher-dimensional function fields over algebraically closed fields. More precisely, we show how to reconstruct a function field $K$ of transcendence degree $\geq 5$ over an algebraically closed field, up-to inseparable extensions, from the mod-$\ell$ abelian-by-central Galois group of $K$ endowed with the collection of mod-$\ell$ rational quotients.

math.AG

Abelian-by-Central Galois groups of fields I: a formal description

Let $K$ be a field whose characteristic is prime to a fixed integer $n$ with $μ_n \subset K$, and choose $ω\in μ_n$ a primitive $n$th root of unity. Denote the absolute Galois group of $K$ by $\operatorname{Gal}(K)$, and the mod-$n$ central-descending series of $\operatorname{Gal}(K)$ by $\operatorname{Gal}(K)^{(i)}$. Recall that Kummer theory, together with our choice of $ω$, provides a functorial isomorphism between $\operatorname{Gal}(K)/\operatorname{Gal}(K)^{(2)}$ and $\operatorname{Hom}(K^\times,\mathbb{Z}/n)$. Analogously to Kummer theory, in this note we use the Merkurjev-Suslin theorem to construct a continuous, functorial and explicit embedding $\operatorname{Gal}(K)^{(2)}/\operatorname{Gal}(K)^{(3)} \hookrightarrow \operatorname{Fun}(K\smallsetminus\{0,1\},(\mathbb Z/n)^2)$, where $\operatorname{Fun}(K\smallsetminus\{0,1\},(\mathbb Z/n)^2)$ denotes the group of $(\mathbb Z/n)^2$-valued functions on $K\smallsetminus\{0,1\}$. We explicitly determine the functions associated to the image of commutators and $n$th powers of elements of $\operatorname{Gal}(K)$ under this embedding. We then apply this theory to prove some new results concerning relations between elements in abelian-by-central Galois groups.

math.NT

Commuting-Liftable Subgroups of Galois Groups II

Let $n$ denote either a positive integer or $\infty$, let $\ell$ be a fixed prime and let $K$ be a field of characteristic different from $\ell$. In the presence of sufficiently many roots of unity in $K$, we show how to recover some of the inertia/decomposition structure of valuations inside the maximal $\ell^n$-abelian Galois group of $K$ using the maximal $\ell^N$-abelian-by-central Galois group of $K$, whenever $N$ is sufficiently large relative to $n$.

math.NT

Galois Module Structure of \Z/\ell^n-th Classes of Fields

In this paper we use the Merkurjev-Suslin theorem to explore the structure of arithmetically significant Galois modules that arise from Kummer theory. Let K be a field of characteristic different from a prime \ell, n a positive integer, and suppose that K contains the (\ell^n)^th roots of unity. Let L be the maximal \Z/\ell^n-elementary abelian extension of K, and set G = \Gal(L|K). We consider the G-module J = L^\times/\ell^n and denote its socle series by J_m. We provide a precise condition, in terms of a map to H^3(G,\Z/\ell^n), determining which submodules of J_{m-1} embed in cyclic modules generated by elements of J_m. This generalizes a theorem of Adem, Gao, Karaguezian, and Minac which deals with the case m=\ell^n=2. This description of J_m/J_{m-1} can be viewed as an analogue of the classical Hilbert's Theorem 90 and it is helpful for understanding the G-module J.

math.NT

Almost-Commuting-Liftable Subgroups of Galois Groups

Let K be a field and \ell be a prime such that char K \neq \ell. In the presence of sufficiently many roots of unity in K, we show how to recover some of the inertia/decomposition structure of valuations inside the maximal (\Z/\ell)-abelian resp. pro-\ell-abelian Galois group of K using its (Z/\ell)-central resp. pro-\ell-central extensions.

math.NT