Fixing Mathlib's morphism hierarchy

Several years ago, Anne Baanen introduced the docs#FunLike class and the associated classes throughout the morphism hierarchy. When this was instituted, the guidelines indicated that for each morphism type FooHom, there should be an associated morphism class FooHomClass. Moreover, it was recommend to add a coercion from a type F satisfying FooHomClass to FooHom. These are still present throughout the library. More recently, we have tried to separate the morphism classes into distinct pieces according to domain (e.g., we don't have ContinuousMonoidHomClass but only ContinuousMapClass and MonoidHomClass), but the coercions have mostly remained in place.

Unfortunately, these coercions have caused tremendous headaches. To start, Lean often has a hard time inferring all the types involved, so one often has to use type ascriptions to specify. This is inconvenient at best. Secondly, since morphisms are instances of their morphism classes, these coercions can be applied to the morphisms themselves (i.e., you can coerce a RingHom to a RingHom, but f and ↑f are not reducibly defeq). This is a bit strange, but in and of itself it wouldn't necessarily cause problems.

Another issue is that we (and I have certainly been guilty of this before I saw the light) have implemented definitions which take a term of a morphism class (rather than a morphism itself) as a parameter. At first, this seems appealing, but the problem is that doing doesn't really create a single definition, but in some sense it is a definition schema, with one new definition for each instance of the morphism class. For example, since docs#AlgHom is an instance of docs#RingHomClass, and since docs#RingHom.ker takes a term of a RingHomClass as an argument, if f : A →ₐ[R] B is an algebra homomorphism we have both RingHom.ker f and RingHom.ker (↑f : A →+* B), and these are not trivially equal. Thus we would need additional API to go between them. So, we should restrict definitions to explicit morphisms, instead of morphism classes in order to avoid proliferating definitions.

Therefore, given a definition Bar that takes FooHom as an argument, a theorem whose statement involves Bar should only ever be written for FooHoms and never FooHomClasses. Indeed in the latter case, the statement would require the coercion from the morphism class to the morphism, thereby making it less general.

Now, these coercions are not all bad, as they can be useful in proofs. A good example is the proof of docs#AlgEquiv.spectrum_eq. The statement says that a term φ of an AlgEquivClass preserves the spectrum, i.e., spectrum R (φ a) = spectrum R a. This statement does not involve a coercion to docs#AlgEquiv, but only the coercion for φ to a function (which is fine). However, the natural proof is to use docs#AlgHom.spectrum_apply_subset to φ (with a) and φ.symm (with φ a). But since φ is an abstract AlgEquiv, not a specific one, we don't have access to φ.symm, but we can coerce φ to an AlgEquiv in the proof and use that instead.

So, there are four things we need to do as a community to address these problems in Mathlib's morphism hierarchy:

• 0. Don't create any new definitions which take a term of a morphism class as an argument!

• 1. Refactor existing definitions like docs#RingHom.ker, docs#LinearMap.range, etc. so that they take an explicit morphism as an argument, not a morphism class.

• 2. Standardize the naming scheme for the declarations that implement the morphism class to morphism coercions. The standardized name should be FooHom.ofClass, which has several benefits:

  • the name is easy to remember and guess
  • it matches the existing names we have for the corresponding declarations for subobjects
  • when Lean expects a FooHom, you can write .ofClass f.

  The following list of classes is almost certainly not exhaustive:

  • LinearMap, SemilinearMap: #43368, #43376
  • StarAlgHomClass, StarAlgEquivClass, NonUnitalStarAlgHom: #43367
  • Order{Hom,Iso}Class: #43367

• 4. Remove the coercion attribute from these FooHom.ofClass declarations, but keep the definitions themselves. it's important that the renaming occurs before removing the attribute to minimize churn and effort at that step. There are already existing PRs trying to do this, but they have been stymied because the other things in this list should happen first. Note(Yael): I believe this should in fact be the first step.

  • RingHom
  • RingEquiv: #21031
  • AlgHom
  • AlgEquiv: #37827
  • LinearMap
  • LinearEquiv: #37944
  • StarRingHom: #43367
  • StarRingEquiv: #43367
  • NonUnitalStarAlgHom, StarAlgHom: #43370
  • StarAlgEquiv: #43370

Note that (1) and (2) above are independent and can happen in parallel, but (3) will be easiest only after (1) and (2) are complete.

The purpose of removing the coercion attribute from FooHom.ofClass is two-fold: (a) it's not that useful anyway since we often have to provide a type ascription, and (b) keeping it around makes it more likely that we silently break the rules specified above (because Lean inserted a coercion and the user and reviewer didn't notice).

Zulip discussion: #mathlib4 > Mathlib's morphism hierarchy

Start by reviewing the checklist and the named declarations, including RingHom.ker and LinearMap.range, along with the linked issues and Zulip discussion. Map the existing morphism-class definitions and FooHom coercion declarations before selecting a focused subset; done means explicit morphism arguments, standardized FooHom.ofClass names, and the planned coercion-attribute changes are completed without leaving the hierarchy inconsistent.