Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: regular elements in a Heyting algebra

Bottom of Page

1 to 22 of 22

- CommentRowNumber1.
- CommentAuthorTodd_Trimble
- CommentTimeMar 12th 2012
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexI've inserted some proofs of statements made at [[Heyting algebra]], particular on the "regular element" left adjoint to the full inclusion $Bool \to Heyt$. The proof that $L \to L_{\neg\neg}$ preserves implication seemed harder than I was expecting it to be. Or maybe my proof is a clumsy one? If anyone knows a shorter route to this result, I'd be interested.

I’ve inserted some proofs of statements made at Heyting algebra, particular on the “regular element” left adjoint to the full inclusion $Bool \to Heyt$ .

The proof that $L \to L_{\neg\neg}$ preserves implication seemed harder than I was expecting it to be. Or maybe my proof is a clumsy one? If anyone knows a shorter route to this result, I’d be interested.
- CommentRowNumber2.
- CommentAuthorMike Shulman
- CommentTimeMar 12th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexThat's intriguing! I would have expected there to be an abstract reason for that, but I can't think of one right now. Abstract nonsense implies that $Bool \to Heyt$ has a left adjoint, whose unit is then necessarily a Heyting algebra map, but then how can we identify the Boolean reflection with $L_{\neg\neg}$?

That’s intriguing! I would have expected there to be an abstract reason for that, but I can’t think of one right now. Abstract nonsense implies that $Bool \to Heyt$ has a left adjoint, whose unit is then necessarily a Heyting algebra map, but then how can we identify the Boolean reflection with $L_{\neg\neg}$ ?
- CommentRowNumber3.
- CommentAuthorTodd_Trimble
- CommentTimeMar 12th 2012
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexActually, your comment made me realize how all this is connected with the [[double negation translation]] (a page I have just started), which I would imagine requires machinations of the sort worked out at [[Heyting algebra]]. Here's something that actually took me by surprise: double negation on a Heyting algebra $\neg\neg: L \to L$ preserves not only finite meets, but the implication operation as well! It follows from this that the inclusion $L_{\neg\neg} \to L$ also preserves implication (contrary to what was stated before at [[Heyting algebra]], so I guess this will take someone else besides me by surprise (-: ).

Actually, your comment made me realize how all this is connected with the double negation translation (a page I have just started), which I would imagine requires machinations of the sort worked out at Heyting algebra.

Here’s something that actually took me by surprise: double negation on a Heyting algebra $\neg\neg: L \to L$ preserves not only finite meets, but the implication operation as well! It follows from this that the inclusion $L_{\neg\neg} \to L$ also preserves implication (contrary to what was stated before at Heyting algebra, so I guess this will take someone else besides me by surprise (-: ).
- CommentRowNumber4.
- CommentAuthorMike Shulman
- CommentTimeMar 12th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexThat does at first seem a little surprising; but then when I think about it in terms of logic, it's obvious. (-:

That does at first seem a little surprising; but then when I think about it in terms of logic, it’s obvious. (-:
- CommentRowNumber5.
- CommentAuthorTodd_Trimble
- CommentTimeMar 12th 2012
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexSorry, could you explain what you mean? Is there an easier way to see this than what I put down in [Heyting algebra: Proofs](http://ncatlab.org/nlab/show/Heyting+algebra#proofs_24)?

Sorry, could you explain what you mean? Is there an easier way to see this than what I put down in Heyting algebra: Proofs?
- CommentRowNumber6.
- CommentAuthorTobyBartels
- CommentTimeMar 12th 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexTodd, I just broke your last link by making it permanent: [Heyting algebra: Proofs](http://ncatlab.org/nlab/show/Heyting+algebra#proofs).

Todd, I just broke your last link by making it permanent: Heyting algebra: Proofs.
- CommentRowNumber7.
- CommentAuthorMike Shulman
- CommentTimeMar 12th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexNo, I think I was jumping to unjustified conclusions and being confused, sorry.

No, I think I was jumping to unjustified conclusions and being confused, sorry.
- CommentRowNumber8.
- CommentAuthorTodd_Trimble
- CommentTimeMar 13th 2012
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexToby, I see you made edits at [[Heyting algebra]], in particular putting the remark in an environment. But it renders funny, and I can't see what's wrong with the syntax. Does it look funny to you, and if so can you fix it?

Toby, I see you made edits at Heyting algebra, in particular putting the remark in an environment. But it renders funny, and I can’t see what’s wrong with the syntax. Does it look funny to you, and if so can you fix it?
- CommentRowNumber9.
- CommentAuthorTobyBartels
- CommentTimeMar 13th 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexIt's an subtle typo; I had +-- {: un_remark} when it should be +-- {: .un_remark} It's fixed now.
It’s an subtle typo; I had
```
+-- {: un_remark}
```
when it should be
```
+-- {: .un_remark}
```
It’s fixed now.
- CommentRowNumber10.
- CommentAuthorTodd_Trimble
- CommentTimeMar 13th 2012
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexOops! Yes, I see it now -- thanks.

Oops! Yes, I see it now – thanks.
- CommentRowNumber11.
- CommentAuthorUrs
- CommentTimeMar 13th 2012
- (edited Mar 13th 2012)
- PermaLink
Author: Urs
Format: MarkdownItex> when it should be > +-- {: .un_remark} I have a general suggestion: let's use +-- {: .num_remark} and similar by default. That's more useful when an entry grows. (And all entries will grow _eventually_...)
when it should be
```
     +-- {: .un_remark}
```
I have a general suggestion: let’s use
```
      +-- {: .num_remark}
```
and similar by default. That’s more useful when an entry grows. (And all entries will grow eventually…)
- CommentRowNumber12.
- CommentAuthorTodd_Trimble
- CommentTimeMar 13th 2012
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexI think that's a good suggestion, Urs (and I've begun doing that, but not consistently). I'd like to propose another suggestion: when including redirects, make a point of including plural forms. That way a link can be made directly from the plural, without extra fuss.

I think that’s a good suggestion, Urs (and I’ve begun doing that, but not consistently).

I’d like to propose another suggestion: when including redirects, make a point of including plural forms. That way a link can be made directly from the plural, without extra fuss.
- CommentRowNumber13.
- CommentAuthorMike Shulman
- CommentTimeMar 13th 2012
- PermaLink
Author: Mike Shulman
Format: MarkdownItexIf we do use numbered theorem environements, I think we should always also include an anchor name: +-- {: .num_remark #MyRemark} IIRC there is an instiki bug that rears its head when some, but not all, of the numbered theorems on a given page have anchor names assigned.
If we do use numbered theorem environements, I think we should always also include an anchor name:
```
+-- {: .num_remark #MyRemark}
```
IIRC there is an instiki bug that rears its head when some, but not all, of the numbered theorems on a given page have anchor names assigned.
- CommentRowNumber14.
- CommentAuthorUrs
- CommentTimeMar 13th 2012
- PermaLink
Author: Urs
Format: MarkdownItexYes, very true. On the other hand, maybe there is hope that this bug will disappear some day? I keep liking the idea that the software helps me save time, instead of me having to invest time to work around it...

Yes, very true.

On the other hand, maybe there is hope that this bug will disappear some day? I keep liking the idea that the software helps me save time, instead of me having to invest time to work around it…
- CommentRowNumber15.
- CommentAuthorMike Shulman
- CommentTimeMar 13th 2012
- PermaLink
Author: Mike Shulman
Format: Text*shrug* Don't ask me.
*shrug* Don't ask me.
- CommentRowNumber16.
- CommentAuthorTobyBartels
- CommentTimeMar 14th 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexBug or no bug, there's not much point to numbering the theorems/remarks/etc if you can't refer to them later by number. And the only safe way to do that is with the anchors.

Bug or no bug, there’s not much point to numbering the theorems/remarks/etc if you can’t refer to them later by number. And the only safe way to do that is with the anchors.
- CommentRowNumber17.
- CommentAuthorUrs
- CommentTimeMar 14th 2012
- (edited Mar 14th 2012)
- PermaLink
Author: Urs
Format: MarkdownItex> Bug or no bug, there's not much point to numbering the theorems/remarks/etc if you can't refer to them later by number. And the only safe way to do that is with the anchors. That's what we currently do anyway, being forced by the bug: if I want to refer to something by number, I need to anchor everything in between in order for the numbers to come out right. But what I am hesitant (no: unwilling) to do is to preemptively think up anchor names for everything in sight even before I refer to a single one. It would be good, I agree, but there is some limit being reached here.

Bug or no bug, there’s not much point to numbering the theorems/remarks/etc if you can’t refer to them later by number. And the only safe way to do that is with the anchors.

That’s what we currently do anyway, being forced by the bug: if I want to refer to something by number, I need to anchor everything in between in order for the numbers to come out right.

But what I am hesitant (no: unwilling) to do is to preemptively think up anchor names for everything in sight even before I refer to a single one. It would be good, I agree, but there is some limit being reached here.
- CommentRowNumber18.
- CommentAuthorTobyBartels
- CommentTimeMar 14th 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItex>But what I am hesitant (no: unwilling) to do is to preemptively think up anchor names for everything in sight even before I refer to a single one. Me too. But in that case, I just leave them unnumbered until I decide that I wish to refer to them. I agree, the bug should be fixed; and when it is, then you can just make everything numbered to start with, without thinking of names. However, so long as you cannot think of a name, then numbering it gives you no additional benefit (and leaving it unnumbered works around the bug, while we have it).

But what I am hesitant (no: unwilling) to do is to preemptively think up anchor names for everything in sight even before I refer to a single one.

Me too. But in that case, I just leave them unnumbered until I decide that I wish to refer to them.

I agree, the bug should be fixed; and when it is, then you can just make everything numbered to start with, without thinking of names. However, so long as you cannot think of a name, then numbering it gives you no additional benefit (and leaving it unnumbered works around the bug, while we have it).
- CommentRowNumber19.
- CommentAuthorTobyBartels
- CommentTimeMar 14th 2012
- PermaLink
Author: TobyBartels
Format: MarkdownItexI've moved the comments on theorem numbering to their own thread: [Theorem numbering](http://nforum.mathforge.org/discussion/3676/theorem-numbering).

I’ve moved the comments on theorem numbering to their own thread: Theorem numbering.
- CommentRowNumber20.
- CommentAuthoreparejatobes
- CommentTimeMar 16th 2012
- (edited Mar 16th 2012)
- PermaLink
Author: eparejatobes
Format: MarkdownItexI don't know if what follows is shorter, but I think is clearer: First, factor the ${\neg\neg}$ monad as \[ L \to L_{\neg\neg} \to L \] and call the reflection $L \to L_{\neg\neg}$ also ${\neg\neg}$; the inclusion $L_{\neg\neg} \to L$ will be implicit. We obviously have 1. ${\neg\neg} \dashv i$ 2. $i$ fully faithful 3. $i$ preserves and $L_{\neg\neg}$ has finite meets From 3 we have that for $a,b \colon L_{\neg\neg}$ \[ a \wedge_{\neg\neg} b = a \wedge b = {\neg\neg}(a \wedge b) \] Now, everything is easy once we note that > $L_{\neg\neg}$ is an exponential ideal in $L$ This is almost immediate from the definition of $\neg(x) = x \Rightarrow 0$; for arbitrary $x,y \colon L$: \[ {\neg\neg}(x \Rightarrow y) = ((x \Rightarrow y) \Rightarrow 0) \Rightarrow 0 = x \Rightarrow ((a \Rightarrow 0) \Rightarrow 0) = x \Rightarrow ({\neg\neg}(y)) \] that is, - ${\neg\neg}(x \Rightarrow y) = x \Rightarrow ({\neg\neg} y)$ Now, from this if $x \colon L, a \colon L_{\neg\neg}$, then \[ {\neg\neg}(x \Rightarrow a) = x \Rightarrow ({\neg\neg} a) = x \Rightarrow a \] so that $x \Rightarrow a \colon L_{\neg\neg}$ and we get $L_{\neg\neg}$ exponential ideal. #### $L_{\neg\neg}$ closed #### We have, for $x,y,c \colon L_{\neg\neg}$: \[ \begin{matrix} L_{\neg\neg}(x\wedge_{\neg\neg} y, c) \simeq \\ L(x \wedge y, c) \simeq \\ L(x, y \Rightarrow c) \simeq \\ L_{\neg\neg}(x, y \Rightarrow c) \end{matrix} \] Note that for $a,b \colon L_{\neg\neg}$ trivially \[ a \Rightarrow_{\neg\neg} b = {\neg\neg}(a \Rightarrow b) = a \Rightarrow b \] and from this both - the reflection $L \to L_{\neg\neg}$ - the inclusion $L_{\neg\neg} \to L$ are _closed_. We get then ${\neg\neg}$ closed. The only thing left is #### reflection preserves finite meets #### Every functor between cartesian categories is colax monoidal, which here amounts to \[ {\neg\neg}(x \wedge y) \leq {\neg\neg}(x)\wedge_{\neg\neg} {\neg\neg}(y) \] (this is the easy one, of course). For the reverse, first note that Kleisli extension yields \[ x \leq {\neg\neg} y \iff {\neg\neg} x \leq {\neg\neg} y \] Now, for $x,y \colon L, a = {\neg\neg} a \colon L_{{\neg\neg}}$ \[ \begin{matrix} & L(x\wedge y, a) \simeq \\ closed: & L(x, y \Rightarrow a) \simeq \\ a = {\neg\neg}a : & L(x, y \Rightarrow {\neg\neg} a) \simeq \\ props of {\neg\neg}: & L(x, {\neg\neg}(y \Rightarrow a)) \simeq \\kleisli + exp ideal: & L({\neg\neg}x, y \Rightarrow a) \simeq \\ closed: & L({\neg\neg}x \wedge y, a) \end{matrix} \] Applying the same steps to $y$, we get a bijection \[ L(x\wedge y, a) \simeq L({\neg\neg}x \wedge {\neg\neg} y, c) \] Taking the map given by the unit at $x\wedge y$, \[ x \wedge y \to {\neg\neg}(x \wedge y) \] we get what we were looking for: \[ {\neg\neg}x \wedge_{\neg\neg} {\neg\neg} y = {\neg\neg}x \wedge {\neg\neg} y \leq {\neg\neg}(x \wedge y) \] This is just _Proposition A.4.3.1_ of the Elephant adapted to this context. As for $L_{\neg\neg}$ being a Boolean algebra, it follows at once from double negation in $L_{\neg\neg}$ being just the double negation of $L$ resctricted to $L_{\neg\neg}$. Then, for $a \colon L_{\neg\neg}$: \[ {\neg\neg}_{\neg\neg} a = {\neg\neg} a = a \] Summing up, - the inclusion $L_{\neg\neg} \to L$ is - fully faithful, - closed, and - preserves any (in particular finite) meets that exist in $L$ - the reflection $L \to L_{\neg\neg}$ is - eso, - closed, and - preserves finite meets - it also preserves joins, of course From this we get that - double negation ${\neg\neg} \colon L \to L$ is - closed, - and preserves finite meets #### De Morgan? #### By symmetry of $\wedge$, we get \[ \neg \dashv \neg^{op} \] and ${\neg\neg} = \neg^{op}\neg$. It'd be nice if being De Morgan would be equivalent to this adjunction being an ambijunction \[ \neg \dashv \neg^{op} \dashv \neg \] one such Heyting algebra is automatically De Morgan; guess there should be examples of De Morgan Heyting algebras for which $\neg^{op}$ is not _left_ adjoint to $\neg$.
I don’t know if what follows is shorter, but I think is clearer:

First, factor the ${\neg\neg}$ monad as
L→L ¬¬→L L \to L_{\neg\neg} \to L
and call the reflection $L \to L_{\neg\neg}$ also ${\neg\neg}$ ; the inclusion $L_{\neg\neg} \to L$ will be implicit. We obviously have
1. ${\neg\neg} \dashv i$
2. $i$ fully faithful
3. $i$ preserves and $L_{\neg\neg}$ has finite meets
From 3 we have that for $a,b \colon L_{\neg\neg}$
a∧ ¬¬b=a∧b=¬¬(a∧b) a \wedge_{\neg\neg} b = a \wedge b = {\neg\neg}(a \wedge b)
Now, everything is easy once we note that

$L_{\neg\neg}$ is an exponential ideal in $L$

This is almost immediate from the definition of $\neg(x) = x \Rightarrow 0$ ; for arbitrary $x,y \colon L$ :
¬¬(x⇒y)=((x⇒y)⇒0)⇒0=x⇒((a⇒0)⇒0)=x⇒(¬¬(y)) {\neg\neg}(x \Rightarrow y) = ((x \Rightarrow y) \Rightarrow 0) \Rightarrow 0 = x \Rightarrow ((a \Rightarrow 0) \Rightarrow 0) = x \Rightarrow ({\neg\neg}(y))
that is,
- ${\neg\neg}(x \Rightarrow y) = x \Rightarrow ({\neg\neg} y)$
Now, from this if $x \colon L, a \colon L_{\neg\neg}$ , then
¬¬(x⇒a)=x⇒(¬¬a)=x⇒a {\neg\neg}(x \Rightarrow a) = x \Rightarrow ({\neg\neg} a) = x \Rightarrow a
so that $x \Rightarrow a \colon L_{\neg\neg}$ and we get $L_{\neg\neg}$ exponential ideal.

$L_{\neg\neg}$ closed

We have, for $x,y,c \colon L_{\neg\neg}$ :
L ¬¬(x∧ ¬¬y,c)≃ L(x∧y,c)≃ L(x,y⇒c)≃ L ¬¬(x,y⇒c) \begin{matrix} L_{\neg\neg}(x\wedge_{\neg\neg} y, c) \simeq \\ L(x \wedge y, c) \simeq \\ L(x, y \Rightarrow c) \simeq \\ L_{\neg\neg}(x, y \Rightarrow c) \end{matrix}
Note that for $a,b \colon L_{\neg\neg}$ trivially
a⇒ ¬¬b=¬¬(a⇒b)=a⇒b a \Rightarrow_{\neg\neg} b = {\neg\neg}(a \Rightarrow b) = a \Rightarrow b
and from this both
- the reflection $L \to L_{\neg\neg}$
- the inclusion $L_{\neg\neg} \to L$
are closed. We get then ${\neg\neg}$ closed.

The only thing left is

reflection preserves finite meets

Every functor between cartesian categories is colax monoidal, which here amounts to
¬¬(x∧y)≤¬¬(x)∧ ¬¬¬¬(y) {\neg\neg}(x \wedge y) \leq {\neg\neg}(x)\wedge_{\neg\neg} {\neg\neg}(y)
(this is the easy one, of course). For the reverse, first note that Kleisli extension yields
x≤¬¬y⇔¬¬x≤¬¬y x \leq {\neg\neg} y \iff {\neg\neg} x \leq {\neg\neg} y
Now, for $x,y \colon L, a = {\neg\neg} a \colon L_{{\neg\neg}}$
L(x∧y,a)≃ closed: L(x,y⇒a)≃ a=¬¬a: L(x,y⇒¬¬a)≃ propsof¬¬: L(x,¬¬(y⇒a))≃ kleisli+expideal: L(¬¬x,y⇒a)≃ closed: L(¬¬x∧y,a) \begin{matrix} & L(x\wedge y, a) \simeq \\ closed: & L(x, y \Rightarrow a) \simeq \\ a = {\neg\neg}a : & L(x, y \Rightarrow {\neg\neg} a) \simeq \\ props of {\neg\neg}: & L(x, {\neg\neg}(y \Rightarrow a)) \simeq \\kleisli + exp ideal: & L({\neg\neg}x, y \Rightarrow a) \simeq \\ closed: & L({\neg\neg}x \wedge y, a) \end{matrix}
Applying the same steps to $y$ , we get a bijection
L(x∧y,a)≃L(¬¬x∧¬¬y,c) L(x\wedge y, a) \simeq L({\neg\neg}x \wedge {\neg\neg} y, c)
Taking the map given by the unit at $x\wedge y$ ,
x∧y→¬¬(x∧y) x \wedge y \to {\neg\neg}(x \wedge y)
we get what we were looking for:
¬¬x∧ ¬¬¬¬y=¬¬x∧¬¬y≤¬¬(x∧y) {\neg\neg}x \wedge_{\neg\neg} {\neg\neg} y = {\neg\neg}x \wedge {\neg\neg} y \leq {\neg\neg}(x \wedge y)
This is just Proposition A.4.3.1 of the Elephant adapted to this context.

As for $L_{\neg\neg}$ being a Boolean algebra, it follows at once from double negation in $L_{\neg\neg}$ being just the double negation of $L$ resctricted to $L_{\neg\neg}$ . Then, for $a \colon L_{\neg\neg}$ :
¬¬ ¬¬a=¬¬a=a {\neg\neg}_{\neg\neg} a = {\neg\neg} a = a
Summing up,
- the inclusion $L_{\neg\neg} \to L$ is
  - fully faithful,
  - closed, and
  - preserves any (in particular finite) meets that exist in $L$
- the reflection $L \to L_{\neg\neg}$ is
  - eso,
  - closed, and
  - preserves finite meets
  - it also preserves joins, of course
From this we get that
- double negation ${\neg\neg} \colon L \to L$ is
  - closed,
  - and preserves finite meets
De Morgan?

By symmetry of $\wedge$ , we get
¬⊣¬ op \neg \dashv \neg^{op}
and ${\neg\neg} = \neg^{op}\neg$ . It’d be nice if being De Morgan would be equivalent to this adjunction being an ambijunction
¬⊣¬ op⊣¬ \neg \dashv \neg^{op} \dashv \neg
one such Heyting algebra is automatically De Morgan; guess there should be examples of De Morgan Heyting algebras for which $\neg^{op}$ is not left adjoint to $\neg$ .
- CommentRowNumber21.
- CommentAuthorTodd_Trimble
- CommentTimeMar 16th 2012
- PermaLink
Author: Todd_Trimble
Format: MarkdownItexSorry, eparejatobes (I don't know your given name) -- how is the second equation in the second line after > $L_{\neg\neg}$ is an exponeital ideal in $L$ (where there is a typo -- you mean $y$ instead of $a$) supposed to be obvious? I mean, I can prove it, but it's not totally obvious to me without some calculation.

Sorry, eparejatobes (I don’t know your given name) – how is the second equation in the second line after

$L_{\neg\neg}$ is an exponeital ideal in $L$

(where there is a typo – you mean $y$ instead of $a$ ) supposed to be obvious? I mean, I can prove it, but it’s not totally obvious to me without some calculation.
- CommentRowNumber22.
- CommentAuthoreparejatobes
- CommentTimeMar 17th 2012
- (edited Mar 17th 2012)
- PermaLink
Author: eparejatobes
Format: MarkdownItexHi Todd, it's Eduardo :) > Sorry, eparejatobes (I don't know your given name) -- how is the second equation in the second line after > >L¬¬ is an exponeital ideal in L > (where there is a typo -- you mean y instead of a) supposed to be obvious? I mean, I can prove it, but it's not totally obvious to me without some calculation. _Whoah!_ that's wrong in _many_ ways! don't know what I was thinking when I wrote that. I mean, it may be true, but not obvious at all, and in fact I don't know how to prove it :) Thanks for spotting it. I've been looking for a way to fix this, and found a nice proof of $\neg\neg$ perserving finite products in this lecture notes: - [_Frames_ - Ales Pultr](http://www.iazd.uni-hannover.de/~pigors/punktfreie-topologie/dateien/Pultr-Frames.pdf) So, here follows what I have: ### negation ### First of all, let's state some properties of negation which will be of great use later on; most of them are direct consequences of the definition $\neg x = x \Rightarrow 0$; note that this means that \[ x \wedge y = 0 \iff x \leq \neg y \] 1. $\neg \dashv \neg^{op}$ from the symmetry of meets 2. $\neg \neg \neg = \neg$ because every poset adjunction is idempotent 3. $a \wedge b = 0 \iff a \wedge (\neg\neg b) = 0$ For this, take $a \wedge b = 0 \iff a \leq \neg b$, and from the previous one $a \leq \neg b \iff a \leq \neg\neg\neg b = \neg(\neg\neg b)$ and then this equivales to $a \wedge (\neg\neg b) = 0$. ### the double negation monad ### We can factor the monad $\neg\neg$ coming from the $\neg \dashv \neg^{op}$ adjunction as: \[ L \to L_{\neg\neg} \to L \] #### reflection preserves finite meets #### Let's see first that the reflection $\neg\neg$ preserves meets; as a reflective subcategory, we have that finite meets in $L_{\neg\neg}$ are just finite meets in $L$; so that $\neg\neg \colon L \to L_{\neg\neg}$ presrving finite meets is equivalent to \[ \neg\neg(a\wedge b) = \neg\neg a \wedge \neg\neg b \] One inclusion is always true for a functor between posets with finite meets \[ \neg\neg(a\wedge b) \leq \neg\neg a \wedge \neg\neg b \] (every functor between cartesian cats is colax monoidal). Now, for the other one: \[ \neg\neg a \wedge \neg\neg b \leq \neg\neg(a\wedge b) \] is equivalent by adjunction to \[ (\neg\neg a \wedge \neg\neg b) \wedge \neg(a\wedge b) = 0 \] reorganizing this to \[ (\neg\neg a \wedge (\neg\neg b \wedge \neg(a\wedge b)) = 0 \] we can apply 3 to get \[ a \wedge (\neg\neg b \wedge \neg(a\wedge b)) = 0 \] doing the same with $b$ we arrive at \[ (a \wedge b) \wedge \neg(a\wedge b) = 0 \] which is always the case, via adjunction and the unit of $\neg\neg$: \[ (a \wedge b) \leq \neg\neg(a\wedge b) \] From this we get that double negation also preserves finite meets. #### $L_{\neg\neg}$ closed #### This is in the Elephant, A.4.3.1. The key is noting that \[ \neg\neg(x\wedge y) = \neg\neg x \wedge \neg\neg y = \neg\neg(\neg\neg x \wedge y) \] because of $\neg\neg$ idempotent. Now, taking $a \in L_{\neg\neg}$, $x,y \in L$ we have \[ \begin{matrix} & L(x, y \Rightarrow a) \simeq \\ closed: & L(x\wedge y, a) \simeq \\ adjunction: & L(\neg\neg(x\wedge y), a) \simeq \\ property above: & L(\neg\neg(\neg\neg x\wedge y), a) \simeq \\ adjunction: & L(\neg\neg x \wedge y, a) \simeq \\ closed: & L({\neg\neg}x, y \Rightarrow a) \simeq \\ \end{matrix} \] So we have \[ x \leq y \Rightarrow a \iff \neg\neg x \leq y \Rightarrow a \] So taking $y = \in L, x = y \Rightarrow a$ we get \[ \neg\neg (y \Rightarrow a) = y \Rightarrow a \] that is, $L_{\neg\neg}$ is an exponential ideal. From this, it is immediate that 1. $L_{\neg\neg}$ is closed, with $\Rightarrow_{\neg\neg} = \Rightarrow$ 2. $i$ closed From this is easy to get that $L_{\neg\neg}$ is a Boolean algebra etc. What I don't know how to get is that also the reflection is closed. I mean, in a different way than what you have. Really nice the expression: \[ \neg(a \Rightarrow b) = \neg\neg a \wedge \neg b \] haven't seen that before. So, sorry for the noise :) Apart from that, does anyone knows something about Heyting algebras for which $\neg \dashv \neg^{op} \dashv \neg$? thanks!
Hi Todd,

it’s Eduardo :)

Sorry, eparejatobes (I don’t know your given name) – how is the second equation in the second line after

L¬¬ is an exponeital ideal in L (where there is a typo – you mean y instead of a) supposed to be obvious? I mean, I can prove it, but it’s not totally obvious to me without some calculation.

Whoah! that’s wrong in many ways! don’t know what I was thinking when I wrote that. I mean, it may be true, but not obvious at all, and in fact I don’t know how to prove it :) Thanks for spotting it. I’ve been looking for a way to fix this, and found a nice proof of $\neg\neg$ perserving finite products in this lecture notes:
- Frames - Ales Pultr
So, here follows what I have:

negation

First of all, let’s state some properties of negation which will be of great use later on; most of them are direct consequences of the definition $\neg x = x \Rightarrow 0$ ; note that this means that
x∧y=0⇔x≤¬y x \wedge y = 0 \iff x \leq \neg y
1. $\neg \dashv \neg^{op}$ from the symmetry of meets
2. $\neg \neg \neg = \neg$ because every poset adjunction is idempotent
3. $a \wedge b = 0 \iff a \wedge (\neg\neg b) = 0$ For this, take $a \wedge b = 0 \iff a \leq \neg b$ , and from the previous one $a \leq \neg b \iff a \leq \neg\neg\neg b = \neg(\neg\neg b)$ and then this equivales to $a \wedge (\neg\neg b) = 0$ .
the double negation monad

We can factor the monad $\neg\neg$ coming from the $\neg \dashv \neg^{op}$ adjunction as:
L→L ¬¬→L L \to L_{\neg\neg} \to L
reflection preserves finite meets

Let’s see first that the reflection $\neg\neg$ preserves meets; as a reflective subcategory, we have that finite meets in $L_{\neg\neg}$ are just finite meets in $L$ ; so that $\neg\neg \colon L \to L_{\neg\neg}$ presrving finite meets is equivalent to
¬¬(a∧b)=¬¬a∧¬¬b \neg\neg(a\wedge b) = \neg\neg a \wedge \neg\neg b
One inclusion is always true for a functor between posets with finite meets
¬¬(a∧b)≤¬¬a∧¬¬b \neg\neg(a\wedge b) \leq \neg\neg a \wedge \neg\neg b
(every functor between cartesian cats is colax monoidal). Now, for the other one:
¬¬a∧¬¬b≤¬¬(a∧b) \neg\neg a \wedge \neg\neg b \leq \neg\neg(a\wedge b)
is equivalent by adjunction to
(¬¬a∧¬¬b)∧¬(a∧b)=0 (\neg\neg a \wedge \neg\neg b) \wedge \neg(a\wedge b) = 0
reorganizing this to
(¬¬a∧(¬¬b∧¬(a∧b))=0 (\neg\neg a \wedge (\neg\neg b \wedge \neg(a\wedge b)) = 0
we can apply 3 to get
a∧(¬¬b∧¬(a∧b))=0 a \wedge (\neg\neg b \wedge \neg(a\wedge b)) = 0
doing the same with $b$ we arrive at
(a∧b)∧¬(a∧b)=0 (a \wedge b) \wedge \neg(a\wedge b) = 0
which is always the case, via adjunction and the unit of $\neg\neg$ :
(a∧b)≤¬¬(a∧b) (a \wedge b) \leq \neg\neg(a\wedge b)
From this we get that double negation also preserves finite meets.

$L_{\neg\neg}$ closed

This is in the Elephant, A.4.3.1. The key is noting that
¬¬(x∧y)=¬¬x∧¬¬y=¬¬(¬¬x∧y) \neg\neg(x\wedge y) = \neg\neg x \wedge \neg\neg y = \neg\neg(\neg\neg x \wedge y)
because of $\neg\neg$ idempotent. Now, taking $a \in L_{\neg\neg}$ , $x,y \in L$ we have
L(x,y⇒a)≃ closed: L(x∧y,a)≃ adjunction: L(¬¬(x∧y),a)≃ propertyabove: L(¬¬(¬¬x∧y),a)≃ adjunction: L(¬¬x∧y,a)≃ closed: L(¬¬x,y⇒a)≃ \begin{matrix} & L(x, y \Rightarrow a) \simeq \\ closed: & L(x\wedge y, a) \simeq \\ adjunction: & L(\neg\neg(x\wedge y), a) \simeq \\ property above: & L(\neg\neg(\neg\neg x\wedge y), a) \simeq \\ adjunction: & L(\neg\neg x \wedge y, a) \simeq \\ closed: & L({\neg\neg}x, y \Rightarrow a) \simeq \\ \end{matrix}
So we have
x≤y⇒a⇔¬¬x≤y⇒a x \leq y \Rightarrow a \iff \neg\neg x \leq y \Rightarrow a
So taking $y = \in L, x = y \Rightarrow a$ we get
¬¬(y⇒a)=y⇒a \neg\neg (y \Rightarrow a) = y \Rightarrow a
that is, $L_{\neg\neg}$ is an exponential ideal. From this, it is immediate that
1. $L_{\neg\neg}$ is closed, with $\Rightarrow_{\neg\neg} = \Rightarrow$
2. $i$ closed
From this is easy to get that $L_{\neg\neg}$ is a Boolean algebra etc.

What I don’t know how to get is that also the reflection is closed. I mean, in a different way than what you have. Really nice the expression:
¬(a⇒b)=¬¬a∧¬b \neg(a \Rightarrow b) = \neg\neg a \wedge \neg b
haven’t seen that before.

So, sorry for the noise :)

Apart from that, does anyone knows something about Heyting algebras for which $\neg \dashv \neg^{op} \dashv \neg$ ? thanks!

1 to 22 of 22

nForum

Discussion Feed

Not signed in

Site Tag Cloud

nLab > Latest Changes: regular elements in a Heyting algebra

L ¬¬L_{\neg\neg} closed

reflection preserves finite meets

De Morgan?

negation

the double negation monad

reflection preserves finite meets

L ¬¬L_{\neg\neg} closed

$L_{\neg\neg}$ closed

$L_{\neg\neg}$ closed