# Zulip Chat Archive

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