algebra injective surjective

Stream: general

[Johan Commelin]

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.)

[Johan Commelin]

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

[Mario Carneiro]

Why not put it in algebra.ring?

[Mario Carneiro]

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

[Johan Commelin]

Ok

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

(with stronger assumptions).

[Johan Commelin]

#2638