Is $mathsf{HA}$ the ind-completion of $mathsf{FinHA}$
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.
category-theory heyting-algebra
add a comment |
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.
category-theory heyting-algebra
add a comment |
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.
category-theory heyting-algebra
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.
category-theory heyting-algebra
category-theory heyting-algebra
edited Dec 6 at 23:59
Eric Wofsey
178k12204331
178k12204331
asked Dec 6 at 23:21
Math Student 020
941616
941616
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
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.
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)?
– Math Student 020
Dec 7 at 0:23
3
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.
– Eric Wofsey
Dec 7 at 3:11
3
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.
– Eric Wofsey
Dec 7 at 3:12
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3029200%2fis-mathsfha-the-ind-completion-of-mathsffinha%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
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.
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)?
– Math Student 020
Dec 7 at 0:23
3
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.
– Eric Wofsey
Dec 7 at 3:11
3
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.
– Eric Wofsey
Dec 7 at 3:12
add a comment |
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.
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)?
– Math Student 020
Dec 7 at 0:23
3
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.
– Eric Wofsey
Dec 7 at 3:11
3
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.
– Eric Wofsey
Dec 7 at 3:12
add a comment |
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.
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.
answered Dec 6 at 23:59
Eric Wofsey
178k12204331
178k12204331
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)?
– Math Student 020
Dec 7 at 0:23
3
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.
– Eric Wofsey
Dec 7 at 3:11
3
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.
– Eric Wofsey
Dec 7 at 3:12
add a comment |
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)?
– Math Student 020
Dec 7 at 0:23
3
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.
– Eric Wofsey
Dec 7 at 3:11
3
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.
– Eric Wofsey
Dec 7 at 3:12
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)?
– Math Student 020
Dec 7 at 0:23
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)?
– Math Student 020
Dec 7 at 0:23
3
3
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.
– Eric Wofsey
Dec 7 at 3:11
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.
– Eric Wofsey
Dec 7 at 3:11
3
3
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.
– Eric Wofsey
Dec 7 at 3:12
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.
– Eric Wofsey
Dec 7 at 3:12
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3029200%2fis-mathsfha-the-ind-completion-of-mathsffinha%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown