too many FunLikes

Stream: mathlib4

[Kevin Buzzard]

A student got into the following mes:

import Mathlib

example (R A B : Type) [CommRing R] [CommRing A] [Algebra R A]
    (I J : Ideal A) (f : A →ₐ[R] A) (h : Ideal.map (f : A →+* A) I = J) (x : A) :
    x ∈ Ideal.map f I ↔ x ∈ I := by
  /-
  h : Ideal.map (↑f) I = J
  ⊢ x ∈ Ideal.map f I ↔ x ∈ I
  -/
  sorry

Their goal involved Ideal.map ffor f an algebra hom (in fact it was an algebra equiv) and they had some hypothesis which involved Ideal.map (f : A ->+* A) and so rw was failing. Is there some painless way to move from one to the other (here f was a very complex function).

[Ruben Van de Velde]

One might wonder whether there is or should be a simp lemma

[Adam Topaz]

What would such a simp lemma say?

[Adam Topaz]

you can always change: change Ideal.map f I = J at h

[Kevin Buzzard]

The problem with change is that f is huge

[Adam Topaz]

Alternatively we could redefine Ideal.map to have the following type:

def Ideal.map {R : Type u} {S : Type v} [Semiring R] [Semiring S] (f : R → S) (I : Ideal R) : Ideal S

... yes, that's a plain old function.

[Adam Topaz]

then rely on the coercion to functions for all these FunLikes

[Adam Topaz]

Now I'm sure that @Yaël Dillies will tell us why that's a terrible idea.

[Adam Topaz]

we really need some automation that would let us write letMatch Ideal.map $f I = J := \goal to obtain let f := ... in context, so that you can work easily with f. I think @Jireh Loreaux was trying to implement such a thing at some point?

[Timo Carlin-Burns]

Adam Topaz said:

What would such a simp lemma say?

I guess you would need a simp lemma like Ideal.map_toRingHom below for every XXXHomClass :

import Mathlib

@[simp] lemma Ideal.map_toRingHom {R S F : Type*} [Semiring R] [Semiring S] [FunLike F R S]
    [RingHomClass F R S] (f : F) (I : Ideal R) : Ideal.map (f : R →+* S) I = Ideal.map f I := rfl

example (R A : Type) [CommRing R] [CommRing A] [Algebra R A]
    (I J : Ideal A) (f : A →ₐ[R] A) (h : Ideal.map (f : A →+* A) I = J) (x : A) :
    x ∈ Ideal.map f I ↔ x ∈ J := by
  simp at h
  simp [h]

[Adam Topaz]

note that Ideal.map only needs a plain old FunLike.

[Jireh Loreaux]

I was going to work on it, but then @Gareth Ma wanted to do it. He was getting help from @Thomas Murrills, but I think got too busy and it languished. There is a PR #7890, but it's not finished.

[Jireh Loreaux]

I'm a bit busy with other things, but I could hopefully attempt to return to it in a few weeks if no one else does.

[Gareth Ma]

FWIW the PR kinda works, it's just buggy

[Jireh Loreaux]

Gareth, can you find the old thread about it and we can continue discussion of this there? It would be good to know exactly what the bugs are.

[Yaël Dillies]

Adam Topaz said:

Now I'm sure that Yaël Dillies will tell us why that's a terrible idea.

Actually, I don't think it's a bad idea. The current definition of docs#Ideal.map strikes me as a bit weird: It doesn't use an unbundled function nor does it assume f preserves addition and scalar multiplication.

[Gareth Ma]

ya https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Help.20with.20writing.20tactic/near/428201984

[Gareth Ma]

https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Help.20with.20writing.20tactic/near/398919178 you can see the "works" and "fails" here
But at least there's a "work"! :sweat:

[Timo Carlin-Burns]

It looks like Ideal.map use to assume RingHomClass F R S as well, but after the FunLike refactor, the variable assumptions split into FunLike F R S and RingHomClass F R S, and the latter was no longer assumed by Ideal.map definition since it's unused. (Git blame)

[Jireh Loreaux]

Yes, I think we should redefine Ideal.map to take a bare function.

[Adam Topaz]

In any case, adding simp lemmas such as

@[simp] lemma Ideal.map_toRingHom {R S F : Type*} [Semiring R] [Semiring S] [FunLike F R S]
    [RingHomClass F R S] (f : F) (I : Ideal R) : Ideal.map (f : R →+* S) I = Ideal.map f I := rfl

seems like a very bad idea to me.

[Timo Carlin-Burns]

Should docs#Ideal.comap also be changed to take R →+* S instead of F where [RingHomClass F R S]?

[Adam Topaz]

Maybe!

[Adam Topaz]

@Anne Baanen do you have any thoughts about this?

[Yaël Dillies]

The point of hom classes is precisely to avoid taking specific hom types in

[Jireh Loreaux]

Right, Ideal.comap should not change.

[Timo Carlin-Burns]

Couldn't the motivating example at the top of the thread have happened just as easily with comap? We're solving it for map but not for comap

[Adam Topaz]

I disagree. IMO the point of hom classes is to avoid duplication for lemmas about homs. In this case, you're using a hom to construct some object. You can modify Kevin's example as follows:

import Mathlib

example (R A B : Type) [CommRing R] [CommRing A] [Algebra R A]
    (I J : Ideal A) (f : A →ₐ[R] A) (h : Ideal.comap (f : A →+* A) I = J) (x : A) :
    x ∈ Ideal.comap f I ↔ x ∈ J := by
  rw [h] --fails

[Yaël Dillies]

Adam Topaz said:

IMO the point of hom classes is to avoid duplication for lemmas about homs. In this case, you're using a hom to construct some object.

I'll let Anne disagree

[Adam Topaz]

How do you propose to resolve the example above then?

[Adam Topaz]

And if it's okay for Ideal.map to take a function, why is it not okay for Ideal.comap to take an actual ring hom?

[Adam Topaz]

please explain to me the benefits of the current definition of Ideal.comap using RinHomClass

[Yaël Dillies]

The benefit is that you don't need to coerce to ring homs every time, nor do you need to even have a coercion anymore.

[Adam Topaz]

what's the issue with coercing?

[Yaël Dillies]

That you now need to write $n^2$ lemmas about those coercions where $n$ is the depth of your hierarchy

[Adam Topaz]

What lemmas?

[Adam Topaz]

I'm just talking about Ideal.comap.

[Adam Topaz]

The point I'm trying to make is that I see at least two issues with the use of RinHiomClass in the definition of Ideal.comap. One is essentially Kevin's example. The other is that quite often I want to write J.comap _ and get some help from Lean in filling in the blank, but at that point lean has no way of telling the actual type of _, so I have to go in blind.

[Adam Topaz]

I completely understand and agree that these hom classes are useful for avoiding duplication in lemmas like map_add and map_mul, etc., but I honestly don't see any benefit in using them in the definition of things like Ideal.comap.

[Jireh Loreaux]

1. Kevin's example is weird because the hypothesis has an unnecessary coercion.
2. If you don't take a class and instead take an actual hom, then you actually have to coerce your algebra morphism to a ring morphism when you call Ideal.comap

[Adam Topaz]

Re (2), I understand, but why is that a problem?

[Adam Topaz]

Lean will know to expect a ring hom, and it should insert the coercion without any further hints from the user in almost all cases

[Adam Topaz]

import Mathlib

variable (R S F : Type*) [CommRing R] [CommRing S] [FunLike F R S] [RingHomClass F R S]

def Ideal.comap' {R S : Type*} [CommRing R] [CommRing S]
    (I : Ideal S) (f : R →+* S) : Ideal R := sorry

example (I : Ideal S) (f : F) : Ideal R := I.comap' f

[Yaël Dillies]

Yes so the idea was to get rid of that coercion F → R →+* S in the presence of RingHomClass F R S because this has bad performance

[Timo Carlin-Burns]

For what it's worth, from a loogle search, we are not consistent on this either way. e.g. docs#Subsemigroup.comap uses bundled homs

[Jireh Loreaux]

That's correct, but it's because we never got around to finishing it.

[Adam Topaz]

Is it not possible to solve such performance issues with unification hints?

[Jireh Loreaux]

Adam, there are a few issues that can arise, including having multiple of these FunLike coercions. This can be a royal pain because If f : A →ₐ[R] A, then we have no rewrite lemmas that allow you change ((f : A →+* A) : A →* A) into (f : A →* A), and indeed, having such lemmas would lead to the n ^ 2 problem Yaël mentioned.

[Jireh Loreaux]

Mario has told me that using unification hints is bad. I think the idea is that if you need a unification hint, then there's something about unification that should be improved, but maybe I've misunderstood that point.

[Adam Topaz]

Ok, I still don't see how this $n^2$ issue plays any role for the very specific example of Ideal.comap.

[Jireh Loreaux]

And I think the performance issue is more closely linked to the need to repeatedly bundle into a new morphism. (but maybe I'm wrong here.)

[Adam Topaz]

Jireh Loreaux said:

And I think the performance issue is more closely linked to the need to repeatedly bundle into a new morphism. (but maybe I'm wrong here.)

Wouldn't this bundling happen precisely once?

[Jireh Loreaux]

Once every time you call Ideal.comap, but like I said, I may be misdiagnosing here.

[Adam Topaz]

Maybe it's just me, but I think examples like this are really bad:

import Mathlib

example (R A B : Type) [CommRing R] [CommRing A] [Algebra R A]
    (I J : Ideal A) (f : A →ₐ[R] A) (h : Ideal.comap (f : A →+* A) I = J) (x : A) :
    x ∈ Ideal.comap f I ↔ x ∈ J := by
  rw [h] --fails

[Jireh Loreaux]

Again, that's just weird. Why is there a coercion in h?

[Adam Topaz]

These clearly show up in nature, as Kevin pointed out above.

[Jireh Loreaux]

But should it have? I mean, how did this h show up naturally? I'm not saying it couldn't, only that I don't understand yet how.

[Adam Topaz]

It's not unreasonable for such issues to show up. For example what if you're using morphisms in RingCat. It's not like we can generalize the category of rings using RingCatHom!

[Adam Topaz]

Maybe @Kevin Buzzard can tell us how his student wound up with such a situation.

[Jireh Loreaux]

I don't hear the music here. How does using morphisms in RingCat cause this to arise naturally?

[Jireh Loreaux]

I may have an idea for how to deal with these issues, but I haven't yet fleshed it out enough to know.

[Timo Carlin-Burns]

Due to the missing n^2 simp lemmas that Yaël's talking about, I think we can end up with a very similar issue to Kevin's if we switch Ideal.comap to use bundled homs:

import Mathlib

def Ideal.comap' {R S : Type*} [Semiring R] [Semiring S]
    (f : R →+* S) (I : Ideal S) : Ideal R := sorry

-- Adaptation of Kevin's example:
example {R A F : Type} [CommRing R] [CommRing A] [Algebra R A] [FunLike F A A] [AlgHomClass F R A A]
    (I J : Ideal A) (f : F) (h : Ideal.comap' ((f : A →ₐ[R] A) : A →+* A) I = J) (x : A) :
    x ∈ Ideal.comap' f I ↔ x ∈ J := by
  rw [h] --fails

-- Ideally this would be solved by simp:
example {R A B F : Type*} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
    [FunLike F A B] [AlgHomClass F R A B] (I : Ideal B) (f : F) :
    I.comap' ((f : A →ₐ[R] B) : A →+* B) = I.comap' f := by
  simp -- fails because we don't have those n^2 simp lemmas

[Adam Topaz]

okay, yes, that's a good example.

[Adam Topaz]

But the same issues would arise even if we don't rededefine comap.

[Jireh Loreaux]

Eric Wieser was (is?) not a fan of these FunLike class-to-morphism coercions for this reason.

[Adam Topaz]

And if you don't believe that examples such as Kevin arise in nature, then I hope you also don't believe that such an example would show up in nature.

[Adam Topaz]

Anyway, in case it's not clear, I have a love/hate relationship with these hom classes :-/

[Adam Topaz]

I'm perfectly happy to use erw [h] in the first case and rfl in the second case.

[Jireh Loreaux]

well, I only agree these won't show up in nature if we're not making defs like Ideal.comap' which automatically include a coercion.

[Timo Carlin-Burns]

Adam Topaz said:

And if it's okay for Ideal.map to take a function, why is it not okay for Ideal.comap to take an actual ring hom?

It seems like the answer here is because we do have simp lemmas for (⇑(↑f : XXXHom A B) : A → B) = (⇑f : A → B) where f : F and [XXXHomClass F A B], e.g. docs#RingHom.coe_coe

[Jireh Loreaux]

Yes, once you go all the way down to functions, everything is fine. My current idea is to try to encode this coe_coe theorem as a class in a suitable way, so that we can get the $n^2$ lemmas as a single one for each morphism class (and maybe also allow for deleting the ↑ in the hypothesis in Kevin's example (with an additional lemma).

[Kevin Buzzard]

I can't tell you how it happened because a student just put their laptop in front of me and said "why is this rewrite with a really long f failing when it looks syntactically the same?" And it took me a long time to spot the coercion. Maybe the student did something silly, I don't know. I felt like it could plausibly happen but my real question was whether something like norm_cast or whatever could fix it

[Jireh Loreaux]

In case it wasn't answered clearly above, no, norm_cast can't fix it.

[Adam Topaz]

erw [h] might work

[Adam Topaz]

Why can't we just write a metaprogram to generate all $n^2$ lemmas and call it a day?

[Jireh Loreaux]

No, because they may not even be declared at the time you would need to run the metaprogram.

[Adam Topaz]

or just write some tactic to normalize such coercions of coercions.

[Adam Topaz]

Jireh Loreaux said:

No, because they may not even be declared at the time you would need to run the metaprogram.

I'm envisioning generating additional lemmas after each hom class is declared.

[Jireh Loreaux]

But you don't have access to all the other hom classes you might need.

[Adam Topaz]

only the ones downstream of the class that was just defined, no?

[Adam Topaz]

Adam Topaz said:

or just write some tactic to normalize such coercions of coercions.

This is probably easier TBH

[Adam Topaz]

shoot, we can even make it a simproc :)

[Jireh Loreaux]

no (re: downstream), for instance, whenStarAlgHomClass is defined, you don't have access to ContinuousMapClass but for certain types, having the former means you have the latter.

[Jireh Loreaux]

(update: I couldn't make my idea work)

[Eric Wieser]

Jireh Loreaux said:

Eric Wieser was (is?) not a fan of these FunLike class-to-morphism coercions for this reason.

Indeed; these coercions are a pain because they let you pick any sequence of points through a connected graph between AlgHom and (say) AddHom , and we have pretty much no lemmas that let you move between those paths.

[Eric Wieser]

The old strategy of going one step at a time gave you an arbitrary path, but it was easy to rewrite by commuting one diamond at a time

[Eric Wieser]

I think to make def foo [HomClass _ _ F] (f : F) viable, every such definition needs a lemma theorem foo_coe (f : F) : foo (f : Hom) = foo f, and we also don't have those lemmas

[Eric Wieser]

I think the most compelling reason for why comap should take a RingHom and not a RingHomClass is that otherwise you can't state comap_comp.

[Eric Wieser]

Or worse, you have to state it over again for every morphism type

[Eric Wieser]

Adam Topaz said:

I disagree. IMO the point of hom classes is to avoid duplication for lemmas about homs.

I completely agree with this. The morphism classes are awesome for theorems using map_foo, but I think that more often than not, they are footguns when they appear in the signature of a definition.

[Timo Carlin-Burns]

Yaël Dillies said:

That you now need to write $n^2$ lemmas about those coercions where $n$ is the depth of your hierarchy

I'm realizing that I've been overestimating this $O(n^2)$ figure. I'm pretty sure $n < 10$ in the case of the morphism hierarchy because we only need new morphism types for new operators, not for new properties. Furthermore, I think we already have $O(n^2)$ code size anyway. Any class hierarchy of depth $n$ that has at least one concrete instance of each class will take at least $O(n^2)$ lines of code to write because defining each concrete instance at height $n$ requires providing values for its $O(n)$ properties.

[Mario Carneiro]

that has at least one concrete instance of each class

honestly I would not be surprised if this assumption is false in mathlib

[Jireh Loreaux]

Eric Wieser said:

I think the most compelling reason for why comap should take a RingHom and not a RingHomClass is that otherwise you can't state comap_comp.

IMO, this just highlights a long-standing issue with the morphsim-class hierarchy, which is that it is incapable of handling composition.

[Johan Commelin]

Maybe $\circ$ should be a macro...

[Moritz Doll]

There is a possible solution, but it hasn't been tested on larger scale : https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Bundled.20sets.2Ffunctions.20with.20even.20more.20classes/near/421284443

[Jireh Loreaux]

Johan Commelin said:

Maybe $\circ$ should be a macro...

I'm sure Core would love that idea :laughing:

But anyway, it wouldn't really solve the problem. I'm not saying the issue is that we have different composition defs for each kind of bundled morphism (although it would be nice if they were unified), but rather that we have no way to compose (f : F) and (g : G) when the types have FunLike instances where the domain and codomain match.

[Kevin Buzzard]

I was thinking of PRing ∘ₐ to go with ∘ₗ by the way -- I had a bunch of students working on Hopf algebras and I think it slightly has the edge over .comp in terms of readability

[Eric Wieser]

I think that would be unobjectionable

[Jireh Loreaux]

Should we define a notation class for ∘ₘ? (the ₘ is for "morphism" but it could be something else). Then we can just have a single notation for morphism composition?

[Robert Maxton]

Jireh Loreaux said:

Should we define a notation class for ∘ₘ? (the ₘ is for "morphism" but it could be something else). Then we can just have a single notation for morphism composition?

I would support this.

[Yury G. Kudryashov]

Should we have a generic FunLike.comp?

[Jireh Loreaux]

The issue with that is that right now we can't, see my post above. We could define a notation class, for which we could provide individual instances though.

[Yury G. Kudryashov]

I meant something like

class DFunLike.Comp {α β γ : Type*} (F G : Type*) (H : outParam Type*) [FunLike F β γ] [FunLike G α β] [FunLike H α γ] where
  comp (f : F) (g : G) : H
  comp_apply (f : F) (g : G) (x : α) : comp f g x = f (g x)

[Jireh Loreaux]

I was under the impression that @Anne Baanen had tried this a while ago but that Lean continually had elaboration problems arising from too many outParams.

[Yury G. Kudryashov]

Was it in Lean 3 or Lean 4?

[Jireh Loreaux]

Both, I believe.

[Anne Baanen]

If I recall correctly, the problem starts more specifically when you add a generic id function too. Then comp id f would not elaborate because it doesn't know what ids type is supposed to be. I guess we can make id take the intended type as parameter but I'm not sure that we should prefer id (RingHom R R) over RingHom.id R.

[Anne Baanen]

And similarly for EquivLikes symm and trans, I couldn't find a comfortable way of assigning which parameters were in and which were out.