Properties of morphisms: Difference between revisions
| Line 368: | Line 368: | ||
</pre></code> | </pre></code> | ||
==Definitions== | ==Definitions and non-theorems== | ||
<code><pre> | <code><pre> | ||
define('closed immersion',['closed', 'immersion']) | define('closed immersion',['closed', 'immersion']) | ||
define('etale',['formally etale','locally of finite presentation']) | define('etale',['formally etale','locally of finite presentation']) | ||
define('finite',['affine','proper']) | define('finite',['affine','proper']) | ||
define('finite type',['locally finite type','quasi-compact']) | define('finite type',['locally finite type','quasi-compact']) | ||
define('finitely presented',['locally of finite presentation','quasi-compact']) | define('finitely presented',['locally of finite presentation','quasi-compact']) | ||
| Line 386: | Line 385: | ||
# define('separated',['quasi-compact diagonal']) # right definition? | # define('separated',['quasi-compact diagonal']) # right definition? | ||
define('smooth',['formally smooth','locally of finite presentation']) | define('smooth',['formally smooth','locally of finite presentation']) | ||
define('unramified',['formally unramified','locally of finite presentation']) | define('unramified',['formally unramified','locally of finite presentation']) | ||
addthm(['locally finite type','noetherian base'],'noetherian source') | |||
addthm(['locally finite type','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') | |||
</pre></code> | </pre></code> | ||
==Theorems== | ==Theorems== | ||
<code><pre> | <code><pre> | ||
define('affine',['cohomologically affine','representable']) # Serre's criterion for affineness | |||
addthm(['affine','stein'],'isomorphism') | addthm(['affine','stein'],'isomorphism') | ||
addthm(['proper'],'f_*(coh)=coh') | addthm(['proper'],'f_*(coh)=coh') | ||
addthm(['good moduli space'],'f_*(coh)=coh') | addthm(['good moduli space'],'f_*(coh)=coh') | ||
addthm(['good moduli space'],'universally closed') | addthm(['good moduli space'],'universally closed') | ||
addthm(['fppf'],'open') | addthm(['fppf'],'open') | ||
addthm(['smooth','regular base'],'regular source') | 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','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','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(['proper','quasi-finite'],'finite') # somewhere in EGA IV.18.12 | ||
</pre></code> | |||
==Effective descent classes | |||
<code><pre> | |||
addthm(['quasi-affine'],'representable') | |||
addthm(['immersion'],'representable') | |||
</pre></code> | </pre></code> | ||
Revision as of 14:34, 7 October 2011
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.
| 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) | ||
| 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) | ||
| 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('separated',['quasi-compact diagonal']) # right definition?
define('smooth',['formally smooth','locally of finite presentation'])
define('unramified',['formally unramified','locally of finite presentation'])
addthm(['locally finite type','noetherian base'],'noetherian source')
addthm(['locally finite type','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')
Theorems
define('affine',['cohomologically affine','representable']) # Serre's criterion for affineness
addthm(['affine','stein'],'isomorphism')
addthm(['proper'],'f_*(coh)=coh')
addthm(['good moduli space'],'f_*(coh)=coh')
addthm(['good moduli space'],'universally closed')
addthm(['fppf'],'open')
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
==Effective descent classes
addthm(['quasi-affine'],'representable')
addthm(['immersion'],'representable')