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

Discussion 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).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeDec 5th 2012

    I felt we were lacking an entry closure operator. I have started one, but don’t have more time now. It’s left in a somewhat sad incomplete state for the moment.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 5th 2012

    Well, we did have such a thing under Moore closure; I’m surprised there wasn’t a redirect.

    • CommentRowNumber3.
    • CommentAuthorTobyBartels
    • CommentTimeDec 5th 2012

    I’m surprised too, although closure does redirect there. (Topological closure is a special case of Moore closure, so there’s no conflict.) The page Moore closure starts at a much more concrete and SetSet-specific level, but it is about the same thing.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeDec 5th 2012
    • (edited Dec 5th 2012)

    I am not so surprised to see redirects missing. I spend a good bit of my time adding missing redirects. :-P

    I created the entry to satisfy the long-broken link to “universal closure operator” at Lawvere-Tierney topology. I had no idea that Moore clsoure exists.

    So wel’ll merge them. But I can’t do so right this moment.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeDec 5th 2012

    It’s not always that someone is lazy about adding redirects; sometimes it’s hard to think of all the names that might want to redirect to a page.

    Of course, sometimes it is someone being lazy, or not knowing about redirects, or occasionally that a page was created before redirects existed.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeDec 5th 2012

    Also: I want to edit this page because I think it is very wrong, but I don’t know where to start. A “universal closure operator” is not the operation on the subobject classifier; it is the operation on posets of subobjects which is stable under pullback. If there is a subobject classifier, then this to give such a thing is equivalent to giving an idempotent monad on the subobject classifier, but that’s not the definition of universal closure operator.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeDec 5th 2012

    For instance, universal closure operators also make sense on quasitoposes.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeDec 6th 2012

    Maybe I shouldn’t announce entries in “sad state”.

    Have adjusted the first sentence now.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeDec 6th 2012

    I have moved over the discussion for reflective subcategories that I had once written in the entry on Lawvere-Tierney topologies.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeDec 6th 2012

    Ah, much better. Shouldn’t this page really be called universal closure operator, though? Moore closure is a special case of a general notion of “closure operator” on a poset, but not a special case of this.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeDec 6th 2012
    • (edited Dec 6th 2012)

    How about putting it like this:

    In logic a closure operator is a monad/comonad on a subobject lattice (of some object in some category). Often one requires an idempotent monad (or idempotent comonad). The collection of subobjects that are taken by this operator to itself (the modal types) form the corresponding closure.

    If one considers a hyperdoctrine of subobject lattices, hence a collection of them parameterized over a category of contexts and equipped with pullback/substitution/context extension, then a universal closure operator or modality is one acting on each of the slices and being compatible with the pullback operation.

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 6th 2012

    In the first paragraph, I think we could just say a closure operator is a monad on a poset (“lattice” generally presupposes meets and joins, which are unnecessary). A comonad on a poset is also called a coclosure operator (I wouldn’t say “monad/comonad” – I definitely do not consider an interior operator on PSP S, defining a topology on SS, to be a closure operator). If a closure operator is understood to be operating on a poset, then you do not need to say “one often requires an idempotent monad” because the idempotence will come for free. Finally, I don’t think one has to say “in logic”.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 6th 2012
    • (edited Dec 6th 2012)

    I have edited the first paragraph to read

    A closure operator is a monad/comonad on a poset of subobjects (of some object in some category). In logic this is often referred to as a modal operator. The collection of subobjects that are taken by this operator to itself (the modal types) form the corresponding closure.

    and moved the remark on idempotency to the last paragraph:

    Instead of subobjects one may consider more generally closures acting on the full slice categories. This promotes the corresponding modal logic to modal type theory. Often one requires the closure operator to be an idempotent monad (or idempotent comonad).

    Concerning the interior operation: this is listed as one example at Moore closure. (?!) Also monads are referred to there. (?!)

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeDec 6th 2012

    The interior is a monad on 𝒫X op\mathcal{P}X^{op}, hence a closure operator there, as it says at Moore closure. Regarded as an operation on 𝒫X\mathcal{P}X, where it is a comonad, it is a coclosure operator.

    • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 6th 2012

    Okay, thanks; I think that looks better, although I still think “monad/comonad” invites confusion (see below). Just say “monad”.

    Concerning the interior operation: this is listed as one example at Moore closure. (?!) Also monads are referred to there. (?!)

    Interior conceived as an operator on (PX) op(P X)^{op}, where it is a monad, sure. The initial part of the article makes clear that a closure operator is a monad. You can of course always say that a comonad Cl:PPCl: P \to P on a poset PP is the same as a closure operator on P opP^{op}; I didn’t think the article was claiming any more than that.

    (I’m a slow thinker and slow typist; Mike beat me to it.)

    • CommentRowNumber16.
    • CommentAuthorRodMcGuire
    • CommentTimeDec 6th 2012
    • (edited Dec 6th 2012)

    To what extent can a closure endofunctor CC simply be defined as one that when restricted to its image is an identity?

    Is there a name (?iso-closure) for the more general case of an endofunctor where the restriction is an automorphism? In this case if AA is the automorphism then there is some mm such that A mA^m is the identity.

    An endofunctor FF is sometimes called a fixed point if there is some nn such that F n+1F^{n+1} is a closure. Is there a corresponding notion (?iso-fixpoint) that uses an ?iso-closure?

    To what extent can all endofunctors be classified by a pair of numbers (n,m)(n,m) that describe a lasso like picture where mm is the length of the loop and nn is the length of the rope leading to the loop?

    • (0, 1) is an identity
    • (0, m) is an automorphism
    • (1, 1) is a closure
    • (1, m) is a iso-closure
    • (n, 1) is a fixpoint
    • (n, m) is an iso-fixpoint
    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 6th 2012

    To what extent can a closure endofunctor C simply be defined as one that when restricted to its image is an identity?

    One thing a closure operator must be is inflationary, i.e., xf(x)x \leq f(x). That plus your conditions, that (1) we have an endofunctor (if xyx \leq y then f(x)f(y)f(x) \leq f(y)), and (2) f(y)=yf(y) = y whenever y=f(x)y = f(x), which is the same as idempotence ff=ff \circ f = f, are the conditions for being a closure operator.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeDec 6th 2012
    • (edited Dec 6th 2012)

    Okay, I have added after the first paragraph the sentence

    Dually, a comonad on a poset is called co-closure operator and the elements fixed by it are called co-closed.

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeDec 7th 2012

    In the interest of clarity, I have renamed the page in question to universal closure operator and started a separate stub closure operator. Hope nobody objects.

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 7th 2012

    So like Tarski’s Boolean algebras with operator (or modal algebras) are to Boolean algebras, you can equip a hyperdoctrine with a universal closure operator. These are sometimes called ’modal hyperdoctrines’.

    I was trying to construct a cube to help me think through the three directions of adding modality, Stone dualizing and shifting between hyperdoctrines and syntactic categories.

    • CommentRowNumber21.
    • CommentAuthorTobyBartels
    • CommentTimeDec 7th 2012

    @Urs re interior:

    this is listed as one example at Moore closure. (?!)

    No, it's listed as an example of a generalisation of Moore closure from power sets to arbitrary posets, and the poset in this case is not a power set but instead the opposite of a power set. So it's not a Moore closure, which (as I know the term) is a closure operator only on power sets.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeDec 9th 2012

    No, it’s listed as an example of a generalisation

    Yes, and that’s why it is an example of the discussion at closure operator.

    But never mind, I think it has been sorted out already.

    • CommentRowNumber23.
    • CommentAuthorTobyBartels
    • CommentTimeDec 10th 2012

    It (topological interior) wasn't listed as an example at closure operator, so I put it there.

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeApr 4th 2013

    Earlier today I had added some stuff to closure operator in a new section induced closure on slices.

    This is a detailed walk through the construction of an idempotent monad on a slice from an idempotent monad on the full category. I used this for a discussion with a student.