has_coe_t for semilinear_map_class

Stream: general

[Jireh Loreaux]

@Anne Baanen @Frédéric Dupuis : there doesn't seem to be any coercion from an F with an instance of semilinear_map_class F σ M₁ M₂ to M₁ →ₛₗ[σ] M₂. Likewise for linear_map_class and alg_hom_class. I assume this is intentional, and not just an oversight. Right? If it's intentional, what is the reason?

[Anne Baanen]

I don't see any important reason not to add this coercion (except the ratio of Lean time : TODO list length) so please go ahead and add it!

[Eric Wieser]

The danger of adding these coercions is that it becomes very easy to end up with things that aren't simp-normal form; for instance, you'll need a simp lemma that says that the coe : (M₁ →ₛₗ[σ] M₂) → (M₁ →ₛₗ[σ] M₂) induced by this instance is just id

[Eric Wieser]

Does making the instance @[reducible] make this a non-issue? (I don't remember what reducible means on instances)

[Jireh Loreaux]

@Eric Wieser, I can certainly add such a lemma (although I'm not sure how one might actually get it to show up naturally). However, do you realize that we have these coercions all over? And I think this is part of the point of the morphism refactor (of course not the only point). docs#mul_hom.has_coe_t, docs#ring_hom.has_coe_t, docs#continuous_map.has_coe_t, etc. I thought the utility of this is that if f : A →ₐ[R] B, for example, then you can just write f : A →+ B directly to get the add_monoid_hom instead of chaining things together.

[Eric Wieser]

Yes, my concern applies to the pattern as a whole and not the idea of extending it

[Eric Wieser]

The utility here is a false promise right now; as soon as you use one of those coercions, you end up with goals that can only be solved with change (or by knowing the term mode proof already)

[Eric Wieser]

Using your example, I don't think we have any lemmas to solve

example (f : A →ₐ[R] B) (x : A) : (f : A →+ B) x = f x :=

[Eric Wieser]

But also these interact poorly with things like docs#linear_map.range_to_add_submonoid; now we need two versions of the lemma, one for coe and one for to_add_monoid_hom.

[Jireh Loreaux]

So, the first one should be easily fixed right? We just need lemmas like this:

@[simp, norm_cast] lemma add_hom.coe_coe {F M N : Type*} [add_zero_class M] [add_zero_class N]
  [add_monoid_hom_class F M N] (f : F) : ⇑(f : M →+ N)  = f := rfl

and I agree these should exist if we have these coercions. For your second issue, I guess my thinking would be that we just phase out to_add_monoid_hom in favor of these hom class coercions instead. But maybe this is a stupid idea for some reason.

[Eric Wieser]

So, the deeper problem here relates to the commutative diagram between various homs and their range, where you can either go via to_weaker_hom or to_weaker_subobject at each step (eg f.to_ring_hom.srange.to_add_submonoid). Generally speaking, we should have a lemma for each square in this diagram.

The coercions being described in this thread add all the transitive edges to this graph too, which means now we need lemmas that either:

• correspond to each of the transitive squares in the diagram.
• unfold each transitive edge to an arbitrary path through the diagram.

[Jireh Loreaux]

I very much see what you mean, but I'm wondering whether the solution isn't just "more use of hom / subobject classes." I guess what I'm saying is what if that wasn't ring_hom.srange in the sense that it didn't take a ring_hom as an argument, but rather a member of ring_hom_class? As long as the actual data is defined in terms of ⇑f (which it should be) wouldn't this mean that all these would produce the same ring_hom.srange f?

Maybe this actually makes things worse and not better; I have trouble parsing all the effects in my head.

[Eric Wieser]

I think your suggestion for srange would probably work reasonably well, ignoring elaboration pain

[Eric Wieser]

Perhaps I should have given (f.comp g).to_monoid_hom = f.to_monoid_hom.comp g.to_monoid_hom as the troublesome example instead

[Jireh Loreaux]

We don't have norm_cast or simp lemmas like this currently, do we? And you can still prove it with something like ext, refl if necessary, right?

[Jireh Loreaux]

@Eric Wieser, thoughts?

[Eric Wieser]

We do have simp lemmas in some places for this (docs#non_unital_ring_hom.coe_comp_mul_hom for instance)

[Eric Wieser]

Matters are made worse by the fact that we already have coercions defined from ring_hom to monoid_hom (or similar), and these instances may not match the same simp lemmas as the ones that go via monoid_hom_class

[Jireh Loreaux]

Hmm... I'm confused. You gave examples of ↑(g.comp f) = ↑g.comp ↑f where ↑ is the coercion coming from the class instance, but not something like (g.comp f).to_monoid_hom = g.to_monoid_hom.comp f.to_monoid_hom). Searching the docs for "comp to hom" only led me to alg_hom.comp_to_ring_hom which is actually just another ↑ lemma.

I guess my point is: if the to_monoid_hom versions don't exist, then it's because we have essentially never needed them. In that case, I think my argument would be that we don't need the ↑ versions either (I wrote docs#non_unital_ring_hom.coe_comp_mul_hom, so it's totally possible it's not necessary) and we should get rid of them.

As for the existing coercions, I would think we just want to get rid of them because I agree that otherwise we could end up with mismatched simp lemmas.

[Jireh Loreaux]

@Anne Baanen @Yaël Dillies @Frédéric Dupuis , it would be good to have your input on this issue too, since we have all been involved with the morphism refactor. (not sure if there are other people to ping about this, please do if so)

[Yaël Dillies]

/me is still thinking

[Eric Wieser]

If you want one with comp not coe, how about docs#ring_equiv.to_ring_hom_trans ?

[Eric Wieser]

A lot of the hom stuff already doesn't agree or decide upon whether to_foo_hom or a coercion implemented via to_foo_hom is the simp-normal form

[Jireh Loreaux]

Yes, I've noticed this lack of consistency.

[Eric Wieser]

Adding a third option when we already make a mess of picking between the two choices we currently have is what worries me, especially since the third option is now transitive and adds even more options.

[Jireh Loreaux]

I definitely understand your concern. I'm just wondering if we can come up with a solution to have our cake and eat it too.

[Anne Baanen]

In my opinion, the has_coe_t version of the casts are the best option. We have a couple of them right now and they seem to work well enough. Yes, we hadn't standardised on one option before, but I don't see why that means we can't choose the best standard now.

[Anne Baanen]

I've been thinking about dealing with comp in a generic way, with no solution being entirely satisfactory. We could add an extra class lawful_comp (F G : Type*) (GF : out_param Type*) {A B C : out_param Type*} [fun_like F A B] [fun_like G B C] [fun_like GF A C], but it seems finding these instances often gets too complicated. Another attempt was to define a bundled type of composition operators, which seems to work well except you can't really rewrite with ↑(comp₁ g f) = comp₂ ↑g ↑f since comp₂ could be any composition operator.

[Anne Baanen]

Hmm, although we could try assuming inhabited (comp F G) (or unique), and setting comp to be a notation for default...

[Jireh Loreaux]

@Eric Wieser @Yaël Dillies @Anne Baanen it would be nice to make a decision on this. I've started running into issues where I find myself really wanting these coercions. For example, in #16835 I want to compose an element of the character space with a star algebra homomorphism, and return an element of the character space. There is an equiv between the character space and alg_hom so basically I compose them as alg_hom's and then go through the equiv, but first I have to manually finagle each of them to an alg_hom. But since they are both members of an alg_hom_class, if these coercions existed I could just do it with a type ascription. it would look and feel much cleaner. Should we vote on this publicly?

[Anne Baanen]

I haven't changed my opinion, I think a has_coe_t instance for coercing any alg_hom_class to alg_hom is still the way we should go.

[Anne Baanen]

Especially since we recently extended the has_coe_t interface for hom_classes and didn't see any issues there.