IsarMathLib 1.9.0 released

I have released version 1.9.0 of IsarMathLib. This is a quite large release with 10 new theory files and 155 new theorems, all contributed by Daniel de la Concepción Sáez. The first of the files contributed by Daniel (released in 1.8.0), Topology_ZF_4 about nets, filters and convergence in topological spaces is now presented on the isarmathlib.org site. The rest of Daniel’s contributions for now can be viewed in the proof document and the outline.

Here is a short description of what is in the new theories:

Cardinal_ZF

There are a couple of theorems about cardinals that are mostly used for studying  properties of topological properties (yes, this is kind of meta).  The main result (proven without AC) is that if two sets can be injectively mapped into an infinite cardinal, then so can be their union. There is also a definition of the Axiom of Choice specific for a given cardinal (so that the choice function exists for families of sets of given cardinality). Some properties are proven for such predicates, like that for finite families of sets the choice function always exists (in ZF) and that the axiom of choice for a larger cardinal implies one for a smaller cardinal.

Group_ZF_4

This theory considers conjugate of subgroup and defines simple groups. A nice theorem here is that endomorphisms of an abelian group form a ring. The first isomorphism theorem (a group homomorphism $h$ induces an isomorphism between the group divided by the kernel of $h$ and the image of $h$) is proven.

Topology_ZF_properties_2

Turns out given a property of a topological space one can define a local version of a property in general. This is studied in the the Topology_ZF_properties_2 theory and applied to local versions of property of being finite or compact or Hausdorff (i.e. locally finite, locally compact, locally Hausdorff). To be honest I didn’t know that FOL allows to reason about predicates on this level of abstraction. There are a couple of nice applications, like one-point compactification that allows to show that every locally compact Hausdorff space is regular. Also there are some results on the interplay between hereditability (there is probably no such word, but you know what I mean, right?) of a property and local properties.

Topology_ZF_8

For a given surjection $f : X\rightarrow Y$, where $X$ is a topological space one can consider the weakest topology on $Y$ which makes $f$ continuous, let’s call it a quotient topology generated by $f$.  The quotient topology generated by an equivalence relation $r$ on $X$ is actually a special case of this setup, where $f$ is a natural projection of $X$ on the quotient $X/r$. The properties of these two ways of getting new topologies are studied in this theory. The main result is that any quotient topology generated by a function is homeomorphic to a topology given by an equivalence relation, so these two approaches to quotient topologies are kind of equivalent.

Topology_ZF_9

As we all know, automorphisms of a topological space form a group. This fact is proven here and the automorphism groups for co-cardinal, included-set, and excluded-set topologies are identified. For order topologies it is shown that order isomorphisms are homeomorphisms of the topology induced by the order. Properties preserved by continuous functions are studied and as an application it is shown for example that quotient topological spaces of compact (or connected) spaces are compact (or connected, resp.)

Topology_ZF_10

This short theory deals with products of two topological spaces. It is proven that if two spaces are $T_0$ (or $T_1$, $T_2$, regular, connected) then their product is as well.

Topology_ZF_11

Given a total order on a set one can define a natural topology on it generated by taking the rays and intervals as the base. This theory studies relations between the order and various properties of generated topology.  For example one can show that if the order topology is connected, then the order is complete (in the sense that for each set bounded from above the set of upper bounds has a minimum). For a given cardinal $\kappa$ we can consider generalized notion of $\kappa$-separability. Turns out $\kappa$ separability is related to (order) density of sets of cardinality $\kappa$ for order topologies.

Topological_Group_ZF_1.thy

Being a topological group imposes additional structure on the topology of the group, in particular its separation properties. In this theory it is shown that if a topology is $T_0$, then it must be $T_3$ , and that the topology in a topological group is always regular.

Topological_Group_ZF_2.thy

For a given normal subgroup of a topological group we can define a topology on the quotient group in a natural way. At the end of this theory it is shown that such topology on the quotient group makes it a topological group.

Topological_Group_ZF_3.thy

This theory studies the topologies on subgroups of a topological group. A couple of nice basic properties are shown, like that the closure of a subgroup is a subgroup, closure of a normal subgroup is normal and, a bit more surprising (to me) property that every locally-compact subgroup of a $T_0$ group is closed.