stacky wiki - User contributions [en]

Properties of morphisms

2011-10-26T22:43:01Z

132.239.145.162: /* Effective descent classes */

=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.

{|class="wikitable"
|-
|
|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
| bgcolor="pink" | NO
|EGA IV2, 2.6.1(iv)
| bgcolor="pink" | NO
|-
|closed
|EGA I, 2.2.6
|EGA I, 2.2.7(i)
| bgcolor="pink" | NO
|EGA IV2, 2.6.2(ii)
| bgcolor="red" |
|-
|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)
| bgcolor="pink" | NO
| bgcolor="red" |
| bgcolor="red" |
|-
|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
| bgcolor="red" |
|-
|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)
| bgcolor="red" |
|-
|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)
| bgcolor="red" |
|-
|flat
|EGA I, 0:6.7.1
|EGA IV2, 2.1.6
|EGA IV2, 2.1.4
|EGA IV2, 2.2.11(iv)
| bgcolor="red" |
|-
|formally etale
|EGA IV4, 17.1.1
|EGA IV4, 17.1.3(ii)
|EGA IV4, 17.1.3(iii)
| bgcolor="red" |
| bgcolor="red" |
|-
|formally smooth
|EGA IV4, 17.1.1
|EGA IV4, 17.1.3(ii)
|EGA IV4, 17.1.3(iii)
| bgcolor="red" |
| bgcolor="red" |
|-
|formally unram.
|EGA IV4, 17.1.1
|EGA IV4, 17.1.3(ii)
|EGA IV4, 17.1.3(iii)
| bgcolor="red" |
| bgcolor="red" |
|-
|fppf
|Definition 3.4.1
|YES
|YES
|YES
| bgcolor="red" |
|-
|fpqc
|[http://arxiv.org/abs/math/0412512 Vis05], 2.34
|[http://arxiv.org/abs/math/0412512 Vis05], 2.35(i)
|[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
|
|YES
| bgcolor="pink" | NO
|EGA IV2, 2.6.2(iv)
|-
|immersion
|EGA I, 4.2.1
|EGA I, 4.2.5
|EGA I, 4.3.2
| bgcolor="red" |
|EGA IV3, 8.10.5(iii)
|-
|injective
|EGA I, 3.5.11
|YES
| bgcolor="pink" | NO
|EGA IV2, 2.6.1(ii)
| bgcolor="pink" | 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
| bgcolor="red" |
|-
|loc. isomorphism
|EGA I, 4.5.2
|EGA I, 4.5.5(i)
|EGA I, 4.5.5(iii)
| bgcolor="red" |
| bgcolor="red" |
|-
|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)
| bgcolor="red" |
|-
|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)
| bgcolor="pink" | NO
|EGA IV2, 2.6.2(i)
| bgcolor="red" |
|-
|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)
| bgcolor="pink" | 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)
| bgcolor="red" |
|-
|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)
| bgcolor="pink" | 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)
| bgcolor="red" |
|-
|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
| bgcolor="pink" | NO
|EGA IV3, 11.10.5(i)
| bgcolor="red" |
|-
|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)
| bgcolor="red" |
| bgcolor="red" |
|-
|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)
| bgcolor="red" |
|-
|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)
| bgcolor="red" |
|-
|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)
| bgcolor="red" |
|-
|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 <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>

Properties of morphisms

2011-10-26T22:42:05Z

132.239.145.162: /* Effective descent classes */