# 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_class`

es and didn't see any issues there.

Last updated: Dec 20 2023 at 11:08 UTC