IsarMathLib 1.28.1: Update to Isabelle2023

Following the Isabelle2023 release I have released an updated version of IsarMathLib. This release does not contain new formalized material, but I have edited two old (from around 2013, with some later additions) theory files contributed by Daniel de la Concepción Sáez so that they can be included in the isarmathlib.org site.

The first theory file is about quotient topologies.

Suppose we have a topology and is a an equivalence relation on . Let be the set of equivalence classes of this relation and be the projection that maps to it’s equivalence class i.e. . Then a natural way to define a topology on is to take . Note that is the strongest topology on in which is continuous.

A slightly more general approach is to start not with an equivalence relation but a surjection , where is any set. Then the collection is a topology on , which might be called the quotient topology in by . Again is the strongest topology on which makes continuous.

These two approaches can be unified by noticing that if we define relation as then is an equivalence relation on and the quotient topology defined by that relation is homeomorphic to the quotient topology in by . So, in a way, all quotient topologies arise from an equivalence relation given by a quotient function.

The second theory added to isarmathlib.org in this release is about group homomorphisms. Results formalized include the fact that endomorphisms of an abelian group form a ring and that any homomorphism between groups and induces an isomorphism between and the image .