Mathlib's morphism hierarchy

Stream: mathlib4

[Jireh Loreaux]

The following is the result of a discussion among the maintainers and reviewers a few months ago, which I am only now managing to disseminate publicly.

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.

3. 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 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).

[Yaël Dillies]

Note that I have #21031 open which does all of 1, 2 and 3 together (but is WIP). I would greatly appreciate help on it!

[Jireh Loreaux]

I highly recommend splitting them. That's seems like it would be nearly impossible to review.

[Yaël Dillies]

My goal is to make sure #21031 passes CI doing all of them, then to split PRs off

[Jireh Loreaux]

I think it shouldn't be necessary to do it that way though? It should be much easier to do this in a distributed fashion, especially because there are really three separate concerns.

[Yaël Dillies]

The reason why I am doing it this way around is that it lets me automatically find which definitions need to be updated in step 1

[Jireh Loreaux]

Can't we just have a metaprogram to find those? If Loogle let us filter to include only definitions, it would even be possible to use that.

[Jireh Loreaux]

I've createe the tracking issue #31365

[Kenny Lau]

Jireh Loreaux said:

Can't we just have a metaprogram to find those? If Loogle let us filter to include only definitions, it would even be possible to use that.

Indeed, that's what Breitner and I figured out:

• ⊢ RingHomClass _ _ _ → (_ : Type)

This finds all of the definitions using RingHomClass.

[Kenny Lau]

now 5 of these are actually good (tho 2 of these 5 are coercions which will be removed in step 3), so the 8 remaining ones are bad

[Kenny Lau]

And then "Class", ⊢ FunLike _ _ _ → Prop reveals 91 hom classes

[Kenny Lau]

if each hom class has 10 definitions then we'll have 910 definitions, and if we refactor one definition a day then we'll be done in 3 years!

[Kenny Lau]

Also, should we publicise this somewhere on the mathlib website? I think it would be helpful to have just a place to store our consensus.

[Jireh Loreaux]

I think the rule should be specified somewhere, yes, but I would recommend that it appears in the FunLike documentation in Mathlib itself.

[Jireh Loreaux]

For now I think the tracking issue is fine.

[Patrick Massot]

If this story changes significantly then it would be nice to make sure Mathematics in Lean still says the correct thing. People shouldn’t hesitate to ping me or Jeremy about this if needed.

[Antoine Chambert-Loir]

A related question: should morphism types depend on the validity of axioms on the types they act on, or just on the existence of laws?
For example, should docs#RingHom be defined for docs#NonAssocSemiring, as it is now, or shouldn't it be defined whenever we have docs#Add, docs#Zero, docs#Mul and docs#One?

[Aaron Liu]

Is it interesting for types with zero one add mul that aren't nonassocsemirings?

[Aaron Liu]

if it isn't, then we're just making the expression bigger

[Yaël Dillies]

Something that is coming up in my PR #28141: When we have four hom classes A B C D such that A -> B -> D and A -> C -> D are coercions, should we have any lemma about the composition A -> D?

[Yaël Dillies]

@Andrew Yang is arguing that "yes" on the basis of discoverability. I personally think that the only people that care are experts for whom discoverability is not a concern. Is this a problem that should be solved by a tactic?

[Andrew Yang]

My claim is that I don't want to remember implementation details such as the preferred path of A to D is A -> B -> D and not A -> C -> D and not A -> D. I think this is still a cognitive cost for expert users and I would happily accept having more lemmas in mathlib as a trade off.