Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: logic

Topic: Ideal Notation

view this post on Zulip Morgan Rogers (he/him) (Sep 05 2020 at 17:28):

Hi there folks! I'm wondering if someone can help me come up with some good notation.
I'm working with ideals of relations over a bunch of objects. I mean relations in the sense you might expect (in regular logic or algebraic logic, say), R↪A1,…,AnR \hookrightarrow A_1, \dotsc, A_n; you may understand this completely formally, or to be interpreted in a category as a subobject of a product, or as a jointly monic collection of morphisms.
In any case, because relations are ordered, and under the right circumstances I can take joins of them, they form ideals. That is, I can consider non-empty, downward-closed, upward-directed collections of relations with common codomain A1,…,AnA_1, \dotsc,A_n. Clearly ideals are nicely ordered by inclusion, and there is a maximal ideal and possibly a minimal one.

Now, I'm building a fragment of logic where I shall interpret such an ideal as a quotient of the coproduct A1,…,AnA_1,\dotsc,A_n. It would make sense a priori to notate ideals by size (so ⊤\top or 11 for the maximal ideal and ⊥\bot or 00 for the minimal one), but when I take quotients, this order gets reversed! This gives me problems. The notation A1,…,An/I⇒A1,…,An/JA_1,\dotsc,A_n/I \Rightarrow A_1,\dotsc,A_n/J is a clunky way of denoting that the former quotient covers the latter, but on the other hand if I don't include some in-situ indication that the ideals are intended to be interpreted as quotients I get expressions like I⇒⊥I \Rightarrow \bot to indicate that the quotient corresponding to II must be an isomorphism, which should be a positive assertion but looks like it's expressing emptyness or impossibility of something.

In particular, an equational condition like h=kh=k gets expressed as one of this form, I⇒⊥I \Rightarrow \bot, which just feels wrong. I've omitted a lot of details of what I'm doing, but maybe that's enough for someone to have a creative idea that could help?