# 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'))

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.
addthm(['quasi-affine'],'representable') addthm(['immersion'],'representable') addthm(['separated','locally quasi-finite'],'representable')