Zulip Chat Archive

Stream: maths

Topic: bundling ring_equiv


view this post on Zulip Kevin Buzzard (Jul 30 2019 at 19:07):

Currently we have

structure ring_equiv (α β : Type*) [ring α] [ring β] extends α  β :=
(hom : is_ring_hom to_fun)

infix ` r `:25 := ring_equiv

I am on a bundling mission at the minute, and propose changing the definition to

structure ring_equiv (α β : Type*) [ring α] [ring β] extends α  β :=
(map_add' :  x y : α, to_fun (x + y) = to_fun x + to_fun y)
(map_mul' :  x y : α, to_fun (x * y) = to_fun x * to_fun y)

infix ` +* `:25 := ring_equiv

The field changes are so we can move away from is_ring_hom in general. The notation change is to align the notation for ring equivs with ≃* and ≃+ , which are monoid equivs and add_monoid equivs.

Would this change be welcome?

view this post on Zulip Kevin Buzzard (Jul 30 2019 at 19:09):

Oh -- the primes are because to_fun is not the canonical notation -- I am proposing a coe to fun and then defining map_add etc using the coercion notation.

view this post on Zulip Kevin Buzzard (Jul 30 2019 at 19:10):

I have spent some time over the last few weeks trying to imagine a coherent bundled algebraic hierarchy, with subthings, morphisms, equivs all bundled, and this PR suggestion is somehow the sort of thing that comes out of it.

view this post on Zulip Chris Hughes (Jul 30 2019 at 19:17):

This change would be welcome.

view this post on Zulip Floris van Doorn (Jul 30 2019 at 19:27):

Sounds good to me


Last updated: May 12 2021 at 07:17 UTC