Zulip Chat Archive

Stream: maths

Topic: Equivalence of algebras


view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip Oliver Nash (May 06 2020 at 19:32):

Well I can hold off of course.

view this post on Zulip 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.

view this post on Zulip Oliver Nash (May 06 2020 at 19:34):

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

view this post on Zulip 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.

view this post on Zulip Oliver Nash (May 06 2020 at 19:34):

Yep

view this post on Zulip Kevin Buzzard (May 06 2020 at 19:34):

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

view this post on Zulip Oliver Nash (May 06 2020 at 19:34):

Thanks, will do.

view this post on Zulip Yury G. Kudryashov (May 06 2020 at 19:35):

You should extend ring_equiv copying an extra axiom from alg_hom.

view this post on Zulip Oliver Nash (May 06 2020 at 19:36):

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

view this post on Zulip Yury G. Kudryashov (May 06 2020 at 19:36):

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

view this post on Zulip 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.

view this post on Zulip Oliver Nash (May 06 2020 at 19:37):

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

view this post on Zulip Oliver Nash (May 06 2020 at 19:37):

But I can do that.

view this post on Zulip Yury G. Kudryashov (May 06 2020 at 19:37):

What did you do?

view this post on Zulip 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 ≃+*

view this post on Zulip Yury G. Kudryashov (May 06 2020 at 19:38):

Note that alg_hom includes unnecessary axioms like map_zero'

view this post on Zulip Oliver Nash (May 06 2020 at 19:38):

Yeah I did notice that.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (May 06 2020 at 21:42):

leanproject up

view this post on Zulip Oliver Nash (May 06 2020 at 21:42):

I'm a bit afraid of that command!

view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 06 2020 at 21:43):

yes

view this post on Zulip Oliver Nash (May 06 2020 at 21:44):

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

view this post on Zulip Oliver Nash (May 06 2020 at 21:44):

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

view this post on Zulip 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.

view this post on Zulip Oliver Nash (May 07 2020 at 13:32):

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

view this post on Zulip Oliver Nash (May 07 2020 at 13:32):

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

view this post on Zulip 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?

view this post on Zulip 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