Changing domain of a function

Stream: new members

[Xavier Roblot]

Let's say I have a function f : A →+* B and an equality A = C. What is the clean way to get the corresponding function f : C →+* B . I know how to do it by constructing explicitly the ring_hom but it is a bit messy and I was wondering if there is a better way.

I guess I have the same question if I have instead B = D and want to change the range of the function...

[Yaël Dillies]

What are A and C? Types? If so, don't use an equality!

[Yaël Dillies]

Also, how do you know that the equality between A and C preserves ring operations? After all, mul_opposite X = X but they certanly aren't the same ring!

[Riccardo Brasca]

Yes, the idea is that you shouldn't have an equality of types at the beginning. Can you be more explicit?

[Xavier Roblot]

Yes, sorry about that, I was not really clear. In fact A and C are subring of the same ring in my case.

[Yaël Dillies]

Is either of A and C a free variable? If so, you can subst your_equality

[Riccardo Brasca]

If this doesn't work we probably have iso_of_eq or something similar (I will look for this once I am at the computer)

[Riccardo Brasca]

docs#ring_equiv.subring_congr

[Xavier Roblot]

Thanks a lot. I’ll try that!

[Riccardo Brasca]

Hopefully simp is smart enough to make it disappear when you apply it...

[Kevin Buzzard]

A is a term in A : subring R, and a type in f : A ->+* B. Equality of terms is not evil :-) Maybe post a #mwe ? There might be several independent things going on here.