nLab
sharp modality

Definition

On a local topos $H$ acts a monad $♯$ corresponding to the extra right adjoint of the global section geometric morphism. The sharp modality. It has a left adjoint modality, the flat modality.

Properties

Relation to discrete and codiscrete objects

• The codiscrete objects in a local topos are the modal types for the sharp modality.

• The discrete object in a local topos are the modal types for the flat modality.

Related concepts

cohesion

• (shape modality $⊣$ flat modality $⊣$ sharp modality)

  $(ʃ⊣♭⊣♯)$

  • discrete object, codiscrete object, concrete object

  • structures in cohesion

differential cohesion

• (reduction modality $⊣$ infinitesimal shape modality $⊣$ infinitesimal flat modality)

  $(\mathrm{Red}⊣{ʃ}_{\inf }⊣{♭}_{\inf })$

  • reduced object, coreduced object, formally smooth object

  • formally étale map

  • structures in differential cohesion

References

See the references at local topos.