3
$\begingroup$

We know that the category of Boolean algebras and homomorphisms is the ind-completion of $\mathsf{FinBA}$, the full subcategory of $\mathsf{BA}$ of finite Boolean algebras. I am wondering if the same holds for the category $\mathsf{HA}$ of Heyting algebras and Heyting morphisms.

Since Heyting algebras are models of an algebraic theory we know that it has filtered colimits. But I don't know how to prove that every Heyting algebra is the colimit of the diagram of its finite subalgebras.

|cite|improve this question
$\endgroup$
5
$\begingroup$

It's not true that every Heyting algebra is the filtered colimit of its finite subalgebras. Very generally, a finitary algebraic structure is the filtered colimit of its finite substructures iff every finitely generated substructure is finite. But not every finitely generated Heyting algebra is finite (in fact, even a Heyting algebra generated by just one element can be infinite; here is a picture of the free Heyting algebra on one generator).

The ind-completion of the category of finite Heyting algebras is the category of "locally finite" Heyting algebras, the Heyting algebras for which every finitely generated subalgebra is finite.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Thanks for this answer! Do you know of a good book or paper where this is treated in more detail (e.g. the statement that a finitary algebraic structure is the filtered colimit of its finite substructure iff every finitely generated substructure is finite, and related topics)? $\endgroup$ – Math Student 020 Dec 7 '18 at 0:23
  • 4
    $\begingroup$ I don't know a reference. I would consider that statement "obvious" once you've gotten an understanding of how filtered colimits work. In particular, any finitary algebraic structure is the filtered colimit of its finitely generated substructures (that's because the structure is finitary so everything about it is determined by looking at finitely many elements at a time). So that gives the reverse direction of the iff. $\endgroup$ – Eric Wofsey Dec 7 '18 at 3:11
  • 4
    $\begingroup$ For the forward direction, note that if $X$ is a filtered colimit of substructures, every element of $X$ must be in one of those structures, and thus every finite subset of $X$ must be contained in one of those substructures since the system is filtered. So, if $X$ is the filtered colimit of its finite substructures, every finite subset of $X$ must generated a finite substructure. $\endgroup$ – Eric Wofsey Dec 7 '18 at 3:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.