synthetic-zariski

Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos

https://github.com/felixwellen/synthetic-zariski

Science Score: 64.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • CITATION.cff file
    Found CITATION.cff file
  • codemeta.json file
    Found codemeta.json file
  • .zenodo.json file
    Found .zenodo.json file
  • DOI references
  • Academic publication links
    Links to: arxiv.org
  • Committers with academic emails
    4 of 13 committers (30.8%) from academic institutions
  • Institutional organization owner
  • JOSS paper metadata
  • Scientific vocabulary similarity
    Low similarity (6.9%) to scientific vocabulary

Keywords from Contributors

agda dependent-types programming-language proof-assistant type-theory
Last synced: 6 months ago · JSON representation ·

Repository

Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos

Basic Info
  • Host: GitHub
  • Owner: felixwellen
  • License: mit
  • Language: TeX
  • Default Branch: main
  • Size: 4.62 MB
Statistics
  • Stars: 62
  • Watchers: 29
  • Forks: 7
  • Open Issues: 22
  • Releases: 0
Created over 3 years ago · Last pushed 6 months ago
Metadata Files
Readme License Citation

README.md

Synthetic Algebraic Geometry in the Zariski-Topos

Stay updated on synthetic algebraic geometry by watching this repository, joining the next meeting or with the mailing list. Due to a bug in the mailinglist-service of chalmers, it does not work to just answer to the email-confirmation email - so use the link to confirm your email address instead. You know that you really signed up to the list, if you can login on the page linked above.

This is a latex documentation of our understanding of the synthetic theory of the Zariski-Topos and related ideas. The drafts below are currently built hourly - if you want to make sure you are viewing the latest built, CTRL+F5 should clear all caches in most browsers. There are currently the following preprints/articles: - Foundations (latest pdf, arxiv, talk) - Automorphisms of and line bundles on projective space (latest pdf, arxiv, talk) - Synthetic stone duality (latest pdf, arxiv, old extended version) - Differential Geometry/étale maps (pdf, arxiv, full notes pdf)

And the following drafts and notes: - Čech-Cohomology (early draft pdf) - Proper Schemes (early draft pdf) - Topology of Synthetic Schemes (early draft pdf) - $\mathbb A^1$-homotopy theory (early draft pdf) - Algebraic spaces and stacks (very early draft pdf) - More general topologies, in particular fppf (very early draft pdf) - Calculations with (elliptic) curves and divisors (very early draft pdf) - Preliminaries for Serre-Duality (very early draft pdf) - Synthetic stone duality (pdf, summary) - Cohomology and homotopy theory in synthetic stone duality (very early draft pdf) - Notes on a model for synthetic stone duality (very early draft pdf) - Finite schemes in SAG (very early draft pdf) - Random Facts, i.e. a collection of everything that still needs to find a good place (very early draft pdf) - Collection of exercises (pdf with exercise-ideas)

There is a related formalization project. Here is an overview of the current ongoing work in SAG and related areas.

Questions

  • Is every étale proposition (formally étale and a scheme) an open proposition?
  • Is every étale scheme a sub-quotient of a finite set?
  • If $A$ is an étale $R$-algebra (finitely presented and the spectrum is étale), is it impossible to have an injective algebra map $R[X] \to A$?
  • Can every bundle (on $Sp A$) of strongly quasicoherent $R$-modules be recovered from its $A$-module of global sections?
  • Can we compute some interesting étale/fppf cohomology groups?
  • Is the intergral closure of $R$ in a finitely presented $R$-algebra $A$ finitely presented?

Answered Questions

  • Is the proposition "X is affine" not-not-stable, for X a scheme? (Then deformations ($D(1) \to \mathrm{Sch}$) of affine schemes would stay affine.)

No: Let $X$ be an open proposition, then up to $\neg\neg$ it is $1$ or $\emptyset$, which are both affine, but we know that not all open propositions are affine.

  • Is $\mathrm{Spec} A$ quasi-complete ("compact") for $A$ a finite $R$-algebra (fin gen as $R$-module)?

Yes: By the discussion in #5 and #6, $\mathrm{Spec} A$ is even projective, whenever $A$ is finitely generated as an $R$-module. - Can there be a flat-modality for $\mathbb{A}^1$-homotopy theory which has the same properties as the flat in real-cohesive HoTT?

No: By the disucssion in #18, this should not be possible, because it would imply that the category of $\mathbb{A}^1$-local types is a topos, which is known to be false. There can still be a flat-modality with weaker properties, for example, the global section functor should generally induce such a modality.

  • For $f : A$, is $f$ not not zero iff $f$ becomes zero in $A \otimes R/\sqrt{0}$?

No: for $r : R$, we have $r + (r^2)$ not not zero in $R/(r^2)$, but if it were always zero in $R/(r^2,\sqrt{0})$, then we would have a nilpotent polynomial $f : R[x]$ such that $x \in f + (x^2)$, which is false.

Learning material

There are some recordings of talks from the last workshop on synthetic algebraic geometry. And there is a hottest talk on the foundations article.

Building the drafts

We use latex now instead of xelatex, to be compatible with the arxiv. For each draft, a build command may be found at the start of main.tex.

Arxiv

To put one of the drafts on the arxiv, we have to

  • make sure there is a good abstract for the draft
  • make a temporary folder, e.g. synthetic-zariski/projective/tmp copy all tex-files there and run ../../util/zar-rebase.sh ../../util/
  • run latexmk -pdf -pvc main.tex to produce the main.bbl and check if the draft builds.
  • put all the files into a .tar.gz, so everything can be uploaded in one step, e.g. tar -czv -f DRAFT.tar.gz *.tex *.cls *.sty main.bbl
  • Login to the arxiv
  • Fill in forms - usually we choose the arxiv perpetual license.
  • upload the tar
  • Fill in more forms - for the foundations we used the following MSC subject classification: MSC-class: 14A99 (Primary), 03B38, 18N99 (Secondary) # Watching this repo ... is a good idea since we started to use the issue-tracker

grafik

for mathematical discussions. If you watch this repo, you should be notified by email if there are new posts. You can watch it, by clicking this button:

grafik

Owner

  • Name: Felix Cherubini
  • Login: felixwellen
  • Kind: user
  • Location: Gothenburg, Sweden
  • Company: Chalmers

Citation (CITATION.cff)

cff-version: 1.2.0
message: "Use this information to cite the whole synthetic algebraic geometry project, use more specific information to cite individual drafts or articles."
authors:
  - family-names: Arndt
    given-names: Peter
  - family-names: Blechschmidt
    given-names: Ingo
  - family-names: Cherubini
    given-names: Felix
  - family-names: Coquand
    given-names: Thierry
  - family-names: Geerligs
    given-names: Freek
  - family-names: Hutzler
    given-names: Matthias
  - family-names: Moeneclaey
    given-names: Hugo
  - family-names: Wärn
    given-names: David
  - family-names: Nieper-Wißkirchen
    given-names: Marc
title: "The Synthetic Algebraic Geometry Project"

GitHub Events

Total
  • Create event: 7
  • Commit comment event: 1
  • Issues event: 5
  • Watch event: 9
  • Issue comment event: 2
  • Member event: 4
  • Push event: 443
  • Pull request event: 3
  • Fork event: 1
Last Year
  • Create event: 7
  • Commit comment event: 1
  • Issues event: 5
  • Watch event: 9
  • Issue comment event: 2
  • Member event: 4
  • Push event: 443
  • Pull request event: 3
  • Fork event: 1

Committers

Last synced: 8 months ago

All Time
  • Total Commits: 1,986
  • Total Committers: 13
  • Avg Commits per committer: 152.769
  • Development Distribution Score (DDS): 0.535
Past Year
  • Commits: 665
  • Committers: 10
  • Avg Commits per committer: 66.5
  • Development Distribution Score (DDS): 0.674
Top Committers
Name Email Commits
Felix Cherubini f****i@p****e 924
coquand t****d@i****m 338
hmoeneclaey h****o@c****e 260
Freek f****s@g****m 197
Matthias Hutzler m****r@p****t 184
David Wärn c****n@g****m 35
Ingo Blechschmidt i****h@s****e 15
JonasHoefer h****j@c****e 11
hmoenecl h****y@i****r 10
Lukas Stoll l****l@p****e 5
Marc Nieper-Wißkirchen m****r@g****m 4
Fabian Endres (Archbook) f****e@w****e 2
Evan Cavallo e****c@c****e 1
Committer Domains (Top 20 + Academic)

Issues and Pull Requests

Last synced: 8 months ago

All Time
  • Total issues: 32
  • Total pull requests: 11
  • Average time to close issues: 3 months
  • Average time to close pull requests: about 2 months
  • Total issue authors: 5
  • Total pull request authors: 4
  • Average comments per issue: 4.69
  • Average comments per pull request: 0.91
  • Merged pull requests: 8
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 2
  • Pull requests: 5
  • Average time to close issues: about 1 month
  • Average time to close pull requests: 2 months
  • Issue authors: 1
  • Pull request authors: 3
  • Average comments per issue: 1.5
  • Average comments per pull request: 1.2
  • Merged pull requests: 4
  • Bot issues: 0
  • Bot pull requests: 0
Top Authors
Issue Authors
  • felixwellen (23)
  • xuanruiqi (3)
  • mnieper (3)
  • space3time1 (1)
  • dwarn (1)
  • MatthiasHu (1)
Pull Request Authors
  • felixwellen (11)
  • lkstl (6)
  • ecavallo (2)
  • mnieper (1)
Top Labels
Issue Labels
Pull Request Labels