Zulip Chat Archive

Stream: general

Topic: has_coe_t for semilinear_map_class

Jireh Loreaux (Aug 09 2022 at 15:06):

@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 (Aug 09 2022 at 19:43):

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 (Aug 09 2022 at 21:58):

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 (Aug 09 2022 at 21:58):

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

Jireh Loreaux (Aug 10 2022 at 00:30):

@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 (Aug 10 2022 at 00:32):

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

Eric Wieser (Aug 10 2022 at 00:34):

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 (Aug 10 2022 at 00:37):

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 (Aug 10 2022 at 00:40):

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 (Aug 10 2022 at 01:22):

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 (Aug 10 2022 at 11:45):

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 (Aug 10 2022 at 21:39):

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 (Aug 10 2022 at 23:07):

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

Eric Wieser (Aug 10 2022 at 23:09):

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 (Aug 11 2022 at 01:39):

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 (Aug 15 2022 at 18:32):

@Eric Wieser, thoughts?

Eric Wieser (Aug 15 2022 at 22:11):

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

Eric Wieser (Aug 15 2022 at 22:11):

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 (Aug 16 2022 at 16:36):

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 (Aug 16 2022 at 16:39):

@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 (Aug 16 2022 at 16:40):

/me is still thinking

Eric Wieser (Aug 16 2022 at 16:43):

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

Eric Wieser (Aug 16 2022 at 16:44):

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 (Aug 16 2022 at 16:46):

Yes, I've noticed this lack of consistency.

Eric Wieser (Aug 16 2022 at 16:58):

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 (Aug 16 2022 at 17:04):

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 (Aug 17 2022 at 07:15):

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 (Aug 17 2022 at 07:21):

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 (Aug 17 2022 at 07:22):

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

Jireh Loreaux (Oct 09 2022 at 02:43):

@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 (Oct 09 2022 at 14:30):

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 (Oct 09 2022 at 14:31):

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

Last updated: Aug 03 2023 at 10:10 UTC