search

felixwellen / synthetic-geometry

Synthetic geometry. Probably mostly algebraic geometry.
MIT License
23 stars 4 forks source link

Define 'D(f)' #31

Open felixwellen opened 1 year ago

felixwellen commented 1 year ago

$D(f)$ is the open subscheme given as the elements of an affine scheme $\mathrm{Spec}(A)$, where a function $f:\mathrm{Spec}(A)\to R$ has an invertible value. $D(f)$ is a type which is an affine scheme and defines an (qc-)open proposition on $\mathrm{Spec}(A)$.

felixwellen commented 1 year ago

One problematic thing is to define the fp algebra $A_f$, which should probably be done in the cubical library. This might lead to a type checking speed problem.