Equivalence of algebras

Stream: maths

[Oliver Nash]

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]

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]

Well I can hold off of course.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Oliver Nash]

Yep

[Kevin Buzzard]

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

[Oliver Nash]

Thanks, will do.

[Yury G. Kudryashov]

You should extend ring_equiv copying an extra axiom from alg_hom.

[Oliver Nash]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Oliver Nash]

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

[Oliver Nash]

But I can do that.

[Yury G. Kudryashov]

What did you do?

[Oliver Nash]

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

[Yury G. Kudryashov]

Note that alg_hom includes unnecessary axioms like map_zero'

[Oliver Nash]

Yeah I did notice that.

[Oliver Nash]

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]

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

[Oliver Nash]

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]

leanproject up

[Oliver Nash]

I'm a bit afraid of that command!

[Oliver Nash]

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

[Kenny Lau]

yes

[Oliver Nash]

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

[Oliver Nash]

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

[Kevin Buzzard]

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

[Oliver Nash]

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

[Oliver Nash]

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

[Yury G. Kudryashov]

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]

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.