## 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