Skip to main content
added 1 character in body
Source Link
Simon Henry
  • 42.4k
  • 5
  • 107
  • 205

I recently fondfound an answer for coherent locales, which was enough for my purpose although the argument can probably be expanded to an arbitrary coherent geometric morphism (see at the end, if someone can be bring some precision about this it would be very interesting for me).

Let $f : \mathcal{T} \rightarrow \mathcal{S}$ be an open surjection.

Let $\mathcal{L} \rightarrow \mathcal{S} $ be a locale in $\mathcal{S}$ such that, internally in $\mathcal{T}$, $f^* \mathcal{L}$ is coherent.

We will prove that $\mathcal{L}$ is already coherent in $\mathcal{S}$.

Internally in $\mathcal{T}$, $f^* \mathcal{L}$ is then the stone spectrum of a distributive lattice $I$, and $I$ can be chosen canonically: it is the set of open compact subspaces of $f^* \mathcal{L}$. In particular, when $\gamma: \mathcal{M} \rightarrow \mathcal{N}$ is an isomorphism between two coherent locales it induces an isomorphism between the corresponding distributive lattice, and hence the descent data on $f^* \mathcal{L}$ gives rise to a descent data on the corresponding distributive lattice $I$. (We are also using the fact that the pullback of a spectrum of a distributive lattice is the spectrum of the pullback of the distributive lattice)

Open surjections are of effective descent for sets (objects) hence $I$ (and its descent data) are of the form $f^* I'$ for some $I'$ a distributive lattice (in the base topos). The construction $I \mapsto \text{spec } I$ is compatible with pullback along geometric morphisms hence the isomorphism between $f^* \mathcal{L}$ and $\text{spec } I = f^* \text{spec } I'$ (which is compatible with the descent data simply because we used the isomorphism to construct them) descend into an isomorphism between $\mathcal{L}$ and $\text{spec } I'$ over $\mathcal{S}$, proving that $\mathcal{L}$ is coherent.

So one has the answer for coherent locales, and the open surjection can be replaced by any geometric morphism which is of effective descent for locales (claim: a geometric morphism which is of effective descent for locales is also of effective descent for objects).

This technique can maybe be extended to coherent toposes, but one needs an argument of descent for categories (and for "week descent data") because the distributive lattice of compact open subspace will be replaced by the pre-topos of coherent objects. I have never seen such a result of descent for categories stated but it will probably be not too difficult to obtain at least for hyperconnected geometric morphism.

I recently fond an answer for coherent locales, which was enough for my purpose although the argument can probably be expanded to an arbitrary coherent geometric morphism (see at the end, if someone can be bring some precision about this it would be very interesting for me).

Let $f : \mathcal{T} \rightarrow \mathcal{S}$ be an open surjection.

Let $\mathcal{L} \rightarrow \mathcal{S} $ be a locale in $\mathcal{S}$ such that, internally in $\mathcal{T}$, $f^* \mathcal{L}$ is coherent.

We will prove that $\mathcal{L}$ is already coherent in $\mathcal{S}$.

Internally in $\mathcal{T}$, $f^* \mathcal{L}$ is then the stone spectrum of a distributive lattice $I$, and $I$ can be chosen canonically: it is the set of open compact subspaces of $f^* \mathcal{L}$. In particular, when $\gamma: \mathcal{M} \rightarrow \mathcal{N}$ is an isomorphism between two coherent locales it induces an isomorphism between the corresponding distributive lattice, and hence the descent data on $f^* \mathcal{L}$ gives rise to a descent data on the corresponding distributive lattice $I$. (We are also using the fact that the pullback of a spectrum of a distributive lattice is the spectrum of the pullback of the distributive lattice)

Open surjections are of effective descent for sets (objects) hence $I$ (and its descent data) are of the form $f^* I'$ for some $I'$ a distributive lattice (in the base topos). The construction $I \mapsto \text{spec } I$ is compatible with pullback along geometric morphisms hence the isomorphism between $f^* \mathcal{L}$ and $\text{spec } I = f^* \text{spec } I'$ (which is compatible with the descent data simply because we used the isomorphism to construct them) descend into an isomorphism between $\mathcal{L}$ and $\text{spec } I'$ over $\mathcal{S}$, proving that $\mathcal{L}$ is coherent.

So one has the answer for coherent locales, and the open surjection can be replaced by any geometric morphism which is of effective descent for locales (claim: a geometric morphism which is of effective descent for locales is also of effective descent for objects).

This technique can maybe be extended to coherent toposes, but one needs an argument of descent for categories (and for "week descent data") because the distributive lattice of compact open subspace will be replaced by the pre-topos of coherent objects. I have never seen such a result of descent for categories stated but it will probably be not too difficult to obtain at least for hyperconnected geometric morphism.

I recently found an answer for coherent locales, which was enough for my purpose although the argument can probably be expanded to an arbitrary coherent geometric morphism (see at the end, if someone can be bring some precision about this it would be very interesting for me).

Let $f : \mathcal{T} \rightarrow \mathcal{S}$ be an open surjection.

Let $\mathcal{L} \rightarrow \mathcal{S} $ be a locale in $\mathcal{S}$ such that, internally in $\mathcal{T}$, $f^* \mathcal{L}$ is coherent.

We will prove that $\mathcal{L}$ is already coherent in $\mathcal{S}$.

Internally in $\mathcal{T}$, $f^* \mathcal{L}$ is then the stone spectrum of a distributive lattice $I$, and $I$ can be chosen canonically: it is the set of open compact subspaces of $f^* \mathcal{L}$. In particular, when $\gamma: \mathcal{M} \rightarrow \mathcal{N}$ is an isomorphism between two coherent locales it induces an isomorphism between the corresponding distributive lattice, and hence the descent data on $f^* \mathcal{L}$ gives rise to a descent data on the corresponding distributive lattice $I$. (We are also using the fact that the pullback of a spectrum of a distributive lattice is the spectrum of the pullback of the distributive lattice)

Open surjections are of effective descent for sets (objects) hence $I$ (and its descent data) are of the form $f^* I'$ for some $I'$ a distributive lattice (in the base topos). The construction $I \mapsto \text{spec } I$ is compatible with pullback along geometric morphisms hence the isomorphism between $f^* \mathcal{L}$ and $\text{spec } I = f^* \text{spec } I'$ (which is compatible with the descent data simply because we used the isomorphism to construct them) descend into an isomorphism between $\mathcal{L}$ and $\text{spec } I'$ over $\mathcal{S}$, proving that $\mathcal{L}$ is coherent.

So one has the answer for coherent locales, and the open surjection can be replaced by any geometric morphism which is of effective descent for locales (claim: a geometric morphism which is of effective descent for locales is also of effective descent for objects).

This technique can maybe be extended to coherent toposes, but one needs an argument of descent for categories (and for "week descent data") because the distributive lattice of compact open subspace will be replaced by the pre-topos of coherent objects. I have never seen such a result of descent for categories stated but it will probably be not too difficult to obtain at least for hyperconnected geometric morphism.

added 123 characters in body
Source Link
Simon Henry
  • 42.4k
  • 5
  • 107
  • 205

I recently find a partialfond an answer thatfor coherent locales, which was enough for my purpose. although the argument can probably be expanded to an arbitrary coherent geometric morphism (butsee at the end, if someone can confirm that what follows is correct Ibe bring some precision about this it would be a bite reassured...very interesting for me).

Let $f : \mathcal{T} \rightarrow \mathcal{S}$ be an open surjection.

Let $\mathcal{L} \rightarrow \mathcal{S} $ be a locale in $\mathcal{S}$ such that, internally in $\mathcal{T}$, $f^* \mathcal{L}$ is coherent.

We will prove that $\mathcal{L}$ is already coherent in $\mathcal{S}$.

internallyInternally in $\mathcal{T}$, $f^* \mathcal{L}$ is then the stone spectrum of a distributive lattice $I$, and $I$ can be chosen canonically: it is the set of open compact subspaces of $f^* \mathcal{L}$. In particular, when $\gamma: \mathcal{M} \rightarrow \mathcal{N}$ is an isomorphism between two coherent locales it induces an isomorphism between the corresponding distributive lattice, and hence the descentedescent data on $f^* \mathcal{L}$ gives rise to a descent data on the corresponding distributive lattice $I$. (We are also using the fact that the pullback of a spectrum of a distributive lattice is the spectrum of the pullback of the distributive lattice)

Open surjections are of effective descent for sets (objects) hence $I$ (and its descent data) are of the form $f^* I'$ for some $I'$ a distributive lattice (in the base topos). The construction $I \mapsto \text{spec } I$ is compatible with pullback along geometric morphisms hence the isomorphism between $f^* \mathcal{L}$ and $\text{spec } I = f^* \text{spec } I'$ (which is compatible with the descent data simply because we used the isomorphism to construct them) descend into an isomorphism between $\mathcal{L}$ and $\text{spec } I'$ over $\mathcal{S}$, proving that $\mathcal{L}$ is coherent.

So one has the answer for coherent locales, and the open surjection can be replaced by any geometric morphism which is of effective descent for locales (claim: a geometric morphism which is of effective descent for locales is also of effective descent for objects).

This technique can maybe be extended to coherent toposes, but one needs an argument of descent for categories (and for "week descent data") because the distributive lattice of compact open subspace will be replaced by the pre-topos of coherent objects. I have never seen such a result of descent for categories stated but it will probably be not too difficult to obtain at least for hyperconnected geometric morphism.

I recently find a partial answer that was enough for my purpose. (but if someone can confirm that what follows is correct I would be a bite reassured...)

Let $f : \mathcal{T} \rightarrow \mathcal{S}$ be an open surjection.

Let $\mathcal{L} \rightarrow \mathcal{S} $ be a locale in $\mathcal{S}$ such that, internally in $\mathcal{T}$, $f^* \mathcal{L}$ is coherent.

We will prove that $\mathcal{L}$ is already coherent in $\mathcal{S}$.

internally in $\mathcal{T}$, $f^* \mathcal{L}$ is then the stone spectrum of a distributive lattice $I$, and $I$ can be chosen canonically: it is the set of open compact subspaces of $f^* \mathcal{L}$. In particular, when $\gamma: \mathcal{M} \rightarrow \mathcal{N}$ is an isomorphism between two coherent locales it induces an isomorphism between the corresponding distributive lattice, and hence the descente data on $f^* \mathcal{L}$ gives rise to a descent data on the corresponding distributive lattice $I$. (We are also using the fact that the pullback of a spectrum of a distributive lattice is the spectrum of the pullback of the distributive lattice)

Open surjections are of effective descent for sets (objects) hence $I$ (and its descent data) are of the form $f^* I'$ for some $I'$ a distributive lattice (in the base topos). The construction $I \mapsto \text{spec } I$ is compatible with pullback along geometric morphisms hence the isomorphism between $f^* \mathcal{L}$ and $\text{spec } I = f^* \text{spec } I'$ (which is compatible with the descent data simply because we used the isomorphism to construct them) descend into an isomorphism between $\mathcal{L}$ and $\text{spec } I'$ over $\mathcal{S}$, proving that $\mathcal{L}$ is coherent.

So one has the answer for coherent locales, and the open surjection can be replaced by any geometric morphism which is of effective descent for locales (claim: a geometric morphism which is of effective descent for locales is also of effective descent for objects).

This technique can maybe be extended to coherent toposes, but one needs an argument of descent for categories (and for "week descent data") because the distributive lattice of compact open subspace will be replaced by the pre-topos of coherent objects. I have never seen such a result of descent for categories stated but it will probably be not too difficult to obtain at least for hyperconnected geometric morphism.

I recently fond an answer for coherent locales, which was enough for my purpose although the argument can probably be expanded to an arbitrary coherent geometric morphism (see at the end, if someone can be bring some precision about this it would be very interesting for me).

Let $f : \mathcal{T} \rightarrow \mathcal{S}$ be an open surjection.

Let $\mathcal{L} \rightarrow \mathcal{S} $ be a locale in $\mathcal{S}$ such that, internally in $\mathcal{T}$, $f^* \mathcal{L}$ is coherent.

We will prove that $\mathcal{L}$ is already coherent in $\mathcal{S}$.

Internally in $\mathcal{T}$, $f^* \mathcal{L}$ is then the stone spectrum of a distributive lattice $I$, and $I$ can be chosen canonically: it is the set of open compact subspaces of $f^* \mathcal{L}$. In particular, when $\gamma: \mathcal{M} \rightarrow \mathcal{N}$ is an isomorphism between two coherent locales it induces an isomorphism between the corresponding distributive lattice, and hence the descent data on $f^* \mathcal{L}$ gives rise to a descent data on the corresponding distributive lattice $I$. (We are also using the fact that the pullback of a spectrum of a distributive lattice is the spectrum of the pullback of the distributive lattice)

Open surjections are of effective descent for sets (objects) hence $I$ (and its descent data) are of the form $f^* I'$ for some $I'$ a distributive lattice (in the base topos). The construction $I \mapsto \text{spec } I$ is compatible with pullback along geometric morphisms hence the isomorphism between $f^* \mathcal{L}$ and $\text{spec } I = f^* \text{spec } I'$ (which is compatible with the descent data simply because we used the isomorphism to construct them) descend into an isomorphism between $\mathcal{L}$ and $\text{spec } I'$ over $\mathcal{S}$, proving that $\mathcal{L}$ is coherent.

So one has the answer for coherent locales, and the open surjection can be replaced by any geometric morphism which is of effective descent for locales (claim: a geometric morphism which is of effective descent for locales is also of effective descent for objects).

This technique can maybe be extended to coherent toposes, but one needs an argument of descent for categories (and for "week descent data") because the distributive lattice of compact open subspace will be replaced by the pre-topos of coherent objects. I have never seen such a result of descent for categories stated but it will probably be not too difficult to obtain at least for hyperconnected geometric morphism.

Source Link
Simon Henry
  • 42.4k
  • 5
  • 107
  • 205

I recently find a partial answer that was enough for my purpose. (but if someone can confirm that what follows is correct I would be a bite reassured...)

Let $f : \mathcal{T} \rightarrow \mathcal{S}$ be an open surjection.

Let $\mathcal{L} \rightarrow \mathcal{S} $ be a locale in $\mathcal{S}$ such that, internally in $\mathcal{T}$, $f^* \mathcal{L}$ is coherent.

We will prove that $\mathcal{L}$ is already coherent in $\mathcal{S}$.

internally in $\mathcal{T}$, $f^* \mathcal{L}$ is then the stone spectrum of a distributive lattice $I$, and $I$ can be chosen canonically: it is the set of open compact subspaces of $f^* \mathcal{L}$. In particular, when $\gamma: \mathcal{M} \rightarrow \mathcal{N}$ is an isomorphism between two coherent locales it induces an isomorphism between the corresponding distributive lattice, and hence the descente data on $f^* \mathcal{L}$ gives rise to a descent data on the corresponding distributive lattice $I$. (We are also using the fact that the pullback of a spectrum of a distributive lattice is the spectrum of the pullback of the distributive lattice)

Open surjections are of effective descent for sets (objects) hence $I$ (and its descent data) are of the form $f^* I'$ for some $I'$ a distributive lattice (in the base topos). The construction $I \mapsto \text{spec } I$ is compatible with pullback along geometric morphisms hence the isomorphism between $f^* \mathcal{L}$ and $\text{spec } I = f^* \text{spec } I'$ (which is compatible with the descent data simply because we used the isomorphism to construct them) descend into an isomorphism between $\mathcal{L}$ and $\text{spec } I'$ over $\mathcal{S}$, proving that $\mathcal{L}$ is coherent.

So one has the answer for coherent locales, and the open surjection can be replaced by any geometric morphism which is of effective descent for locales (claim: a geometric morphism which is of effective descent for locales is also of effective descent for objects).

This technique can maybe be extended to coherent toposes, but one needs an argument of descent for categories (and for "week descent data") because the distributive lattice of compact open subspace will be replaced by the pre-topos of coherent objects. I have never seen such a result of descent for categories stated but it will probably be not too difficult to obtain at least for hyperconnected geometric morphism.