Properties of morphisms
Bjorn Poonen's table
The following table is taken from page 179 of Bjorn Poonen's Rational points on varieties. I copied it because it's slightly more accessible to me as a web page, and so that I can add information to it.
[Todo: add column for local on the source]
| Definition | Composition | Base Change | fpqc Descent | Spreading Out | |
| affine | EGA II, 1.6.1 | EGA II, 1.6.2(ii) | EGA II, 1.6.2(iii) | EGA IV2, 2.7.1(xiii) | EGA IV3, 8.10.5(viii) |
| bijective | YES | NO | EGA IV2, 2.6.1(iv) | NO | |
| closed | EGA I, 2.2.6 | EGA I, 2.2.7(i) | NO | EGA IV2, 2.6.2(ii) | |
| closed immersion | EGA I, 4.2.1 | EGA I, 4.2.5 | EGA I, 4.3.2 | EGA IV2, 2.7.1(xii) | EGA IV3, 8.10.5(iv) |
| dominant | EGA I, 2.2.6 | EGA I, 2.2.7(i) | NO | ||
| etale | EGA IV4, 17.3.1 | EGA IV4, 17.3.3(ii) | EGA IV4, 17.3.3(ii) | EGA IV4, 17.7.4(vi) | EGA IV4, 17.7.8(ii) |
| faithfully flat | EGA I, 0:6.7.8 | YES | YES | YES | |
| finite | EGA II, 6.1.1 | EGA II, 6.1.5(ii) | EGA II, 6.1.5(iii) | EGA IV2, 2.7.1(xv) | EGA IV3, 8.10.5(x) |
| finite presentation | EGA IV1, 1.6.1 | EGA IV1, 1.6.2(ii) | EGA IV1, 1.6.2(iii) | EGA IV2, 2.7.1(vi) | |
| finite type | EGA I, 6.3.1 | EGA I, 6.3.4(ii) | EGA I, 6.3.4(iv) | EGA IV2, 2.7.1(v) | |
| flat | EGA I, 0:6.7.1 | EGA IV2, 2.1.6 | EGA IV2, 2.1.4 | EGA IV2, 2.2.11(iv) | |
| formally etale | EGA IV4, 17.1.1 | EGA IV4, 17.1.3(ii) | EGA IV4, 17.1.3(iii) | ||
| formally smooth | EGA IV4, 17.1.1 | EGA IV4, 17.1.3(ii) | EGA IV4, 17.1.3(iii) | ||
| formally unram. | EGA IV4, 17.1.1 | EGA IV4, 17.1.3(ii) | EGA IV4, 17.1.3(iii) | ||
| fppf | Definition 3.4.1 | YES | YES | YES | |
| fpqc | Vis05, 2.34 | Vis05, 2.35(i) | Vis05, 2.35(v) | ||
| good moduli space | Alp08 4.1 | YES | Alp08 4.7(i) | Alp08 4.7(ii) | |
| homeomorphism | YES | NO | EGA IV2, 2.6.2(iv) | ||
| immersion | EGA I, 4.2.1 | EGA I, 4.2.5 | EGA I, 4.3.2 | EGA IV3, 8.10.5(iii) | |
| injective | EGA I, 3.5.11 | YES | NO | EGA IV2, 2.6.1(ii) | NO |
| isomorphism | EGA I, 2.2.2 | YES | YES | EGA IV2, 2.7.1(viii) | EGA IV3, 8.10.5(i) |
| loc. immersion | EGA I, 4.5.1 | EGA I, 4.5.5(i) | EGA I, 4.5.5(iii) | YES | |
| loc. isomorphism | EGA I, 4.5.2 | EGA I, 4.5.5(i) | EGA I, 4.5.5(iii) | ||
| loc. of finite pres. | EGA IV1, 1.4.2 | EGA IV1, 1.4.2(ii) | EGA IV1, 1.4.2(iii) | EGA IV2, 2.7.1(iv) | |
| loc. of finite type | EGA I, 6.6.2 | EGA I, 6.6.6(ii) | EGA I, 6.6.6(iii) | EGA IV2, 2.7.1(iii) | |
| monomorphism | EGA I, 0:4.1.1 | YES | YES | EGA IV2, 2.7.1(ix) | EGA IV3, 8.10.5(ii) |
| open | EGA I, 2.2.6 | EGA I, 2.2.7(i) | NO | EGA IV2, 2.6.2(i) | |
| open immersion | EGA I, 4.2.1 | EGA I, 4.2.5 | EGA I, 4.3.2 | EGA IV2, 2.7.1(x) | EGA IV3, 8.10.5(iii) |
| projective | EGA II, 5.5.2 | EGA II, 5.5.5(ii). | EGA II, 5.5.5(iii) | NO. | EGA IV3, 8.10.5(xiii) |
| proper | EGA II, 5.4.1 | EGA II, 5.4.2(ii) | EGA II, 5.4.2(iii) | EGA IV2, 2.7.1(vii) | EGA IV3, 8.10.5(xii) |
| quasi-affine | EGA II, 5.1.1 | EGA II, 5.1.10(ii) | EGA II, 5.1.10(iii) | EGA IV2, 2.7.1(xiv) | EGA IV3, 8.10.5(ix) |
| quasi-compact | EGA I, 6.6.1 | EGA I, 6.6.4(ii) | EGA I, 6.6.4(iii) | EGA IV2, 2.6.4(v) | |
| quasi-finite | EGA II, 6.2.3 | EGA II, 6.2.4(ii) | EGA II, 6.2.4(iii) | EGA IV2, 2.7.1(xvi) | EGA IV3, 8.10.5(xi) |
| quasi-projective | EGA II, 5.3.1 | EGA II, 5.3.4(ii) | EGA II, 5.3.4(iii) | NO | EGA IV3, 8.10.5(xiv) |
| quasi-separated | EGA IV1, 1.2.1 | EGA IV1, 1.2.2(ii) | EGA IV1, 1.2.2(iii) | EGA IV2, 2.7.1(ii) | |
| radicial | EGA I, 3.5.4 | EGA I, 3.5.6(i) | EGA I, 3.5.7(ii) | EGA IV2, 2.6.1(v) | EGA IV3, 8.10.5(vii) |
| sch.-th. dominant | EGA IV3, 11.10.2 | YES | NO | EGA IV3, 11.10.5(i) | |
| separated | EGA I, 5.4.1 | EGA I, 5.5.1(ii) | EGA I, 5.5.1(iv) | EGA IV2, 2.7.1(i) | EGA IV3, 8.10.5(v) |
| smooth | EGA IV4, 17.3.1 | EGA IV4, 17.3.3(ii) | EGA IV4, 17.3.3(iii) | EGA IV4, 17.7.4(v) | EGA IV4, 17.7.8(ii) |
| surjective | EGA I, 2.2.6 | EGA I, 2.2.7(i) | EGA I, 3.5.2(ii) | EGA IV2, 2.6.1(i) | EGA IV3, 8.10.5(vi) |
| univ. bicontinuous | EGA IV2, 2.4.2 | EGA IV2, 2.4.3(ii) | EGA IV2, 2.4.3(iii) | ||
| univ. closed | EGA II, 5.4.9 | EGA IV2, 2.4.3(ii) | EGA IV2, 2.4.3(iii) | EGA IV2, 2.6.4(ii) | |
| univ. homeom. | EGA IV2, 2.4.2 | EGA IV2, 2.4.3(ii) | EGA IV2, 2.4.3(iii) | EGA IV2, 2.6.4(iv) | |
| univ. open | EGA IV2, 2.4.2 | EGA IV2, 2.4.3(ii) | EGA IV2, 2.4.3(iii) | EGA IV2, 2.6.4(i) | |
| unramified | EGA IV4, 17.3.1 | EGA IV4, 17.3.3(ii) | EGA IV4, 17.3.3(iii) | EGA IV4, 17.7.4(iv) | EGA IV4, 17.7.8(ii) |
Deducer
I had the idea to stupidly deduce properties of morphisms (in algebraic geometry) with a computer. This is not an attempt to write a clever proof generator. This isn't really working yet, but it shouldn't take much more effort to get it working.
Each property is a string, like locally finitely presented. Each "theorem" is a rule that if a given set of properties are known to be true, then an additional property is known to be true. A "definition" of a property is a theorem that says that a given property is true if and only if each of the properties on a list is true.
Basic objects and functions
atomic_properties = [] # these are properties which are not defined in terms of others
properties = []
theorems = []
def define(prop,lst,atomic=False):
if prop not in properties: properties.append(prop)
if prop in atomic_properties and not atomic:
atomic_properties.remove(prop) # turns out it *is* defined in terms of other things
theorems.append((lst,prop))
for x in lst:
theorems.append(([prop],x))
if x not in properties:
print 'Warning: "'+x+'" is not a known property. Adding it to the list.'
atomic_properties.append(x)
properties.append(x)
def addthm(hyplist,conclusion):
for x in hyplist:
if x not in properties:
print 'Warning: "'+x+'" is not a known property. Adding it to the list.'
properties.append(x)
atomic_properties.append(x)
if conclusion not in properties:
print 'Warning: "'+conclusion+'" is not a known property. Adding it to the list.'
properties.append(conclusion)
atomic_properties.append(conclusion)
theorems.append((hyplist,conclusion))
def deduced_from(given):
deduced = given
done = False
while not done:
done = True
for hypotheses, conclusion in theorems:
if conclusion not in deduced and False not in [x in deduced for x in hypotheses]:
# if all hypotheses satisfied and conclusion is not known yet
deduced.append(conclusion)
done = False # still making deductions
return deduced
Definitions and non-theorems
define('closed immersion',['closed', 'immersion'])
define('etale',['formally etale','locally of finite presentation'])
define('finite',['affine','proper'])
define('finite type',['locally finite type','quasi-compact'])
define('finitely presented',['locally of finite presentation','quasi-compact'])
define('formally etale',['formally smooth','formally unramified'])
define('fppf',['flat','locally of finite presentation']) # missing faithfulness because fppf is local on the source
define('good moduli space',['cohomologically affine','stein'])
define('open immersion',['open', 'immersion'])
define('proper',['separated','finite type','universally closed'])
define('quasi-separated',['separated diagonal'])
define('separated',['proper diagonal'])
define('quasi-separated',['quasi-compact diagonal'])
define('smooth',['formally smooth','locally of finite presentation'])
define('unramified',['formally unramified','locally of finite presentation'])
It would be nice to set things up so that the following trivial theorems didn't have to be loaded.
addthm(['locally finite type','locally noetherian base'],'locally noetherian source')
addthm(['locally finite type','locally noetherian base'],'locally of finite presentation')
addthm(['affine'],'separated')
addthm(['closed immersion'],'finite type')
addthm(['closed immersion'],'affine')
addthm(['immersion'],'monomorphism')
addthm(['monomorphism'],'formally unramified')
addthm(['universally closed'],'closed')
addthm(['universally open'],'open')
addthm(['open immersion'],'locally of finite type')
addthm(['projective'],'proper')
addthm(['finite'],'quasi-finite')
addthm(['affine','stein'],'isomorphism')
Theorems
define('affine',['cohomologically affine','representable']) # Serre's criterion for affineness
addthm(['proper'],'f_*(coh)=coh')
addthm(['good moduli space'],'f_*(coh)=coh')
addthm(['good moduli space'],'universally closed')
addthm(['fppf'],'open') # EGAIV 2.4.6
addthm(['smooth','regular base'],'regular source')
define('smooth',['fppf','geometrically regular fibers']) # flat + geometrically regular fibers doesn't imply formally smooth, right?
addthm(['proper','stein','representable'],'connected fibers') #Zariski's Main Theorem; needs representable?
addthm(['proper','birational','quasi-finite','normal base','representable'],'isomorphism') #Zariski's Main Theorem ... deduce from other one?
addthm(['proper','quasi-finite'],'finite') # somewhere in EGA IV.18.12
addthm(['affine','universally closed'],'integral') # EGAIV 18.12.8
addthm(['quasi-finite','separated'],'quasi-affine') # EGAIV 18.12.12
Desirables
- It's be nice to handle compositions of morphisms. For example, ZMT (EGAIV 18.12.13) says that a quasi-compact quasi-separated quasi-finite separated morphism is an open immersion followed by a finite morphism. (note: must have representable) Perhaps the right thing to do is to simply have a syntax where a composition is represented by a tuple:
addthm(['representable','quasi-separated','quasi-compact','quasi-finite','separated'],('open immersion','finite'))
then we could also say things like
define('quasi-affine',('open immersion','affine'))
addthm(('*','isomorphism'),'*')
addthm(('isomorphism','*'),'*')
Note that we would want to redefine immersions as compositions of open then closed, and make open/closed immersions atomic.
The problem is that this could lead to combinatorial explosion, with properties like (['quasi-compact','immersion'],[('smooth','separated'),'finite type']) to mean "a quasi-compact open immersion, followed by a finite type morphisms which is a composition of a smooth morphism and a separated morphism".
- Can prefixes like "locally" and "universally" be handled well? For example, we should have
addthm('*','locally *'). This seems like it would be hard, since it would require trying to handle base change in general, which would be tricky. However, if there were a way to do it, it would make sense to encode descent theorems.
Effective descent classes
addthm(['quasi-affine'],'representable')
addthm(['immersion'],'representable')
addthm(['separated','locally quasi-finite'],'representable')