Stream: maths

Topic: bundling ring_equiv

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?

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.

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.

Chris Hughes (Jul 30 2019 at 19:17):

This change would be welcome.

Floris van Doorn (Jul 30 2019 at 19:27):

Sounds good to me

Last updated: May 12 2021 at 07:17 UTC