Zulip Chat Archive

Stream: general

Topic: algebra injective surjective


view this post on Zulip Johan Commelin (May 09 2020 at 09:54):

What would be a good filename for a file that contains all variations of

def comm_ring_of_injective (f : α'  β) (inj : injective f)
  (zero : f 0 = 0) (one : f 1 = 1) (add :  {x y}, f (x + y) = f x + f y)
  (mul :  {x y}, f (x * y) = f x * f y) (neg :  {x}, f (-x) = - f x) :
  comm_ring α' :=
begin
  refine_struct { ..has_zero α', ..has_one α', ..has_add α', ..has_mul α', ..has_neg α' },
  all_goals { intros, apply inj,
    repeat { erw zero <|> erw one <|> erw add <|> erw mul <|> erw neg },
    try {simp [mul_assoc, mul_add, add_mul] } },
  rw add_comm,
  rw mul_comm
end

(There is also version for surjective f, and then versions for monoid, comm_monoid, group, comm_group, semiring, comm_semiring, ring, and comm_ring. So in total there will be 12 definitions.)

view this post on Zulip Johan Commelin (May 09 2020 at 09:55):

Or should these just be lumped into algebra.basic (which doesn't exist)?

view this post on Zulip Mario Carneiro (May 09 2020 at 09:58):

Why not put it in algebra.ring?

view this post on Zulip Mario Carneiro (May 09 2020 at 09:58):

the first 4 go in algebra.group and the second 4 go in algebra.ring

view this post on Zulip Johan Commelin (May 09 2020 at 09:59):

Ok

view this post on Zulip Yury G. Kudryashov (May 09 2020 at 10:21):

Do you have some [...] in variables? I guess [comm_ring β] [has_zero α'] [has_one α'] [has_mul α'] [has_neg α'] [has_add α']?

view this post on Zulip Yury G. Kudryashov (May 09 2020 at 10:22):

Note that we have something similar with data.equiv.transfer_instance.

view this post on Zulip Yury G. Kudryashov (May 09 2020 at 10:23):

(with stronger assumptions).

view this post on Zulip Johan Commelin (May 09 2020 at 12:11):

#2638


Last updated: May 10 2021 at 00:31 UTC