After this Math.StackExchange question I have proved that binary relations are essentially the same as pointfree funcoids between powersets.
Full proof is available in my draft book.
The most interesting aspect of this is that is that we can construct filtrator with core being pointfree funcoids from to for every poset of pointfree funcoids between filters on and filters on , by analogy with the filtrator of funcoids whose core is a set of binary relations (the same as a pointfree funcoids, by the above bijective correspondence). This way the theory of filtrators of funcoids generalizes for pointfree funcoids.
By the way, this bijective correspondence is a functor.
Not understood? Read my book.
I wrote a section on ideals, free stars, and mixers in my book.
Now free stars (among with ideals and mixers) are studied as first class objects, being shown isomorphic to filters on posets.
In (not so far) future it should allow to extend our research of pointfree funcoids and staroids/multifuncoids, using now comprehensive theory of free stars (as now we know that they are isomorphic to filters and so their properties are quite clear).
See the development version of my book.
Previously I wrote my research monograph with TeXmacs word processors.
TeXmacs is a very good program. However annoying bugs of TeXmacs (incorrect file “saved” status, failure to work well when multiple windows with the same document are opened, etc.) and also its slowness when working with a long (300 pages) document, forced me to switch to another software.
So I have rewritten my draft book with LyX word processor (based on LaTeX).
There are also small changes which I accomplished due rewriting:
- notatiton change and for the least and the greatest element of a poset
- notatiton change for applying a function to a set ; for existence of a point such that .
- other small changes
Now I am going to start the boring process of checking if I rewrite the book correctly, paragraph by pragraph.
The following are suggestions how to replace math books with hyperlinked modules, in general, and particularly suggestions how to support it in a future version of TeXmacs software. TeXmacs is an advanced math writing software, and the easiest way to implement my ideas are to modify this existing software, rather than writing a completely new software from scratch.
We want presenting math as hyperlinked modules published on the Web. In principle, it is possible to do with TeXmacs, as that software supports hyperlinks and exporting into HTML+MathML (or HTML with images) format. However, the current version of TeXmacs does not provide all features to do it effectively.
First I will describe what I want (irrespective of any particular software).
I want to split a math book (a collection of related math knowledge) into modules.
Every module should contain one theorem or one definition. I may also contain a proof or several proofs of the same statement.
Also, for a given theorem, its module should contain:
- (hyperlinked) list of theorems and definitions this theorem depends on
- (hyperlinked) list of its generalizations
- (hyperlinked) list of other theorems it generalizes
- (hyperlinked) list of counterexamples of non-possible generalizations (example: we cannot strengthen “x=y implies x/z=y/z for nonzero z” for zero z)
- (hyperlinked) list of its consequences (“consequence” probably should not be defined formally as implication, because otherwise every true theorem is a consequence of every other true theorem, but understood in a human way)
We also need the possibility to transform a set of modules into a traditional linearly ordered PDF (or HTML) book. We should have the option to exclude some of features when forming a book, as described in the following paragraph:
When converting into book form, we shall have the option to exclude all proofs. Not being too pedantic, we may allow some users to believe us without reading proofs.
Problems with existing TeXmacs version: We can implement this as modules being separate TeXmacs .tm files. Hyperlinks are already supported by TeXmacs. But we have no TeXmacs feature to transform a set of modules into a linear book. For this, we may make a “content” TeXmacs module, which would contain an ordered list of modules, to make a book of this order. We need the feature to export (say in HTML format, into a folder on a disk) all modules from the “content” file, without manually exporting the files one-by-one.
Most of the following can be done with TeXmacs macroses, without modifying its core. However, who knows, we may probably need changes in TeXmacs itself.
We also need to add to TeXmacs a mechanism to check for invalid forward references, for example when “list of theorems and definitions this theorem depends on” is circular.
We need hyperlinks ordering the list of modules linearly, for the case if somebody wants to read it completely. These links should be based on the above mentioned “content” file.
We also need to generate an index and a list of notations from all modules in a “book”
Also it may probably be sometimes useful to put several modules into one file. This issue should be further investigated.
Just a few minutes ago I conceived a definition of generalized Fréchet filters with definition for every poset on which filters are considered (however, I have not yet calculated the class of posets for which generalized Fréchet filter is defined; it should be easy but I am busy with other business).
Generalized Fréchet filter on a poset is a filter such that
See my book for a definition of .