Comments on A Neighborhood of Infinity: Mongruences

I've just stumbled across your post having bee...

2009-09-18T08:04:22.790-07:00

I've just stumbled across your post having been struggling with the same issues as you describe in your post. Yes, the conaturals do seem a little disappointing.

Proof by induction relies on the initiality of N as an algebra of F(X) = 1 + X. Any monomorphism into an initial object is an isomorphism. So a predicate carving out a subset of N, and defining a subalgebra is going to have to be the whole of N.

So coinduction ought to rely on the finality of the conaturals, and that any epimorphism out of them will be an isomorphism. Hence the effort to find a binary relation compatible with the destructors. If one exists, it can only relate pairs of the same element. Rutten puts it to use to prove commutativity of addition on the conaturals on page 36 of Universal coalgebra: a theory of systems.

But, as you note, the duality isn't so apparent. There can't be an equivalence relation on the conaturals with more than one element in the same class. So if I have two expressions for conaturals and I suppose they are related, then either I will be led to contradiction by deducing that predecessors of each are related, or else the original conaturals were identical.

Tricky to imagine using it. What if I say that ((sum of i from 1 to n) - s) relates to (1/2 n(n+1) - s), for all n, all 0 less than or equal to s less than n. Then given any such pair, the predecessors of each are obviously related, the only cases to check being when s = n-1.

In that case we check that (sum of i from 1 to n) - n) = (sum of i from 1 to n-1). And (1/2 n(n+1) - n) = (1/2 (n-1)n), and we know that this pair is related.

So equivalence classes must be individuals, hence (sum i from 1 to n) = 1/2 n(n+1).

Dear sigfpe,

Thanks for the comments, as we...

2006-04-12T05:58:00.000-07:00

Dear sigfpe,

Thanks for the comments, as well as the meta-comments. Whenever one witnesses a play within a play, one should always sit back and enjoy. And I did.

Best wishes,
Paul

It seems ironic that soon after writing this on the subject of 'quoting' code within code I'm facing it as a problem.

In order to make a symbol appear in a post you need to type in the 'quoted' form of it which is turned into the actual symbol.

In order to explain this in detail I need to enter the quoted form of the quoted form. But for some reason the doubly quoted form is being unquoted twice. This is pretty weird behaviour - it makes me wonder of blogger.com iterates your source until it reaches a fixed point. Anyway let me explain how to enter A⇒x⊗y using a quoted form it has no chance of unquoting. You type 'A' followed by ampersand followed by "rArr;x" followed by another ampersand followed by "otimes;y".

He he! Looks like I can't tell you how to include ...

2006-04-11T09:56:00.000-07:00

He he! Looks like I can't tell you how to include those symbols because blogger.com erroneously turns my instructions into the actual symbols.

The symbols can be found here. For example the tensor product x⊗y is written as x⊗y.

This stuff has been around for many years but only in a tiny proportion of browsers. I was astonished to find that it actually works in the majority of browsers now.

(And blogger.com appears to have a bug in the handling of these symbols. When I tried to edit the comment it replaced ⊗ with ⊗ in the source.

The symbols are also working fine for me (Firefox ...

2006-04-11T07:20:00.000-07:00

The symbols are also working fine for me (Firefox 1.5.0.1). Thanks for all your good work.

P.S. How did you get the symbols working? They are nice

Ditto everything from ansobel, except I'm using Wi...

2006-04-10T23:11:00.000-07:00

Ditto everything from ansobel, except I'm using Windows XP instead of Mac, and Google Reader instead of Bloglines.

I'd be interested in feedback on whether the ma...

2006-04-10T23:06:00.000-07:00
I'd be interested in feedback on whether the mathematical symbols below are visible in your browser. Things like right arrow ⇒, infinity ∞ and union ∪.

Yes they are (Firefox 1.5.0.1 and Safari 2.0.3 on a Macintosh). They also show up in a summary of your post on Bloglines.com, which I check in Firefox.

Incidentally, thanks for your blog which I always read with interest.