IsarMathLib 1.20.0: Ordered loops and loop valued metrics

Just to be clear, the loops in the title are algebraic structures and are not related to continuous images of circles or flow control constructs in programming languages.

Some time ago I got curious about a minimal setup in which a (pseudo) metric defined on a set would result in making this set a topological space. It turned out that if the metric is defined as a function with values in an partially ordered group we can use the standard definition of an open disk and the collection of unions of such open disks is a topology. However, I noticed then that this should be possible to be pushed a step farther and one should be able to define a metric as a function valued in an ordered loop and still get a topological space. In this release I added some material on ordered loops and rewrote the metric spaces section to be based on metrics valued in ordered loops.

Loops (the algebraic structures) are similar to groups, except that their binary operation does not have to be associative (I wrote more about loops in the previous post). An ordered loop (see for example Lattice-ordered loops and quasigroups by T. Evans) is a loop with a partial order such that if and only if and if and only if . The “if and only if” is worth noting here as this is different from the ordered group definition where one-sided implications are sufficient (I lost a couple of hours working with a wrong definition).

IsarMathLib 1.19.0: Loops

This release adds a theory file about loops. Loops (the kind we talk about here, not to be confused with for example loop algebras) are algebraic structures that are almost like groups, except that we don’t require the operation to be associative. Wikipedia has a nice picture illustrating dependencies between various algebraic structures between magmas and groups which I copy below:

As the picture shows we get a loop when we take a quasigroup and require that an identity (a neutral element of the operation) exists. It can be shown that that identity is unique in the loop. If we denote the loop identity as , then we can define the left and right inverses of a loop element as the only solutions to the equations and . In a loop these inverses do not have to be the same in general. If the loop operation is associative then we get a group and the left and right inverses unify to become the group inverse.

IsarMathLib 1.18.0: Quasigroups

In this release I added a small theory about quasigroups.

A quasigroup is a set with a binary operation (usually written with the multiplicative notation) that supports a certain kind of “divisibility”: every equation of the form or has a unique solution. So, a quasigroup is like a group except we do not require associativity or existence of a neutral element. If we denote those solution as and respectively we get the identities and by definition and, with the uniqueness, we get and , which may serve as an alternative definition of quasigroup.

According to this paper “One of the mathematical subfields where automated theorem provers are heavily used is the field of quasigroup and loop theory”.

IsarMathLib 1.17.0: Real numbers as a metric and topological space

In this release I added a new theory about real numbers. It’s mostly about setting up notation and validating other contexts (related to ordered fields, rings, groups, metric spaces etc.) so that theorems formulated in those contexts can be used when considering real numbers. At the end there are two theorems about the distance function being a metric and one stating that the collection of unions of open disks is a topology on reals.

IsarMathLib had been upgraded to Isabelle2021 in the previous release 1.16.1 (not announced on this blog) but at that time I didn’t notice that the proof documents were not generated properly. The pdf files generated by Isabelle didn’t get the formal text right, some symbols (like and , very important in mathematics based on set theory) were replaced by some placeholder symbol. Errors related to LaTeX are difficult to debug in Isabelle (at least for me), but this time I was lucky. The Isabelle2021 release notes contained information that the “The standard LaTeX engine is now lualatex, according to settings
variable ISABELLE_PDFLATEX.” . Indeed changing the ISABELLE_PDFLATEX="lualatex --file-line-error" line in the settings file back to ISABELLE_PDFLATEX="pdflatex -file-line-error" like it was in Isabelle2020 fixed the problem.

IsarMathLib version 1.16.0: metric spaces

In this release I added a new theory on (pseudo-)metric spaces. Daniel de la Concepción Sáez contributed a theorem stating that in topological groups the group inverse is uniformly continuous with respect to the Roelcke uniformity.

A pseudo-metric is typically defined as a function that satisfies the conditions , and for all . This is sufficient to prove that the collection of subsets of that are unions of disks (defined as ) is a topology, making this metric space a topological space. If we replace the interval in the definition of pseudo-metric by the nonnegative set of a linearly ordered, abelian, Archimedean group then we are not changing anything as such group is isomorphic to a subgroup of the additive group of real numbers. I was curious: what is really needed to get a topological space from a pseudo-metric space this way? Do we really need the group to be Archimedean? Does the group operation have to be commutative? Do we need the order to be total? Amusingly, the answer to these questions is “no”. The group does not have to be abelian and the Archimedean property is not needed. The linear order condition can be relaxed by assuming that the positive set is a meet semi-lattice (every two-element subset has a greatest lower bound) under the group order relation. I don’t know if this is useful to know, but surely my personal curiosity got satisfied.

IsarMathLib version 1.15.0: comparison with Mizar

Some time ago Victor Makarov asked on the Mizar forum about two theorems in group theory. The first theorem states that the union of two subgroups is a subgroup iff one of the subgroups is a subset of the other subgroup. The other one gives a criterion for when for two subgroups the set is also a subgroup. These theorems turned out not to be in the Mizar Mathematical Library, but Roland Coghetto posted formalization of those two theorems in the Mizar proof language. In this release I added the formalization of those two theorems to IsarMathLib so that one can easily compare the syntax and style of Isabelle’s Isar proof language (as it is used in IsarMathLib) and the Mizar proof language.

The result can be viewed as theorems named union_subgroups and prod_subgr_subgr. For the proof of the first one I followed the informal source on Stack Exchange provided by Roland, so it can be directly compared to its Mizar version. The proof of the second one is probably different than the Mizar version, but I think they are still useful as examples of the same theorem in different proof assistants.

IsarMathLib version 1.14.0: lattices

I released the next version of IsarMathLib. This release adds a short theory file about lattices with definitions, notation and a proof that join and and meet-semilattices form idempotent () semigroups.

IsarMathLib version 1.13.0: Roelcke uniformity

I have released version 1.13.0 of IsarMathLib. This release adds the definition and basic properties of the Roelcke uniformity, contributed by Daniel de la Concepción Sáez.

So, what is Roelcke uniformity? As we all know each topological group is a uniform space with two natural uniformities: the left uniformity and right uniformity. The collection of uniformities on a set forms a lattice (in fact, a complete one) so it is natural to ask what are the meet and join of the left and right uniformities. The meet is called the Roelcke uniformity. More details with references can be found in answers to this StackExchange question and the formalization is available in the IsarMathLib’s TopologicalGroup_Uniformity_ZF theory.

 

IsarMathLib version 1.12.1: update to Isabelle2020

This version updates IsarMathLib to Isabelle2020. It was the easiest update ever – nothing had to be changed, so I just changed the abstract in the proof document with the project description.

IsarMathLib version 1.12.0: topological groups and uniformities

This release adds three theory files contributed by Daniel de la Concepción Sáez. Two of them, Topology_ZF_properties_2 and Topology_ZF_properties_3 have been in IsarMathLib for a long time, but I forgot to add them to the file that lists theories to be presented, so they were not showing up in the Isabelle generated HTML presentation or the proof document. Now they do.

The third theory TopologicalGroup_Uniformity_ZF (see also the section Topological groups – uniformity in the proof document or the outline) is brand new in this release and contains a proof that  every topological group is a uniform space.