interne-methoden.txt

=== Topos der G-Mengen

Borceux, Volume 3, Seite 391.


=== Integration

Idee: Betrachte nicht fertige Integrale, sondern Riemann-Summen mit
Intervallzerlegung, die feiner werden kann.

    Z |== ...  heißt dann: Für die Zerlegung Z gilt ...

Und man betrachtet nur Eigenschaften, die unter Verfeinerung erhalten bleiben.

Beispiel:

    Z |== Box \int delta(x) f(x) dx = f(0).

Vgl. Seite 33 von /Eine Erweiterung der Infinitesimalrechnung/, Mathematische
Zeitschrift (69).


=== Entscheidbarkeit der Gleichheit reeller Zahlen

In vielen Zugängen gilt "negneg (x = 0) ==> x = 0", etwa bei den dedekindschen
reellen Zahlen oder bei Taos cheap nonstandard analysis.
http://terrytao.wordpress.com/2012/04/02/a-cheap-version-of-nonstandard-analysis/

Bei den dedekindschen Zahlen sieht man das so: Sei alpha ein Cauchy-Prozess.
Sei x eine epsilon-Näherung. Wir wollen zeigen, dass |x| <= 2 epsilon --
unter der Voraussetzung, dass nicht nicht alpha gleich Null ist.

Wäre |x| > 2 epsilon, so wäre nicht alpha gleich Null. Widerspruch.
Also |x| <= 2 epsilon.


=== Unterringe der dedekindschen reellen Zahlen in Sh(X)

* Habe {lokal konstante Fkt.} <= {glatte Fkt.} <= {stetige Fkt.} = R_dedekind.

* Habe auf R_glatt eine Endoabbildung d und eine Endoabbildung \int, zumindest
  im Fall X = R. Für d gilt: ker(R_glatt --d--> R_glatt) = R_lc = R_Cauchy.
  Sollte das auf Vektorbündel mit flachem Zusammenhang verallgemeinern können.

* http://nforum.mathforge.org/discussion/6315/internal-definitions-of-cohesion/


=== Gruppenobjekte

Mike Shulman in
https://mathematicswithoutapologies.wordpress.com/2015/05/23/language-about-language/:

A nice example of the usefulness of this is that it is quite easy to prove that
the inverse of an element in a group is unique. Therefore, it follows
automatically that the inverse morphism of a group object in a category is
unique. In particular, since (commutative) Hopf algebras are the same as group
objects in the opposite category of (commutative) rings, it follows that the
antipode of a Hopf algebra is unique. This can, of course, be proven by hand,
but it’s surprisingly tricky to figure out what you have to do if you attack it
directly. Probably the easiest way to do it is to take the usual proof for
groups, translate it into commutative diagrams, and dualize it. The point of
the internal language is that you don’t have to do all that at all; there’s a
machine that does it for you automatically.


=== Verklebung

Mike Shulman in
https://mathematicswithoutapologies.wordpress.com/2015/05/23/language-about-language/:

Even very small relationships between a few “little toposes” can be captured
internally to an auxiliary topos. For instance, if we have a geometric morphism
f:X->Y, then by gluing along the functor f^* we obtain a new topos, inside
which X and Y sit as open and closed subtoposes, and in which both parts of the
morphism f are visible by composing the relevant reflectors. The internal logic
of this glued topos can then be used to reason about the geometric morphism f.
In particular, the relationship between a topos X and the standard ∞-topos
∞Gpd, which is described by the unique geometric morphism X -> ∞Gpd and encodes
information about X such as its local connectedness, compactness, and
cohomology, can be discussed internally by gluing along that geometric
morphism. More complicated gluing constructions for more complicated diagrams
of toposes and morphisms are also possible. In one direction, this leads to
Urs’s work on cohesive ∞-toposes and cohesive HoTT; but other than that, this
avenue seems to be largely unexplored to date.


=== Ein paar Eigenschaften

* Eig. koh. Moduln kann man super intern zeigen!
  vgl. http://amathew.files.wordpress.com/2010/07/031.pdf

* X reduziertes Schema <==>
    Sh(X) |== für alle s : O_X. [s nicht invertierbar ==> s = 0].

* X beliebiges Schema. Dann erfüllt O_X in Sh(X) folgende Eigenschaft:
    für alle s : O_X. [s nicht invertierbar ==> s nilpotent].

  Beispiel, wenn X zudem quasikompakt: Sei f globale Funktion.
  Dann: f verschwindet in allen k(x) <==> f nicht invertierbar in allen Halmen
  <==> Sh(X) |= f nicht invertierbar <==> Sh(X) |= f nilpotent <==> f^n = 0 für
  ein n (hier geht Quasikompaktheit ein).

* Sei f ein Element eines Rings A. Dann sind äquivalent:

  1. Spec A |== forall g. fg nilpotent ==> g nilpotent
  2. Spec A |== nicht (f nilpotent)
  3. f schwach-regulär in folgendem Sinn: Ist fh nilpotent in A,
     so auch h.

  Schwächer ist 2'. Spec A |== nicht (f = 0). Das ist gleichbedeutend mit:
  Ist fh in A Null, so ist h nilpotent.

* Topologischer Raum X zusammenhängend <==>
    Die interne Sprache von Sh(X) erfüllt folgende Eigenschaft:
    Seien phi, psi zwei disjunkte Aussagen (d.h. phi und psi ==> _|_).
    Dann folgt aus Sh(X) |== (phi oder psi), dass Sh(X) |== phi oder
    dass Sh(X) |== psi.

* Sei X topologischer Raum und phi eine Aussage der internen Sprache von Sh(X).
  Dann gilt: [[phi]] ist genau dann eine dichte Teilmenge von X, wenn
      Sh(X) |== nicht nicht phi.

* Sei X topologischer Raum. Dann ist genau dann jede nichtleere offene
  Teilmenge von X dicht, wenn für jede Aussage phi gilt:
      nicht (Sh(X) |== nicht phi)   ==>   Sh(X) |== nicht nicht phi.

* X reduziertes Schema, F Modul von endlichem Typ.
  Dann gilt: Sh(X) |== F ist nicht nicht frei (von endlichem Rang),
  also ist F lokal frei auf einer dichten Teilmenge!


=== Offenheit

* Eine Idee ist: Eine Teilmenge U <= X heißt genau dann offen,
  wenn für jede Abbildung f : Delta --> X mit f(0) in U schon
  im(f) <= U ist.

  Mit dieser Definition sind aber alle Teilmengen von pt
  offen.


=== Kategorien intern in Sch/S

* Akhil Mathew. Categories parametrized by schemes and representation theory in
  complex rank. http://arxiv.org/abs/1006.1381v1


=== Dimension

* dim X <= n gdw. Sh(X) |== krulldim O_X <= n.

  Schön wäre es, wenn man für Affine das mit Hilfe des generischen Filters
  zeigen könnte:

      dim A <= n  gdw.  Sh(Spec(A)) |== dim AA[F^(-1)] <= n.

  Die Hinrichtung ist trivial, die Rückrichtung ist mir nicht klar. Ich will
  ein geeignetes Ideal aufstellen, dass dann von F getroffen wird und daher das
  Einsideal ist.

* dim X <= 1 gdw. Sh(X) |== forall a,b : O_X.
      a inv.  v  (a. inv ==> (b inv. v neg (b inv))).

* F_xi = 0 ==> supp F echte Teilmenge von X ==> dim supp F < dim X.

  dim F = dim O_X/Ann(F).

* depth A := sup { r | es gibt eine reguläre Sequenz der Länge r in A }.
  Damit kann man sowohl "depth A >= r" als auch "depth A <= r" formulieren:
  * depth A >= r  <==>  es gibt eine reguläre Sequenz der Länge r in A.
  * depth A <= r  <==>  jede reguläre Sequenz in A hat Länge <= r.

* Die Ungleichung depth A <= dim A gilt stets. Man kann sie etwa so beweisen:

  Sei x_1, ..., x_r eine reguläre Sequenz. Wir wollen zeigen, dass r <= dim A.
  Wir haben dim A/(x_1,...,x_r) <= dim A - r. Also (?) dim A - r >= 0.
  Also dim A >= r.

* Ein Ring A heißt circa dann Cohen-Macauley, wenn depth A >= dim A.
  Manchmal werden noch Noether-Bedingungen gestellt.

* Schön wäre sowas wie: Sh(X) |== dim O_X <= depth O_X genau dann, wenn X
  Cohen-Macauley.

  Die linke Seite hat ausgeschrieben folgende Form:

      Es gibt eine reguläre Sequenz x_1,...,x_r sodass dim O_X <= r.

  Der letzte Teil ("dim O_X <= r") ist eine geometrische Implikation.

  Wenn die linke Seite stimmt, dann sind alle lokalen Ringe Cohen-Macauley.
  Wenn X durch Spektren von noetherschen Cohen-Macauley-Ringen überdeckt werden
  kann, stimmt die linke Seite. Zumindest, wenn die für
  http://stacks.math.columbia.edu/tag/02IP relevante Definition von
  Cohec-Macauley zu meiner äquivalent ist.

* Man könnte denken, dass sowas wie "dim O_X = dim_{O_X/m} m/m^2" gelten würde
  (Georg L.). Aber das stimmt nicht. Denn m = sqrt(0); ist X reduziert,
  vereinfacht sich die rechte Seite also zu (0)/(0) = (0).

* Dimension von glatten Mannigfaltigkeiten: Siehe Fourman,
  http://www.numdam.org/article/CTGDC_1975__16_3_217_0.pdf.

  "dim <= n" genau dann, wenn Dedekindzahlen x_1, ..., x_n existieren, sodass
  jede Dedekindzahl x Bild dieser Zahlen unter einer Standardfunktion f : R^n --> R
  sind. Dabei bedeutet "Standardfunktion", dass sie Cauchyzahlen auf
  Cauchyzahlen abbildet.


=== Dominanz

* Siehe grundwissen-algebraische-geometrie.txt.


=== Noether

* X ist noethersch gdw.:

      Sh(X) |== phi_i ==> phi_(i+1) für alle i
  ==> ex. n: Sh(X) |== phi_n <==> phi_(n+1) <==> ...


=== Unterschema

* Definiere für Punkte x0 \in X (X ein LRS) einen neuen Operator in der internen
  Sprache:

      U |== !x0  gdw.  x0 \not\in U.

  Diese Erweiterung erfüllt weiterhin das Lokalitätsaxiom. Sie ist auch einfach
  das Prädikat zum offenen Kern von (X \ {x0}).

  Bemerkung: Falls x0 abgeschlossen ist, gilt für Punkte x: Genau dann gibt es
  eine offene Umgebung U von x, sodass U |== !x0, falls x ungleich x0.
  Daher kann man "!x0" als geometrische Formel ansehen, deren Rückzug auf den
  Halm bei x "x != x0" bedeutet.

* Für eine Funktion f \in O_X(X) gilt:

      f = 0 \in k(x0)  <==>  X |== (f inv. ==> !x0).

  "==>": Sei U \subseteq X. Sei f auf U invertierbar. Dann ist f auch in allen
  k(x), x \in U, invertierbar. Also x0 \not\in U.

  "<==": Auf D(f) ist f invertierbar. Also muss x0 \not\in D(f) sein. Also ist
  f in O_{X,x0} nicht invertierbar, liegt somit im maximalen Ideal und ist im
  Körper k(x0) Null.

  Das ist auch völlig klar:

       f = 0 \in k(x0)

  <==> f ist in O_{X,x0} nicht invertierbar

  <==> X |== (f ist nicht invertierbar)^Box

  <==> X |== (exists g. fg = 1)^Box ==> Box(bot)

  <==> X |== Box(exists g. fg = 1) ==> Box(bot)

  <==> X |== (exists g. fg = 1) ==> Box(bot)

* Daraus folgere ich: Das Ideal vorne in der kurzen exakten Sequenz zum
  Unterschema Spec k(x0) (falls x0 abgeschlossen),

      0 --> I --> O_X --> i_* O_k(x0) --> 0,

  kann in der internen Sprache durch

      { f : O_X | f invertierbar ==> !x0 }

  gegeben werden. Man kann intern nachweisen, dass I ein Radikalideal ist und
  quasikohärent ist.

  Wenn x0 nicht abgeschlossen ist, kann man immer noch die exakte Sequenz

      0 --> I --> O_X --> O_X/I --> 0

  hinschreiben; das ist dann die exakte Sequenz zum reduzierten abgeschlossenen
  Unterschema V(I) = clos {x0}.

* Kann also intern auch die Abbildung ev_x : O_X --> i_* k(x)
  verstehen: Das ist einfach die Projektionsabbildung O_X/{...}.

  i_* k(x) ist aus interner Sicht ein Ring, schwacher Integritätsbereich,
  Körper im Sinn von "jedes Element ist Null oder invertierbar"; aber "1 neq 0"
  gilt nicht. (1 neq 0 ist gleichwertig zu neg(Bot false).)

* Kann man modale Operatoren der Form ((__ -> !x) -> !x) intern
  charakterisieren?

* Was passiert bei anderen Aussagen phi statt "!x0"? Ideale erhält man in jedem
  Fall.

* Kann man dadurch auch größere Unterschemata charakterisieren?

* Kann man die Ideale der obigen Form irgendwie charakterisieren?

* J ist eine Art maximales Ideal -- aber nicht ganz:

  * X |== 1 \in J ist gleichbedeutend mit X |== !x0.
    Das ist genau dann richtig, wenn X = {x0}.
    Aber obacht: X |== nicht (1 \in J) gilt leider nicht.
    Das würde bedeuten, dass für alle offenen Teilmengen U gilt:
    Sollte x0 nicht in U liegen, dann ist U leer.

  * X |== forall f,g : O. fg \in J ==> f \in J oder g \in J
    gilt, denn für f, g : O(U) mit fg = 0 in k(x0) folgt
    f = 0 oder g = 0 in k(x0). (Falls x0 \not\in U, ist "= 0" in k(x0) eine
    triviale wahre Aussage.)

  * U |== nicht (f \in J) bedeutet für f \in O(U),
    dass f auf einer dichten offenen Teilmenge von U invertierbar ist und
    dass alle nichtleeren offenen Teilmengen von U x0 enthalten.

  * Daher gilt X |== forall f : O. f \not\in J ==> J + (f) = (1).
    Denn sei f \in O(U) beliebig mit U |== nicht (f in J).
    Ohne Einschränkung sei U nicht leer.
    Dann ist f auf einer offenen dichten Teilmenge V von U invertierbar. Diese
    muss x0 enthalten. Überdecke U durch V und (U \ {x0}); hierbei geht die
    Abgeschlossenheit von x0 ein. Auf V gilt intern, dass (f) das Einsideal
    ist. Auf (U \ {x0}) gilt intern, dass J das Einsideal ist (da dort !x0
    gilt).

* Sei J ein Ideal von O_X. Sei j(phi) := phi v (1 \in J).
  Dann ist O_X/J eine j-Garbe und aus Sh_j-Sicht auch ein lokaler Ring:

  Dazu ist zu zeigen, dass für alle s,t : O_X/J mit s + t = 1 in O_X/J
  folgt, dass j(s inv. oder t inv.).

  Das ist klar.

* Sei Z = V(I) <= X ein abgeschlossenes Unterschema. Sei E quasikohärent.
  Dann supp(E) <= Z genau dann, wenn (1 in I ==> E = 0); genau dann, wenn

      forall f in I: forall s in E: exists n >= 0: f^n s = 0.

  Ist E endlich erzeugt, ist das genau dann der Fall, wenn

      I <= sqrt(Ann E).

* Sei I ein Ideal von O_X. Dann ist I genau dann nilpotent (das soll heißen:
  jedes Element aus I ist nilpotent), wenn Sh(X) |== (1 in I ==> bot).

* Sei E ein O_X-Modul. Sei Z = V(I) <= X ein abgeschlossenes Unterschema.
  Dann liegt E genau dann im wesentlichen Bild von i_*, wenn
  supp(E) <= Z (d.h. Sh(X) |= (1 in I ==> E = 0)) und I E = 0.

  "==>": E trägt also sogar eine O/I-Modulstruktur und wird zum O-Modul durch
  Skalareinschränkung. Dann ist I E = 0 klar.

  "<==": Kann auf E eine O/I-Modulstruktur definieren.

* Sei I ein Ideal mit I^n = (0). Dann ist topologisch V(I) = X, denn jedes
  Element aus I ist nilpotent. Damit besitzt jeder O_X-Modul E die Filtrierung

      0 = I^n E <= I^{n-1} E <= ... <= I E <= E,

  wobei für die Quotienten Q jeweils I Q = 0 gilt, d.h. von Moduln auf V(I)
  herkommen.


=== Internes Spektrum

* O_X in Sh(X), also dem kleinen Zariski-Topos, hat im Allgemeinen noch viele
  maximale Ideale: die Idealgarben zu abgeschlossenen Punkten. Jein, so
  wirklich maximal sind die nicht.

* Etwa im Fall X = Spec Z besitzt O_X aber keine interessanten Primelemente:
  Die Bedingung "p|xy ==> p|x oder p|y" ist eine geometrische Sequenz und gilt
  daher genau dann, wenn sie halmweise gilt. Am generischen Halm ist sie aber
  nur für p = 0 \in Q erfüllt. Also gilt auch p = 0 \in Z (bzw. Z[(...)^{-1}],
  wenn nicht mit einem globalen Element gestartet).

* D(f) \subseteq Omega ist vermutlich lokal kompakt. Hilft das was?

* Bezug von meinem zu Hakims Spektrum: Vielleicht ist
  http://mathoverflow.net/a/26471 interessant.

* Ein Mittelding zwischen der richtigen Definition fürs interne Spektrum
  und der völlig falschen ist:

      R(A) = { I <= A | I Radikalideal, forall s:A. (s inv => s in I) => s in I }.

  Aber das ist Quatsch: R(A) = Ouv(pt) für beliebiges A (sofern 0 != 1 in A).

  Explizit auch für X = Spec k, A = k[x]_(x)^~... Verstehe das Gegenbeispiel
  nicht mehr.


=== Endlichkeit

* Sei X = A^n über einem Ring R. Dann ist O_X als "Algebra, wo man auch
  Quotienten bilden darf" über R[X_1,...,X_n] (konstante Garbe) endlich
  erzeugt, d.h. es gilt

      Sh(X) |==
          forall f : O_X. exists g, h : R[X_1,...,X_n].
          h(x_1,...,x_n) invertierbar in O_X und
          f = g(x_1,...,x_n) / h(x_1,...,x_n).

  Somit gilt auch O_X = Quot R[X_1,...,X_n], wobei nach den Elementen
  lokalisiert wird, die in O_X invertierbar sind.

* Tieferer Hintergrund ist natürlich die Konstruktion von O_X als Lokalisierung
  nach dem universellen Filter.

* Sollte genauso für jede endlich erzeugte R-Algebra statt speziell R[X_1,...,X_n]
  funktionieren. Die x_i beziehen sich dann auf die gegebenen Erzeuger.
  (Nutze: f^(-1) A ist e.e. f^(-1)k-Algebra, falls A e.e. k-Algebra.)

* Vielleicht gilt für ein S-Schema X folgendes:

  X --> S ist genau dann lokal von endlichem Typ, wenn:

      Sh(S) |== exists w_1,...,w_n : Ouv(IX).
          T = w_1 v ... v w_n,
          alle w_i quasikompakt,
          O_S --> Gamma(w_i, O_X) von endlichem Typ.

  Die Interpretation der internen Aussage ist aber etwas mühevoll.


=== Aussagen an Halmen

Sei box die Modalität ((__ --> !x) --> !x). Es gilt

    U |== box phi

genau dann, wenn x \not\in U oder wenn eine offene Teilmenge V von U mit x \in
V und V |== phi existiert.

* "Sei F v.e.T. um x und F_x = 0 (Halm). Dann F = 0 um x."

  Das folgt sofort aus:
  "box(F endl.erz.), forall s:F. box(s=0).  ==>  box(forall s:F. s=0)."

  Denn: "F_x = 0" ist äquivalent zu "(F = 0)^box" (wie negneg-Übersetzung). Das
  ist nach dem bekannten Vereinfachungslemma äquivalent zu "forall s:F.
  box(s=0)".

* "Sei F v.e.P. um x und F_x ~~ O_x^n. Dann F frei v.R. n um x."

  Das folgt sofort aus:

      box(F endlich präsentiert), (F frei v. R. n)^box
        ==> box(F frei v. R. n).

  Unter der Präsentationsvoraussetzung ist die Eigenschaft, frei vom Rang n zu
  sein, eine geometrische: Es soll Elemente aus HOM(O^n,F) und HOM(F,O^n)
  geben, die miteinander verknüpft beide Male die Identität geben. Daher
  ist (F frei v. R. n)^box äquivalent zu box(F frei v. R. n). Damit ist schon
  alles klar.


=== Aussagen an offenen Unterräumen

Sei U eine offene Teilmenge von X. Dann ist

    U ==> ___

eine Lawvere-Tierney-Topologie. Der Topos der Garben bezüglich dieser Topologie
ist gerade Sh(U).

* Definiere eine Formelübersetzung analog zur Doppelnegationsübersetzung,
  bei der vor jeden Junktor ein "U ==>" vorangestellt wird.

  Dann kann man aber zeigen, dass für alle Formeln phi
  gilt: phi^circ <==> (U ==> phi).

  Daher ist Zurückziehen auf U ein logischer Funktor.

* Folgende Aussagen sind äquivalent:

  * Sh(X) |== phi^circ
  * Sh_j(X) |== phi
  * Sh(U) |== phi
  * Sh(X) |== U ==> phi
  * U |== phi


=== Aussagen an abgeschlossenen Unterräumen

Sei A eine abgeschlossene Teilmenge von X. Dann ist

    j(___) = ___ vee A^c

eine Lawvere-Tierney-Topologie. Der Topos der Garben bezüglich dieser Topologie
ist gerade Sh(A). (Zurückziehen auf Sh(A) entspricht Garbifizieren,
Vorwärtsdrücken entspricht Vergessen.)

* X |== f = g vee A^c
  ist äquivalent zu: f = g in allen F_x, x \in A.

* Spec A |== b \in iota_*(Z)
  ist äquivalent zu: forall p: a_1,...,a_n \in p ==> b \in p.

  Dabei ist iota die Inklusion Spec A/(a_i) --> Spec A
  und Z das universelle Primideal auf Spec A/(a_i).

* Omega_j := { j(phi) | phi in Omega } = { phi | j(phi) <=> phi }
  ist kompakt! Sei bigvee U_i = T in Omega_j, d.h.
  bigcup U_i vee A^c = T in Omega. Dann bigcup U_i = T und damit
  U_i = T für ein i, oder A^c. Damit aber Omega_j = { T } und damit ist (das
  mindestens eine existente) U_i auch gleich T.


=== Reduzierte Schemastruktur

* X_red ist wirklich X mit Strukturgarbe O_X/sqrt(0).

* Die U-Schnitte von sqrt(0) sind übrigens die auf ganz U nilpotenten
  Funktionen, falls U quasikompakt ist.

* Es ist auch recht leicht zu zeigen, dass X_red --> X
  das universelle reduzierte abgeschlossene Unterschema mit X als
  zugrundeliegenden topologischen Raum ist.

  Dass es selbst ein solches ist, ist klar. (Benutze, dass sqrt(0) qcoh ist.)

  Sei Z --> X ein weiteres solches. Dazu gehört ein surjektiver lokaler
  Ringhomo O_X --> O_Z. Da O_Z reduziert ist, induziert dieser einen Morphismus
  O_X/sqrt(0) --> O_Z. Damit faktorisiert Z --> X über X_red --> X.


=== Garbifizierung

Sei j eine Lawvere-Tierney-Topologie.

* Ein Unterobjekt U --> X ist genau dann j-dicht, wenn

      forall x:X. j(x \in U).

* Ein Unterobjekt U --> X ist genau dann j-abgeschlossen, wenn

      forall x:X. j(x \in U) ==> x \in U.

* Ein Objekt X ist genau dann j-separiert, wenn

      forall x,y:X. j(x = y) ==> x = y.

* Ein Objekt X ist genau dann eine j-Garbe, wenn

      forall S \subseteq X:
          j(S Singleton) ==> exists! x:X. j(x \in S).

  Bemerkung: Falls X j-separiert ist, sind äquivalent:
  * j(S Singleton).
  * S Subsingleton und j(S bewohnt).

  In diesem Fall sind ferner äquivalent:
  * j(x \in S).
  * j(S = {x}).

* Freyd definiert den Reflektor in die separierten Prägarben wie folgt:

      X^sep := { K : P(X) | exists x : X. K = { y : X | j(x = y) } }
      (https://ncatlab.org/spahn/files/aspects_of_topoi.pdf, Lemma 2.615)

  Und den Reflektor in die Garben so:

      X^sh := j-Abschluss der Teilmenge { { y : X | j(x = y) } | x : X }
      in der j-Garbe Omega_j^X, also der Menge derjenigen Teilmengen von X,
      für die Zugehörigkeit j-stabil ist.

* Die Plus-Konstruktion kann man so definieren:

      X^+ := { S \subseteq X | j(S Singleton) }/~,

  wobei S ~ T :<==> j(S = T).

  Man kann auch gleich nur j-stabile Repräsentanten nehmen.
  Wenn das hier alles in einem Garbentopos mit j = negneg passiert, kann man
  damit X^+ super extern deuten: Deren U-Schnitte sind Paare <V,f>, wobei V
  eine dichte offene Teilmenge von U, f ein Schnitt von X auf V und dieser
  *maximal definiert* ist (d.h. jede Fortsetzung ist schon gleich <V,f>).

  Mit der ursprünglichen Definition ist die Interpretation folgende:
  U-Schnitte sind Äquivalenzklassen von Paaren <V,f>, wobei zwei Paare als
  gleich gelten, wenn auf einer dichten offenen Teilmenge des gemeinsamen
  Definitionsbereichs die gegebenen Schnitte übereinstimmen.

* Dann gelten die üblichen Resultate zur Plus-Konstruktion.

* Insbesondere gilt, wenn X schon j-separiert war, dass

      X^+ = { S \subseteq X | S Subsingleton, j(S bewohnt) }/~

  die j-Garbifizierung von X ist.

* J = { phi | j(phi) } klassifiziert j-dichte Unterobjekte,
  Omega_j = { phi | j(phi) <==> phi } klassifiziert j-abgeschlossene
  Unterobjekte.

  Omega_j ist eine j-Garbe und der Unterobjektklassifizierer in Sh_j.
  Aber Omega_j ist nicht die Vergarbung von Omega.
  (Denke an Halme von Omega eines Garbentopos!)
  [ Es stimmt doch, wenn j folgende spezielle Eigenschaft hat:
  j(phi ==> psi) <==> (phi ==> j(psi)). Das ist etwa für negneg der Fall. Siehe
  Borceaux, Seite 512, Exercise 9.5.7. ]

  Potenzobjekte berechnet man in Sh_j wie in Sh.

  Sh_j(E) ist äquivalent zu Sh_E(Omega_j) durch
  X j-Garbe |--> (U |-> Hom(U,X)) und
  F Garbe auf Omega_j |-> F(T).

* { x : F | phi^Box(x) }^+ ~~ { xquer : F^+ | phi^Boxplus(xquer) },
  als Teilmengen von F^+.

* { x : F | phi(x) }^+ ~~ { x : F | Box(phi(x)) }^+.

* Daraus wird ersichtlich: Wenn Box(phi(x)) <==> phi^Box(x),
  dann { x : F | phi(x) }^+ ~~ { xquer : F^+ | phi^Boxplus(xquer) }.

  Das drückt aus: {x:F|phi(x)}_a ~~ {[x]:F_a|phi(x)} für Punkte a.

* In einem Garbentopos Sh(X) gilt:

  * Ein Unterobjekt A --> B ist genau dann negneg-dicht,
    wenn jeder Schnitt von B zumindest auf einer offenen dichten Teilmenge ein
    Urbild unter der Inklusion besitzt.

  * Eine Garbe ist genau dann negneg-separiert, wenn
    Schnitte, die auf einer offenen dichten Teilmenge übereinstimmen,
    sondern ganz übereinstimmen.

  * Eine Garbe ist genau dann eine negneg-Garbe, wenn
    jeder Schnitt, der auf einer offenen dichten Teilmenge definiert ist,
    genau eine Fortsetzung besitzt.

* Sei f : F --> E ein geometrischer Morphismus. Sei j ein lokaler Operator in E.
  Dann faktorisiert f genau dann über E_j --> E, wenn für alle X aus F das
  Objekt f_*(X) eine j-Garbe ist.

* Literatur:

  Vladimir Lifschitz.
  An intuitionistic definition of classical natural numbers.
  Er arbeitet mit der negneg-Garbifizierung der natürlichen Zahlen.

  Fer-Jan de Vries.
  Applications of constructive logic to sheaf constructions in toposes.
  Vorsicht: Dort wurde "j-dicht" mit "j-abgeschlossen" verwechselt!

  Peter Johnstone.
  The associated sheaf functor in an elementary topos.

  M.F. Farina & G.C. Meloni, The associated sheaf functor, Istit. Lombardo
  Accad. Sci. Lett. Rend. A 114 (1982), 50--55.
  unzugänglich!

* Vergleiche auch: Repleteness and the associated sheaf.
  Die haben einen anderen Ansatz.

  Ebenso: Borceux, Volume 3, Thm. 9.2.10.
  Ich denke, dass er die Garbifizierung so definiert:

      aA := { K <= A | forall x:A. Box(x in K) ==> x in K
                wedge Box(exists x:A. K = { y:A | Box(y = x) }) }

* Garbifizierung ist logisch genau dann, wenn bezüglich der Topologie
  zu einer offenen Unterörtlichkeit (Borceux, Seite 512).

* Die Menge { x:1 | phi } ist für eine Aussage phi genau dann eine Box-Garbe,
  wenn phi Box-stabil ist.

  Allgemeiner ist { x : X | phi(x) } für eine Aussage phi(x) und eine Box-Garbe X
  genau dann wieder eine Box-Garbe, wenn phi Box-stabil ist.

* Sei E auf X eine j-Garbe. Sei i : X_j --> X die Inklusion.
  Dann gilt: (i^(-1) E)(U) = E(U) für alle U in Ouv(X_j), d.h. für alle U aus
  Ouv(X) mit j(U) = U.

  Denn: (i^{-1,pre} E)(U) = colim_{U <= jV} E(V) = colim_{U <= jV} E(jV) = E(jU) = E(U).
  Das erste Gleichheitszeichen ist nach Definition.
  Das zweite, da E eine j-Garbe ist. (Stimmt doch, oder? XXX)
  Das dritte, da die Indexmenge ein kleinstes V enthält, nämlich jU.
  Das vierte wieder, da E eine j-Garbe ist.

  Also: Schreiben wir E = i_*(F), so ist i^{-1,pre}(E) = F.
  Also ist i^{-1,pre} schon eine Garbe auf X_j. Garbifizierung ändert sie also
  nicht mehr.

* Mike Shulman auf Seite 29 von https://arxiv.org/pdf/1703.03007.pdf:
  Eine Menge A ist genau dann eine negneg-Garbe, falls die kanonische Abbildung

      A ---> ([|phi|] --> A)

  für alle Aussagen phi mit negneg(phi) bijektiv ist.

  Das gilt auch für alle anderen modalen Operatoren.


=== Modale Operatoren

* Benno veröffentlichte im August 2017 ein paar Dinge zur Box-Übersetzung:
  https://arxiv.org/abs/1708.08791 (Das sehe ich erst jetzt, Dezember 2018.)

* Sei P(psi) irgendeine Aussageform. Dann definiert Box mit

      Box(phi) := forall psi. P(psi) wedge (phi ==> psi) ==> psi

  einen modalen Operator. So zeigt man
  
      Box(phi) wedge Box(phi') ==> Box(phi wedge phi'):

  Sei psi mit P(psi) und (phi wedge phi' ==> psi) gegeben. Zeige psi.
  Hypothetisch gelte phi. Dann phi' ==> psi. Also (da Box(phi')): psi.
  Somit: phi ==> psi.
  Da Box(phi): psi.

  Der so definierter Operator Box ist der größte Operator ("wenn BOX(phi), so
  Box(phi)") mit der Eigenschaft, dass P(phi) ==> (Box(phi) ==> phi), dass also
  Aussagen phi mit P(phi) Box-stabil sind.

  Denn sei BOX ein Operator mit dieser Eigenschaft. Gelte BOX(phi). Wir zeigen
  Box(phi). Sei dazu psi mit P(psi) und phi ==> psi gegeben. Wir zeigen psi.
  Da P(psi) gilt nach Voraussetzung BOX(psi) ==> psi. Außerdem glt natürlich
  BX(phi) ==> BOX(psi). Das genügt schon.

* Speziell könnte P(psi) folgende Aussage sein: "Das Ideal { f | f nilpotent
  oder psi } ist pseudokohärent." Dann kann man sich zum Beispiel fragen, ob
  ein Radikalideal einer Algebra A genau dann pseudokohärent ist, wenn es eine
  Box-Garbe ist, wobei Box wie oben definiert. Klar ist mir die Antwort nicht.

* Folgende Setzungen definieren *keine* modalen Operatoren:

  1. Box(phi) := ({ f | f nilpotent oder phi } ist pseudokohärent).

  2. Box(phi) := ({ f | f invertierbar ==> phi } ist pseudokohärent).

  Sind jeweils nicht monoton.

* Sei (a -| i) : Sh_j(E) --> E ein Untertopos. Wie kann man daraus j
  rekonstruieren? So:

  1. j(phi) <==> forall psi:Omega. ((j(psi) ==> psi) wedge (phi ==> psi)) ==> psi.
  2. (j(psi) ==> psi) <==> { x : 1 | psi } ist eine j-Garbe, d.h. liegt im
  wesentlichen Bild von i.


=== Gillams Lokalisierung

* Ausgangspunkt bei Gillam ist ein Primsystem, d.h. die Angabe einer
  Teilmenge M_x von Spec O_{X,x} für jedes x in X. Wichtige Beispiele sind das
  lokale Primsystem (x |-> { m_x }) und das terminale (x |-> Spec O_{X,x}).
  Außerdem Pullbacks von Primsystemen.

* Mögliche Globalisierung wäre also die Angabe einer internen Menge
  von Filtern von O_X. Im Fall vom lokalen Primsystem etwa { O_X^\times }.

  Ist phi : O_X --> A ein Ringhomo und ist M eine Menge von Filtern von O_X, so
  ist phi_*(M) := { Filter F in A | phi^(-1)[F] in M } eine Filtermenge von A.


=== Subtilitäten bei der Definition der Kripke--Joyal-Semantik

* Bei vee/bigvee/exists kann man entweder definieren: Auf einer Überdeckung
  stimmt's. Oder: Die Menge derjenigen Stages, wo es stimmt, ist eine
  Überdeckung.

  Wenn der Situs hinreichend gesättigt ist, sind die Definitionen äquivalent.


=== Lokale Kripke--Joyal-Semantik

* Kann definieren: U |==_negneg phi genau dann,
  wenn auf einer offenen dichten Teilmenge V von U gilt: V |== phi.
  (Das ist zu j = negneg.)

  Analog: U |==_x phi genau dann,
  wenn x kein Element von U ist oder eine Teilmenge V von U
  mit x in V und V |== phi existiert.
  (Das ist zu j = ((__ --> !x) --> !x).)

* Somit U |==_j phi genau dann, wenn U |== phi^j (Übersetzung, bei der
  eigentlich vor alles, eigentlich aber nur vor atomare Aussagen, vee
  und exists ein j kommt).

* Die so definierte interne Sprache ist klassisch (erfüllt LEM).


=== Rationale Funktionen I

* Intern kann man die Teilmenge

      S := { f : O_X | f regulär }

  definieren. Diese ist multiplikativ abgeschlossen. Da "f regulär" für festes
  f \in O_X(U) eine geometrische Implikation ist, gilt:

      S(U) = { f \in O_X(U) | f regulär in allen O_{X,x}, x \in U }.

  Dabei verwendet: [[ { x : F | phi(x) } ]](U) = { x \in F(U) | U |== phi(x) },
  siehe kategorielle-logik.txt.

  Obacht: Da die Konstruktion von S nicht an sich geometrisch ist, stimmt der
  Halm S_x NICHT mit der Menge der regulären Elemente in O_{X,x} überein.

* Daher kann man intern S^(-1) O_X bilden.

* Die extern definierte Ringgarbe K rationaler Funktionen erfüllt dieselbe
  universelle Eigenschaft:

      Sei U \subseteq X. Sei F Ringgarbe auf U. Sei phi : O_X --> F
      Ringhomo, der aus interner Sicht reguläre Elemente auf invertierbare
      schickt; das ist extern äquivalent dazu, dass er auf allen offenen Teilmengen V
      die Elemente aus S(V) auf invertierbare Elemente schickt.

      Dann gibt es genau einen Morphismus K^pre|_U --> F, der das Dreieck
      O_U --> K^pre --> F zum Kommutieren bringt. Wegen der Lokalität der
      Vergarbung gibt es daher genau einen Morphismus K|_U = a(K^pre|_U), der
      das Dreieck K^pre|_U --> K|_U --> F zum Kommutieren bringt.
 
  Dabei verwendet: Stack-Semantik, um die universelle Eigenschaft richtig zu
  interpretieren; Lokalität der Vergarbung; Beschreibung von K aus
  http://therisingsea.org/notes/Section2.6-Divisors.pdf.
  Siehe auch http://therisingsea.org/notes/Section2.8-Differentials.pdf.

* Also kann ich K intern verstehen als S^(-1) O_X! :-)

* Da Lokalisierung eine geometrische Konstruktion ist, gilt
  (S^(-1) O_X)_x = S_x^(-1) O_{X,x}. Der Halm S_x bettet zwar immer
  injektiv ein, kann aber echt kleiner sein als die Menge der regulären
  Elemente in O_{X,x}. Daher ist der Halm im Allgemeinen NICHT gleich dem
  totalten Quotientenring von O_{X,x}.

  Kleiman schreibt, dass wenn X lokal noethersch oder wenn X reduziert ist und
  die Menge der irreduziblen Komponenten lokal endlich ist, es doch stimmt.

* Wenn O_X reduziert ist, ist S^(-1) O_X ein Körper von Brüchen, d.h. erfüllt
  "ungleich Null ==> invertierbar": Sei f/s nicht Null. Dann ist auch f nicht
  Null. Dann ist f auch in O_X nicht Null. Also ist f in O_X regulär. Also ist f
  und somit f/s in S^(-1) O_X invertierbar.

  Ferner ist er (wie O_X) ein Körper in dem Sinn, dass er "nicht invertierbar
  ==> gleich Null" erfüllt.

  Ein lokaler Ring ist S^(-1) O_X im Allgemeinen aber nicht. Dazu müsste S
  einen Filter bilden, d.h. es müsste gelten:

      x + y regulär  ==>  x regulär  oder  y regulär.


=== Rationale Funktionen II

* Sei zu einer Menge F folgende Menge P, ausgeschrieben
  P_{<= 1}^{\neg\neg bewohnt}(F), definiert:

      P = { W \subseteq F | W Subsingleton und nicht nicht bewohnt }.

  * Falls F etwa ein Ring ist, erbt P auch die Ring-Operationen:

      W + W' := { w + w' | w \in W, w' \in W' }
          -W := { -w | w \in W }
           0 := { 0 }

    Allerdings gelten nicht alle Axiome. Etwa ist W + (-W) nicht unbedingt
    gleich { 0 }, sondern nur nicht nicht gleich { 0 }.

  * Falls x in W, so W = { x }.

  * Man kann auch P/negneg betrachten. Das ist dann wirklich ein Ring.

* Falls Gleichheit in F nichtnicht-stabil ist, lässt sich die Bedingung an W
  äquivalent wie folgt schreiben:

      Nicht nicht ist W ein Singleton.

  Extern bedeutet die Nichtnichtstabilität, dass für jede offene Menge U
  und für je zwei Schnitte s, s' von F auf U gilt: Sollten s und s' auf einer
  dichten offenen Teilmenge von U übereinstimmen, so stimmen sie schon auf ganz U
  überein.

* Falls R ein Ring mit s regulär <==> --(s invertierbar) ist
  (das gilt zum Beispiel für O_X, falls X reduziert ist), so
  gibt es einen injektiven Ringhomo Reg^(-1) R --> P(R)/negneg.

  Schicke einen Bruch f/s auf die Klasse von W := { uf | u : R, us = 1 }.
  W ist sicherlich ein Subsingleton und nach Voraussetzung an R auch
  nicht nicht bewohnt.

  Surjektiv ist dieser Homo aber nicht immer -- wohl aber im Anwendungsfall in
  der algebraischen Geometrie, siehe unten.

* Für die volle Potenzmengengarbe PP von F gilt:

      Gamma(U, PP) = Hom(U_, [F, Omega]) = Hom(U_ x F, Omega)
          = Sub(U_ x F) = Sub(F|_U), denn:

  * Gamma(V, U_ x F) = { s \in F(V) | V \subseteq U }.
    Insbesondere also (U_ x F)|_U = F.
    (Es gilt NICHT: U_ x F = i_* i^(-1) F = i_* F|_U. Das kann nämlich noch
    viele globale Schnitte haben.)

  * Ist G ^--> U_ x F ein Unterobjekt, so ist
    G|_U --> F|_U das zugehörige Unterobjekt von F|_U.

  * Ist H ^--> F|_U ein Unterobjekt, so ist
    (V |-> { s \in H(U \cap V) | V \subseteq U }) das zugehörige Unterobjekt
    von U_ x F.

* Für die Garbe PPP der Subsingletons gilt:

      Gamma(U, PPP)
          = { S \in Gamma(U, PP) | U |== forall x,y \in S. x = y }
          = { [S ^--> F|_U]      | U |== forall x,y : S.   x = y }
          = { [S ^--> F|_U]      | alle Halme S_x sind Subsingletons }
  
  Beim zweiten Schritt muss man kurz nachdenken, da die Beschreibung der vollen
  Potenzmengengarbe ausgenutzt wird.

* Für die Garbe P gilt:

      Gamma(U, P)
          = { [S ^--> F|_U] | U |== S Subsingleton und nicht nicht bewohnt }
          = { [S ^--> F|_U] | alle Halme S_x Subsingletons und
                                  es existiert eine offene dichte Teilmenge V in U
                                  sodass alle Halme auf V Singletons sind }.
  
  Das kann man weiter vereinfachen zu

          = { <V in U offen dicht, s \in F(V)> }.

  Die Zuordnung geht so: Zu einem Unterobjekt S kann man die Menge
  V := { x \in U | S_x bewohnt } = Vereinigung über all die offenen Mengen W,
  für die S(W) bewohnt ist, bilden. Auf dieser gibt es einen Schnitt s als
  Verklebung der gegebenen Keime.

  Umgekehrt kann man zu <V,s> ein Unterobjekt S durch

        S(W) = { s|_{W cap Z} \in F(W cap Z) | Z \subseteq W }

  definieren.

* Als nächstes kann man P(F)/negneg betrachten. 

* Beispiel: F = C, F = C^\infty und F = O_X auf reduzierten Schemata X
  sind negneg-separiert. Daher sind Schnitte von P(F)/negneg durch das gegeben, was
  man gemeinhin rationale Funktionen nennt.


=== Rationale Funktionen III

Sei X mit forall s:O_X. nicht (s invertierbar) ==> s = 0.
Dann ist Gleichheit auf O_X negneg-stabil.

* Dann ist S^(-1) O_X negneg-separiert.

* Ist (intern) B eine Teilmenge von S^(-1) O_X, die ein Subsingleton
  und nicht nicht bewohnt ist, so kann man sich fragen, ob ein
  f aus S^(-1) O_X existiert, sodass f nicht nicht in B enthalten ist.
  (Eindeutig ist ein solches f auf jeden Fall.)

  Im Folgenden sei das "Bedingung #".

* Unabhängig von # gibt es O_X --> S^(-1) O_X.

* Ferner gibt es für jede negneg-Garbe G und jeden Morphismus
  O_X --> G eine eindeutige Fortsetzung S^(-1) O_X --> G.
  (Hierbei nutzt man aus, dass jedes Element von S^(-1) O_X
  nicht nicht von der Form u/1 für ein u aus O_X ist.)

* Bedingung # sagt extern: Jeder Schnitt von S^(-1) O_X,
  der auf einer offenen dichten Teilmenge definiert ist, lässt sich fortsetzen.

Die kritische Frage ist nun, wann Bedingung # erfüllt ist. Ist sie es nämlich,
so ist S^(-1) O_X einfach die negneg-Garbifizierung von O_X. Das zeigt (?),
dass Schnitte von S^(-1) O_X einfach durch Äquivalenzklassen von Schnitten von
O_X gegeben sind, die auf offenen dichten Teilmengen definiert sind.

* Beispiel: Sei X = Spec A, A ein Integritätsbereich. Dann stimmt es:
  Denn ein Schnitt auf D(h) hat die Form a/s, wobei a = b/h^n,
  s = c/h^m. Also ist a/s = bh^m / (ch^n) eine globale Fortsetzung.

* Beispiel: Sei X ein integres Schema. Dann stimmt es auch.
  Denn lokal sieht das aus wie Spec A, A Integritätsbereich.

* Beispiel: Sei X nur ein reduziertes Schema. Dann stimmt es auch!
  Es genügt, die Behauptung für X = Spec A, A reduziert aber vielleicht kein
  Integritätsbereich, nachzuweisen. Sei dazu U eine beliebige offene dichte
  Teilmenge. Sei ein Schnitt von S^(-1) O_X gegeben. Dieser ist von der Form
  a/s, wobei a = g^(-1) b, s = h^(-1) c, g in JU, h in JU, s auf U regulär.
  [ Stimmt das? Verwechsele ich hier nicht die Prägarbe mit der Garbe S^(-1) O_X? ]
  Wenn man U = bigcup_i D(f_i) schreibt, so bedeutet g in JU, dass
  sqrt((f_i)_i) subseteq sqrt(g); und analog für h.

  Der gegebene Schnitt ist dann gleich (bh) / (cg). Zu zeigen ist, dass cg
  regulär auf ganz Spec A ist. Dann haben wir den Schnitt nämlich fortgesetzt.

  Sei dazu cg x = 0 in A[z^(-1)]. Dann also cg z^a x = 0 in A, insbesondere
  in A[(JU)^(-1)]. Da c auf U regulär ist, folgt g z^a x = 0 dort, also
  p g z^a x = 0 für ein p aus JU. Für jedes i gibt es ein n_i mit
  f_i^(n_i) = u_i p. Daher ist für jedes i f_i g z^a x nilpotent.
  Und somit (Dichtheit!) ist g z^a x nilpotent, also Null.

  Nun nochmal: Für jedes i gibt es ein m_i mit f_i^(m_i) = v_i g.
  Daher ist für jedes i f_i z^a x nilpotent. Und somit (Dichtheit) ist
  z^a x nilpotent, also Null. Somit ist x Null in A[z^(-1)]. Das war zu zeigen.

* Nichtbeispiel: X Schema, das nicht reduziert ist.
  Dann ist O_X im Allgemeinen nicht negneg-separiert und S^(-1) O_X daher auch
  nicht. Also kann S^(-1) O_X (im Allgemeinen) keine negneg-Garbe sein.

  Aufgabe: Genaue Charakterisierung finden, wann S^(-1) O_X bzw. O_X
  negneg-separiert ist, und wann S^(-1) O_X schon eine negneg-Garbe ist.
  Sollte klassisches Wissen sein.

* Beispiel: Sei X ein topologischer Raum und O_X die Garbe der stetigen
  Funktionen. Dann sehe ich NICHT, wieso # gelten sollte.
  Es wird aber in [Mulvey] behauptet. Ein Gegenbeispiel sollte sin(1/x)
  sein.

* Bemerkung: negneg-Vergarbung ist dasselbe wie Pullback und Pushforward
  auf die kleinste dichte Unterörtlichkeit.


=== Rationale Funktionen IV

* Falls X lokal Noethersch, kann man leicht zeigen,
  dass K_{X,x} = Quot O_{X,x}. Siehe Artikel.

* Ass = { x \in X | m_x ist in O_{X,x} ein assoziiertes Primideal,
  also von der Form Ann(s) für ein s \in O_{X,x} }.

  Ist lokal endlich (d.h. Schnitte mit den Mengen einer geeigneten offenen
  Überdeckung, nämlich einer durch affinoffennoethersche Teilmengen), denn die
  Menge der assoziierten Primideale eines noetherschen Rings ist endlich.

* Es gilt auf lokal noetherschen Schemata: O_X ist genau dann Box-separiert für
  Box = (U ==> __), wenn Ass subseteq U.

* K_X sollte Vergarbung von O_X bezüglich j sein, wobei

      j(phi) = (O_X ist (phi => __)-separiert).

  Kann intern zeigen, dass das wirklich ein Kern ist.
  Die Separiertheitseigenschaft kann man auch intern nachweisen.

* Falls X integer: j(phi) <==> negneg phi.


=== Assoziierte Punkte

* Sei E ein Modul. Dann können wir den modalen Operator Box mit

      Box(phi) = (E ist (phi => __)-separiert)

  definieren. Manchmal schneidet dieser Operator genau die Unterörtlichkeit der
  assoziierten Punkte von E aus. Das stimmt zumindest im Fall E = O_X auf einem
  Schema, welches eine offene Überdeckung durch affine Teilmengen mit
  Eigenschaft (**) (jede offene schematheoretisch dichte Teilmenge umfasst eine
  standardoffene schematheoretisch dichte Teilmenge) zulässt.

* Ich bezeichne mal die von Box ausgeschnittene Unterörtlichkeit trotzdem als
  Ass(E). Dann gilt:

         Ass(E) cap V(J) = emptyset
    <==> Ass(E) <= D(J)
    <==> forall phi. (1 in J ==> phi) ==> Box(phi)
    <==> Box(1 in J)
    <==> forall x:E. (1 in J ==> x = 0) ==> x = 0
    <AA> forall x:E. J <= sqrt(ann(x)) ==> x = 0
    <BB> forall x:E. J <= ann(x) ==> x = 0
    <CC> forall x:E. fx = 0 ==> x = 0

  Zu <CC> ist zu sagen: Gilt, falls J = (f).

  Zu <AA> ist zu sagen: "==>" gilt. "<==" gilt, falls E das interne
  Quasikohärenzkriterium erfüllt.

  Zu <BB> ist zu sagen: "==>" gilt, da ann(x) <= sqrt(ann(x)).
  Für die Umkehrung muss J endlich erzeugt sein. Denn sei J = (f_1,...,f_n).
  Ohne Einschränkung n >= 1. Dann zeigen wir mit Induktion über m:

      forall a_1, ..., a_n mit sum a_i <= m:
          forall x.
              [forall i. f_i^{a_i} x = 0] ==> x = 0.

  Der Induktionsschritt ist trivial. Im Induktionsschritt schreibe f_i^{a_i}
  als f_i^{a_i - 1} f_i um (ohne Einschränkung alle a_i >= 1) und erhalte nach
  Induktionsvoraussetzung, dass alle f_i x Null sind. Mit der Voraussetzung
  folgt, dass x selbst Null ist.


=== Quasikohärenz

* Kann ich Vakil p. 368, 13.3.H hard exercise intern lösen?

* Kann mit dem einfachen Kriterium zeigen, dass Kerne von Abbildungen
  zwischen qcoh Moduln wieder qcoh sind. Kokerne haben nicht auf Anhieb
  funktioniert.

  Bilder funktionieren auch nicht so leicht: Dazu wäre das Lemma, dass das
  Prägarben-Bild schon das Garben-Bild ist, hinreichend. Dieses Lemma ist aber
  falsch.

* Ich bekomme es nicht hin, zu zeigen, dass das endlich erzeugte Ideal
  (h) von O_X wieder qcoh ist. Es ist dann trivial, wenn h regulär ist, denn
  dann ist (h) isomorph zu O_X; aber das ist ja ein langweiliger Fall. (Oder?)

* Kann mit Kompaktheitshilfe (siehe kategorielle-logik.txt) zeigen,
  dass das Ideal sqrt(0) qcoh ist.

* Habe gesehen, dass qcoh Untermoduln eines Moduls v.e.T. wieder v.e.T. ist,
  auf lokal noetherschen Schemata. Vielleicht gibt es aber noch ein anderes
  Theorem. Etwa, dass Untermoduln, die von geometrischen Aussagen
  ausgeschnitten werden, stets qcoh sind (oder aber stets die Konklusion
  erfüllen!). Das wäre sehr schön. Aber vielleicht zu sehr Wunschdenken ...?

* Es gilt für Ringe A, Elemente g, Ideale J:

      Spec A |== g in J~   <==>   g in J.

* M projektiv über A
  ==> M_ projektiv über A_  (Achtung! Nur in der Kategorie der konstanten A_-Moduln! Ist das schlimm?)
  ==> M_[S^(-1)] projektiv über A_[S^(-1)] = O_{Spec A}
  ==> M~ endlich frei (da A[S^(-1)] lokal)

* Sei A eine quasikohärente O_X-Algebra auf einem Schema. Dann:

      forall f : O_X. forall s : A.
          (f inv. in O_X ==> s inv. in A) ==> s inv. in A[f^(-1)].

* Muss noch mal die Details prüfen, aber es scheint folgendes zu gelten:

  Genau dann ist ein O_X-Modul E quasikohärent, wenn E[F^(-1)] in Spec(O_X) eine
  Garbe bezüglich der Topologie ist, die Spec(O_X|O_X) in Spec(O_X) ausschneidet.

  Und eine O_X-Algebra A ist genau dann quasikohärent, wenn A[F^(-1)] in
  Spec(A) eine Garbe bezüglich der Topologie ist, die Spec(A|O_X) in Spec(A)
  ausschneidet.

* Sei O_X --> A eine lokale O_X-Algebra, die lokal über O_X ist.

  Sei a <= A ein Radikalideal. Dann gilt: Wenn 1 in Coh(a), dann 1 in a.
  Dabei ist mit Coh der Reflektor der Radikalideale in die pseudokohärenten
  Radikalideale gemeint.

  Denn mit Knaster--Tarski-Induktion kann man zeigen:

      Coh(a) <= { s : A | s inv. ==> (1 in a) }.


=== Cartier-Divisoren und Geradenbündel

* Ein rationaler Schnitt eines Geradenbündels L ist wohl dasselbe wie
  ein globaler Schnitt von L tensor_O K.

* So einem Schnitt kann man ein eindeutiges Element aus K_X/O_X^* zuordnen
  (f ~ g <==> f = u g für ein u aus O_X^*), und zwar wie folgt:

  Sei q aus L[S^(-1)] vorgegeben.
  Dann gibt es x, s mit q = x/s.
  Ferner gibt es phi : L --> O_X Iso.
  Setze f := phi(x) / s in K_X.
  Dann ist [f] die gesuchte Klasse.

  Man kann nachrechnen, dass diese Klasse nicht von den Wahlen (x, s, phi)
  abhängt. Daher definiert das wirklich ein globales Element von K_X^*/O_X^*.
  Formal zeigt man also:

      exists! a : K_X/O_X^*:
          exists f : K_X. exists x : L. exists s : S. exists phi : L --> O_X.
              a = [f] und q = x/s und f = phi(x)/s.

* Zu einem nichtverschwindenden Element D aus K_X^*/O_X^* kann ich ein
  Geradenbündel O_X(D) zuordnen:

  Schreibe D = [f]. Dann O_X(D) := 1/f * O_X \subseteq K_X.

  Wie oben ist das Unabhängigkeit von der Wahl von f. Mit "nicht verschwindend"
  muss gemeint sein, dass f in K_X invertierbar ist. Das ist genau dann der
  Fall, wenn der Zähler regulär ist.

* Sei dann s ein nichtverschwindender rationaler Schnitt eines Geradenbündels L.
  Dann kann man in der internen Sprache explizit einen Iso

      L --> O(div s)

  hinschreiben: Sei z aus L beliebig. Sei s = x/s. Sei phi : L --> O_X.
  Dann div(s) = [phi(x)/s]. Also O(div(s)) = s/phi(x) * O_X. Ordne daher z auf
  s/phi(x) * phi(z) ab.

* Dann kann man in der internen Sprache beweisen:
  Genau dann hat man einen globalen Iso O(D) --> O(D'),
  wenn man einen globalen Schnitt f von K_X^* mit D - D' = [f] hat.

  Explizit: Sei phi : O(D) --> O(D') ein Iso. Schreibe D = [g], D' = [g'].
  Dann gibt es ein p : O_X mit phi(1/g) = 1/g' * p.
  Setze dann f := phi(1/g) / (1/g) = g/g' * p : K_X.
  Dann kann man nachrechnen, dass f in K_X invertierbar ist (also p regulär in
  O_X ist), dass g/g' = u f für ein invertierbares u : O_X (also p invertierbar
  in O_X) und dass f unabhängig von der Wahl von g ist.

  Umgekehrt: Sei f ein globaler Schnitt von K_X^* mit D - D' = [f].
  Schreibe D = [g] und D' = [g']. Dann g/g' = u f für ein invertierbares u : O_X.
  Dann ist O(D) --> O(D'), h |--> h * f ein Iso. Die Wohldefiniertheit kann man
  natürlich intern zeigen: Ein h = p/g wird auf pf/g = u^(-1) p/g' abgebildet.

* Ebenso einfach: Jeder O_X-Untermodul F von K_X, der lokal vom Rang 1 ist, ist
  von der Form O(D) für einen Cartier-Divisor D.

  Intern habe einen Iso phi : F --> O_X.
  Es ist phi^(-1)(1) \in F \subseteq K_X.
  Kann also D := [ 1 / phi^(-1)(1) ] definieren.

  Dann kann man zeigen: D ist wohldefiniert (d.h. phi^(-1)(1) ist tatsächlich
  in K_X invertierbar) und unabhängig von der Wahl von phi.
  Nutze für letzteres die Identität psi(phi^(-1)(h)) = h * psi(phi^(-1)(1)),
  wobei der zweite Faktor ein invertierbares Element aus O_X ist.


=== Kählerdifferentiale

* Die Konstruktion, Kählerdifferentiale zu bilden, ist geometrisch (siehe
  kategorielle-logik.txt). Daher ist völlig klar: Der Halm von Omega_{B/A}
  ist Omega_{B_x/A_x}.

* Zeige intern: glatt <==> Omega dort frei


=== Antiklassische Prinzipien im kleinen Zariski-Topos

Grothendiecks "generic freeness lemma" sagt (in der schwachen Version):

    Let A be a Noetherian integral domain, M a finitely generated A-module. Then
    there there exists f \in A, f \neq 0, with M[f^(-1)] a free A[f^(-1)]-module.

Daraus folgt folgendes Prinzip für die interne Welt des kleinen Zariski-Topos
von A:

    Ein endlich erzeugter O_X-Modul ist bereits nicht nicht frei.

Das ist leider, anders als der Titel versprechen lässt, KEIN antiklassisches
Prinzip: Denn O_X ist ja aus interner Sicht eine Art Körper. Für Körper ist
diese Aussage aber (klassisch) zu erwarten.


=== Grothendieck's generic freeness lemma auf den Kopf gestellt

* Habe Zorn im kleinen Topos, wenn ich draußen an es glaube! Kann also eine
  maximale linear unabhängige Familie betrachten ...


=== Induktionsbeweise für Vektorbündel

Beweise Lemma 3 von
http://mathriding.wordpress.com/2012/12/06/vector-bundles-locally-free-sheaves-and-divisors-on-a-curve/:

Sei E ein Vektorbündel vom Rang r. Dann gibt es eine kurze exakte Sequenz

    0 --> L --> E --> E' --> 0,

wobei L ein Geradenbündel und E' ein Vektorbündel vom Rang r-1 ist.


=== Untertopoi

Ist U eine offene Teilmenge von X, kann man das Prädikat ?U mit

    V |== ?U  gdw.  V \subseteq U

betrachten. Ist A eine abgeschlossene Teilmenge von X, so gilt

    V |== ?A^c  gdw.  V \subseteq A^c  gdw.  V \cap A = leer.

* V |== (?U ==> phi) gdw. (V cap U) |== phi.

* Was bedeutet V |== (?A^c vee phi)? Etwa (V \cap A) |==_A phi?
  Ist Zurückziehen auf abgeschlossene Teilmengen ein logischer Funktor?

* Es gilt: F_x = {s} genau dann, falls F^++ = {s}, wobei "++" die
  Vergarbung bezüglich ((__ --> !x) --> !x) bezeichnet.


=== Generische Elemente I

Ziel: Verstehen, wie man "Sei N eine unbeschränkte natürliche Zahl." rigoros
machen kann.

Eine Möglichkeit: Arbeite im Topos E := [N, Set], wobei N mit der gewöhnlichen
Ordnung versehen wird.

* Es gilt p |== neg neg phi (wobei n eine Abkürzung für Hom_{N^op}(__, n) ist)
  genau dann, wenn nicht nicht ein q >= p existiert mit q |== phi.

* In E habe ein Objekt natürlicher Zahlen: NN, die konstante Koprägarbe N.

* Führe eine neue Termkonstante # vom Typ NN ein. Deren Interpretation im
  Kontext p soll Hom(__, p) --> NN, gegeben durch das Element p \in NN(p),
  sein. (Unter Rückzügen bleibt # #!)

* Dann gilt:

      p |== forall n : NN. neg neg (# >= n),

  denn das ist gleichbedeutend mit

      fa. q >= p, n in N:
          neg neg exists r >= q:
              r |== # >= n

  und ist also für r := max { q, n } wahr.

* Aber: Diese Formalisierung ist nicht verträglich mit klassischer Logik.
  Wenn man die möchte, sollte man vielleicht nicht auf Teufel komm Raus
  unbedingt die nichtnicht-Modalität verwenden, sondern eine andere (neue)!

  Ein Axiom der Form "top |-_{n:N} box (# >= n)" ist aber schlecht.
  Denn dann wäre auch "box (# >= # + 1)" und somit "box bot" ableitbar.
  Das soll vermutlich nicht sein.

* Wie kann man das umsetzen? Was wären Modelle dafür?

* Wie auf andere Arten von generischen Objekten ausweiten?


=== Generische Elemente II

Betrachte den Topos E = Sh(R). Darin gibt es die universelle reelle Zahl #,
gegeben durch die Identitätsfunktion als globalen Schnitt von C.

* Falsch ist: E |== # != #.

* Es gilt: E |== forall q : Q. # != q.

* Falsch ist: E |== forall r : R. # != r.

* Es gilt: E |== neg \vee_n exists a_0,...,a_(n-1) : Q. #^n + sum_i a_i #^i = 0.

  Denn normierte Polynome vom Grad n können nicht auf nichtleeren offenen
  Teilmengen verschwinden.

* Es gilt: E |== negneg exists q:Q. |#| >= q > 0,
  d.h. E |== negneg (# apart 0).

* In E' := Sh_negneg(R) gilt also: 

      E' |== # apart 0.

  In E' kann man also klassisch arbeiten und hat eine reelle Zahl #
  zur Verfügung, die apart von jeder rationalen Zahl ist.

* Frage: Welche Interpretation haben Ergebnisse, die man in E' erzielt?
  Das betrifft insbesondere solche, in deren Formulierung # nicht vorkommt.


=== Generische Elemente III

* Idee: Arbeite mit kleinster dichten Unterörtlichkeit und verwende geeignete
  Sprache, um sinnvoll vorgeben zu können, dass diese Punkte enthält.

  Damit soll folgendes funktionieren: Wenn man argumentieren kann
  "Sei x in D. Dann x in U_1, U_2, U_3. Wegen U_1 cap U_2 cap U_3 subseteq V
  folgt also x in V.", dann soll folgen, dass V eine dichte Teilmenge ist.

* Vielleicht sollte man in Sh(Loc) arbeiten, um vorgeben zu können,
  dass Örtlichkeiten Punkte haben. Vergleiche Johnstones Artikel über den
  topologischen Topos und Diagrammjagden in allgemeinen abelschen Kategorien.

* Verstehe Zusammenhang zu Terence Taos Mini-NSA: Offensichtlich haben
  "auf offener dichter Teilmenge" und "nach Übergang zu einer Teilfolge"
  ähnlichen Charakter.

  Siehe: http://math.stackexchange.com/questions/454393/does-cheap-nonstandard-analysis-take-place-in-a-topos/


=== Transferprinzipien M vs. M~

* Es gilt: M~ ist in Sh(Spec A) die Lokalisierung MM[F^(-1)], wobei
  MM die konstante Garbe und F den universellen Filter bezeichnet.

* Da first-order Eigenschaften von M dieselben wie die von MM sind,
  gilt: Die Beziehung von M zu M~ ist die einer Lokalisierung.

* Gelte, dass MM[F^(-1)] endlich erzeugt ist. Das impliziert:

      Spec A |== bigvee_n exists x_1, ..., x_n : MM.
          forall x : MM. exists u in F.
              exists a_1, ..., a_n : AA.
                  ux = sum_i a_i x_i.

  Die ersten beiden Quantoren/Junktoren kann man zu

      bigvee_{n; x_1,...,x_n in M}

  zusammenfassen. Also liegt hier eine gerichtete Disjunktion vor. Somit gibt
  es eine natürliche Zahl n und Elemente x_1,...,x_n in M mit

      Spec A |== forall x : MM. exists u in F.
          exists a_1, ..., a_n : AA.
              ux = sum_i a_i x_i.

  Das zeigt, dass M durch die x_i erzeugt wird.

* Spec A |== AA[F^(-1)] reduziert  <==>  Spec A |== AA reduziert  <==>  A reduziert.

* Ebenso: alpha[F^(-1)] injektiv/surjektiv, M[F^(-1)] flach über A[F^(-1)],
  M[F^(-1)] endlich erzeugt/A[F^(-1)].

* Sei Spec A |== dim AA[F^(-1)] <= n. Dann dim A <= n.

  Seien dazu x_0,...,x_n aus A beliebig.
  Dann habe

      Spec A |== bigvee_{y_0,...,y_n aus A} exists s:F.
          s         in sqrt(x_0, y_0),
          s x_0 y_0 in sqrt(x_1, y_1),
          s x_1 y_1 in sqrt(x_2, y_2),
          ...,
          s x_n y_n in sqrt(0).

  Diese Disjunktion ist zwar nicht gerichtet. Trotzdem kann man sich durch
  explizite Rechnung davon überzeugen, dass dadurch die Existenz einer zu
  (x_0,...,x_n) komplementären Sequenz folgt: Multipliziere die lokalen y_i
  auf. XXX: Nein, das funktioniert nicht.

  Die Behauptung sollte trotzdem stimmen, denn zumindest klassisch gilt

      dim A <= n  <==>  dim(Spec A) <= n  <==>  Spec A |== dim O_X <= n.


=== Sonderstellung der Auswertung auf affinoffenen Teilmengen

Oft hat man doch folgende Situation: Man macht irgendwas mit Modulgarben, und
ausgewertet auf affinoffenen Teilmengen gibt das dasselbe, wie wenn man das mit
den entsprechenden Schnitten der Modulgarben gemacht hätte.

Das hat einen tieferen Grund.

Beispiel:

    Sei X ein ganzes Schema. Sei E eine quasikohärente Modulgarbe. Wir
    definieren intern:

        E_tors := { s : E | exists a : O_X. a regulär und as = 0 }.

    Dann gilt für affinoffene Teilmengen U: E_tors(U) = E(U)_tors.

    Denn, da E quasikohärent ist, gilt E|_U = M~ für einen A-Modul M
    (U = Spec A). Somit:

        E_tors = MM[F^(-1)]_tors = MM_tors[F^(-1)] = (konst. Garbe zu M_tors)[F^(-1)]
               1                 2                 3

    Das zeigt, dass E_tors selbst wieder quasikohärent ist, und zwar auf U
    gleich (M_tors)~. Insbesondere ist E_tors(U) = M_tors = E(U)_tors.

    Schritt 1 ist nach Definition.

    Schritt 2 ist, weil Lokalisieren mit Torsionsuntermodul bilden vertauscht.
    Das stimmt aber nur, wenn das multiplikative System, nach dem man
    lokalisiert, eine Teilmenge der regulären Elemente ist. Das ist unter der
    Voraussetzung, dass X ganz ist, der Fall. Denn dann ist A ein
    Integritätsbereich, und das ist dafür hinreichend. Siehe
    kommutative-algebra.txt.

    Schritt 3 ist allgemein, denn die Torsionsbedingung bezieht sich nur auf
    konstante Garben. Denk dran, dass MM_tors so gegeben ist:

        MM_tors = { s : MM | exists a : AA. a regulär und as = 0 }.

* Anderes Beispiel: sqrt(0) <= O_X. Für affinoffene U gilt

      sqrt(0)(U) = { f in O_X(U) | f nilpotent }.

  Denn, wenn wir U = Spec A schreiben, haben wir auf U:

      sqrt(0) = sqrt(0) von AA[F^(-1)] = (sqrt(0) von AA)[F^(-1)] =
          (konstante Garbe zu (sqrt(0) von A))[F^(-1)],

  also sqrt(0)|_U = (sqrt(0) von A)~.

* Noch ein Beispiel. Sei F eine Untermodulgarbe von E. Seien beide
  quasikohärent. Dann gilt für affinoffene U:

      (E/F)(U) = E(U) / F(U).

  Denn auf U gilt, wenn wir E = M~ und F = N~ schreiben:

      E/F = MM[F^(-1)] / NN[F^(-1)] = (MM / NN)[F^(-1)] =
          (konstante Garbe zu M/N)[F^(-1)].

  Beim zweiten Schritt geht ein, dass Lokalisieren exakt ist. Beim dritten
  Schritt geht ein, dass konstante Garben bilden Kolimiten bewahrt.

* Seien E und F quasikohärent. Dann ist auch E tensor F quasikohärent:

      E tensor F = MM[F^(-1)] tensor NN[F^(-1)] =
          (MM tensor NN)[F^(-1)] = (konstante Garbe zu (M tensor N))[F^(-1)].

* So zeigt man, dass (f) <= O_X für f in O_X(X) quasikohärent ist:
  Ohne Einschränkung sei X = Spec(A) und somit f in A. Dann:

      (f) in O_X = ((f) in AA)[F^(-1)] = (konst. Garbe zu (f) in A)[F^(-1)].

  Der erste Schritt ist wegen der allgemeinen Regel "(S^(-1) A) a = S^(-1) a".

* Interessante Aufgabe: Zeige, dass Kerne zwischen quasikohärenten Modulgarben
  wieder quasikohärent sind. Noch interessanter: Zeige, dass die mittlere
  Modulgarbe in einer kurzen exakten Sequenz, in denen die anderen beiden
  Modulgarben quasikohärent sind, quasikohärent ist.

  Ganz einfach für Kerne und Kokerne: Lokalisieren ist exakt.

* Untermodulgarben von quasikohärenten Modulgarben, welche von endlichem Typ
  sind, sind quasikohärent. Denn der zugehörige Quotient ist es (einfach
  weitere Relationen).


=== Nächste Schritte

* "Lemma 3" oben beweisen

* Welches Transferprinzip gilt zwischen Aussagen für
  A-Moduln M und A~-Moduln M~ auf Spec A?

* Wie Marcs topos-theoretische Sicht auf Arbeit mit generischen Situationen
  formalisieren?

* Ist eine Garbe genau dann lokal konstant, wenn sie aus interner Sicht diskret
  ist? Vermutlich nicht! Gegenbeispiel? Wie kann man denn konstante oder lokal
  konstante Garben intern erkennen? Vielleicht irgendwie, dass sie unter jedem
  phi gleich aussehen?

  Relevant: Johnstone, Topos Theory, Seite 133.
  http://books.google.de/books?id=rLrFAgAAQBAJ&pg=PA133&lpg=PA133&dq=topos+locally+constant+sheaves&source=bl&ots=J66DRhmBON&sig=UfZGh1mXCnxKQiI5Z-Mceoi3q4U&hl=de&sa=X&ei=QUNfVLzlNMeTPOXCgLAO&ved=0CBQQ6AEwADgK

  Seite 285 dort: Unterkategorie der endlichen Objekte (lokal isomorph zu [n])
  ist ein Topos.

* Was hat Marc zu internen Dedekindringen gesagt?
  Sei X = Spec(Zahlkörper). Dann Sh(X) |= "O_X ist ein Hauptidealbereich". ?

* Schema X genau dann lokal von endlicher Präsentation,
  wenn Hom(__, X) (bestimmte) Limiten bewahrt!
  Siehe: http://stacks.math.columbia.edu/download/limits.pdf

* Erhalte ich X_red, indem ich O_X/sqrt(0) intern betrachte?

* Richmans "enabling conditions" topostheoretisch verstehen!

* Klassifikation der Vektorbündel auf P^1 und A^1 intern möglich?
  (Siehe Vakil 18.5.6.) Könnte etwas mit der Smithschen Normalform zu tun
  haben.

* Endlich relatives Spektrum als internes Spektrum verstehen.
  Spec(O_X) ist vielleicht nicht unbedingt der Punkt (sollte er aber sein!),
  aber zumindest ein lokaler Raum. Juhu! Verstanden! Spec(O_X) ist nicht und
  soll nicht der Punkt sein.

* Sei E --> X ein topologisches Vektorbündel.
  Dann kann man seine Projektivierung konstruieren: P(E) --> X.
  Kann man das intern verstehen?

* Unter gewissen Umständen gilt bei eigentlichen Abbildungen f, dass
  f_* O_X ~~ O_Y. Siehe
  http://mathoverflow.net/questions/63301/when-will-the-pushforward-of-a-structure-sheaf-still-be-a-structure-sheaf.
  Kann man das verwenden, um intern Eigentlichkeit zu charakterisieren?

* Geht das valuative criterion für Separiertheit und/oder Eigentlichkeit
  auch für "relative DVRs"? Das sollen Schemamorphismen X --> Y sein,
  sodass es eine affine Überdeckung von Y gibt, sodass die zurückgezogenen
  Morphismen Spec B --> Spec A gerade DVR bzw. der zugehörige Quotientenkörper
  sind.

  Damit könnte man Separiertheit/Eigentlichkeit vielleicht im großen
  Zariskitopos charakterisieren, indem man eine neue Art Allquantor einfügt,
  die nur über relative DVRs quantifiziert.

* Dubuc bemerkt in /Logical opens and real numbers in topoi/ ("Some Examples"),
  dass (der Punktefunktor eines) Schemas im großen Zariski-Topos genau dann
  Penon-separiert ist, wenn das Schema es im üblichen Sinn ist. Zumindest über
  einem algebraisch abgeschlossenen Grundkörper.

  Können wir das verwenden?

* X qc, O_{X,x} reduziert für alle abgeschlossenen Punkte x ==> O_X reduziert.
  Wie intern zeigen? Welche Modalität fasst "für alle abgeschlossenen Punkte"?

* Was ist ein Geradenbündel "mit einer Trivialisierung beim generischen Punkt",
  und wie schlägt sich das intern nieder?

* Zar(A) --> Sh(Spec A) ist lokal, laut dem nLab! Konsequenzen?
  Vielleicht große. Habe damit jedenfalls einen modalen Operator in Zar(A),
  dessen Garbenkategorie gerade die Basiskategorie Sh(Spec A) ist.

  Habe versucht, den Garbifizierungsfunktor herzuleiten. Der sieht (in der
  Notation von grundwissen-algebraische-geometrie.txt) so aus:

      i_* pi_*(E) = i_*(E|_Sh) = (T |-> lim_{U <= Spec A, U --> T} E(U)).

  Sieht Zar(S) aus Sicht von Sh(S) aus wie Zar(Spec O_S)? Oder wie
  Zar(Spec^pcoh O_S), also Zar((pt, O_S))?

* "G --> F, G veT, F koh., phi_x inj ==> phi|_U inj"

* Lesen: http://sbseminar.wordpress.com/2009/08/06/algebraic-geometry-without-prime-ideals

* Kurz prüfen, ob alle relevanten Aussagen bei der Stack-Semantik gültig
  bleiben.

* Splitting-Prinzip intern beweisen?

* Famously, for simplicial sets, the concrete objects are precisely the
  ¬¬-separated presheaves.
  http://nforum.mathforge.org/discussion/1955/on-quasitoposes/

* M~ lokal frei <==> M projektiv und endlich erzeugt. Kann man das intern
  zeigen?

* If A is not noetherian but has a finite number of minimal prime ideals (i.e.,
  the spectrum has a finite number of irreducible components), then it still
  holds that A/*I* is flat iff Spec(A/I)->Spec(A) is open and closed. Indeed,
  there is a result due to Lazard [Laz, Cor. 5.9] which states that the
  flatness of A/*I* implies that I is of finite type in this case.
  http://mathoverflow.net/questions/208/can-a-quotient-ring-r-j-ever-be-flat-over-r

* In kohärenten Topoi sind die kohärenten Objekte genau die lokal endlichen.
  Oder so ähnlich. Siehe Moerdijk/Vermeulen, Seite 81.

* Allgemeines Motto: Wenn man eine Aussage der Form "forall x in X: ..." hat,
  kann man sie vielleicht als "für alle Punkte x des Topos E gilt:
  ...x^{-1}(...)..." erkennen. Dann kann man sie einfach uminterpretieren als
  "in E gilt: ...". Falls E (konstruktiv) nicht genügend viele Punkte hat, ist
  das möglicherweise eine geeignete Verstärkung.

* Habe ein Spektrum an Klassizitätsaussagen in Sh(X), X ein Schema:

    dim O_X <= 0  ==>  dim O_X <= 1  ==> ...
   voll klassisch

* Christiane Rousseau. Topos theory and complex analysis. 1976.

* Christiane Rousseau. Spectral decomposition theorem for real symmetric
  matrices in topoi and applications. 1985.

* Sei F --> E ein surjektiver geometrischer Morphismus. Dann sieht F aus
  Sicht von E aus wie ein Topos, dessen geometrischer Morphismus nach "Set"
  surjektiv ist. Kann man das nutzen? Zum Beispiel für
  Konservativitätsresultate?

* Ist Zar(S) --> Sh(S) essenziell?


=== math.se-Antwort

http://math.stackexchange.com/questions/394194/what-does-a-proof-in-an-internal-logic-actually-look-like/394981#394981

Here is an arbitrary example from algebraic geometry. We'll prove the following
well-known statement about $\mathcal{O}_X$-modules on reduced schemes $X$ by
reducing to constructive linear algebra interpreted in the topos
$\mathrm{Sh}(X)$ of sheaves on $X$:

> Let $\mathcal{F}$ be an $\mathcal{O}_X$-module locally of finite type.
> Then $\mathcal{F}$ is locally free iff its rank is constant.

We can translate this statement into the internal language of $\mathrm{Sh}(X)$
by the following dictionary:

 - In the internal language, the sheaf of rings $\mathcal{O}_X$ looks like an ordinary ring.
 - Accordingly, $\mathcal{F}$ looks like an ordinary module on that ring.
 - $\mathcal{F}$ is locally of finite type iff it is finitely generated from
   the internal point of view.
 - $\mathcal{F}$ is locally free iff it is a free module from the internal
   point of view.
 - Internally, we can define the rank of $\mathcal{F}$ as the minimal number
   of elements needed to generate $\mathcal{F}$. But constructively,
   the natural numbers may fail to have minima of arbitrary inhabited sets (see
   [this enlightening blog post by Andrej Bauer][1]), so this minimal number
   might not actually be an (internal) natural number, but be an element of a
   suitable completion. Externally, the rank defined this way induces a upper
   semicontinuous function on $X$ (see [nLab and the Mulvey reference therein][2]); it is constant iff internally, the minimal number of
   generators is an actual natural number.
 - Finally, the scheme $X$ is reduced iff $\mathcal{O}_X$ looks like an
   ordinary reduced ring from the internal perspective. This in turn is
   equivalent to $\mathcal{O}_X$ being a so-called residue field from the
   internal point of view (i.e. a non-trivial ring with every non-unit being
   zero).

So the statement follows if we can give a constructive proof of the following
linear algebra fact:

> Let $A$ be a residue field and let $M$ be a finitely generated $A$-module.
> Then $A$ is free iff the minimal number of elements needed to generate $M$
> as an $A$-module is an actual natural number.

The direction "$\Rightarrow$" is clear. For the direction "$\Leftarrow$",
consider a minimal generating family $x_1,\ldots,x_n$ of $M$ (which exists by
assumption). This family is linearly independent (and therefore a basis): Let $\sum_i \lambda_i x_i =
0$. If any $\lambda_i$ were invertible, the family
$x_1,\ldots,x_{i-1},x_{i+1},\ldots,x_n$ would too generate $M$, contradicting
the minimality. So each $\lambda_i$ is not invertible and thus zero (by assumption on $A$).

  [1]: http://math.andrej.com/2009/09/08/constructive-stone-minima-of-sets-of-natural-numbers/
  [2]: http://ncatlab.org/nlab/show/one-sided+real+number


=== Zweite math.se-Antwort

A topological space (or locale) $X$ is *local* (i.e. in any covering of $X$ by
open subsets at least one such subset is already equal to $X$) iff the internal
language of $\mathrm{Sh}(X)$ fulfils the following disjunction property: If
$(\phi_i)_{i \in I}$ is an arbitrary family of formulas and $\mathrm{Sh}(X)
\models \bigvee_{i \in I} \phi_i$, then there exists an index $i \in I$ such
that $\mathrm{Sh}(X) \models \phi_i$.

Also, if $X$ is local, the internal language fulfils the following existence
property: If $\mathrm{Sh}(X) \models \exists x : \mathcal{F}. \phi(x)$, then
there actually exists a global section $x \in \Gamma(X,\mathcal{F})$ such that
$\mathrm{Sh}(X) \models \phi(x)$.

A topological space $X$ is *compact* iff the internal language of
$\mathrm{Sh}(X)$ fulfils the following property: If $I$ is a directed set,
$(\phi_i)_{i \in I}$ is a monotone family of formulas (meaning $\mathrm{Sh}(X)
\models (\phi_i \Rightarrow \phi_j)$ for $i \preceq j$) and $\mathrm{Sh}(X)
\models \bigvee_{i \in I} \phi_i$, then there exists an index $i \in I$ such
that $\mathrm{Sh}(X) \models \phi_i$. This follows directly from the
order-theoretic characterization of compactness (a space $X$ being compact iff
for any monotone family $(U_i)_{i \in I}$ of open sets with $X = \bigcup_i
U_i$, there exists $i \in I$ such that $X = U_i$).

As an example, you can use the latter characterization to give an internal
proof of [lemma 01BB in the Stacks Project][1] (saying that if a filtered
colimit $\mathcal{F} = \mathrm{colim}_i \mathcal{F}_i$ of
$\mathcal{O}_X$-modules is of finite type on a quasi-compact scheme $X$, then
one of the maps $\mathcal{F}_i \to \mathcal{F}$ is an epimorphism) by reducing
to the following familiar fact of constructive linear algebra: If a filtered
colimit $A = \mathrm{colim}_i A_i$ is finitely generated, one of the maps $A_i
\to A$ is surjective.

Unfortunately, the logical principles above are *meta* properties of the
internal language, so I'm not sure this answers your question.

**Addendum:** An intrinsic characterization of compactness is not possible,
i.e. there cannot exist a formula $\phi$ such that the internal language of the
sheaf topos of a topological space satisfies $\phi$ iff the space is compact:
If a topological space $X$ can be covered by compact subspaces $U_i$, the
formula $\phi$ would be satisfied on each $U_i$ and hence, by the local
character of the internal language, on $X$ as well. If $X$ itself is not
compact, this is a contradiction.

  [1]: http://stacks.math.columbia.edu/tag/01BB


=== Graphen

Siehe Andrej Bauers MO-Post und Sebastiano Vigna, A guided tour in the topos
of graphs.


=== Lefschetz-Prinzip

Siehe Lefschetz's principle, J Barwise, P Eklof.
http://www.sciencedirect.com/science/article/pii/0021869369901173

Lefschetz's principle and local functors.
http://www.ams.org/journals/proc/1973-037-02/S0002-9939-1973-0325389-7/S0002-9939-1973-0325389-7.pdf


=== Mail an Ravi Vakil

Hello Ravi,

in your notes on Algebraic Geometry, you state on page 119 the general
principle that if a property holds at the generic point then it tends to
hold on a dense open subset.

In fact, there is a general metatheorem describing which properties
spread out in this manner. This is true for all properties which can be
formulated as a "geometric formula", and false in general for other
properties.

In categorical logic, a formula is called "geometric" if and only if it
consists only of "=", "wedge", "vee", "exists", but not "==>", not
"forall" and not "not". Sometimes, a non-geometric formula may be
equivalently reformulated in a geometric way.

I hope this is of some interest to you. Here are three examples:

* In concise notation, the property that a sheaf F of modules is zero
  reads "forall s:F. s = 0". Because of the "forall", this is not a
  geometric formula, and indeed it is not the case that being zero on a
  dense open subset is equivalent to the stalk at the generic point
  being zero.

* But if we have the additional assumption that F is of finite type,
  concisely expressed as "exists s_1,...,s_n:F. forall s:F. s is a
  linear combination of the s_i" (with the passage to open coverings
  implicit), then "forall s:F. s = 0" can be reformulated as "s_1 = 0
  wedge ... wedge s_n = 0" and is thus geometric.

  And indeed: If F is of finite type, then being zero on a dense open
  subset is equivalent to the stalk at the generic point being zero.

* The property of a sheaf being locally free is not geometric in
  general. But it is if the sheaf in question is coherent. [This
  requires some checking.] With this in mind, it's completely obvious
  that a coherent sheaf is locally free on a dense open subset if and
  only if the stalk at the generic point xi is a free O_{X,xi}-module.
  (This is your exercise 13.7.F.)

In fact, the generic point is not special in this regard: A geometric
formula holds on some open subset containing a point x if and only if it
holds at the stalk of x.

Best regards,
Ingo

PS: If you are into such things, here is the logical background:

1. Above "concise notation" actually uses the Bénabou-Mitchell internal
   language of the sheaf topos over the given scheme X.

2. An arbitrary formula phi holds at the generic point iff its "double
   negation translation" holds on X.

   The double negation translation of a formula is obtained by tacking a
   "\neg \neg" in front of each "exists", each "vee" and each "=".

   The double negation translation itself is classical; the particular
   application to schemes is probably well-known to the experts, even
   though I have not found it in the literature.

3. It is a classical [and easy] result of mathematical logic that for
   geometric formulas phi, the double negation translation of phi is
   equivalent to "\neg \neg phi" (i.e. all negneg's pulled to the
   front). This is easily proved by induction on the structure of phi.

4. One can check that the interpretation of "\neg \neg phi" with the
   sheaf semantics is precisely that phi holds on a dense open subset.


=== Charakterisierung von Schemata

* Ein Vorschlag: Eine lokal geringte Örtlichkeit X ist genau dann
  ein Schema, wenn: neg (f inv.) ==> f nilpotent und f im internen Sinn qcoh.

* Zumindest gilt nämlich: Ist der zugrundeliegende Raum der Punkt,
  so folgt schon (in klassischer Logik), dass O_X nur ein Primideal hat und
  daher der Raum isomorph zu Spec O_X ist.

* Außerdem erfüllt (M, C) für topologische Mannigfaltigkeiten diese
  Bedingung im Allgemeinen nicht: Zwar ist C[f^{-1}] noch f-separiert, aber
  keine f-Garbe. Betrachte den Fall M = R und die Funktion e^(1/x) auf D(x).
  Keine Funktion der Form x^n e^(1/x) ist im Ursprung stetig.

  Etwas genauer: Erfülle eine topologische Mannigfaltigkeit die interne
  Bedingung, dass C[f^{-1}] für alle f eine f-Garbe ist. Dann ist die
  Mannigfaltigkeit leer. Dazu muss man nur den Fall M = R^n betrachten.
  Und dort funktioniert das Gegenbeispiel.

* Dasselbe Beispiel funktioniert auch für (C, O_C) komplexe Mannigfaltigkeit.

* Wie steht's um formale Schemata? Da stimmt es vermutlich nicht.
  Man bräuchte sowas wie, dass Vervollständigen und Lokalisierung vertauschen.
  Aber das ist im Allgemeinen falsch. Die Separiertheit ist noch erfüllt.

* Wie steht es um folgende Bedingung? "Ex. Ring A lok.konst., sodass O_X
  die Lokalisierung von A an einer saturierten Menge S, die sogar ein Filter
  ist, ist mit x \not\in S <==> x nilpotent".

  Für Set funktioniert es wieder.

* Die Bedingung, O_X sei aus interner Sicht qcoh, genügt nicht.
  Denn in Set mit klassischer Logik erfüllt ja jeder Ring diese.


=== Diskrete Bewertungsringe

* Die Eigenschaften

  - schwacher Integritätsbereich
  - lokal
  - endlich erzeugte Ideale sind Hauptideale
  - von je zwei Elementen teilt eines das andere

  sind geometrische Implikationen und gelten dann für O_X genau dann, wenn sie
  halmweise gelten. Etwa gilt das in X = Spec Z und allgemeiner für alle
  Dedekindschemata!


=== Differentialformen zu Unterschemata

* Kann man auf sinnvolle/einfache Art und Weise Omega_Y aus Sicht von X
  (Y abgeschlossenes Unterschema von X) beschreiben?

* Triviale Bemerkungen: O/J ist eine Box-Garbe, für Box = (__ v J=(1)).
  a(O) --> O/J ist surjektiv, aber nicht injektiv. Sei K der Kern.
  Dann ist K/K^2 die Konormalgarbe von V(J) in X!


=== Marcs Wunsch nach einer Sprache für Analysis

* Könnte mit NSA zusammenhängen. Denn dort schreibt sich Stetigkeit von f
  wie folgt:

      x ~ x'  ==> f(x) ~ f(x').

  Bin durch http://angg.twu.net/LATEX/2008filterp.pdf auf die Idee gekommen.


=== Stetigkeit

* Sei f_0 : R --> R eine stetige Funktion. Sei X ein metrischer Raum.
  Sei f : C_X --> C_X die von f durch Postkomposition induzierte Abbildung.

  Dann ist aus Sicht der internen Sprache f punktweise stetig. Für gleichmäßige
  Stetigkeit müsste aber glaub ich f_0 selbst gleichmäßig stetig sein. (Ja,
  klar, nimm X = pt.) Es ist f aber wohl gleichmäßig stetig auf jedem
  abgeschlossenen Intervall (wenn man von f_0 weiß, dass es auf abgeschlossenen
  Intervallen gleichmäßig stetig ist).

  Wenn man den Zwischenwertsatz für R hat, hat man ihn auch für f im Topos
  Sh(X).

  http://mathoverflow.net/questions/253059/approximate-intermediate-value-theorem-in-pure-constructive-mathematics


=== Baby-Version von Barrs Theorem

* Barr sagt: Zu jedem Topos E gibt es einen boolschen Topos E', der sogar
  das Auswahlaxiom erfüllt und der mit einer geometrischen Surjektion E' --> E
  daher kommt. Daher gelten geometrische Aussagen genau dann in E, wenn sie in E'
  gelten.

  Der Beweis dieses Theorems ist (angeblich) "highly unconstructive" (nLab).

  (Siehe https://arxiv.org/abs/1603.03374 für eine Kritik!)

* Eine konstruktiv beweisbare Abschwächung erhält man, wenn man darauf
  verzichtet, dass in E' das Auswahlaxiom gilt. Dann kann man E' explizit als
  E' := Sh_j(E/Omega) erhalten, wobei j(phi) = ((phi => t) => t). Dabei ist t
  das universelle Unterobjekt 1 --> Omega, was in E/Omega dann ein Wahrheitswert
  ist. http://mathoverflow.net/a/142230

* Diese Konstruktion von E' sammelt durch Verwendung des generischen
  Wahrheitswerts all folgende Teilresultate auf:

  Sei phi eine geometrische Aussage. Sei phi klassisch beweisbar. Dann ist für
  alle modalen Operatoren Box, sodass die Box-Übersetzung von LEM gilt,
  phi^Box intuitionistisch beweisbar. Da phi geometrisch ist, ist das
  äquivalent zu Box(phi). Wenn man nun Box speziell als Box(alpha) =
  ((alpha => phi) => phi) wählt, erhält man phi.

  Gewissermaßen hat man hier also einen *eigenen* boolschen Topos E'
  für jede zu beweisende Aussage phi.


=== Großer Zariski-Topos

* Aus Sicht von Sh(S) ist Zar(S) vermutlich (im affinen Fall stimmt's)
  gleich "Zar(O_S|O_S)", also der klassifizierende Topos der geometrischen
  Theorie der lokalen O_S-Algebren, für die der Strukturmorphismus lokal ist.

  Allgemeiner sollte Zar(Spec_S A) aus Sh(S)-Sicht der klassifizierende Topos der
  geometrischen Theorie derjenigen lokalen A-Algebren R, für die der Morphismus
  O_S --> A --> R lokal ist, sein; in Übereinstimmung mit der Charakterisierung
  des kleinen Zariski-Topos. Ich denke, dass das aus der Erkenntnis Zar(S) =
  [| Zar(O_S|O_S) |] folgt.

* Definiere Omega^1 als Modul der Kählerdifferentiale von O_S~ --> A^1.
  (Dabei ist O_S~ die Garbe T |--> Gamma(T, mu^(-1) O_S).)

  Da die Kählerdifferentialkonstruktion geometrisch ist, gilt Omega^1|_X =
  Omega^1_{X|S}.

* Auflösung der Unbestimmtheit rationaler Abbildungen durch Blowup -- intern verstehen!

* Kann P^n im großen Zariskitopos über einem Basisschema S ganz naiv als

      { (x_0,...,x_n) | exists i: x_i != 0 } / Reskalierung

  realisieren. Danke an Zhen Lin, der mich (per Mail) darauf gestoßen hat.

  Als Vorstufe ist { (x_0,...,x_n) | exists i: x_i invertierbar } interessant.
  Auf X --> S ist das { (f_0,...,f_n) | f_i in O_X(X) ohne gemeinsame
  Nullstelle }.

  Kann dann schön zeigen: Alle Abbildungen f : P^1 --> A^1 sind konstant.
  Schränke dazu f auf D(x) bzw. D(y) ein. Erhalte so Abbildungen A^1 --> A^1,
  die durch Polynome darstellbar sind.

* Der Punktefunktor zu Spec Sym Omega^1_{X/S} (als S-Schema, nicht als X-Schema)
  ist einfach [Delta, X].

* Kann man die Aufblasung vielleicht wie folgt konstruieren?

      Bl_x0 X = { (x,v) | x in X, v in ... },

  wobei "..." ein geeigneter Ausdruck ist, der im Fall x = x0 zu P(T_x0 X)
  wird. Dabei ist T_x0 X natürlich { f : Delta --> X | f(0) = x0 }.

* Sei J <= O_S eine Idealgarbe. Dann gibt es J~ --> O_S~ und J~~ --> O_S~~.
  Dabei ist J~(T) = Gamma(T, f^{-1} J) und J~~(T) = Gamma(T, f^* J). Der erste
  Morphismus ist weiterhin ein Mono, der zweite aber nicht.

  Das S-Schema V(J) ist intern nicht

      { * | J~~ = (0) },

  sondern

      { * | J~~ --> A^1 ist die Nullabbildung }

  oder äquivalent

      { * | J~ --> A^1 ist die Nullabbildung }.

  Die Konormalgarbe ist gegeben durch (x : V(J) |- J~~).

* Allgemein gilt für f : X --> S:

      (f^* E)~~ = (x:X |- E~~).

* Die Konormalgarbe eines abgeschlossenen Unterschemas zu einer O_S-Modulgarbe E
  ist gegeben durch (x : V(E) |- ann_{O_S~}(E~) tensor_{O_S~} A^1).

  (Ich solte noch prüfen, ob ann_{O_S~}(E~) gleich (ann_{O_S}(E))~ ist.)

  Leider gibt es wohl keine Möglichkeit, den Annulator irgendwie als Annulator
  von E~~ auszudrücken.

* E~ tensor_{O_S~} A^1 = E~~. Schnell kann man das einsehen, wenn man
  die Einschränkung auf Sh(X) betrachtet. Tensorprodukt vertauscht mit
  Einschränkung, da die Tensorproduktkonstruktion geometrisch ist und da
  Einschränkung der Urbildteil eines geometrischen Morphismus ist. Die
  Einschränkung lautet also:

      E~|_Sh(X) tensor_{O_S~|_Sh(X)} A^1|_Sh(X) =
          f^{-1}(E) tensor_{f^{-1}(O_S)} O_X = f^*(E).

  Man muss zwischen Auswertung auf X und Einschränkung auf Sh(X) unterscheiden.
  Letzteres ist sogar bistetig. Ersteres ist die Komposition von einem
  Urbildteil gefolgt von einem Pushforwardteil geometrischer Morphismen.

* Sei f : X --> S. Dann ist Omega^1_{X|S} intern durch

      (Kählerdifferentiale zu \ul{O_S~} --> O_X~) tensor_{O_X~} A^1

  definierbar. Diese Garbe ist gleich (Omega^1_{X|S,klassisch definiert})~~.

  Das zeigt, wie wichtig es ist, O_X~ zu kennen. Als Motto: "Zar(S) ist nichts
  ohne seinen Strukturmorphismus nach Sh(S)! Und O_S~ kontrolliert diesen."

  Es gilt ja, dass Spec_X(Sym Omega^1_{X|S}) = [Delta, X] ist. Vollständig
  intern ausgeschrieben heißt das, dass

      Sigma_{x:X} [Omega_{O_S~ --> O_X~(x)}, A^1]_{O_X~(x)-Mod} =
      Sigma_{x:X} Der_{O_S~}(O_X~(x), A^1) =
      Sigma_{x:X} [Delta, X]_{0 |-> x} =
      [Delta, X]

  ist. Das zweite Gleichheitszeichen ist dabei nichttrivial. Vielleicht könnte
  man es irgendwie zur Charakterisierung von O_X~ verwenden. Noch mal
  übersichtlich ausgeschrieben:

      Hom_{A^1-Mod}(Omega(x), A^1) = [Delta, X]_{0 |-> x}.

  Wenn man in Zar(S) ein neues Schema angibt (also eine Menge), sollte man
  auch immer eine Faktorisierung von \ul{O_S~} --> \ul{A^1} angeben (in der
  Kategorie der lokalen Ringe).

  Fürs relative Spektrum X := [E, A^1]_{A^1-Alg} ist diese wohl folgende:

      (wenn E = R tensor_{O_S~} A^1)
      (im Kontext x : X, also x : E --> A^1 oder transponiert x : R --> A^1)

          O_S~ ---> R[(x^{-1}[Einheiten])^{-1}] ---> A^1.

  Zumindest gilt:

      [Delta, [E, A^1]_{A^1}]_{0 |-> x} =
      [Delta x R, A^1]_{im zweiten Argument O_S~-Alg-Homo, (0,?) |-> x(?)} =
      [R, [Delta, A^1]]_{nach Einsetzung von 0 gleich x, O_S~-Alg-Homo} =
      [R, A^1[eps]/(eps^2)]_{...} =
      [R[(...)^{-1}], A^1[eps]/(eps^2)]_{...} =
      Der_{O_S~}(R[(...)^(-1)], A^1)

  Im letzten Schritt geht ein, dass A^1 vermöge x eine R[...]-Algebra ist.

* Genau dann gilt Zar(A) |== (AA --> A^1 ist eine Lokalisierung), wenn A der
  Nullring ist. Statt "AA --> A^1 ist eine Lokalisierung" kann man auch sagen:
  "O_{Spec A}~ --> A^1 ist bijektiv". Sei nun p ein Primideal in A. Dann
  betrachte das A-Schema Spec k(p)[eps]/(eps^2). Der Morphismus ist dann
  A_p --> k(p)[eps]/(eps^2). Dieser ist nur surjektiv, falls 1 = 0 in A.

  Trotzdem ist AA --> A^1 an manchen Punkten eine Lokalisierung! Etwas komisch.

  (Es ist ja O_{Spec A} eine Lokalisierung von AA in Sh(Spec A). Da
  Lokalisierung eine geometrische Konstruktion ist, ist auch der Rückzug von
  O_{Spec A} auf Zar(A) eine Lokalisierung -- am zurückgezogenen Filter.)

* Aus Sicht von Zar(A) gilt: Hom(E, Spec(A)) = [[ AA --> A^1 ist eine
  Lokalisierung in E ]], für alle Topoi E (wie gesagt, aus Sicht von Zar(A);
  und vielleicht sollte ich mich auf Grothendieck-Topoi beschränken, um
  sicherzustellen, dass die universelle Eigenschaft von Spec(A) verwendbar
  ist).

A Sei F qcoh O_S-Algebra. Dann könnte man denken, dass [F~, A^1]_A^1 = RelSpec F.
  Dabei F~(mu : T --> S) = Gamma(T, mu^* F).

B Sei X S-Schema. Dann könnte man denken, dass [X, A^1] = (mu_* O_X)^~.

* Beides ist aber im Allgemeinen falsch. Allerdings:

  B ist korrekt für X --> S affin.

  A ist korrekt in manchen Fällen:

  * [A^1, A^1]_A^1 = pt.
  * [A^1[T_1,...,T_n], A^1]_A^1 = A^n.
  * [A^1 x A^1, A^1]_A^1 = pt \amalg pt.
    (Verwende: Sei A lokaler Ring. Sei phi : A x A --> A ein A-Algebrenhomo.
    Dann ist -- auch, wenn A nicht unbedingt ein Integritätsbereich ist -- phi
    die Projektion auf eine der beiden Komponenten. Schreibe dazu phi als Matrix.)
  * [A[T]/(f), A^1]_A^1 = V(f) <= A^1.

  A ist wohl allgemein dann korrekt, wenn F lokal als Algebra endlich
  präsentiert ist. Dann sollte auch F~ lokal endlich präsentiert sein. Und für
  endlich präsentierte F~ ist es klar.

  Vielleicht gilt: RelSpec A --> S lveP <==> A veP (als Algebra).

  Wenn die Behauptung auch für projektive Morphismen stimmt (RelProj --> Basis),
  stimmt sie dann auch für alle quasiprojektiven?

* Es gilt: [X, A^1](T) = A^1(X x T) = Gamma(O_{X x T})
  und (mu_* O_X)^~(T) = Gamma(T, eps^* mu_* O_X), wenn T -eps-> S und X -mu-> S.
  PBCT sagt: eps^* mu_* O_X = (pi_T)_* O_{X x T}, falls mu eigentlich ist und
  weitere Bedingungen erfüllt sind.

* Man könnte denken: X --> S ist genau dann abgeschlossen, wenn Zar(S)/X -->
  Zar(S) ein abgeschlossener geometrischer Morphismus ist. Das stimmt aber
  nicht. Denn das ist genau dann der Fall, wenn aus Zar(S)-Sicht gilt:

      forall M <= X. forall phi.
          X <= M cup { x:X | phi }  ===>  (X <= M) vee phi.

  Es sollte ja X = V(f) abgeschlossen sein. Aber setzt man M := {}
  und phi := (f = 0), so erhält man, dass f invertierbar oder Null ist.

* Penon definiert ja: Eine Teilmenge U <= X heißt genau dann offen,
  wenn für alle x aus U und alle y aus X gilt: x != y oder y in U.
  Auf dem nLab steht, dass das nur für Hausdorffräume Sinn ergibt.
  Ist aber jedenfalls falsch für X = 1, denn nach Penons Definition ist jede
  Teilmenge offen.

* Was hat die interne Konstruktion des relativen Spektrums mit Isbell-Dualität
  zu tun?

* Was ist denn der Punktefunktor des Hilbertschemas intern?

* Kategorielle Charakterisierung von glatten Morphismen und paar anderen Sachen:
  http://www.kurims.kyoto-u.ac.jp/~motizuki/Categorical%20Representation%20of%20Locally%20Noetherian%20Log%20Schemes.pdf

* A^1 erfüllt den Hilbertschen Nullstellensatz: Seien f_1, ..., f_r Polynome
  aus A^1[X_1,...,X_n] ohne gemeinsame Nullstelle. Dann ist das von den f_i
  erzeugte Ideal das Einsideal. Das folgt sofort aus der Quasikohärenz von
  A^1[X_1,...,X_n]/(f_1,...,f_r).

  Allgemeiner: Seien f_1, ..., f_r Elemente einer quasikohärenten Algebra A.
  Gelte für alle x aus Spec(A), dass die f_i(x) (= x(f_i)) nicht alle Null sind.
  Dann ist das von den f_i erzeugte Ideal das Einsideal. Das folgt sofort aus
  der Quasikohärenz von A/(f_1,...,f_r). Diese Algebra ist etwa als Kokern von
  A^r --> A wirklich quasikohärent.

* Kohomologie intern?

* Ist A^1 in Zar(S) noethersch, falls S lokal noethersch?


=== Garben-EXT

Sei O_X kohärent. Dann kann EXT intern als Ext verstanden werden.
(In Coh(X) jeweils.)

* Um das einzusehen, sei ohne Einschränkung X affin. Sei F^* --> M --> 0
  eine Auflösung durch endlich-freie Moduln. Dann ist bekannt:

      EXT^*(M~, N~) = H^*(HOM(F~^*, N~))

  Intern sieht F~^* --> M~ --> 0 wie eine projektive Auflösung aus, kann also
  zur Berechnung von Ext verwendet werden:

      Ext(M~, N~) = H^*(Hom(F~^*, N~)).

  Das ist dasselbe wie oben.

* Der Beweis hat noch verschiede Lücken. Zum einen zeigt das nur lokale
  Isomorphie. Außerdem treffe ich hier keine Aussage über RHOM, wobei das wohl
  nicht schwieriger wäre. Aber das Grundsatzproblem der Unbestimmtheit bis auf
  Iso bzw. Quasiiso bleibt!


=== fppf-Topologie

* http://arxiv.org/abs/1407.5446v1
  Points in the fppf topology

* Ist R[X]/(...) endlich frei von positivem Rang, so ist es isomorph
  zu R[X]/(normiert). Nach Cayley--Hamilton finden wir ein normiertes Polynom
  positiven Grads f, das den Algebren- und Modulerzeuger X annihiliert.
  Die restlichen Polynome können wir dann durch Polynome vom Grad < deg(f)
  ersetzen. Nun ist (1,X,...,X^{deg(f)-1}) linear unabhängig (denn EZS von
  richtiger Länger). Also sind die Koeffizienten all der anderen Polynome Null.

  Mit anderen Worten: Ist I ein endlich erzeugtes Ideal von R[X] derart, dass
  R[X]/I endlich frei ist, so ist I ein von einem normierten Polynom erzeugtes
  Hauptideal.


=== Étale Morphismen

* Wie hängen étale Morphismen von Schemata mit étalen geometrischen Morphismen
  von Topoi zusammen?


=== Zusammenhängende Schemata

* Siehe grundwissen-algebraische-geometrie.txt; ist das eine Möglichkeit der
  Internalisierung im großen Zariski-Topos?


=== Derivierte Kategorie

* Wenn man die totale Ableitung eines Funktors intern definieren möchte
  (so, dass sie mit der externen Bedeutung übereinstimmt), gibt es folgende
  Probleme.

  * Man muss irgendwie formulieren, "richtige" (externe) injektive Objekte
    zu verwenden, nicht nur solche, die aus interner Sicht injektiv aussehen.
    (Bei projektiven Objekten sind die Sache noch schlimmer aus: Zum Beispiel
    ist ja O_X aus interner Sicht projektiv, da endlich frei; aus externer
    Sicht aber nicht.)

  * Man hat Eindeutigkeit des Komplexes entweder in der Homotopiekategorie oder
    in der derivierten Kategorie bis auf eindeutigen Isomorphismus. Wenn also
    die Homotopiekategorie oder die derivierte Kategorie (aufgefasst als
    lokal-interne Kategorien) Descent erfüllen, so wird durch die entsprechende
    interne Formel auch extern ein Komplex definiert.

    Insbesondere bei der derivierten Kategorie ist sehr zweifelhaft, ob die
    Descent erfüllt: Sind verklebbare Objekte in den D(AbSh(U_i)) gegeben, so
    geben die doch nicht unbedingt ein Objekt in D(AbSh(U)) für U = bigcup_i U_i,
    oder?

    Natürlich könnte hier die Betrachtung von dg-Kategorien Abhilfe schaffen.

  Wenn man sich mit dem klassischen abgeleiteten Funktor zufrieden gibt, fällt
  die zweite Problematik weg: Denn sowas wie die lokal-interne Kategorie der
  abelschen Gruppenobjekte erfüllt Descent. Man muss R^n F(X) aus interner
  Sicht dann so definieren:

      "iota" Y. exists injektive Auflösung X --> I^*: Y = H^n(F(I^*)),

  wobei "iota" sich auf folgende Eindeutigkeitsaussage bezieht:

      forall X --> I^*, X --> I'^*: exists! psi : Y --> Y'.
          psi ist ein Iso und exists f : I^* --> I'^*:
              f ist mit den Augmentierungen verträglich und H^n(f) = psi.

  (Ohne den langen Zusatz ist das "exists!" nicht gerechtfertigt. Dann gibt es
  keine Chance auf die Kozykelbedingung.)

  Zur ersten Problematik: Leider ist ein Objekt nicht genau dann injektiv, wenn
  es lokal injektiv ist. Die eine Richtung gilt bekanntlich. Aber nicht die
  andere, wie das Beispiel O_X in QCoh(X) zeigt (affin ist O_X gleich A, das
  ist projektiv). Gut, das war jetzt ein Beispiel für Projektivität. Aber ist
  es bei Injektivität anders? Ich kann nicht erwarten, dass die lokalen Lifts
  zusammenpassen!

  Die erste Problematik könnte man auch so lösen oder umgehen, indem man eine
  Spracherweiterung durchführt: Für einen internen Ausdruck A, der eine
  abelsche Gruppe beschreibt, ist I^*(A) eine Auflösung aus (extern-)injektiven
  Objekten.

  Interessant: Um die Eindeutigkeit bis auf eindeutige Isomorphie zu zeigen,
  benötigt man gar nicht, dass die auflösenden Objekte aus externer Sicht
  injektiv sind. Es genügt, dass sie das aus interner Sicht sind.

  Genügt vielleich tatsächlich Auflösung durch Objekte I, für die nicht
  Hom(I, __) exakt ist, sondern HOM(I, __) (Garbenhom)?!

  JA!!!?! Scheint so: Sei eine Auflösung durch echte Injektive gegeben und eine
  zweite aus Intern-Injektiven. Aus interner Sicht sind beide Arten von
  Objekten einfach injektiv. Die interne Sprache zeigt dann, dass es zwischen
  H^n(F(I^*)) und H^n(F(I'^*)) genau einen Iso (mit einer gewissen Eigenschaft)
  gibt. Also gibt es auch aus externer Sicht einen Iso.

  Beispiel: Möchte das Tensorprodukt von Garben ableiten. Genügend viele
  Projektive habe ich nicht. Die klassische Vorgehensweise weicht daher auf
  flache Modulgarben aus. Ich kann aber auch einfach aus interner Sicht
  projektive Moduln verwenden. Also zum Beispiel endlich freie! Und so kann ich
  das abgeleitete Tensorprodukt von kohärenten Modulgarben definieren.

  Anwendung: Höhere direkte Bilder sind aus interner Sicht einfach gewöhnliche
  Garbenkohomologiegruppen. Könnte also "interne Čech-Kohomologie" zur
  Berechnung verwenden (wenn alles konstruktiv durchgeht). Bringt das was?


=== Injektive und welke Garben

* Habe interne Charaktierisierung von Welkheit, siehe garben.txt.

* Außerdem glaube ich, dass eine Garbe (von Mengen) genau dann
  extern-injektiv ist, wenn sie es aus interner Sicht ist. Siehe
  topostheorie.txt.


=== Mikrolinearität (microlinearity, infinitesimal linearity)

* Sei X = Spec(A). Dann ist X mikrolinear.

  Damit ist in voller Allgemeinheit gemeint, dass [__, X] "geeignete"
  Kokegeldiagramme von infinitesimalen Objekten auf Kolimesdiagramme schickt.
  Genauer ist folgendes gemeint.

  Sei F ein endliches Diagramm in der Kategorie der A^1-Algebren, dessen
  Objekte alle Weilalgebren sind. Dann gibt es in die Kategorie der
  A^1-Algebren das Limesdiagramm

      F(i) --> lim(F).
      (zum Beispiel: A^1 --------------------> A^1[eps]/(eps^2)
                      |                             |
                      v                             v
                    A^1[delta]/(delta^2) --> A^1[eps,delta]/(eps^2,delta^2,eps*delta))

  Nach Anwendung von Spec erhält man ein Kokegeldiagramm

      Spec(F(i)) <-- Spec(lim(F)),
      (im Beispiel: 1 <----------- Delta
                    ^                ^
                    |                |
                  Delta <--------- Delta(2) = { (x,y) | x^2 = y^2 = xy = 0 })

  das im Allgemeinen kein Kolimesdiagramm sein wird. (Im Beispiel wäre der
  echte Kolimes nämlich ein Objekt, für das jedes Element von einem der beiden
  Deltas herkommt.)

  Nach Anwendung von [__, X] erhält man wieder ein Kegeldiagramm:

      [Spec(F(i)), X] ---> [Spec(lim(F)), X].

  Die Forderung ist, dass dieses Diagramm ein Limesdiagramm ist.

  Kurz: [Spec(__), X] soll Limiten in der Kategorie der Weilalgebren
  auf Limiten in "Set" abbilden.

  Im großen Zariski-Topos gilt: Ist X das Spektrum einer nicht unbedingt
  quasikohärenten A^1-Algebra, so bewahrt [Spec(__), X] Limiten, und zwar von
  quasikohärenten A^1-Algebren, deren in der Kategorie aller A^1-Algebren
  berechneter Limes wieder quasikohärent ist.

* Ein Korollar: Besitzt X eine offene Überdeckung durch Affine (in dem Sinn,
  dass für jeder Punkt x in X eine offene affine Teilmenge U <= X mit x in U
  existiert), so ist X in genau demselben Sinn mikrolinear.

  Zumindest was die Eigenschaft "X empfindet Delta x_0 ... x_0 Delta --> D(n)
  als surjektiv" angeht. Denn sind Abbildungen f_1, ..., f_n : Delta --> X
  mit x := f_1(0) = ... = f_n(0) gegeben, so finde ein Affinoffenes U mit x in U.
  Dann verwende die schon gewonnene Einsicht über Affine, um eine Abbildung
  g : D(n) --> U zu finden. Diese lässt sich natürlich zu einer Abbildung
  D(n) --> X kofortsetzen (richtiger Begriff?).

  Die Eindeutigkeit ist auch klar.

  In beiden Teilen geht das Lemma ein, dass die f_i bzw. g schon über U
  faktorisieren. Dazu nutze die negneg-Stabilität von U und die Tatsache, dass
  in Delta und D(n) alle Elemente nicht nicht gleich Null sind.


=== Projektiver Raum

Sei P(V) die Menge der Ursprungsgeraden in V. Dann kann ich zeigen:

    T(P(V)) := [Delta, P(V)] = { (l : P(V), alpha : l -> V/l linear) }

Die Isomorphie sieht wie folgt aus. Ist ein gamma : Delta --> P(V) gegeben, so
finden wir (!) einen Lift v : Delta --> V mit gamma(eps) = span(v(eps)) für
alle eps. Wir definieren dann das Tupel (gamma(0), alpha) mit

    alpha(x) = [x/v(0) * v'(0)].

Bezüglich konstanter Reskalierungen ist schon der Ausdruck x/v(0) * v'(0)
wohldefiniert. Aber wenn w(eps) = f(eps) v(eps) ein anderer Lift ist, so gilt:

    x/w(0) * w'(0) = x/(f(0) v(0)) * (f(0) v'(0) + f'(0) v(0)) =
        x/v(0) * v'(0) + f'(0)/f(0) x

Also benötigt man schon den Übergang zum Quotienten V/l.

Ist umgekehrt ein Tupel (l, alpha) gegeben, so schreiben wir l = span(x0)
und alpha(x0) = [z] und definieren so den Weg

    gamma(eps) = span(x0 + eps z).

Das ist wohldefiniert unter Skalierung von x0 (klar) und auch unter Änderung
von z zu z + f x0:

    span(x0 + eps (z + f x0)) = span((1 + eps f) x0 + eps z) =
        span(x0 + eps / (1 + eps f) z) = span(x0 + eps z),

denn eps / (1 + eps f) = eps (1 - eps f) = eps.

Schön!


=== ph-Topologie

* Vielleicht gilt für A^1 in der ph-Topologie:

      Für alle Polynome f_1, ..., f_m:

          alle X_i liegen in sqrt((f_j)_j)
              oder
          es gibt eine "nichttriviale" Lösung (damit ist gemeint, dass
          mindestens eine Koordinate invertierbar ist).

* Dieses Prinzip impliziert zumindest, dass a|b oder b|a für alle
  a, b aus A^1. Und dass A^1 ein schwacher Integritätsbereich ist.

* Genau dann ist Proj O_S[...]/(...) --> S surjektiv, wenn in der
  internen Sprache von Zar(S) (oder von Sh(S), egal) gilt:

      neg (1 in (f_...(1,X_2,...,X_n)) wedge 1 in (f_...(X_1,2,X_3,...,X_n)) wedge ...)

  Das beruht darauf, dass Spec_S(A) --> S genau dann surjektiv ist, wenn
  Sh(S) |== neg (1 = 0 : A). Die Richtung "==>" gilt ohne Voraussetzungen. Die
  Richtung "<==" gilt, falls A von endlichem Typ und quasikohärent ist.
  Zumindest werden diese Voraussetzungen für folgenden Beweis benötigt:

  Angenommen, zu s in S gibt's kein Urbild. Dann ist die Faser A(s) = A_s
  tensor_{O_{S,s}} k(s) = 0 (hier geht ein, dass Spec_S(A) ein Schema ist).
  Somit A_s <= m_s A_s. Mit Nakayama folgt A_s = 0.

* Als Korollar fällt ab: Spec_S(A) --> S ist treuflach genau dann (unter den
  obigen Voraussetzungen), wenn 1 != 0 in A aus Sicht von Sh(S) und wenn
  const(O_S) --> const(A)[F^(-1)] flach ist.

* Die ph-Topologie ist wohl die gröbste Topologie mit:

  * a|b v b|a für alle Elemente von A^1
  * A^1 ist ein schwacher Integritätsbereich
  * Wenn die Resultante nilpotent ist, so hat das homogene Gleichungssystem
    "f_1 = ... = f_l = 0" eine nichttriviale Lösung (das heißt, dass mindestens
    eine Komponente invertierbar ist).

  Muss man noch fordern, dass A^1 algebraisch abgeschlossen ist? Das wäre
  jedenfalls richtig.

  Beweisidee: Mit Chows Lemma auf Überdeckungen der Form
  (Proj_S(O_S[...]/(...) --> S) reduzieren. Dafür benötige S lokal noethersch
  (sonst kann ich nicht garantieren, dass das Relationenideal endlich erzeugt
  ist). Dann die Surjektivität über die Resultante charakterisieren. Fertig.


=== Quasikohärenz im großen Topos

* Sei K ein quasikohärentes Ideal in folgendem starken Sinn:

      A^1/K ---> [ Spec(A^1/K), A^1 ]

  ist ein Iso.

  Sei J ein beliebiges Ideal. Gelte: K = (0) ==> J = (0).
  Dann J <= K.

  Denn für f aus J geht [f] auf Null.


=== K-Theorie

* Kann intern die K-Theorie von Coh(O_X) definieren. Aus externer Sicht
  ist K(Coh(O_X)) eine Garbe von abelschen Gruppen.

* Ist X ein überall ganzes dedekindsches Schema, so ist der kanonische
  interne Homo Z --> K(Coh(O_X)) mit n |-> n * O_X ein Iso.

  Zur Surjektivität nutze, dass jeder kohärente O_X-Modul aus interner Sicht
  direkte Summe von O_X/(d)'s ist; dabei ist d Null oder regulär. Im letzten
  Fall ist [O_X/(d)] = 0.

  Zur Injektivität nutze die Rangabbildung K(Coh(O_X)) --> Z, welche
  wohldefiniert ist. Definiere den Rang eines kohärenten Moduls E etwa als den
  Rang des freien K_X-Moduls E tensor_O K_X. Der ist additiv in kurzen exakten
  Sequenzen.

* Dabei ist klar, dass die interne K-Theorie keinesfalls übereinstimmt
  mit der externen: K(P^1) = Z^2, aber aus interner Sicht ist es nur Z.


=== Kategorie der Schemata als volle Unterkategorie der Topoi

* Keine Ahnung.

* Aber: Kann sowas sagen wie "F --> E muss von der Form E/A --> E sein,
  wobei A aus interner Sicht ein qcqs Schema ist".


=== Relevante MO-Fragen

* http://mathoverflow.net/questions/2314/several-topos-theory-questions
* http://mathoverflow.net/questions/606/synthetic-reasoning-applied-to-algebraic-geometry
* http://mathoverflow.net/questions/5211/geometric-meaning-of-the-euler-sequence-on-mathbbpn-example-8-20-1-in-ch-ii


=== Matthias' Ergebnisse

* Der große infinitesimale Topos von Spec(R) über Spec(K) klassifiziert, falls K
  ein beliebiger Ring und R eine endlich präsentierte K-Algebra ist:

  * Lokale K-Algebren A zusammen mit einem K-Algebrenhomo A --> B, wobei B
    noch die Struktur einer R-Algebra trägt und der Kern nilpotent ist (jedes
    Element einzeln).

  Das ist wohl dasselbe wie:

  * Lokale K-Algebren zusammen mit einem nilpotenten Ideal und einer
    R-Algebrenstruktur auf dem Quotienten.

  Das Lokalitätsadjektiv kann man auch gerne auf den Quotienten verschieben.
  Dann hat man also sowas wie:

  * Lokale R-Algebren, zusammen mit einer K-Algebra (die automatisch lokal ist),
    von der die R-Algebra ein Quotient nach einem nilpotenten Ideal ist.

  Also lokale R-Algebren zusammen mit einer gewählten K-Aufdickung.


=== Modaler Operator für reguläre Überdeckung

* Definition: X ist genau dann quasi-bewohnt, wenn:

      ∀Y. ∀f : X → Y. (∀x,x'. f(x) = f(x')) ⇒ ∃y. ∀x. f(x) = y.

* Dann definieren wir ∇φ als "∃X. X quasi-bewohnt & (X bewohnt ⇒ φ)".

* Das schneidet in PSh(C) wohl die Topologie stabil regulärer
  Singleton-Familien aus.


=== Faserungen

* Arbeit von Nico, offensichtlich

* https://mathoverflow.net/questions/456804/how-to-represent-morphisms-in-a-fibration-in-the-internal-type-theory


=== Nächste Schritte

* von Yuri empfohlen: Yves Diers: Categories of commutative algebras