## Stream: maths

### Topic: Equivalence of algebras

#### Oliver Nash (May 06 2020 at 19:27):

Mathlib has R-algebra morphisms but I cannot find a definition for R-algebra equivalences, and I'd like to make use of the concept. Am I missing something, or should I just PR a definition + basic properties?

#### Kevin Buzzard (May 06 2020 at 19:31):

I was about to say "aargh no, all that algebra stuff is built on is_ring_hom which needs to be replaced by ring_hom first", but I see that @Yury G. Kudryashov has refactored!

#### Oliver Nash (May 06 2020 at 19:32):

Well I can hold off of course.

#### Kevin Buzzard (May 06 2020 at 19:33):

No I can't see any reason not to make a PR (@Johan Commelin and @Kenny Lau might want to comment though). Making an "equiv" PR is actually a rather nice kind of PR to make.

#### Oliver Nash (May 06 2020 at 19:34):

OK, I'll go for it and if someone disagrees I can just close the PR.

#### Kevin Buzzard (May 06 2020 at 19:34):

You prove algebra_equiv.id and algebra_equiv.comp, and a few more bits and bobs and it's all over.

Yep

#### Kevin Buzzard (May 06 2020 at 19:34):

You should look to see what is done with e.g. mul_equiv first.

Thanks, will do.

#### Yury G. Kudryashov (May 06 2020 at 19:35):

You should extend ring_equiv copying an extra axiom from alg_hom.

#### Oliver Nash (May 06 2020 at 19:36):

Thanks! I actually have a working local definition and that's what I did.

#### Yury G. Kudryashov (May 06 2020 at 19:36):

OK, then I'll wait till you PR it.

#### Yury G. Kudryashov (May 06 2020 at 19:37):

I wish we had better support for superstructures or some tactic to copy standard equiv theory to a new kind of *_equiv.

#### Oliver Nash (May 06 2020 at 19:37):

Oh wait, sorry that's not what I did.

#### Oliver Nash (May 06 2020 at 19:37):

But I can do that.

What did you do?

#### Oliver Nash (May 06 2020 at 19:37):

set_option old_structure_cmd true
structure algebra.equiv extends A →ₐ[R] A', A ≃ A' -- Probably better to extend ≃+*


#### Yury G. Kudryashov (May 06 2020 at 19:38):

Note that alg_hom includes unnecessary axioms like map_zero'

#### Oliver Nash (May 06 2020 at 19:38):

Yeah I did notice that.

#### Oliver Nash (May 06 2020 at 19:39):

OK I have one other bit of work to finish first and then I'll pick this up and extend ring_equiv as you suggest.

#### Yury G. Kudryashov (May 06 2020 at 19:39):

BTW, other equivs follow naming scheme *_equiv, not *.equiv. So it should be alg_equiv to match alg_hom.

#### Oliver Nash (May 06 2020 at 21:41):

I got unlucky and had to recompile Mathlib (which takes my 2013 Macbook 75 minutes!) so I'll have to wait till tomorrow to pick this up.

#### Kenny Lau (May 06 2020 at 21:42):

leanproject up

#### Oliver Nash (May 06 2020 at 21:42):

I'm a bit afraid of that command!

#### Oliver Nash (May 06 2020 at 21:43):

Does it work when the corresponding branch (master / lean.3.10.0) is still building on GH?

yes

#### Oliver Nash (May 06 2020 at 21:44):

Oh wow; so I could have immediately unblocked myself. Thanks.

#### Oliver Nash (May 06 2020 at 21:44):

Well, I did other productive non-Mathlib things anyway :)

#### Kevin Buzzard (May 06 2020 at 21:50):

I think the oleans which come from the azure server are the ones which were built using the github CI.

#### Oliver Nash (May 07 2020 at 13:32):

https://github.com/leanprover-community/mathlib/pull/2625

#### Oliver Nash (May 07 2020 at 13:32):

And now lunch is over and I must get back to work

#### Yury G. Kudryashov (May 07 2020 at 17:35):

We definitely need a tactic to import lemmas from a substructure while replacing coe_fn instance. I often find out that this or that structure extending equiv lacks a lemma like apply_symm_apply. In the meantime, @Oliver Nash could you please add (some of) the following lemmas to your PR:

• map_add, map_zero, map_mul, map_one, map_neg, map_sub, commutes;
• apply_symm_apply, symm_apply_apply, injective, bijective, surjective;
• coercion to alg_hom with a norm_cast lemma?

#### Oliver Nash (May 07 2020 at 20:36):

Thanks @Yury G. Kudryashov this is excellent feedback which I really appreciate. I will add (hopefully all) of these lemmas + definition, though it might not happen till the weekend.

Last updated: May 18 2021 at 07:19 UTC