essential subtopos

An essential subtopos, also called a level of a topos.

Any subtopos is an internal sublocale of the one-point locale. However, this sublocale is an essential sublocale from the internal point of view if and only if the subtopos is an open subtopos (not an essential one). See essential sublocale for details.

Revised on May 10, 2016 14:47:47 by Ingo Blechschmidt (