There should also be a recording from SAG-4:

In other words: Do we have $H^1(\mathbb A^1,\mathbb Z)=0$ ?
Using reasoning from 2.2 in the A1-homotopy draft, this would also imply that $B\mathbb Z=S^1$ is $\mathbb A^1$-local.

It would be good to have a synthetic version of the Proj construction, as it would be useful for constructing projective schemes.

A type $X$ has choice if $\prod_{x:X}||B(x)||\to ||\prod_{x:X}B(x)||$. We know that closed propositions and more generally every spectrum of a finitely presented local algebra has choice (and finite coproducts thereof). Open propositions should not have choice in general. I tend more to believing that basic open propositions do not satisfy choice, but I don't know if we have a result in either direction.

What we call $f^*$ now is actually a topological pullback and we should use the traditional notation $f^{-1}$. (Comment of @mnieper after my talk today).

The Segre-Embedding shows that (quasi-) projective schemes are closed under products. Is that also true for dependent sums? I don't know the classical answer but there might be a more or less immediate generalization of the classical argument using Zariski-choice and the Segre-Embedding.

So, in algebraic geometry we're often interested in varieties which are usually defined as an integral, separated scheme of finite type over an (algebraically closed) field $k$. Basically, we're studying schemes over $k$ in this case, so I assume we want to be working in the big Zariski topos of $\mathrm{Spec} \ k$ in this case.

Now, we know very well that $R$ is just the internal view of $\underline{\mathbb{A}}^1_{\mathrm{Spec} \ k} = \underline{\mathrm{Spec} \ k[t]}$ (i.e. the functor of points of $\mathrm{Spec} \ k[t]$). The question is, what internal properties would characterize this fact?

Until recently I thought a scheme of finite type is locally of the form $\mathrm{Spec}(R[X_1,\dots,X_n]/(f_1,\dots,f_m))$ - but that is actually called scheme of finite presentation. So this should be wrong in quite a lot of places. We should change all drafts accordingly:

• A1-homotopy
• cech
• diffgeo
• elliptic
• foundations
• proper
• random-facts
• sheaves
• stacks
• topology
• slides

At various points, we would like to quantify internally not over all types, but over "locally locally constant sheaves" (?). For example, naively we would say a general (not necessarily quasi-compact) open proposition is one of the form $\exists (i : I), f(i) \ne 0$, where $I$ is some type and $f : I \to R$. But if we allow all types, then every proposition $P$ is open (take $I = P$ and $f$ constantly $1$). Instead we restrict to finite types.

But how about the following more general notion. (I think we discussed something like this at SAG 2 with @iblech.) We define what it means for a (0-truncated) type $I$ to be external. It is a general fact that $I$ is the filtered colimit of $[n]$ over all $n : \mathbb N$ and maps $[n] \to I$. Say $I$ is external if this colimit is preserved by the functor $(-)^X$ for every affine scheme $X$. I think this means that any map $X \to I$ factors through $[n]$ for some $[n]$, and that two maps $X \to [n] \to I$ and $X \to [m] \to I$ are equal only if there is a common co-refinement $X \to [k] \to I$ (via maps $[n] \to [k]$, $[m] \to [k]$ making everything commute). For example $\mathbb N$ (by boundedness) and any finite set should be external.

I don't know if this is exactly the right definition. But my question is: can we use some definition like this to go beyond finiteness restrictions in SAG, to define general opens and perhaps general schemes (not necessarily finitely presented)?

In Proposition 5.1.3 in the Foundations, it says

basic opens of the affine parts of $X$

where $X$ is a scheme. As the datum of an affine cover of $X$ is truncated to a mere proposition in the definition of a scheme, "basic opens of the" seems superfluous, doesn't it?

This is a sort of continuation to #18.

Does the Nisnevich $(\infty, 1)$-topos on $\mathbf{Sch}/S$ admit a useful cohesive structure?

The nLab page on motivic homotopy theory suggests that if one is working in the right topos (i.e., Nisnevich), then localizing at $\mathbb{A}^1$ will appropriately give one the motivic homotopy theory. Now, I'm probably interpreting it very wrong, but it seems to follow that if one is working in the Nisnevich topos (as one should be), then localization at $\mathbb{A}^1$ will give one the shape modality one wants, giving the higher Nisnevich topos the cohesive structure one wants.

I wonder what one can make out of this.

Shall we make this repo BibTex-aware?

https://citation-file-format.github.io/

Formulated more in line with the A1-homotopy draft:
Is $B\widetilde{\mathbb A^\times}$ an $\mathbb A^1$-local type?
Using reasoning from 2.2 in the A1-homotopy draft, it is enough to show that $H^1(\mathbb A^1,\widetilde{\mathbb A^\times})=0$.

I remember that @fabianmasato and @mnieper discussed a proof with me, that maps from a connected projective scheme, i.e. a connected closed subset of some $\mathbb{P}^n$, to the base ring $R$ should be constant. Does anyone remember the details?

I think we should consider having a table somewhere listing all important definitions and theorems, together with a latex identifier (or issue) and a link to a formalization, if it exists.
One advantage should be, that definitions and usages are easy to find then, using the latex-identifier. On the other hand, those have to be longer then.
Another thing is, that if we start to point to formalization (which I think should always be done by pointing to a part of a file in a specific commit), we might be able to build something which is update-able in a not-so-painful way.

There is one way to ask our base ring R to be of characteristic 0: Define the map $\iota:\mathbb{N}\to R$ and then ask that $\prod_{n:\mathbb{N}}\neg(\iota(n+1)=0)$ holds.

But this is a bit suspicious in light of this excerpt from @iblech 's thesis:

this might be problematic. So one concrete question is: Can we show that $R$ is not of characteristic 0 as defined above?

Can we give a pointwise definition of flat maps between (affine) schemes?

This (hopefully) boils down to the following external question:
Let $i:M\to\mathrm{Sh}(\mathrm{Zar})$ be the inclusion of the $\mathbb A^1$-local sheaves into all Zariski-sheaves. Then the localization is a left adjoint to $i$ and the question if there is a flat modality should be the question if $i$ also has a right adjoint or equivalently preserves homotopy colimits. I am not sure if that would be enough, but if it is false, we can definitely start to seriously question #17 .
Assuming a flat-modality, it should work to use David Jaz Myers idea in the good fibrations article, theorem 5.9 taking for X the type of torsors of crisply discrete groups, to show #17.

Peter Arndt suggested the following classic trick:

There is a map to $\mathbb{P}^n$, from the affine type of matrices $A:R^{(n+1)\times (n+1)}$ such that $A^2=A$ and the characteristic polynomial of $A$ is $X(X-1)$. Then, for example, the fiber over $[(1,0,\dots,0)]:\mathbb{P}^n$ consists of all matrices where the first line is $(1 ~ a_0 \dots a_n)$ and everything else $0$.

The conditions are closed so this type of matrices is affine and all fibers of the map to $\mathbb{P}^n$ are $\mathbb{A}^1$-connected.
The latter implies this map is an $\mathbb{A}^1$-equivalence.

This extends to closed subsets of $\mathbb{P}^n$ by pullback.

For an open subset $U$ of a closed $V\subseteq \mathbb{P}^n$ (i.e. a quasi-projective scheme), we first take a closed complement $Z$ of $U$. $Z$ is also a closed subset of $\mathbb{P}^n$. So we can take the blow-up $B$ of $\mathbb{P}^n$ at $Z$, which is projective again and therefore has a map from an affine type with $\mathbb{A}^1$-connected fibers.

Let $\widetilde{U}$ be the preimage of $U$ in $B$, then the projection $\widetilde{U}\to U$ has $\mathbb{A}^1$-connected fibers. $\widetilde{U}$ is affine, by Serre-Affinity and #10, since it is an locally-standard open (due to properties of the blow-up).

We call a module bundle on a type weakly quasi-coherent (wqc), if its sections on opens are given by (algebraic) localization (in some sense). At some occasions we concluded that the name is not so great, since these module bundles are not really an analogue of quasi-coherent sheaves. I don't remember the details of these past discussions, but I would argue that in general, our theory (in particular wqc modules and their cohomology, pullbacks and push-forwards) diverts from the classic story, so I think it would be good to also divert with our names a bit more.
I think just calling the bundles "local module bundles" would be a good fit. Happy to hear opinions on that.

Write down a proof that the map from the universe to its $\mathbb{A}^1$-shape is constant.
Use that: For types A,B a line in $\mathcal{U}$ parametrized by $x:\mathbb{A}^1$ can be constructed in the following ways (using $0\neq 1$):

(joint idea with @MatthiasHu )

Hugo suggested to me, it might be good to call an affine scheme $\mathrm{Spec} A$ finite, if A is a finite free R-module. So if $A=R^n$ is given, we can directly construct an embedding into $\mathrm{Spec}A\to \mathbb{P}^{n-1}$, by sending a homomorphism $R^n\to R$ to the vector given by the images of a standard basis $(e_i)_i$.
The proposition $C$, to be in this subtype, is closed: For $[v]:\mathbb{P}^n$ let $\lambda_v=\sum \lambda_i v_i$, for $\lambda_i$ such that $\sum \lambda_i e_i=1$. Let $\varphi_v$ be the linear map sending $e_i$ to $v_i$. Then the conjunction of all $\lambda_v\cdot \varphi_v(e_i\cdot e_j)=\varphi_v(e_i)\cdot \varphi_v(e_j)$ is well-defined and closed and cuts out the $[v]$ such that $\varphi_v$ is an algebra homomorphism up to normalization.

I'm planning to remove this warning:

I don't remember what problem made me put it everywhere (I think there was one though). Comment here if you think the warning should stay.

As far as I know, we do not have a common name of the structure sheaf of a scheme $X$, which is the constant $R$-module bundle with value $R^1$. Maybe we should call it $\mathcal O_X$?

We want to refer to axioms when proving theorems, ideally this should be a macro, e.g. '\Loc' and there should be a link.

Classically, we know that a flat morphism between varieties has a constant fibre dimension. Can we use this somehow to be able to define the notion of a flat scheme of dimension $n$ in SAG? A flat morphism of (relative) dimension $n$ would then be a morphism whose fibres are flat of dimension $n$. The notion should correspond to the notion of dimension we have for smooth schemes. A finite flat scheme should be of dimension $0$.

At the last hour of SAG-4, we had a discussion on names. The following was discussed in more detail:

• SQC Axiom. By now we have already started to call it "Duality". This is a bit unspecific. In the discussion, the following proposals were made and not discarded:
  • Duality for fp R-algebras
  • R is dualizing for fp algebras
  • Blechschmidt Duality
    It was considered an advantage of the second option, that R appears very prominently, as it should since duality is a property of R. It could also make sense to use option 2 and call the fact that it is validated by the Zariski topos "Blechschmidt Duality".
• We could call finitely co-presented R-modules "vector spaces".
• Everyone taking part in the discussion agreed after exchanging arguments for a while, that we should abandon the current practice of having different names for "the same" types, e.g. $\mathbb G_m$, $\mathbb A^\times$, $R^\times$ all denote the same, as do $\mathbb A^n$ and $R^n$. The distinction was usually justified by using them to make the coercions to schemes, groups, rings, algebras explicit. However, it does not seems that it is reasonably clear when to use which notation and it has been a source of confusion. Also, just using $R$ everywhere seems a lot simpler and emphasizes the advantage of SAG that this is possible.

A subset $U\subseteq X$ is locally-basic open, if for each point, it is of the form $D(f)$.
Then the inclusion $i$ of this subset has affine fibers and therefore induces an isomorphism on cohomology
$H^k(U,F)\cong H^k(X,i_*F)$

We should write down what we know about those automorphism groups.