Matching works

4 works

math.AT — Algebraic Topology

A Lean Formalization of the Classical Seifert van Kampen Groupoid Theorem

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We explain a Lean 4 formalization of the classical Seifert van Kampen theorem for the full fundamental groupoid. For an arbitrary topological space covered by two open subsets, the inclusion-induced square of ordinary continuous-path fundamental groupoids is a pushout in the category of categories. Every point is retained as an object; no basepoint, connectedness, or separation hypothesis is required. The development identifies an auxiliary directed path category for the indiscrete preorder with Mathlib's fundamental groupoid through strictly inverse functors and naturality equalities. It then assembles the pushout universal property from attributed path-subdivision and homotopy-grid helpers adapted from the directed-topology formalization of Basold, Bruin, and Lawson. We describe the descent construction, its transfer to ordinary fundamental groupoids, and the statement and verification boundaries of the exact artifact registered in Palomar. This is an expository account of a classical theorem and an existing formal artifact, with no claim of mathematical novelty or formalization priority.

Primarily AI-generated textHuman understanding: some partsLean 4MathlibSeifert van Kampen theoremcategorical pushoutfundamental groupoidopen cover

Sep 30, 2026PDF ↗View work →

hexagon:2609.00142v1

math.CO — Combinatorics

Collapsibility of Alexander duals for shade maps

Contributed by Darij Grinberg

Let $E$ be a nonempty finite set. A shade map on $E$ is a map $T:\mathcal{P}(E)\rightarrow\mathcal{P}(E)$ such that toggling an element $u\notin T(F)$ in the input $F$ does not change $T(F)$ . We prove that, if $T$ is an inclusion-reversing shade map and $G\subseteq E$ , then the simplicial complex \[ \{F\subseteq E\mid G\subseteq T(F)\} \] is collapsible. Equivalently, if $S$ is an inclusion-preserving shade map, then the Alexander dual of \[ \{F\subseteq E\mid G\not \subseteq S(F)\} \] is collapsible. This is an Alexander-dual companion to the shade-map collapsibility theorem in \emph{The Elser nuclei sum revisited}. The proof first matches all faces on which $T(F)\neq E$ by a toggle. The remaining faces, characterized by $T(F)=E$ , form the free convex set complex of an associated antimatroidal quasi-closure operator. We give a self-contained recursive acyclic matching on this complex. For ordinary convex geometries, Korte--Lovász--Schrader prove the stronger fact that the free convex set system is non-evasive.

A mix of human-written and AI-generated textHuman understanding: all partsantimatroidsconvex geometriesdiscrete Morse theorygraphssimplicial complexes

Sep 30, 2026PDF ↗View work →

hexagon:2609.00126v1

quant-ph — Quantum Physics

Pauli problem in dimension 4

Contributed by Dmitry Grinko

The finite-dimensional Pauli problem asks how many measurements in orthonormal bases determine every pure state of a $d$ -level quantum system up to a global phase. Four bases always suffice, and the answer is known to be three for $d=2$ and four for $d=3$ and $d\geq5$ . Dimension four remained open because the embedding argument used in other dimensions fails there: the pure-state space $\mathbb{CP}^3$ embeds in $\R^9$ , the space of the nine independent probabilities of three bases. We show that three bases do not suffice in $\C^4$, so exactly four are needed. The same argument shows that no ten vectors in $\C^4$ do phase retrieval. Since eleven vectors are known to suffice, the smallest phase-retrieval frame and the smallest rank-one POVM distinguishing all pure states in $\C^4$ both have eleven elements. All three lower bounds follow from one statement: every six-dimensional real space of traceless Hermitian $4\times4$ matrices with a common isotropic vector, that is, a nonzero $e$ with $e^*Te=0$ for all $T$ in the space, contains a nonzero matrix of rank at most two. We prove it with complex $K$ -theory: otherwise, an odd unitary map on the five-sphere would have a $K^1$ -class that is nonzero by antipodal symmetry but vanishes because of the isotropic vector.

Primarily AI-generated textHuman understanding: some parts

Sep 29, 2026PDF ↗View work →

hexagon:2609.00112v1

math.AT — Algebraic Topology

Swan induction for the finite-local sphere

Contributed by Akhil Mathew

We establish rational Swan induction for ordinary perfect modules over the finite-local sphere $L_n^{p,f}\mathbb S$ . For a finite abelian ambient group, subgroups of $p$ -rank at most $n+1$ suffice, and this bound is sharp. The proof combines cyclic homotopy fixed points in telescopic spectra with the isotropy filtration of a chromatic quotient of finite genuine spectra. The result proves Conjecture~7.22 of Clausen--Mathew--Naumann--Noel for Morava $E$ -theory and gives a new proof of their chromatic upper bound for the algebraic $K$ -theory of $L_n^{p,f}\mathbb S$ -linear categories. The quotient argument also produces finite complexes realizing the induction relations. We formulate the problem of explicit realizations and give two geometric models at the prime two.

Primarily AI-generated textHuman understanding: some partsBurnside ringsSwan inductionchromatic homotopy theory

Sep 27, 2026PDF ↗View work →

math.AC — Commutative Algebra
math.AG — Algebraic Geometry
math.AP — Analysis of PDEs
math.AT — Algebraic Topology
math.CA — Classical Analysis and ODEs
math.CO — Combinatorics
math.CT — Category Theory
math.CV — Complex Variables
math.DG — Differential Geometry
math.DS — Dynamical Systems
math.FA — Functional Analysis
math.GM — General Mathematics
math.GN — General Topology
math.GR — Group Theory
math.GT — Geometric Topology
math.HO — History and Overview
math.IT — Information Theory
math.KT — K-Theory and Homology
math.LO — Logic
math.MG — Metric Geometry
math.NA — Numerical Analysis
math.NT — Number Theory
math.OA — Operator Algebras
math.OC — Optimization and Control
math.PR — Probability
math.QA — Quantum Algebra
math.RA — Rings and Algebras
math.RT — Representation Theory
math.SG — Symplectic Geometry
math.SP — Spectral Theory
math.ST — Statistics Theory
cs.CC — Computational Complexity
cs.CG — Computational Geometry
cs.DM — Discrete Mathematics
cs.DS — Data Structures and Algorithms
cs.FL — Formal Languages and Automata Theory
cs.IT — Information Theory
cs.LO — Logic in Computer Science
cs.MS — Mathematical Software
cs.NA — Numerical Analysis
cs.SC — Symbolic Computation
math-ph — Mathematical Physics
quant-ph — Quantum Physics
stat.TH — Statistics Theory