nLab
flat modality

Definition

On a local topos $H$ acts a comonad $♭$, being the left adjoint to the monad $♯$ induces by the extra right adjoint of the global section geometric morphism. This is the flat modality on the topos.

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.