IsarMathLib 1.29.0: Modules and vector spaces

This release adds definitions and basic facts about modules and vector spaces defined as ring (or field) actions on abelian groups. I also edited two theory files contributed earlier by Daniel de la Concepción Sáez (Ring_ZF_2 and Ring_ZF_3) so that they are now included at the isarmathlib.org site.

What are ring actions?

Let be an abelian group. We know that endomorphisms (i.e. homomorphisms ) of such a group form a ring. The additive operation of this ring is the pointwise addition lifted from the group operation and the composition of endomorphisms is the multiplicative operation of the ring. Now take another ring . A ring homomorphism is called a ring action on the group . Turns out when we define scalar multiplication as , for then such action defines a module and vice versa – every module can be thought of as a ring action. So this provides a nice and concise definition of what a module is. If the ring of scalars is actually a field, we get a vector space the same way.

Comparison with Lean

A couple of weeks ago Tim Gowers posted on Twitter (or whatever it is called now) an amusing characterization of bijections as functions that preserve complements. Alex Kontorovich responded with a Lean verification script certifying that characterization. Lawrence Paulson quoted the Lean verification script on his Machine Logic blog, adding the corresponding Isabelle/HOL proof. In this release I have added an Isabelle/ZF proof of this to IsarMathLib as another comparison of the syntax and proving style of various formal proof languages. This adds to the comparison of Isabelle/ZF with Mizar and Metamath that I wrote about before.

Tags: formalized mathematics, Isabelle/ZF, IsarMathLib, IsarMathLib releases, math, mathematics