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
≃+ , 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