English

Induced morphisms between Heyting-valued models

Category Theory 2021-11-03 v3

Abstract

To the best of our knowledge, there are very few results on how Heyting-valued models are affected by the morphisms on the complete Heyting algebras that determine them: the only cases found in the literature are concerning automorphisms of complete Boolean algebras and complete embedding between them (\emph{i.e}., injective Boolean algebra homomorphisms that preserves arbitrary suprema and arbitrary infima). In the present work, we consider and explore how more general kinds of morphisms between complete Heyting algebras H\mathbb{H} and H\mathbb{H}' induce arrows between V(H)V^{(\mathbb{H})} and V(H)V^{(\mathbb{H}')}, and between their corresponding localic toposes Set(H)\mathbf{Set}^{(\mathbb{H})} (Sh(H)\simeq \mathbf{Sh}(\mathbb{H})) and Set(H)\mathbf{Set}^{(\mathbb{H}')} (Sh(H)\simeq \mathbf{Sh}(\mathbb{H}')). In more details: any {\em geometric morphism} f:Set(H)Set(H)f^* : \mathbf{Set}^{(\mathbb{H})} \to \mathbf{Set}^{(\mathbb{H'})}, (that automatically came from a unique locale morphism f:HHf : \mathbb{H} \to \mathbb{H}'), can be "lifted" to an arrow f~:V(H)V(H)\tilde{f} : V^{(\mathbb{H})} \to V^{(\mathbb{H}')}. We also provide also some semantic preservation results concerning this arrow f~:V(H)V(H)\tilde{f} : V^{(\mathbb{H})} \to V^{(\mathbb{H}')}.

Cite

@article{arxiv.1910.08193,
  title  = {Induced morphisms between Heyting-valued models},
  author = {José Goudet Alvim and Arthur Francisco Schwerz Cahali and Hugo Luiz Mariano},
  journal= {arXiv preprint arXiv:1910.08193},
  year   = {2021}
}

Comments

28 pages

R2 v1 2026-06-23T11:47:21.239Z