Documentation

Mathlib.Algebra.HierarchyDesign

Documentation of the algebraic hierarchy #

A library note giving advice on modifying the algebraic hierarchy. (It is not intended as a "tour".) This is ported directly from the Lean3 version, so may refer to files/types that currently only exist in mathlib3.

TODO: Add sections about interactions with topological typeclasses, and order typeclasses.

source
🔸 coverage
def LibraryNote.the_algebraic_hierarchy :
Batteries.Util.LibraryNote

The algebraic hierarchy #

In any theorem proving environment, there are difficult decisions surrounding the design of the "algebraic hierarchy".

There is a danger of exponential explosion in the number of gadgets, especially once interactions between algebraic and order/topological/etc. structures are considered.

In mathlib, we try to avoid this by only introducing new algebraic typeclasses either

  1. when there is "real mathematics" to be done with them, or
  2. when there is a meaningful gain in simplicity by factoring out a common substructure.

(As examples, at this point we don't have Loop, or UnitalMagma, but we do have LieSubmodule and TopologicalField! We also have GroupWithZero, as an exemplar of point 2.)

Generally in mathlib we use the extension mechanism (so CommRing extends Ring) rather than mixins (e.g. with separate Ring and CommMul classes), in part because of the potential blow-up in term sizes described at https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html However there is tension here, as it results in considerable duplication in the API, particularly in the interaction with order structures.

This library note is not intended as a design document justifying and explaining the history of mathlib's algebraic hierarchy! Instead it is intended as a developer's guide, for contributors wanting to extend (either new leaves, or new intermediate classes) the algebraic hierarchy as it exists.

(Ideally we would have both a tour guide to the existing hierarchy, and an account of the design choices. See https://arxiv.org/abs/1910.09336 for an overview of mathlib as a whole, with some attention to the algebraic hierarchy and https://leanprover-community.github.io/mathlib-overview.html for a summary of what is in mathlib today.)

Instances #

When adding a new typeclass Z to the algebraic hierarchy one should attempt to add the following constructions and results, when applicable:

Subobjects #

When a new typeclass Z adds new data fields, you should also create a new SubZ structure with a carrier field.

This can be a lot of work; for now try to closely follow the existing examples (e.g. Submonoid, Subring, Subalgebra). We would very much like to provide some automation here, but a prerequisite will be making all the existing APIs more uniform.

If Z extends Y, then SubZ should usually extend SubY.

When Z adds only new proof fields to an existing structure Y, you should provide instances transferring Z α to Z (SubY α), like Submonoid.toCommMonoid. Typically this is done using the Function.Injective.Z definition mentioned above.

instance SubY.toZ [Z α] : Z (SubY α) :=
  coe_injective.Z coe ...

Morphisms and equivalences #

Category theory #

For many algebraic structures, particularly ones used in representation theory, algebraic geometry, etc., we also define "bundled" versions, which carry category instances.

These bundled versions are usually named by appending Cat, so for example we have AddCommGrpCat as a bundled AddCommGroup, and TopCommRingCat (which bundles together CommRing, TopologicalSpace, and IsTopologicalRing).

These bundled versions have many appealing features:

  • a uniform notation for morphisms X ⟶ Y
  • a uniform notation (and definition) for isomorphisms X ≅ Y
  • a uniform API for subobjects, via the partial order Subobject X
  • interoperability with unbundled structures, via coercions to Type (so if G : AddCommGrpCat, you can treat G as a type, and it automatically has an AddCommGroup instance) and lifting maps AddCommGrpCat.of G, when G is a type with an AddCommGroup instance.

If, for example you do the work of proving that a typeclass Z has a good notion of tensor product, you are strongly encouraged to provide the corresponding MonoidalCategory instance on a bundled version. This ensures that the API for tensor products is complete, and enables use of general machinery. Similarly if you prove universal properties, or adjunctions, you are encouraged to state these using categorical language!

One disadvantage of the bundled approach is that we can only speak of morphisms between objects living in the same type-theoretic universe. In practice this is rarely a problem.

Making a pull request #

With so many moving parts, how do you actually go about changing the algebraic hierarchy?

We're still evolving how to handle this, but the current suggestion is:

  • If you're adding a new "leaf" class, the requirements are lower, and an initial PR can just add whatever is immediately needed.
  • A new "intermediate" class, especially low down in the hierarchy, needs to be careful about leaving gaps.

In a perfect world, there would be a group of simultaneous PRs that basically cover everything! (Or at least an expectation that PRs may not be merged immediately while waiting on other PRs that fill out the API.)

However "perfect is the enemy of good", and it would also be completely reasonable to add a TODO list in the main module doc-string for the new class, briefly listing the parts of the API which still need to be provided. Hopefully this document makes it easy to assemble this list.

Another alternative to a TODO list in the doc-strings is adding Github issues.

Instances For
    source
    🔸 coverage
    def LibraryNote.«reducible_non-instances» :
    Batteries.Util.LibraryNote

    Some definitions that define objects of a class cannot be instances, because they have an explicit argument that does not occur in the conclusion. An example is Preorder.lift that has a function f : α → β as an explicit argument to lift a preorder on β to a preorder on α.

    If these definitions are used to define instances of this class and this class is an argument to some other type-class so that type-class inference will have to unfold these instances to check for definitional equality, then these definitions should be marked @[reducible].

    For example, Preorder.lift is used to define Units.Preorder and PartialOrder.lift is used to define Units.PartialOrder. In some cases it is important that type-class inference can recognize that Units.Preorder and Units.PartialOrder give rise to the same LE instance. For example, you might have another class that takes [LE α] as an argument, and this argument sometimes comes from Units.Preorder and sometimes from Units.PartialOrder. Therefore, Preorder.lift and PartialOrder.lift are marked @[reducible].

    Instances For
      source
      🔸 coverage
      def LibraryNote.implicit_instance_arguments :
      Batteries.Util.LibraryNote

      There are places where typeclass arguments are specified with implicit {} brackets instead of the usual [] brackets. This is done when the instances can be inferred because they are implicit arguments to the type of one of the other arguments. There are several reasons for doing so.

      When they can be inferred from these other arguments, it is faster to use this method than to use type class inference. For example, when writing lemmas about (f : α →+* β), it is faster to specify the fact that α and β are Semirings as {rα : Semiring α} {rβ : Semiring β} rather than the usual [Semiring α] [Semiring β].

      When handling non-canonical instances, it is necessary that the relevant declarations take these instance arguments implicitly, otherwise Lean will refuse to apply them. For example, in measure theory a space X will often come equipped with a canonical base sigma-algebra MeasurableSpace X along with many sub-sigma algebras, also of type MeasurableSpace X. In homological algebra, ModuleCat ℤ appears regularly as the category of abelian groups, but terms A : ModuleCat ℤ come with two (propeq) Module ℤ A instances: one from being ℤ-modules, and one from being abelian groups.

      Instances For
        source
        🔸 coverage
        def LibraryNote.lower_instance_priority :
        Batteries.Util.LibraryNote

        Certain instances always apply during type-class resolution. For example, the instance AddCommGroup.toAddGroup {α} [AddCommGroup α] : AddGroup α applies to all type-class resolution problems of the form AddGroup _, and type-class inference will then do an exhaustive search to find a commutative group. These instances take a long time to fail. Other instances will only apply if the goal has a certain shape. For example Int.instAddGroupInt : AddGroup ℤ or Prod.instAddGroup {α β} [AddGroup α] [AddGroup β] : AddGroup (α × β). Usually these instances will fail quickly, and when they apply, they are almost always the desired instance. For this reason, we want the instances of the second type (that only apply in specific cases) to always have higher priority than the instances of the first type (that always apply). See also mathlib#1561.

        Therefore, if we create an instance that always applies, we set the priority of these instances to 100 (or something similar, which is below the default value of 1000).

        Instances For
          source
          🔸 coverage
          def LibraryNote.instance_argument_order :
          Batteries.Util.LibraryNote

          When type class inference applies an instance, it attempts to solve the sub-goals from left to right (it used to be from right to left in lean 3). For example in

          instance {p : α → Sort*} [∀ x, IsEmpty (p x)] [Nonempty α] : IsEmpty (∀ x, p x)

          we make sure to write [∀ x, IsEmpty (p x)] on the left of [Nonempty α] to avoid an expensive search for Nonempty α when there is no instance for ∀ x, IsEmpty (p x).

          This helps to speed up failing type class searches, for example those triggered by simp lemmas.

          In some situations, we can't reorder type class assumptions because one depends on the other, for example in

          instance {G : Type*} [Group G] [IsKleinFour G] : IsAddKleinFour (Additive G)

          where the Group G instance appears in IsKleinFour G. Future work may be done to improve the type class synthesis order in this situation.

          Instances For
            source
            🔸 coverage
            def LibraryNote.commutative_subobjects :
            Batteries.Util.LibraryNote

            The algebraic hierarchy is designed so that commutativity (e.g., of multiplication) is bundled into the type class, so that we have, for example Group and CommGroup, Ring and CommRing, etc.

            It is often the case that one may desire to work with a commutative subobject inside an ambient noncommutative type. In cases like Subgroup.center or Subring.center, the subobject is always commutative, and in these cases one should simply imbue those subobjects (coerced to Type) with the appropriate Comm* instance. However, in other cases, the commutativity of the subobject may be conditional on commutativity of some other object. For example, Subgroup.closure s is not always commutative, but it is when s is a commutative subset. Likewise, if S : Subgroup G is a commutative subgroup, then S.topologicalClosure is also commutative.

            For such scenarios, users should prefer to use the unbundled IsMulCommutative typeclass, and to provide theorems such as:

            theorem isMulCommutative_closure {G : Type*} [Group G] {k : Set G}
    (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) :
    IsMulCommutative (closure k)

            or even instances such as

            instance Subgroup.instIsMulCommutative_closure {S G : Type*} [Group G] [SetLike S G]
    [MulMemClass S G] (s : S) [IsMulCommutative s] :
    IsMulCommutative (closure (s : Set G))

            and

            instance Subgroup.isMulCommutative_topologicalClosure [T2Space G] (s : Subgroup G)
    [IsMulCommutative s] : IsMulCommutative s.topologicalClosure

            Note that we prefer to name these instances manually because they are occasionally useful as theorems. For example, the proof of the topological closure instance for subgroups above is proved immediately from the one for monoids via: s.toSubmonoid.isMulCommutative_topologicalClosure.

            In practice, we wish to be able to use the library of theorems about (bundled) commutativity for subobjects as well, and so we also provide instances which take as input the unbundled Group G and IsMulCommutative G and produce the bundled CommGroup G. However, to avoid deleterious effects to type class synthesis for bundled commutativity (by forcing Lean to search the entirery of both the bundled and unbundled hierarchies), these instances are only available inside the IsMulCommutative scope and are simultaneously given the very low priority 50.

            Instances For