Zulip Chat Archive

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.add_group,
  .. 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: Dec 20 2023 at 11:08 UTC