Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 12th 2012

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

    The proof that LL ¬¬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

    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 BoolHeytBool \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 ¬¬L_{\neg\neg}?

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 12th 2012

    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 ¬¬:LL\neg\neg: L \to L preserves not only finite meets, but the implication operation as well! It follows from this that the inclusion L ¬¬LL_{\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

    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

    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

    Todd, I just broke your last link by making it permanent: Heyting algebra: Proofs.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeMar 12th 2012

    No, I think I was jumping to unjustified conclusions and being confused, sorry.

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 13th 2012

    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

    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

    Oops! Yes, I see it now – thanks.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMar 13th 2012
    • (edited Mar 13th 2012)

    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

    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

    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

    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
    *shrug* Don't ask me.
    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeMar 14th 2012

    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)

    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

    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

    I’ve moved the comments on theorem numbering to their own thread: Theorem numbering.

    • CommentRowNumber20.
    • CommentAuthoreparejatobes
    • CommentTimeMar 16th 2012
    • (edited Mar 16th 2012)

    I don’t know if what follows is shorter, but I think is clearer:

    First, factor the ¬¬{\neg\neg} monad as

    LL ¬¬L L \to L_{\neg\neg} \to L

    and call the reflection LL ¬¬L \to L_{\neg\neg} also ¬¬{\neg\neg}; the inclusion L ¬¬LL_{\neg\neg} \to L will be implicit. We obviously have

    1. ¬¬i{\neg\neg} \dashv i
    2. ii fully faithful
    3. ii preserves and L ¬¬L_{\neg\neg} has finite meets

    From 3 we have that for a,b:L ¬¬a,b \colon L_{\neg\neg}

    a ¬¬b=ab=¬¬(ab) a \wedge_{\neg\neg} b = a \wedge b = {\neg\neg}(a \wedge b)

    Now, everything is easy once we note that

    L ¬¬L_{\neg\neg} is an exponential ideal in LL

    This is almost immediate from the definition of ¬(x)=x0\neg(x) = x \Rightarrow 0; for arbitrary x,y:Lx,y \colon L:

    ¬¬(xy)=((xy)0)0=x((a0)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,

    • ¬¬(xy)=x(¬¬y){\neg\neg}(x \Rightarrow y) = x \Rightarrow ({\neg\neg} y)

    Now, from this if x:L,a:L ¬¬x \colon L, a \colon L_{\neg\neg}, then

    ¬¬(xa)=x(¬¬a)=xa {\neg\neg}(x \Rightarrow a) = x \Rightarrow ({\neg\neg} a) = x \Rightarrow a

    so that xa:L ¬¬x \Rightarrow a \colon L_{\neg\neg} and we get L ¬¬L_{\neg\neg} exponential ideal.

    L ¬¬L_{\neg\neg} closed

    We have, for x,y,c:L ¬¬x,y,c \colon L_{\neg\neg}:

    L ¬¬(x ¬¬y,c) L(xy,c) L(x,yc) L ¬¬(x,yc) \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:L ¬¬a,b \colon L_{\neg\neg} trivially

    a ¬¬b=¬¬(ab)=ab a \Rightarrow_{\neg\neg} b = {\neg\neg}(a \Rightarrow b) = a \Rightarrow b

    and from this both

    • the reflection LL ¬¬L \to L_{\neg\neg}
    • the inclusion L ¬¬LL_{\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

    ¬¬(xy)¬¬(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:L,a=¬¬a:L ¬¬x,y \colon L, a = {\neg\neg} a \colon L_{{\neg\neg}}

    L(xy,a) closed: L(x,ya) a=¬¬a: L(x,y¬¬a) propsof¬¬: L(x,¬¬(ya)) kleisli+expideal: L(¬¬x,ya) closed: L(¬¬xy,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 yy, we get a bijection

    L(xy,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 xyx\wedge y,

    xy¬¬(xy) x \wedge y \to {\neg\neg}(x \wedge y)

    we get what we were looking for:

    ¬¬x ¬¬¬¬y=¬¬x¬¬y¬¬(xy) {\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 ¬¬L_{\neg\neg} being a Boolean algebra, it follows at once from double negation in L ¬¬L_{\neg\neg} being just the double negation of LL resctricted to L ¬¬L_{\neg\neg}. Then, for a:L ¬¬a \colon L_{\neg\neg}:

    ¬¬ ¬¬a=¬¬a=a {\neg\neg}_{\neg\neg} a = {\neg\neg} a = a

    Summing up,

    • the inclusion L ¬¬LL_{\neg\neg} \to L is

      • fully faithful,
      • closed, and
      • preserves any (in particular finite) meets that exist in LL
    • the reflection LL ¬¬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 ¬¬:LL{\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 ¬¬=¬ op¬{\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 ¬ op\neg^{op} is not left adjoint to ¬\neg.

    • CommentRowNumber21.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 16th 2012

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

    L ¬¬L_{\neg\neg} is an exponeital ideal in LL

    (where there is a typo – you mean yy instead of aa) 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)

    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:

    So, here follows what I have:


    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 ¬x=x0\neg x = x \Rightarrow 0; note that this means that

    xy=0x¬y x \wedge y = 0 \iff x \leq \neg y
    1. ¬¬ op\neg \dashv \neg^{op} from the symmetry of meets
    2. ¬¬¬=¬\neg \neg \neg = \neg because every poset adjunction is idempotent
    3. ab=0a(¬¬b)=0a \wedge b = 0 \iff a \wedge (\neg\neg b) = 0 For this, take ab=0a¬ba \wedge b = 0 \iff a \leq \neg b, and from the previous one a¬ba¬¬¬b=¬(¬¬b)a \leq \neg b \iff a \leq \neg\neg\neg b = \neg(\neg\neg b) and then this equivales to a(¬¬b)=0a \wedge (\neg\neg b) = 0.

    the double negation monad

    We can factor the monad ¬¬\neg\neg coming from the ¬¬ op\neg \dashv \neg^{op} adjunction as:

    LL ¬¬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 ¬¬L_{\neg\neg} are just finite meets in LL; so that ¬¬:LL ¬¬\neg\neg \colon L \to L_{\neg\neg} presrving finite meets is equivalent to

    ¬¬(ab)=¬¬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

    ¬¬(ab)¬¬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¬¬(ab) \neg\neg a \wedge \neg\neg b \leq \neg\neg(a\wedge b)

    is equivalent by adjunction to

    (¬¬a¬¬b)¬(ab)=0 (\neg\neg a \wedge \neg\neg b) \wedge \neg(a\wedge b) = 0

    reorganizing this to

    (¬¬a(¬¬b¬(ab))=0 (\neg\neg a \wedge (\neg\neg b \wedge \neg(a\wedge b)) = 0

    we can apply 3 to get

    a(¬¬b¬(ab))=0 a \wedge (\neg\neg b \wedge \neg(a\wedge b)) = 0

    doing the same with bb we arrive at

    (ab)¬(ab)=0 (a \wedge b) \wedge \neg(a\wedge b) = 0

    which is always the case, via adjunction and the unit of ¬¬\neg\neg:

    (ab)¬¬(ab) (a \wedge b) \leq \neg\neg(a\wedge b)

    From this we get that double negation also preserves finite meets.

    L ¬¬L_{\neg\neg} closed

    This is in the Elephant, A.4.3.1. The key is noting that

    ¬¬(xy)=¬¬x¬¬y=¬¬(¬¬xy) \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 aL ¬¬a \in L_{\neg\neg}, x,yLx,y \in L we have

    L(x,ya) closed: L(xy,a) adjunction: L(¬¬(xy),a) propertyabove: L(¬¬(¬¬xy),a) adjunction: L(¬¬xy,a) closed: L(¬¬x,ya) \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

    xya¬¬xya x \leq y \Rightarrow a \iff \neg\neg x \leq y \Rightarrow a

    So taking y=L,x=yay = \in L, x = y \Rightarrow a we get

    ¬¬(ya)=ya \neg\neg (y \Rightarrow a) = y \Rightarrow a

    that is, L ¬¬L_{\neg\neg} is an exponential ideal. From this, it is immediate that

    1. L ¬¬L_{\neg\neg} is closed, with ¬¬=\Rightarrow_{\neg\neg} = \Rightarrow
    2. ii closed

    From this is easy to get that L ¬¬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:

    ¬(ab)=¬¬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 ¬¬ op¬\neg \dashv \neg^{op} \dashv \neg? thanks!