An experiment in writing formal mathematics in Coq (2009)
We start from an axiomatization of set theory which is close to what Benjamin Werner constructed [?]. I suppose that if you replace our parameter Ens by the Ens which he constructed, then one should...
On the classification of rank two representations of quasiprojective fundamental groups (2009)
Kevin Corlette, Carlos Simpson
Abstract. Suppose X is a smooth quasiprojective variety over C and ρ: π1(X, x) → SL(2, C) is a Zariski-dense representation with quasiunipotent monodromy at infinity. Then ρ factors through a...
Eyssidieux, Philippe, Simpson, Carlos
We construct a Mixed Hodge Structure on the local complete ring of the representation scheme at the holonomy of a VHS on a compact K\"ahler manifold and prove that the corresponding tautological...
Eyssidieux, Philippe, Simpson, Carlos
We construct a Mixed Hodge Structure on the local complete ring of the representation scheme at the holonomy of a VHS on a compact K\"ahler manifold and prove that the corresponding tautological...
Obstructed bundles of rank two on a quintic surface (2009)
Mestrano, Nicole, Simpson, Carlos
In this note we consider the moduli space of stable bundles of rank two on a very general quintic surface. We study the obstructed points of the moduli space via the spectral covering of a twisted...
Obstructed bundles of rank two on a quintic surface (2009)
Mestrano, Nicole, Simpson, Carlos
In this note we consider the moduli space of stable bundles of rank two on a very general quintic surface. We study the obstructed points of the moduli space via the spectral covering of a twisted...
Obstructed bundles of rank two on a quintic surface (2009)
Mestrano, Nicole, Simpson, Carlos
In this note we consider the moduli space of stable bundles of rank two on a very general quintic surface. We study the potentially obstructed points of the moduli space via the spectral covering of...
Obstructed bundles of rank two on a quintic surface (2009)
Mestrano, Nicole, Simpson, Carlos
In this note we consider the moduli space of stable bundles of rank two on a very general quintic surface. We study the potentially obstructed points of the moduli space via the spectral covering of...
Computer theorem proving in math (2008)
Abstract—We give an overview of issues surrounding computer-verified theorem proving in the standard pure-mathematical context. This is based on my talk at the PQR conference (Brussels, June 2003).
COMPUTER THEOREM PROVING IN MATH (2008)
Abstract. We give an overview of issues surrounding computerverified theorem proving in the standard pure-mathematical context. 1.
... la traduction en langage formalisé ne serait plus qu’un exercise de patience (sans doutes fort pénible).
Formal proof, computation, and the construction problem in algebraic geometry (2008)
Carlos Simpson, Alain Connes, Andy Magid
It has become a classical technique to turn to theoretical computer science to provide computational tools for algebraic geometry. A more recent transformation is that now we also get logical tools,...
Set-theoretical mathematics in Coq (2008)
Abstract: We give a brief discussion of some of the issues which have arisen in the course of formalizing some classical set-theoretical mathematics in the Coq system. This sprouts from, expands and...
Formal proof, computation, and the construction problem in algebraic geometry (2008)
Carlos Simpson, Alain Connes, Andy Magid
It has become a classical technique to turn to theoretical computer science to provide computational tools for algebraic geometry. A more recent transformation is that now we also get logical tools,...
COMPUTER THEOREM PROVING IN MATH (2008)
Abstract. We give an overview of issues surrounding computerverified theorem proving in the standard pure-mathematical context. 1.
COMPUTER THEOREM PROVING IN MATH (2008)
Abstract. We give an overview of issues surrounding computerverified theorem proving in the standard pure-mathematical context. 1.
... la traduction en langage formalisé ne serait plus qu’un exercise de patience (sans doutes fort pénible).
Iterated destabilizing modifications for vector bundles with connection (2008)
Given a vector bundle with integrable connection $(V,\nabla )$ on a curve, if $V$ is not itself semistable as a vector bundle then we can iterate a construction involving modification by the...
Iterated destabilizing modifications for vector bundles with connection (2008)
Given a vector bundle with integrable connection $(V,\nabla )$ on a curve, if $V$ is not itself semistable as a vector bundle then we can iterate a construction involving modification by the...
GEOMETRICITY OF THE HODGE FILTRATION ON THE ∞-STACK OF PERFECT COMPLEXES OVER XDR (2008)
Abstract. We construct a locally geometric ∞-stack MHod(X, Perf) of perfect complexes with λ-connection structure on a smooth projective variety X. This maps to A 1 /Gm, so it can be considered as...
Ludmil Katzarkov, Tony Pantev, Carlos Simpson
Density of monodromy actions on non-abelian cohomology
Calculating maps between n-categories (2007)
This short note addresses the problem of how to calculate in a reasonable way the homotopy classes of maps between two n-categories (by which we mean Tamsamani's n-nerves [10]). The closed model...
Computer Theorem Proving in Math (2007)
We give an overview of issues surrounding computerverified theorem proving in the standard pure-mathematical context.
Regulators of canonical extensions are torsion: the smooth divisor case (2007)
In this paper, we prove a generalization of Reznikov's theorem on the torsion-property of the Chern-Simons classes and in particular the torsion--property of the Deligne Chern classes (in degrees...
On the classification of rank two representations of quasiprojective fundamental groups (2007)
Corlette, Kevin, Simpson, Carlos
Suppose $X$ is a smooth quasiprojective variety over $\cc$ and $\rho : \pi _1(X,x) \rightarrow SL(2,\cc )$ is a Zariski-dense representation with quasiunipotent monodromy at infinity. Then $\rho$...
On the classification of rank two representations of quasiprojective fundamental groups (2007)
Corlette, Kevin, Simpson, Carlos
Suppose $X$ is a smooth quasiprojective variety over $\cc$ and $\rho : \pi _1(X,x) \rightarrow SL(2,\cc )$ is a Zariski-dense representation with quasiunipotent monodromy at infinity. Then $\rho$...
Regulators of canonical extensions are torsion: the smooth divisor case (2007)
In this paper, we prove a generalization of Reznikov's theorem which says that the Chern-Simons classes and in particular the Deligne Chern classes (in degrees $>1$) are torsion, of a flat bundle on...
A weight two phenomenon for the moduli of rank one local systems on open varieties (2007)
The twistor space of representations on an open variety maps to a weight two space of local monodromy transformations around a divisor component at infinty. The space of $\sigma$-invariant sections...
A weight two phenomenon for the moduli of rank one local systems on open varieties (2007)
The twistor space of representations on an open variety maps to a weight two space of local monodromy transformations around a divisor component at infinty. The space of $\sigma$-invariant sections...
Regulators of canonical extensions are torsion: the smooth divisor case (2007)
In this paper, we prove a generalization of Reznikov's theorem which says that the Chern-Simons classes and in particular the Deligne Chern classes (in degrees $>1$) are torsion, of a flat bundle on...
On the classification of rank two representations of quasiprojective fundamental groups (2007)
Corlette, Kevin, Simpson, Carlos
Suppose $X$ is a smooth quasiprojective variety over $\cc$ and $\rho : \pi _1(X,x) \rightarrow SL(2,\cc )$ is a Zariski-dense representation with quasiunipotent monodromy at infinity. Then $\rho$...
In this paper, we obtain an explicit formula for the Chern character of a locally abelian parabolic bundle in terms of its constituent bundles. Several features and variants of parabolic structures...
Set-theoretical mathematics in Coq (2006)
We give a brief discussion of some of the issues which have arisen in the course of formalizing some classical set-theoretical mathematics in the Coq system. This sprouts from, expands and replaces a...
Some properties of the theory of n-categories (2006)
Let $L_n$ denote the Dwyer-Kan localization of the category of weak n-categories divided by the n-equivalences. We propose a list of properties that this simplicial category is likely to have, and...
Calculating maps between n-categories (2006)
We give an explicit way of calculating the set of homotopy classes of morphisms from a Tamsamani n-category A to another one B. This calculation uses a Reedy-cofibrant cosimplicial resolution of A,...
Katz's middle convolution algorithm (2006)
This is an expository account of Katz's middle convolution operation on local systems over ${\bf P}^1-\{ q_1,\ldots , q_n\}$. We describe the Betti and de Rham versions, and point out that they give...
Katz's middle convolution algorithm (2006)
This is an expository account of Katz's middle convolution operation on local systems over ${\bf P}^1-\{ q_1,\ldots , q_n\}$. We describe the Betti and de Rham versions, and point out that they give...
Katz's middle convolution algorithm (2006)
This is an expository account of Katz's middle convolution operation on local systems over ${\bf P}^1-\{ q_1,\ldots , q_n\}$. We describe the Betti and de Rham versions, and point out that they give...
A relation between the parabolic Chern characters of the de Rham bundles (2006)
In this paper, we consider the weight $i$ de Rham--Gauss--Manin bundles on a smooth variety arising from a smooth projective morphism $f:X_U\lrar U$ for $i\geq 0$. We associate to each weight $i$ de...
A relation between the parabolic Chern characters of the de Rham bundles (2006)
In this paper, we consider the weight $i$ de Rham--Gauss--Manin bundles on a smooth variety arising from a smooth projective morphism $f:X_U\lrar U$ for $i\geq 0$. We associate to each weight $i$ de...
A relation between the parabolic Chern characters of the de Rham bundles (2006)
In this paper, we consider the weight $i$ de Rham--Gauss--Manin bundles on a smooth variety arising from a smooth projective morphism $f:X_U\lrar U$ for $i\geq 0$. We associate to each weight $i$ de...
A relation between the parabolic Chern characters of the de Rham bundles (2006)
In this paper, we consider the weight $i$ de Rham--Gauss--Manin bundles on a smooth variety arising from a smooth projective morphism $f:X_U\lrar U$ for $i\geq 0$. We associate to each weight $i$ de...
Katz's middle convolution algorithm (2006)
This is an expository account of Katz's middle convolution operation on local systems over ${\bf P}^1-\{ q_1,\ldots , q_n\}$. We describe the Betti and de Rham versions, and point out that they give...
In this paper, we obtain an explicit formula for the Chern character of a locally abelian parabolic bundle in terms of its constituent bundles. Several features and variants of parabolic structures...
In this paper, we obtain an explicit formula for the Chern character of a locally abelian parabolic bundle in terms of its constituent bundles. Several features and variants of parabolic structures...
Katz's middle convolution algorithm (2006)
This is an expository account of Katz's middle convolution operation on local systems over ${\bf P}^1-\{ q_1,\ldots , q_n\}$. We describe the Betti and de Rham versions, and point out that they give...
A relation between the parabolic Chern characters of the de Rham bundles (2006)
In this paper, we consider the weight $i$ de Rham--Gauss--Manin bundles on a smooth variety arising from a smooth projective morphism $f:X_U\lrar U$ for $i\geq 0$. We associate to each weight $i$ de...
KATZ’S MIDDLE CONVOLUTION ALGORITHM (2006)
Abstract. This is an expository account of Katz’s middle convolution operation on local systems over P 1 − {q1,...,qn}. We describe the Betti and de Rham versions, and point out that they give...
Geometricity of the Hodge filtration on the $\infty$-stack of perfect complexes over $X_{DR}$ (2005)
We construct a locally geometric $\infty$-stack $M_{Hod}(X,Perf)$ of perfect complexes on $X$ with $\lambda$-connection structure for a smooth projective variety $X$. This maps to $A^1 / G_m$, so it...
Geometricity of the Hodge filtration on the $\infty$-stack of perfect complexes over $X_{DR}$ (2005)
We construct a locally geometric $\infty$-stack $M_{Hod}(X,Perf)$ of perfect complexes on $X$ with $\lambda$-connection structure for a smooth projective variety $X$. This maps to $A^1 / G_m$, so it...
Geometricity of the Hodge filtration on the $\infty$-stack of perfect complexes over $X_{DR}$ (2005)
We construct a locally geometric $\infty$-stack $M_{Hod}(X,Perf)$ of perfect complexes on $X$ with $\lambda$-connection structure for a smooth projective variety $X$. This maps to $A^1 / G_m$, so it...
Geometricity of the Hodge filtration on the $\infty$-stack of perfect complexes over $X_{DR}$ (2005)
We construct a locally geometric $\infty$-stack $M_{Hod}(X,Perf)$ of perfect complexes on $X$ with $\lambda$-connection structure for a smooth projective variety $X$. This maps to $A^1 / G_m$, so it...
Explaining Gabriel-Zisman localization to the computer (2005)
This explains a computer formulation of Gabriel-Zisman localization of categories in the proof assistant Coq. It includes both the general localization construction with the proof of GZ's Lemma 1.2,...
Files for Gabriel-Zisman localization (2005)
This preprint contains the Coq proof files for Gabriel-Zisman localization, bundled with the source. The text of this preprint consists of the definitions and lemma statements of the main files, with...
Explaining Gabriel-Zisman localization to the computer (2005)
This explains a computer formulation of Gabriel-Zisman localization of categories in the proof assistant Coq. It includes both the general localization construction with the proof of GZ's Lemma 1.2,...
Files for Gabriel-Zisman localization (2005)
This preprint contains the Coq proof files for Gabriel-Zisman localization, bundled with the source. The text of this preprint consists of the definitions and lemma statements of the main files, with...
Explaining Gabriel-Zisman localization to the computer (2005)
This explains a computer formulation of Gabriel-Zisman localization of categories in the proof assistant Coq. It includes both the general localization construction with the proof of GZ's Lemma 1.2,...
Files for Gabriel-Zisman localization (2005)
This preprint contains the Coq proof files for Gabriel-Zisman localization, bundled with the source. The text of this preprint consists of the definitions and lemma statements of the main files, with...
Explaining Gabriel-Zisman localization to the computer (2005)
This explains a computer formulation of Gabriel-Zisman localization of categories in the proof assistant Coq. It includes both the general localization construction with the proof of GZ's Lemma 1.2,...
Files for Gabriel-Zisman localization (2005)
This preprint contains the Coq proof files for Gabriel-Zisman localization, bundled with the source. The text of this preprint consists of the definitions and lemma statements of the main files, with...
Geometricity of the Hodge filtration on the $\infty$-stack of perfect complexes over $X_{DR}$ (2005)
We construct a locally geometric $\infty$-stack $M_{Hod}(X,Perf)$ of perfect complexes with $\lambda$-connection structure on a smooth projective variety $X$. This maps to $A ^1 / G_m$, so it can be...
Geometricity of the Hodge filtration on the $\infty$-stack of perfect complexes over $X_{DR}$ (2005)
We construct a locally geometric $\infty$-stack $M_{Hod}(X,Perf)$ of perfect complexes with $\lambda$-connection structure on a smooth projective variety $X$. This maps to $A ^1 / G_m$, so it can be...
GEOMETRICITY OF THE HODGE FILTRATION ON THE ∞-STACK OF PERFECT COMPLEXES OVER XDR (2005)
2. λ-connections and the Hodge filtration 3 3. Variation of cohomology—an example 5 4. Perfect complexes over XDR
EXPLAINING GABRIEL-ZISMAN LOCALIZATION TO THE COMPUTER (2005)
2. The general localization construction 5 3. The computer formulation 7
Formalized proof, computation, and the construction problem in algebraic geometry (2004)
An informal discussion of how the construction problem in algebraic geometry motivates the search for formal proof methods. Also includes a brief discussion of my own progress up to now, which...
Formalized proof, computation, and the construction problem in algebraic geometry (2004)
An informal discussion of how the construction problem in algebraic geometry motivates the search for formal proof methods. Also includes a brief discussion of my own progress up to now, which...
Computer theorem proving in math (2004)
We give an overview of issues surrounding computer-verified theorem proving in the standard pure-mathematical context. This is based on my talk at the PQR conference (Brussels, June 2003).
Computer theorem proving in math (2004)
We give an overview of issues surrounding computer-verified theorem proving in the standard pure-mathematical context. This is based on my talk at the PQR conference (Brussels, June 2003).
Set-theoretical mathematics in Coq (2004)
We give a brief discussion of some of the issues which have arisen in the course of formalizing some classical set-theoretical mathematics in the Coq system. This sprouts from, expands and replaces a...
Formalized proof, computation, and the construction problem in algebraic geometry (2004)
An informal discussion of how the construction problem in algebraic geometry motivates the search for formal proof methods. Also includes a brief discussion of my own progress up to now, which...
Computer theorem proving in math (2004)
We give an overview of issues surrounding computer-verified theorem proving in the standard pure-mathematical context. This is based on my talk at the PQR conference (Brussels, June 2003).
Formalized proof, computation, and the construction problem in algebraic geometry (2004)
An informal discussion of how the construction problem in algebraic geometry motivates the search for formal proof methods. Also includes a brief discussion of my own progress up to now, which...
Computer theorem proving in math (2004)
We give an overview of issues surrounding computer-verified theorem proving in the standard pure-mathematical context. This is based on my talk at the PQR conference (Brussels, June 2003).
The construction problem in Kähler geometry (2004)
One of the most surprising things in algebraic geometry is the fact that algebraic varieties over the complex numbers benefit from a collection of metric properties which strongly influence their...
Asymptotics for general connections at infinity (2003)
For a standard path of connections going to a genericpoint at infinity in the moduli space $M_{DR}$ ofconnections on a compact Riemann surface, we show thatthe Laplace transform of the family of...
Asymptotics for general connections at infinity (2003)
For a standard path of connections going to a genericpoint at infinity in the moduli space $M_{DR}$ ofconnections on a compact Riemann surface, we show thatthe Laplace transform of the family of...
Asymptotics for general connections at infinity (2003)
For a standard path of connections going to a genericpoint at infinity in the moduli space $M_{DR}$ ofconnections on a compact Riemann surface, we show thatthe Laplace transform of the family of...
Asymptotics for general connections at infinity (2003)
For a standard path of connections going to a genericpoint at infinity in the moduli space $M_{DR}$ ofconnections on a compact Riemann surface, we show thatthe Laplace transform of the family of...
Asymptotics for general connexions at infinity (2003)
This is a preliminary set of notes on the asymptotic behavior of the monodromy of connexions near a general point at ∞ in the space MDR of connexions on a compact Riemann surface X. We will...
Some properties of the theory of n-categories (2001)
Let $L_n$ denote the Dwyer-Kan localization of the category of weak n-categories divided by the n-equivalences. We propose a list of properties that this simplicial category is likely to have, and...
Calculating maps between n-categories (2000)
We give an explicit way of calculating the set of homotopy classes of morphisms from a Tamsamani n-category A to another one B. This calculation uses a Reedy-cofibrant cosimplicial resolution of A,...
Nonabelian mixed Hodge structures (2000)
Katzarkov, Ludmil, Pantev, Tony, Simpson, Carlos
We propose a definition of ``nonabelian mixed Hodge structure'' together with a construction associating to a smooth projective variety $X$ and to a nonabelian mixed Hodge structure $V$, the...
Theorem (after Giraud, SGA 4): Suppose $A$ is a simplicial category. The following conditions are equivalent: (i) There is a cofibrantly generated closed model category $M$ such that $A$ is...
Algebraic aspects of higher nonabelian Hodge theory (1999)
We look more closely at the higher nonabelian de Rham cohomology of a smooth projective variety or family of varieties that had been defined in some previous papers. We formalize using $n$-stacks the...
On the Breen-Baez-Dolan stabilization hypothesis for Tamsamani's weak n-categories (1998)
We show that if $2k\geq n$, then a k-connected weak n-category $A$ can be ``delooped'' to a k+1-connected weak n+1-category $Y$ with $Hom_Y(y,y)\cong A$. This is the essential part of the...
Homotopy types of strict 3-groupoids (1998)
We look at strict $n$-groupoids and show that if $\Re$ is any realization functor from the category of strict $n$-groupoids to the category of spaces satisfying a minimal property of compatibility...
Descente pour les n-champs (Descent for n-stacks) (1998)
Hirschowitz, André, Simpson, Carlos
We develop the theory of n-stacks (or more generally Segal n-stacks which are $\infty$-stacks such that the morphisms are invertible above degree n). This is done by systematically using the theory...
Secondary Kodaira-Spencer classes and nonabelian Dolbeault cohomology (1997)
If $X$ is a smooth projective variety moving in a family, we define a secondary Kodaira-Spencer class for nonabelian Dolbeault cohomology $Hom(X_{Dol}, T)$ of $X$ with coefficients in the...
Effective generalized Seifert-Van Kampen: how to calculate $\Omega X$ (1997)
Suppose $X$ is a 1-connected simplicial set with finitely many nondegenerate simplices. We give an effective algorithm to calculate a simplicial set with the $n$-type of the loop space $\Omega X$....
Limits in $n$-categories (1997)
We define notions of direct and inverse limits in an $n$-category. We prove that the $n+1$-category $nCAT'$ of fibrant $n$-categories admits direct and inverse limits. At the end we speculate...
Mixed twistor structures (1997)
The purpose of this paper is to introduce the notion of mixed twistor structure, a generalization of the notion of mixed Hodge structure. The utility of this notion is to make possible a theory of...
We define a closed model category containing the $n$-nerves defined by Tamsamani, and admitting internal $Hom$. This allows us to construct the $n+1$-category $nCAT$ by taking the internal $Hom$ for...
Algebraic (geometric) $n$-stacks (1996)
We propose a generalization of Artin's definition of algebraic stack, which we call {\em geometric $n$-stack}. The main observation is that there is an inductive structure to the definition whereby...
The topological realization of a simplicial presheaf (1996)
The purpose of this article is to define the topological realization of a simplicial presheaf and to prove (under appropriate conditions) that it is homotopy-invariant under Illusie weak equivalence....
We look at homotopy-coherent diagrams of spaces (after Segal, Leitch, Vogt, Mather, Cordier) over a Grothendieck site; we call these ``flexible presheaves''. After some preliminary materiel, we...
A relative notion of algebraic Lie group and applications to $n$-stacks (1996)
If $S$ is a scheme of finite type over $k=\cc $, let $\Xx /S$ denote the big etale site of schemes over $S$. We introduce {\em presentable group sheaves}, a full subcategory of the category of...
The Hodge filtration on nonabelian cohomology (1996)
This is partly a survey article on nonabelian Hodge theory, but we also give proofs of results that have only been announced elsewhere. In the introduction we discuss a wide range of recent work on...