Properties of morphisms: Difference between revisions

From stacky wiki
No edit summary
 
(14 intermediate revisions by 2 users not shown)
Line 1: Line 1:
The following table is taken from page 179 of [http://www-math.mit.edu/~poonen/ Bjorn Poonen's] [http://math.mit.edu/~poonen/papers/Qpoints.pdf Rational points on varieties]
=Bjorn Poonen's table=
 
The following table is taken from page 179 of [http://www-math.mit.edu/~poonen/ Bjorn Poonen's] [http://math.mit.edu/~poonen/papers/Qpoints.pdf 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''}}


{|class="wikitable"
{|class="wikitable"
Line 20: Line 24:
|
|
|YES
|YES
|NO
| bgcolor="pink" | NO
|EGA IV<sub>2</sub>, 2.6.1(iv)
|EGA IV<sub>2</sub>, 2.6.1(iv)
|NO
| bgcolor="pink" | NO
|-
|-
|closed
|closed
|EGA I, 2.2.6
|EGA I, 2.2.6
|EGA I, 2.2.7(i)
|EGA I, 2.2.7(i)
|NO
| bgcolor="pink" | NO
|EGA IV<sub>2</sub>, 2.6.2(ii)
|EGA IV<sub>2</sub>, 2.6.2(ii)
|
| bgcolor="red" |
|-
|-
|closed immersion
|closed immersion
Line 41: Line 45:
|EGA I, 2.2.6
|EGA I, 2.2.6
|EGA I, 2.2.7(i)
|EGA I, 2.2.7(i)
|NO
| bgcolor="pink" | NO
|
| bgcolor="red" |
|
| bgcolor="red" |
|-
|-
|etale
|etale
Line 50: Line 54:
|EGA IV<sub>4</sub>, 17.3.3(ii)
|EGA IV<sub>4</sub>, 17.3.3(ii)
|EGA IV<sub>4</sub>, 17.7.4(vi)
|EGA IV<sub>4</sub>, 17.7.4(vi)
|EGA IV<sub>4</sub>, 17.7.8(ii).
|EGA IV<sub>4</sub>, 17.7.8(ii)
|-
|-
|faithfully flat
|faithfully flat
Line 57: Line 61:
|YES
|YES
|YES
|YES
|
| bgcolor="red" |
|-
|-
|finite
|finite
Line 71: Line 75:
|EGA IV<sub>1</sub>, 1.6.2(iii)
|EGA IV<sub>1</sub>, 1.6.2(iii)
|EGA IV<sub>2</sub>, 2.7.1(vi)
|EGA IV<sub>2</sub>, 2.7.1(vi)
|
| bgcolor="red" |
|-
|-
|finite type
|finite type
Line 78: Line 82:
|EGA I, 6.3.4(iv)
|EGA I, 6.3.4(iv)
|EGA IV<sub>2</sub>, 2.7.1(v)
|EGA IV<sub>2</sub>, 2.7.1(v)
|
| bgcolor="red" |
|-
|-
|flat
|flat
Line 85: Line 89:
|EGA IV<sub>2</sub>, 2.1.4
|EGA IV<sub>2</sub>, 2.1.4
|EGA IV<sub>2</sub>, 2.2.11(iv)
|EGA IV<sub>2</sub>, 2.2.11(iv)
|
| bgcolor="red" |
|-
|-
|formally etale
|formally etale
Line 91: Line 95:
|EGA IV<sub>4</sub>, 17.1.3(ii)
|EGA IV<sub>4</sub>, 17.1.3(ii)
|EGA IV<sub>4</sub>, 17.1.3(iii)
|EGA IV<sub>4</sub>, 17.1.3(iii)
|
| bgcolor="red" |
|
| bgcolor="red" |
|-
|-
|formally smooth
|formally smooth
Line 98: Line 102:
|EGA IV<sub>4</sub>, 17.1.3(ii)
|EGA IV<sub>4</sub>, 17.1.3(ii)
|EGA IV<sub>4</sub>, 17.1.3(iii)
|EGA IV<sub>4</sub>, 17.1.3(iii)
|
| bgcolor="red" |
|
| bgcolor="red" |
|-
|-
|formally unram.
|formally unram.
Line 105: Line 109:
|EGA IV<sub>4</sub>, 17.1.3(ii)
|EGA IV<sub>4</sub>, 17.1.3(ii)
|EGA IV<sub>4</sub>, 17.1.3(iii)
|EGA IV<sub>4</sub>, 17.1.3(iii)
|
| bgcolor="red" |
|
| bgcolor="red" |
|-
|-
|fppf
|fppf
Line 113: Line 117:
|YES
|YES
|YES
|YES
|
| bgcolor="red" |
|-
|-
|fpqc
|fpqc
|Vis05, 2.34
|[http://arxiv.org/abs/math/0412512 Vis05], 2.34
|Vis05, 2.35(i)
|[http://arxiv.org/abs/math/0412512 Vis05], 2.35(i)
|Vis05, 2.35(v)
|[http://arxiv.org/abs/math/0412512 Vis05], 2.35(v)
|
| bgcolor="red" |
|
| bgcolor="red" |
|-
|good moduli space
|[http://arxiv.org/abs/0804.2242 Alp08] 4.1
|YES
|[http://arxiv.org/abs/0804.2242 Alp08] 4.7(i)
|[http://arxiv.org/abs/0804.2242 Alp08] 4.7(ii)
| bgcolor="red" |
|-
|-
|homeomorphism
|homeomorphism
|
|
|YES
|YES
|NO
| bgcolor="pink" | NO
|EGA IV<sub>2</sub>, 2.6.2(iv)
|EGA IV<sub>2</sub>, 2.6.2(iv)
|-
|-
Line 132: Line 143:
|EGA I, 4.2.5
|EGA I, 4.2.5
|EGA I, 4.3.2
|EGA I, 4.3.2
|
| bgcolor="red" |
|EGA IV<sub>3</sub>, 8.10.5(iii)
|EGA IV<sub>3</sub>, 8.10.5(iii)
|-
|-
Line 138: Line 149:
|EGA I, 3.5.11
|EGA I, 3.5.11
|YES
|YES
|NO
| bgcolor="pink" | NO
|EGA IV<sub>2</sub>, 2.6.1(ii)
|EGA IV<sub>2</sub>, 2.6.1(ii)
|NO
| bgcolor="pink" | NO
|-
|-
|isomorphism
|isomorphism
Line 153: Line 164:
|EGA I, 4.5.5(i)
|EGA I, 4.5.5(i)
|EGA I, 4.5.5(iii)
|EGA I, 4.5.5(iii)
|
|YES
|
| bgcolor="red" |
|-
|-
|loc. isomorphism
|loc. isomorphism
Line 160: Line 171:
|EGA I, 4.5.5(i)
|EGA I, 4.5.5(i)
|EGA I, 4.5.5(iii)
|EGA I, 4.5.5(iii)
|
| bgcolor="red" |
|
| bgcolor="red" |
|-
|-
|loc. of finite pres.
|loc. of finite pres.
Line 168: Line 179:
|EGA IV<sub>1</sub>, 1.4.2(iii)
|EGA IV<sub>1</sub>, 1.4.2(iii)
|EGA IV<sub>2</sub>, 2.7.1(iv)
|EGA IV<sub>2</sub>, 2.7.1(iv)
|
| bgcolor="red" |
|-
|-
|loc. of finite type
|loc. of finite type
Line 186: Line 197:
|EGA I, 2.2.6
|EGA I, 2.2.6
|EGA I, 2.2.7(i)
|EGA I, 2.2.7(i)
|NO
| bgcolor="pink" | NO
|EGA IV<sub>2</sub>, 2.6.2(i)
|EGA IV<sub>2</sub>, 2.6.2(i)
|
| bgcolor="red" |
|-
|-
|open immersion
|open immersion
Line 201: Line 212:
|EGA II, 5.5.5(ii).
|EGA II, 5.5.5(ii).
|EGA II, 5.5.5(iii)
|EGA II, 5.5.5(iii)
|NO.
| bgcolor="pink" | NO.
|EGA IV<sub>3</sub>, 8.10.5(xiii).
|EGA IV<sub>3</sub>, 8.10.5(xiii)
|-
|-
|proper
|proper
Line 223: Line 234:
|EGA I, 6.6.4(iii)
|EGA I, 6.6.4(iii)
|EGA IV<sub>2</sub>, 2.6.4(v)
|EGA IV<sub>2</sub>, 2.6.4(v)
|
| bgcolor="red" |
|-
|-
|quasi-finite
|quasi-finite
Line 234: Line 245:
|quasi-projective
|quasi-projective
|EGA II, 5.3.1
|EGA II, 5.3.1
|EGA II, 5.3.4(ii).
|EGA II, 5.3.4(ii)
|EGA II, 5.3.4(iii)
|EGA II, 5.3.4(iii)
|NO.
| bgcolor="pink" | NO
|EGA IV<sub>3</sub>, 8.10.5(xiv).
|EGA IV<sub>3</sub>, 8.10.5(xiv)
|-
|-
|quasi-separated
|quasi-separated
Line 244: Line 255:
|EGA IV<sub>1</sub>, 1.2.2(iii)
|EGA IV<sub>1</sub>, 1.2.2(iii)
|EGA IV<sub>2</sub>, 2.7.1(ii)
|EGA IV<sub>2</sub>, 2.7.1(ii)
|
| bgcolor="red" |
|-
|-
|radicial
|radicial
Line 256: Line 267:
|EGA IV<sub>3</sub>, 11.10.2
|EGA IV<sub>3</sub>, 11.10.2
|YES
|YES
|NO
| bgcolor="pink" | NO
|EGA IV<sub>3</sub>, 11.10.5(i)
|EGA IV<sub>3</sub>, 11.10.5(i)
|
| bgcolor="red" |
|-
|-
|separated
|separated
Line 272: Line 283:
|EGA IV<sub>4</sub>, 17.3.3(iii)
|EGA IV<sub>4</sub>, 17.3.3(iii)
|EGA IV<sub>4</sub>, 17.7.4(v)
|EGA IV<sub>4</sub>, 17.7.4(v)
|EGA IV<sub>4</sub>, 17.7.8(ii).
|EGA IV<sub>4</sub>, 17.7.8(ii)
|-
|-
|surjective
|surjective
Line 285: Line 296:
|EGA IV<sub>2</sub>, 2.4.3(ii)
|EGA IV<sub>2</sub>, 2.4.3(ii)
|EGA IV<sub>2</sub>, 2.4.3(iii)
|EGA IV<sub>2</sub>, 2.4.3(iii)
|
| bgcolor="red" |
|
| bgcolor="red" |
|-
|-
|univ. closed
|univ. closed
Line 293: Line 304:
|EGA IV<sub>2</sub>, 2.4.3(iii)
|EGA IV<sub>2</sub>, 2.4.3(iii)
|EGA IV<sub>2</sub>, 2.6.4(ii)
|EGA IV<sub>2</sub>, 2.6.4(ii)
|
| bgcolor="red" |
|-
|-
|univ. homeom.
|univ. homeom.
Line 300: Line 311:
|EGA IV<sub>2</sub>, 2.4.3(iii)
|EGA IV<sub>2</sub>, 2.4.3(iii)
|EGA IV<sub>2</sub>, 2.6.4(iv)
|EGA IV<sub>2</sub>, 2.6.4(iv)
|
| bgcolor="red" |
|-
|-
|univ. open
|univ. open
Line 307: Line 318:
|EGA IV<sub>2</sub>, 2.4.3(iii)
|EGA IV<sub>2</sub>, 2.4.3(iii)
|EGA IV<sub>2</sub>, 2.6.4(i)
|EGA IV<sub>2</sub>, 2.6.4(i)
|
| bgcolor="red" |
|-
|-
|unramified
|unramified
Line 314: Line 325:
|EGA IV<sub>4</sub>, 17.3.3(iii)
|EGA IV<sub>4</sub>, 17.3.3(iii)
|EGA IV<sub>4</sub>, 17.7.4(iv)
|EGA IV<sub>4</sub>, 17.7.4(iv)
|EGA IV<sub>4</sub>, 17.7.8(ii).
|EGA IV<sub>4</sub>, 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 <code>locally finitely presented</code>. 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==
<code><pre>
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
</pre></code>
==Definitions and non-theorems==
<code><pre>
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'])
</pre></code>
It would be nice to set things up so that the following trivial theorems didn't have to be loaded.
<code><pre>
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')
</pre></code>
==Theorems==
<code><pre>
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
</pre></code>
==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 <code>(['quasi-compact','immersion'],[('smooth','separated'),'finite type'])</code> 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 <code>addthm('*','locally *')</code>. 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==
<code><pre>
addthm(['quasi-affine'],'representable')
addthm(['immersion'],'representable')
addthm(['separated','locally quasi-finite'],'representable')
</pre></code>

Latest revision as of 18:11, 17 February 2012

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')
Retrieved from "https://stacky.net/wiki/index.php?title=Properties_of_morphisms&oldid=921"