## Stream: general

### Topic: (fixed) comm_ring issues

#### Johan Commelin (Jul 18 2018 at 07:14):

I've got the following context/goal:

R : Type,
_inst_1 : ring.{0} R,
S : set.{0} R,
_inst_2 : @is_subring R _inst_1 S,
_inst_3 : comm_ring.{0} R,
a : R,
a_property : @has_mem.mem.{0 0} R (set.{0} R) (@set.has_mem.{0} R) a S,
b : R,
b_property : @has_mem.mem.{0 0} R (set.{0} R) (@set.has_mem.{0} R) b S
⊢ @eq.{1} R
(@has_mul.mul.{0} R
(@mul_zero_class.to_has_mul.{0} R (@semiring.to_mul_zero_class.{0} R (@ring.to_semiring.{0} R _inst_1)))
a
b)
(@has_mul.mul.{0} R
(@mul_zero_class.to_has_mul.{0} R (@semiring.to_mul_zero_class.{0} R (@ring.to_semiring.{0} R _inst_1)))
b
a)


#### Johan Commelin (Jul 18 2018 at 07:15):

For the record, here is my silly attempt to prove that subrings of comm rings are comm_ring:

instance subset.comm_ring [comm_ring R] : comm_ring S :=
{ mul_comm :=
begin
rintro ⟨a,_⟩ ⟨b,_⟩,
apply subtype.eq,
show a * b = b * a,
rw mul_comm,
end,
.. subset.ring }


#### Johan Commelin (Jul 18 2018 at 07:16):

Somehow Lean turns R into a semiring, instead of a comm_semigroup... And therefore I can't apply mul_comm.

#### Johan Commelin (Jul 18 2018 at 07:17):

For even more record:

instance subset.ring : ring S :=
{ add_comm      := assume ⟨a,_⟩ ⟨b,_⟩, subtype.eq $add_comm _ _, left_distrib := assume ⟨a,_⟩ ⟨b,_⟩ ⟨c,_⟩, subtype.eq$ left_distrib _ _ _,
right_distrib := assume ⟨a,_⟩ ⟨b,_⟩ ⟨c,_⟩, subtype.eq \$ right_distrib _ _ _,
.. subtype.monoid }


That was nice and easy... (and maybe with Scott's tactics it will become even easier!) but if I substitute mul for add it borks out.

#### Johan Commelin (Jul 18 2018 at 07:21):

Fixed. Lean starts crying if I tell it that R is a ring and a comm_ring.

#### Johan Commelin (Jul 18 2018 at 07:21):

And I understand why.

#### Johan Commelin (Jul 18 2018 at 07:22):

It just means that I cannot use the variables {R : Type} [ring R] from the top of my file.

#### Mario Carneiro (Jul 18 2018 at 07:41):

If you put {R} [comm_ring R] in the statement instead of just [comm_ring R] it will override the R in the enclosing section

#### Johan Commelin (Jul 18 2018 at 07:42):

OTOH, then I still can't use the variables {S : set R} [is_subring S] from the top of my file.

#### Johan Commelin (Jul 18 2018 at 07:43):

What I would need is to somehow tell lean: "Hey, in addition to all the other hypotheses, please extend the ring instance into a comm_ring instance."

#### Patrick Massot (Jul 18 2018 at 07:51):

I don't understand what you are doing. Haven't you already done that in https://github.com/kbuzzard/lean-perfectoid-spaces/blob/master/src/for_mathlib/subring.lean?

#### Johan Commelin (Jul 18 2018 at 07:54):

Not the bit on commutative rings.

#### Johan Commelin (Jul 18 2018 at 07:55):

Only plain old rings

Last updated: May 16 2021 at 05:21 UTC