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 comma 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 finite 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 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 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.
    • CommentAuthorUrs
    • CommentTimeDec 14th 2010

    I tried to structure the entry Heyting algebra a bit more. Check if you like it.

    I also added a little bit to the Examples-section.

    In the section on toposes it says that a “Grothendieck (0,1)-topos” is a locale. Is that correct? Shouldn’t it say: a Grothendieck (0,1)-topos is a category of open subsets of a topological space?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeDec 14th 2010

    The entry looks good.

    Shouldn’t it say: a Grothendieck (0,1)-topos is a category of open subsets of a topological space?

    Why do you say that? Just like a Grothendieck 1-topos need not have enough points, a (0,1)-topos need not either.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeDec 14th 2010

    OK, I can vaguely see the point of all those Definition boxes, especially if we were later to put in proofs for the equivalences between them, but is there a reason for separating out Remarks like that? Is there no room for a paragraph that just stands on its own?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeDec 14th 2010
    • (edited Dec 14th 2010)

    Why do you say that?

    Sorry, that was nonsense. Not sure why I said that.

    is there a reason for separating out Remarks like that?

    I like it. It helps me scan the entry very quickly for information. But feel free to delete the remark-environments again, or some of them, if you feel that’s better.

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeDec 15th 2010

    I’ve never liked Remark environments in books; Definition/Theorem/Proof are formal but remarks are not, so Remark environments only make sense to me in books (like Walter Rudin’s) where every paragraph is numbered and you want a word to stick in front of the number when citing it. After our discussion about the proof environment at Eckmann-Hilton argument, I was afraid that you wanted these too. But since you write

    feel free to delete the remark-environments again, or some of them

    I don’t feel threatened that the Lab will become as ugly as all that. (^_^)

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeDec 15th 2010

    I think Remark environments make sense when (1) you want to refer back to the remark later (“see Remark 4.3”) or (2) you want a paragraph or a group of paragraphs to be “set apart” from the rest of the text as a sort of “side comment,” so that upon encountering the line space after the remark-environment the reader thinks “okay, that digression is over, now back to the main development.”

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeDec 15th 2010

    My only aim is to make the nLab a useful source of information. Useful for me also means that I can extract information from an entry efficiently and quickly – – say when having a quick glance at an entry while in the middle of the discussion with somebody else. For that i want to have it a structure as clear as possible.

    We have or had a bunch of entries that were not structured very well. One had to read the whole entry carefully line by line to get the relevant information. For instance there were some tendencies to write historical or terminological remarks before the definition was even stated, to intersperse the definition with plenty of paranthetical remarks or with examples or consequences before it was even fully stated, and things like that. I tried and will continuously try to restructure such entries, to make them more efficiently readible, will move historical remarks to the end of the entry, will try to separate clearly definitions from side remarks from examples, etc.

    In my attempts to add structure to entries, maybe I am overshooting here and there and adding too much structure. Since I am not dogmatic about any of this but just want to have useful entries, you should all feel free to in turn polish my edits if you find them misguided.

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeDec 15th 2010
    • (edited Dec 15th 2010)

    I agree that the organisation of entries is often bad, (although of course this is better than no entry at all).

    If a remark is truly an aside, then it probably belongs in a different place. I’ve done this with half of one remark, which began “for example” (and also added to it). The rest of that remark, however, seems to me part of the main development of the definition, so I removed it from the Remark environment. Another Remark environment remains.

    • CommentRowNumber9.
    • CommentAuthorzskoda
    • CommentTimeDec 15th 2010

    Urs, the thing which I do not like about structuring is that the entries grow with all the extra data, extra tables, extra titles, extra fonts, extra boxes etc. I myself remember things very visualy and the shorter is the text i comprehend and remember it better, after I understand it once. So in conclusion I like the structure and levels of strcuture when an entry grows already big before blwing it additionally. But for small entries which have 2-3 paragraphs and where the visual memory and visual comprehension works best, I am irritated when it becomes full of tables.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 15th 2010

    So in conclusion I like the structure and levels of strcuture when an entry grows already big before blwing it additionally. But for small entries which have 2-3 paragraphs and where the visual memory and visual comprehension works best, I am irritated when it becomes full of tables.

    We can do something about this: expand these short entries! ;-)

    (The thing is if you create an entry that is still very short, I will add the TOC immediately so that it is there later when the entry grows bigger. For if I don’t do it immediately, I will forget to do it. And since many of you don’t do it, nobody would.)

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeDec 15th 2010

    And since many of you don’t [add the TOC], nobody would.

    I’m now good at adding the TOC, so that I get a chance to add it the right way rather than Urs’s wrong way. (We don’t change each other’s versions.) Without Urs to spur me, I might forget!

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeDec 15th 2010

    I agree with Zoran that there is an advantage to shorter things; it’s easier for me to “grok” a page, or a section of a page, if it doesn’t require lots of scrolling up and down (or even left and right!) to read. For this reason I sometimes change displayed equations to inline ones, if they are small, and collapse bulleted/numbered lists into a paragraph.

    For instance, if a definition has only two fairly short conditions, I think it is easier to read in a paragraph rather than in a numbered list. I think lists are only helpful when they contain at least three entries, and often three or even four conditions can be more easily grasped when described in a paragraph.

    I’m not against organization/structure as such, but I think the point is not to let the structure overshadow the content.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 17th 2010

    Okay. I get the point.

    • CommentRowNumber14.
    • CommentAuthorTobyBartels
    • CommentTimeDec 17th 2010

    In contrast to Mike, I’ve come to like spread out white space and bulleted lists after seeing Urs’s usage of them! I use the latter a lot more now, even in simple emails.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeDec 17th 2010

    Okay, that’s useful to know, too! :-)

    • CommentRowNumber16.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJan 16th 2021

    Added references: original papers and Borceux.

    diff, v41, current

  1. State explicitly that Heyting algebras are distributive as lattices, with proof

    Greg Price

    diff, v45, current

  2. Clean up proof that ¬¬ preserves finite meets.

    The section about Boolean algebras is somewhat disorganized and I’d like to give it a better organization. As a start here, just make this proof more explicit about what it’s proving, and try to tighten it up a bit.

    Greg Price

    diff, v46, current

  3. Add references from deferred proofs to what they’re proving.

    This way the numbers agree exactly, rather than “theorem 1” vs. “Theorem 2.1”.

    Greg Price

    diff, v46, current

    • CommentRowNumber20.
    • CommentAuthorgregprice
    • CommentTimeJul 5th 2022

    Start cleaning up proof that L_{¬¬} is a Boolean algebra

    diff, v48, current

    • CommentRowNumber21.
    • CommentAuthorgregprice
    • CommentTimeJul 15th 2022

    Explicitly state a number of simple properties used in the proofs.

    These facts are frequently useful in themselves when thinking about Heyting algebras, so it’s good to have them stated cleanly in the “Properties” section. This should also help with simplifying the proofs of the theorems, letting them focus on the main ideas.

    diff, v50, current

    • CommentRowNumber22.
    • CommentAuthorgregprice
    • CommentTimeJul 15th 2022

    Define negation sooner, and explicitly state basic facts about it.

    diff, v51, current

    • CommentRowNumber23.
    • CommentAuthorgregprice
    • CommentTimeJul 15th 2022

    Add section on double negation; move the facts that it preserves meets and implications there, and simplify the latter.

    diff, v51, current

    • CommentRowNumber24.
    • CommentAuthorgregprice
    • CommentTimeJul 15th 2022
    I've just made some changes that I hope already make the page more useful: pulling out a number of important basic facts explicitly, as exercises to avoid cluttering the page with many trivial proofs, and then beginning to simplify the proofs of the main theorems accordingly.

    I intend to come back and simplify those proofs much further, and at the same time give them (or at least NegnegAdjoint, the Booleanization adjunction) a more explicit conceptual narrative. But it's late here, so setting this down for the night.
    • CommentRowNumber25.
    • CommentAuthorgregprice
    • CommentTimeJul 16th 2022

    Simplify proof of NegnegAdjoint, and give it hopefully a clearer overall narrative arc.

    diff, v52, current

    • CommentRowNumber26.
    • CommentAuthorgregprice
    • CommentTimeJul 16th 2022

    Move proofs next to theorems, for the adjunctions between Heyt and Bool.

    Now that these proofs are shorter, they fit better in the flow of this section than they would have before; and bringing them together like this simplifies the organization.

    diff, v52, current

    • CommentRowNumber27.
    • CommentAuthorgregprice
    • CommentTimeJul 16th 2022

    Add an “Idea” section, as suggested at Template page.

    diff, v54, current

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeJul 16th 2022

    I have added more hyperlinks to technical terms (such as to logical conjunction for “and”, etc.) and I have taken the liberty of slightly adjusting the wording in the first paragraph (here).

    diff, v55, current

    • CommentRowNumber29.
    • CommentAuthorgregprice
    • CommentTimeJul 17th 2022

    Thanks, Urs! (I’ve adjusted links slightly: one went to conjunction which seems to be something different.)

    I think I’ve made most of the changes to this page that I had my eye on for now. There’s one more which I’d like to get feedback on before I go and try to make it: currently the page defines a Heyting algebra to be a poset. But it seems to me that some important examples of Heyting algebras are most naturally modeled instead as preorders/prosets.

    In particular, perhaps the prototypical Heyting algebra is the collection of propositions in some logic, ordered by syntactic entailment. Given two propositions that are syntactically different (e.g., PP and P(PQ)P \wedge (P \vee Q) for some P,QP, Q), I think one typically doesn’t want to take them to be the same proposition, even when there’s a theorem that they’re equivalent. Accordingly, the implication page already describes this as a preorder.

    So my feeling is that the most natural definition of a Heyting algebra should not require \leq to be antisymmetric. The main consequence of that in this page would be that instead of equations like x=yx = y, we should be writing equivalences. The definition also should then make clear that \leq is only a preorder, not a poset, and add that many authors do require a Heyting algebra to be a poset. What do you think?

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeJul 17th 2022

    This is not different from the situation with Boolean algebras, and it’s completely standard to require antisymmetry in that case. I think it’s best to stick to the standard definitions. In the merely preordered case one sometimes says Heyting prealgebra.

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeJul 17th 2022

    In the case of the propositions in logic, I would just say that they syntactic Heyting algebra is the quotient of propositions by bi-entailment. Two propositions that entail each other aren’t the same proposition, but they induce the same object of the Heyting algebra. This, again, has plenty of analogues elsewhere in categorical logic, e.g. two terms in type theory that are judgmentally equal aren’t the same term, syntactically speaking (in the fully explicit sense that terms would be represented in a proof assistant), but they induce the same morphism of the syntactic category.

    I sort of agree that the categorically natural notion doesn’t require asymmetry. But then we have to treat those objects category-theoretically, in particular considering two of their elements “the same” when they are isomorphic rather than just equal. From a univalent perspective, therefore, the notion of “equality” for those elements should be isomorphism – and in the preordered case we’re fortunate that we can even achieve that in classical set-theoretic foundations by simply taking the poset quotient.

    • CommentRowNumber32.
    • CommentAuthorGuest
    • CommentTimeJul 17th 2022

    If one wants to make Heyting algebras only a preorder, one would have to do the same thing with every other structure in (0,1)-category theory, such as lattices, distributive lattices, semilattices, pseudolattices, suplattices, complete lattices, frames, sigma-frames, coframes et cetera.

    • CommentRowNumber33.
    • CommentAuthorGuest
    • CommentTimeJul 17th 2022

    Lattices have a purely algebraic definition based upon the meets and joins of lattices being commutative idempotent monoid operations satisfying certain absorption laws, where any statement involving the partial order could be rewritten as an equation involving the meet or join. As a result, Heyting algebras could be defined in any symmetric monoidal category with diagonals. If one makes Heyting algebras a preorder they can only be defined in a finitely complete category, since lattices without antisymmetry are not algebraic.

    • CommentRowNumber34.
    • CommentAuthorGuest
    • CommentTimeJul 17th 2022
    meant to write "cartesian monoidal category", not "symmetric monoidal category with diagonals"
    • CommentRowNumber35.
    • CommentAuthorgregprice
    • CommentTimeJul 22nd 2022

    Thanks, Mike, that’s helpful. I’ll limit myself in that direction to adding a link to Heyting prealgebra, then, and perhaps trying to expand the latter page a bit with the thoughts in your last comment.

    Is there a term for the non-antisymmetric version of a lattice, or of a Boolean algebra? There is preframe, but with a different meaning.

    • CommentRowNumber36.
    • CommentAuthorGuest
    • CommentTimeJul 22nd 2022

    A non-antisymmetric version of a lattice is a thin bicartesian category, or equivalently a bicartesian proset.

    • CommentRowNumber37.
    • CommentAuthormattecapu
    • CommentTimeApr 29th 2023

    Create ref to new page about implicative structures

    diff, v60, current

    • CommentRowNumber38.
    • CommentAuthormattecapu
    • CommentTimeApr 29th 2023

    Added redirects for complete Heyting algebra(s), plus remark about their meaning after the definition

    diff, v60, current

    • CommentRowNumber39.
    • CommentAuthormattecapu
    • CommentTimeApr 29th 2023

    Reverted redirects, see discussion at complete Heyting algebra

    diff, v60, current