Zulip Chat Archive

Stream: general

Topic: is_group_hom field name


view this post on Zulip Kevin Buzzard (Mar 18 2019 at 21:02):

https://github.com/leanprover-community/mathlib/blob/e8bdc7fc14c6d56d4040892d16929f310e9d03d5/src/algebra/group.lean#L627

says TODO rename fields of is_group_hom: mul ↝ map_mul?. Hey, cool squiggly arrow Scott. @Chris Hughes @Mario Carneiro that looks like a sensible change to me. Would a PR making the change be welcomed?

class is_ring_hom {α : Type u} {β : Type v} [ring α] [ring β] (f : α  β) : Prop :=
(map_one : f 1 = 1)
(map_mul :  {x y}, f (x * y) = f x * f y)
(map_add :  {x y}, f (x + y) = f x + f y)
class is_monoid_hom [monoid α] [monoid β] (f : α  β) : Prop :=
(map_one : f 1 = 1)
(map_mul :  {x y}, f (x * y) = f x * f y)

class is_add_monoid_hom [add_monoid α] [add_monoid β] (f : α  β) : Prop :=
(map_zero : f 0 = 0)
(map_add :  {x y}, f (x + y) = f x + f y)

but

class is_group_hom [group α] [group β] (f : α  β) : Prop :=
(mul :  a b : α, f (a * b) = f a * f b)

view this post on Zulip Patrick Massot (Mar 18 2019 at 21:22):

Did you study applications of these axioms? Does it read weird? I guess using bundled maps everywhere would make clearer here...

view this post on Zulip Chris Hughes (Mar 19 2019 at 14:20):

I would accept that PR.


Last updated: May 12 2021 at 04:19 UTC