# Zulip Chat Archive

## Stream: general

### Topic: ring of injective

#### Johan Commelin (Jun 14 2019 at 08:36):

How do I prove this in a one-liner:

section open function variables {α : Type*} [has_zero α] [has_one α] [has_add α] [has_mul α] [has_neg α] variables {β : Type*} [comm_ring β] 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 {sorry} end end

#### Johan Commelin (Jun 14 2019 at 09:00):

I was hoping that `all_goals { intros, apply inj, simp [zero, one, mul, add, neg] },`

would close most of the goals. But it doesn't...

#### Kevin Buzzard (Jun 14 2019 at 09:04):

I guess we have some instance that says that a subgroup of a group is a group. Maybe there is some analogous instance that a subring of a ring is a ring. So you could just use this instance and then `transfer`

the structure over to alpha via the canonical bijection.

#### Johan Commelin (Jun 14 2019 at 09:13):

I was hoping there would be a 1-line tactic proof that works with the current state of mathlib... `transfer`

doesn't currently work.

#### Kevin Buzzard (Jun 14 2019 at 09:14):

Oh well, stick it on the list at https://github.com/leanprover-community/mathlib/issues/408

#### Johan Commelin (Jun 14 2019 at 15:38):

@Kenny Lau How would you prove this?

#### Kenny Lau (Jun 14 2019 at 16:12):

lemme see...

#### Kenny Lau (Jun 14 2019 at 16:41):

I can't prove it. It's because of `+`

being elaborated differently in the two different contexts.

#### Johan Commelin (Jun 14 2019 at 17:04):

Huh? This should be provable, right?

#### Kenny Lau (Jun 14 2019 at 17:07):

like I can't prove it using tactics

#### Johan Commelin (Jun 14 2019 at 17:14):

Any proof is fine... but I expected/hoped that a tactic proof would be way shorter than a term-mode proof

#### Kenny Lau (Jun 14 2019 at 17:14):

as in I can't prove it using a few lines

#### Johan Commelin (Jun 14 2019 at 17:16):

What exactly is the elaboration issue?

#### Kenny Lau (Jun 14 2019 at 17:21):

in `add`

, the `+`

is `@has_add.add \a _inst_3`

or something like that

#### Kenny Lau (Jun 14 2019 at 17:21):

but in the goals it is `@has_add.add \a (semigroup.to_has_add ...)`

etc

#### Johan Commelin (Jun 14 2019 at 17:25):

Hmm, that's sad...

#### Johan Commelin (Jun 14 2019 at 17:26):

I also need the dual version, with a surjective map...

#### Johan Commelin (Jun 14 2019 at 17:26):

I guess I will just manually proof all the goals

#### Andrew Ashworth (Jun 14 2019 at 17:39):

I'm just now sort of getting an inkling of why everyone wants a beefed up `transfer`

, since I rarely deal in very abstract types. But I'm unsure of why people think a 1-line proof is possible. For any map between two types equipped with a ring instance you will always have to prove that it is a ring homomorphism, right? Isn't isomorphism in the context of rings an equivalence relation, so you could use the same machinery to reason about them? (sorry if this observation sounds incredibly stupid to those who have spent much more time thinking about this sort of thing)

#### Kevin Buzzard (Jun 14 2019 at 17:42):

Mathematicians look at the question and cannot see what the issue is.

#### Kevin Buzzard (Jun 14 2019 at 17:43):

alpha is a subset of beta closed under all the operations and it will inherit all of the axioms automatically -- of course it's a ring. What frustrates us is that apparently this is not obvious to computer scientists.

#### Kevin Buzzard (Jun 14 2019 at 17:44):

Johan's assumptions identify alpha with a subtype of beta in a way which preserves everything of interest, so whatever is there left to check?

#### Kevin Buzzard (Jun 14 2019 at 17:45):

Mathematicians have a zero-line proof that alpha is a ring. In a maths lecture you would just deduce it immediately.

#### Kevin Buzzard (Jun 14 2019 at 17:47):

For example `f (x + y) = f x + f y`

and injectivity of `f`

immediately imply associativity of alpha's + because we imagine alpha as literally being a subset of beta with the induced +.

#### Johan Commelin (Jun 14 2019 at 17:55):

Here is the one-line maths proof:

"All the data is there, and `f`

is structure preserving. The ring axioms are universal formulas in the language of rings. Since `f`

is injective this means we are done."

#### Johan Commelin (Jun 14 2019 at 17:56):

The Lean proof should be

all_goals { intros, apply inj, simp [*] }

#### Johan Commelin (Jun 14 2019 at 18:21):

@Kenny Lau `erw`

helps. This is what I've got for the surjective variant:

def comm_ring_of_surjective (f : β → α') (sur : surjective 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 { try { intro a, rcases sur a with ⟨a, rfl⟩ }, try { intro b, rcases sur b with ⟨b, rfl⟩ }, try { intro c, rcases sur c with ⟨c, rfl⟩ }, repeat { erw ← zero <|> erw ← one <|> erw ← add <|> erw ← mul <|> erw ← neg }, try {simp [mul_assoc, mul_add, add_mul] } }, rw mul_comm, end

#### Kenny Lau (Jun 14 2019 at 19:19):

so we should have `esimp`

#### Reid Barton (Jun 14 2019 at 19:24):

Sounds eslow

#### Koundinya Vajjha (Jun 14 2019 at 19:31):

I never could understand how `erw`

is different from `rw`

.

#### Kenny Lau (Jun 14 2019 at 20:51):

import tactic.interactive section open function variables {α : Type*} [has_zero α] [has_one α] [has_add α] [has_mul α] [has_neg α] variables {β : Type*} [comm_ring β] 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 }, simp [mul_assoc, mul_add, add_mul] }, rw mul_comm end end

#### Johan Commelin (Jun 14 2019 at 20:54):

Yep, I also found that one.

#### Johan Commelin (Jun 14 2019 at 20:54):

It's sad that it seems a bit slow...

#### Johan Commelin (Jun 14 2019 at 20:54):

But it works (-;

#### Kenny Lau (Jun 14 2019 at 20:58):

import tactic.interactive section open function variables {α : Type*} [has_zero α] [has_one α] [has_add α] [has_mul α] [has_neg α] variables {β : Type*} [comm_ring β] set_option profiler true -- elaboration of comm_ring_of_injective took 493ms 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 mul }, repeat { erw add }, repeat { erw mul }, try { erw neg }, try { erw zero }, try { erw one }, }, exacts [add_assoc _ _ _, zero_add _, add_zero _, add_left_neg _, add_comm _ _, mul_assoc _ _ _, one_mul _, mul_one _, mul_add _ _ _, add_mul _ _ _, mul_comm _ _] end end

#### Jesse Michael Han (Jun 15 2019 at 04:48):

I never could understand how

`erw`

is different from`rw`

.

The source is quite transparent about this:

meta def rewrite (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit := propagate_tags (rw_core q l cfg) meta def erewrite (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {md := semireducible}) : tactic unit := propagate_tags (rw_core q l cfg)

The difference is that `rewrite_core`

is allowed to peek into `semireducible`

definitions, where `reducible`

is the default. This means you need to do less explicit unfolding for your rewrites to succeed, but because more definitions are exposed and unification is expensive, `erw`

can be an order of magnitude slower.

Last updated: May 15 2021 at 00:39 UTC