bundling ring_equiv

Stream: maths

[Kevin Buzzard]

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]

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]

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]

This change would be welcome.

[Floris van Doorn]

Sounds good to me