Zulip Chat Archive

Stream: maths

Topic: comm_ring.closure


view this post on Zulip Patrick Massot (Oct 09 2018 at 20:16):

@Kenny Lau Do you secretely have comm_ring.closure with a subring instance somewhere in your repositories?

view this post on Zulip Kenny Lau (Oct 09 2018 at 20:16):

I don't think so.

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:19):

Too bad. Do you want to sprint through it?

view this post on Zulip Kenny Lau (Oct 09 2018 at 20:19):

sure

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:20):

I began with

import ring_theory.subring

namespace group
variables {α : Type*} [group α]
theorem exists_list_of_mem_closure {s : set α} {a : α} (h : a  closure s) :
  (l:list α, (xl, x  s  x⁻¹  s)  l.prod = a) :=
begin
  induction h,
  case in_closure.basic : a ha { existsi ([a]), simp [ha] },
  case in_closure.one { existsi ([]), simp },
  case in_closure.mul : a b _ _ ha hb {
    rcases ha with la, ha, eqa,
    rcases hb with lb, hb, eqb,
    existsi (la ++ lb),
    simp [eqa.symm, eqb.symm, or_imp_distrib],
    exact assume a, ha a, hb a
  },
  case in_closure.inv : a a_in_clo hlist {
    rcases hlist with la, ha, eqa,
    existsi (la.reverse.map (λ x, x⁻¹)),
    split,
    { intros x x_in,
      rw list.mem_map at x_in,
      rcases x_in with b, b_in, hb,
      rw list.mem_reverse at b_in,
      specialize ha b b_in,
      have hb' : b = x⁻¹, by rw hb ; simp,
      rw [hb, hb'] at ha,
      cc },
    { rw [eqa, inv_prod la] } }
end
end group

namespace add_group
variables {α : Type*} [add_group α]

theorem exists_list_of_mem_closure {s : set α} {a : α} (h : a  closure s) :
  (l:list α, (xl, x  s  -x  s)  l.sum = a) :=
sorry
end add_group

namespace comm_ring
variables {R : Type*} [comm_ring R]

def closure (s : set R) := add_group.closure (monoid.closure s)

instance {s : set R} : is_subring (closure s) :=
begin
  dunfold closure,
  exact
    { zero_mem := is_add_submonoid.zero_mem _,
      add_mem := λ a b ha hb, is_add_submonoid.add_mem ha hb,
      neg_mem := λ a h, is_add_subgroup.neg_mem h,
      one_mem := add_group.mem_closure (is_submonoid.one_mem _),
      mul_mem := begin
        intros a b a_in b_in,
        rcases add_group.exists_list_of_mem_closure a_in with la, hla, sum_a,
        rcases add_group.exists_list_of_mem_closure b_in with lb, hlb, sum_b,
        rw [sum_a, sum_b],
        sorry,
      end }
end

end comm_ring

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:21):

But I lost courage because of https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/to_additive.20multiplicative/near/135470227 and sum manipulations

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:21):

The trouble is that the big_operator stuff in mathlib is all about sums over finset, not lists

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:22):

(here I mean the trouble with the final sorry, the to_additive stuff is simply total mystery)

view this post on Zulip Kenny Lau (Oct 09 2018 at 20:40):

import ring_theory.subring

universe u

@[elab_as_eliminator]
theorem add_monoid.in_closure.rec_on {α : Type u} [add_monoid α] {s : set α} {C : α  Prop}
  {a : α} (H : a  add_monoid.closure s)
  (H1 :  {a : α}, a  s  C a) (H2 : C 0)
  (H3 :  {a b : α}, a  add_monoid.closure s  b  add_monoid.closure s  C a  C b  C (a + b)) :
  C a :=
monoid.in_closure.rec_on H (λ _, H1) H2 (λ _ _, H3)

@[elab_as_eliminator]
theorem add_group.in_closure.rec_on {α : Type u} [add_group α] {s : set α} {C : α  Prop}
  {a : α} (H : a  add_group.closure s)
  (H1 :  {a : α}, a  s  C a) (H2 : C 0) (H3 :  {a : α}, a  add_group.closure s  C a  C (-a))
  (H4 :  {a b : α}, a  add_group.closure s  b  add_group.closure s  C a  C b  C (a + b)) :
  C a :=
group.in_closure.rec_on H (λ _, H1) H2 (λ _, H3) (λ _ _, H4)

namespace comm_ring
variables {R : Type u} [comm_ring R]

def closure (s : set R) := add_group.closure (monoid.closure s)

local attribute [reducible] closure

instance {s : set R} : is_subring (closure s) :=
{ zero_mem := is_add_submonoid.zero_mem _,
  add_mem := λ a b ha hb, is_add_submonoid.add_mem ha hb,
  neg_mem := λ a h, is_add_subgroup.neg_mem h,
  one_mem := add_group.mem_closure (is_submonoid.one_mem _),
  mul_mem := λ a b ha hb, add_group.in_closure.rec_on hb
    (λ b hb, add_group.in_closure.rec_on ha
      (λ a ha, add_group.subset_closure (is_submonoid.mul_mem ha hb))
      ((zero_mul b).symm  is_add_submonoid.zero_mem _)
      (λ a ha hab, (neg_mul_eq_neg_mul a b)  is_add_subgroup.neg_mem hab)
      (λ a c ha hc hab hcb, (add_mul a c b).symm  is_add_submonoid.add_mem hab hcb))
    ((mul_zero a).symm  is_add_submonoid.zero_mem _)
    (λ b hb hab, (neg_mul_eq_mul_neg a b)  is_add_subgroup.neg_mem hab)
    (λ b c hb hc hab hac, (mul_add a b c).symm  is_add_submonoid.add_mem hab hac) }

end comm_ring

view this post on Zulip Kenny Lau (Oct 09 2018 at 20:40):

@Patrick Massot

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:42):

Thanks!

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:42):

Could we still get the list statements analogue to what is already in mathlib for monoids?

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:43):

Is the reducible attribute purely intended to save a couple of dunfold in the instance building?

view this post on Zulip Kenny Lau (Oct 09 2018 at 20:46):

Is the reducible attribute purely intended to save a couple of dunfold in the instance building?

yes

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:49):

Why do you get monoid.in_closure.rec_on for free when defining monoid.in_closure but need to write add_monoid.in_closure.rec_on?

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:49):

Is it because of the multiplicative to additive magic?

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:49):

which is not magic enough?

view this post on Zulip Kenny Lau (Oct 09 2018 at 20:51):

because add_monoid.closure is not defined using to_additive

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:55):

And why isn't it defined using to_additive?

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:56):

The definition is really weird. At some point earlier Lean was completely confused and asked me to prove stuff involving 1 in an additive context

view this post on Zulip Patrick Massot (Oct 09 2018 at 20:58):

I would have never thought of proving that instance using these nested inductions. The real world proof manipulating sums is so easy, it seems beyond masochistic to write your proof.

view this post on Zulip Kenny Lau (Oct 09 2018 at 21:01):

theorem exists_list_of_mem_closure {s : set α} {a : α} (h : a  closure s) :
  (l:list α, (xl, x  s  -x  s)  l.sum = a) :=
group.exists_list_of_mem_closure h

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:01):

this is even more confusing

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:03):

I thought you would be using your custom recursor

view this post on Zulip Kenny Lau (Oct 09 2018 at 21:03):

me too

view this post on Zulip Kenny Lau (Oct 09 2018 at 21:03):

and halfway I realized

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:04):

Do you understand what's going on with this way of turning multiplicative stuff into additive one?

view this post on Zulip Kenny Lau (Oct 09 2018 at 21:04):

somewhat.

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:22):

What about the exists_lists_of_mem_closure in the ring case?

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:22):

something like

theorem exists_list_of_mem_closure {s : set R} {a : R} (h : a  closure s) :
  ( L : list (list R), ( l  L,  x  l, x  s  -x  s)  (list.map list.prod L).sum = a)

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:23):

I guess I would try to use the previous theorems but you'll run crazy inductions...

view this post on Zulip Kenny Lau (Oct 09 2018 at 21:24):

why do we need list (list R)?

view this post on Zulip Kenny Lau (Oct 09 2018 at 21:24):

ah I see

view this post on Zulip Kenny Lau (Oct 09 2018 at 21:25):

maybe we should prove the recursor for comm_ring.closure first

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:25):

of course the maths proof is not at all by induction

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:26):

but in Lean it would probably be easier by induction

view this post on Zulip Kenny Lau (Oct 09 2018 at 21:26):

oh how do you prove it in maths?

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:28):

The maths proof starts with rcases add_group.exists_list_of_mem_closure h with ⟨L1, hL1, L1sum⟩,

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:29):

Then you need to apply monoid.exists_list_of_mem_closure everywhere you see monoid.closure in hL1

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:29):

of course it's already beyond my Lean fu, because of the binder

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:30):

and this get you get your list of lists

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:30):

except for the substractions

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:30):

I guess my statement is wrong

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:31):

no, it's ok

view this post on Zulip Reid Barton (Oct 09 2018 at 21:32):

I think it is wrong, because of -1. s could even be empty.

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:32):

edge cases...

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:32):

who cares about those?

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:35):

I clearly need to sleep though. I'm sure the Kenny tactic can fix the statement while writing the proof

view this post on Zulip Kenny Lau (Oct 09 2018 at 21:35):

of what?

view this post on Zulip Patrick Massot (Oct 09 2018 at 21:40):

ring.exists_list_of_mem_closure

view this post on Zulip Kenny Lau (Oct 26 2018 at 09:00):

import ring_theory.subring

universe u

@[elab_as_eliminator]
theorem add_monoid.in_closure.rec_on {α : Type u} [add_monoid α] {s : set α} {C : α  Prop}
  {a : α} (H : a  add_monoid.closure s)
  (H1 :  {a : α}, a  s  C a) (H2 : C 0)
  (H3 :  {a b : α}, a  add_monoid.closure s  b  add_monoid.closure s  C a  C b  C (a + b)) :
  C a :=
monoid.in_closure.rec_on H (λ _, H1) H2 (λ _ _, H3)

@[elab_as_eliminator]
theorem add_group.in_closure.rec_on {α : Type u} [add_group α] {s : set α} {C : α  Prop}
  {a : α} (H : a  add_group.closure s)
  (H1 :  {a : α}, a  s  C a) (H2 : C 0) (H3 :  {a : α}, a  add_group.closure s  C a  C (-a))
  (H4 :  {a b : α}, a  add_group.closure s  b  add_group.closure s  C a  C b  C (a + b)) :
  C a :=
group.in_closure.rec_on H (λ _, H1) H2 (λ _, H3) (λ _ _, H4)

instance int.cast_hom {R : Type u} [comm_ring R] : is_ring_hom (int.cast :   R) :=
int.cast_one, int.cast_mul, int.cast_add

instance int.coe_hom {R : Type u} [comm_ring R] : is_ring_hom (coe :   R) :=
int.cast_one, int.cast_mul, int.cast_add

namespace comm_ring
variables {R : Type u} [comm_ring R]

def closure (s : set R) := add_group.closure (monoid.closure s)

local attribute [reducible] closure

theorem exists_list_of_mem_closure {s : set R} {a : R} (h : a  closure s) :
  ( L : list (list R), ( l  L,  x  l, x  s  -x  s  x = (-1:R))  (L.map list.prod).sum = a) :=
add_group.in_closure.rec_on h
  (λ x hx, match x, monoid.exists_list_of_mem_closure hx with
    | _, L, h1, rfl := [L], list.forall_mem_singleton.2 (λ r hr, or.inl (h1 r hr)), zero_add _⟩
    end)
  [], list.forall_mem_nil _, rfl
  (λ b _ ih, match b, ih with
    | _, L1, h1, rfl := L1.map (list.cons (-1)),
      λ L2 h2, match L2, list.mem_map.1 h2 with
        | _, L3, h3, rfl := list.forall_mem_cons.2 or.inr $ or.inr rfl, h1 L3 h3
        end,
      by simp only [list.map_map, (), list.prod_cons, neg_one_mul];
      exact list.rec_on L1 neg_zero.symm (λ hd tl ih,
        by rw [list.map_cons, list.sum_cons, ih, list.map_cons, list.sum_cons, neg_add])
    end)
  (λ r1 r2 hr1 hr2 ih1 ih2, match r1, r2, ih1, ih2 with
    | _, _, L1, h1, rfl, L2, h2, rfl := L1 ++ L2, list.forall_mem_append.2 h1, h2,
      by rw [list.map_append, list.sum_append]
    end)

instance {s : set R} : is_subring (closure s) :=
{ zero_mem := is_add_submonoid.zero_mem _,
  add_mem := λ a b ha hb, is_add_submonoid.add_mem ha hb,
  neg_mem := λ a h, is_add_subgroup.neg_mem h,
  one_mem := add_group.mem_closure (is_submonoid.one_mem _),
  mul_mem := λ a b ha hb, add_group.in_closure.rec_on hb
    (λ b hb, add_group.in_closure.rec_on ha
      (λ a ha, add_group.subset_closure (is_submonoid.mul_mem ha hb))
      ((zero_mul b).symm  is_add_submonoid.zero_mem _)
      (λ a ha hab, (neg_mul_eq_neg_mul a b)  is_add_subgroup.neg_mem hab)
      (λ a c ha hc hab hcb, (add_mul a c b).symm  is_add_submonoid.add_mem hab hcb))
    ((mul_zero a).symm  is_add_submonoid.zero_mem _)
    (λ b hb hab, (neg_mul_eq_mul_neg a b)  is_add_subgroup.neg_mem hab)
    (λ b c hb hc hab hac, (mul_add a b c).symm  is_add_submonoid.add_mem hab hac) }

end comm_ring

view this post on Zulip Kenny Lau (Oct 26 2018 at 09:01):

@Patrick Massot will you PR this?

view this post on Zulip Patrick Massot (Oct 26 2018 at 09:07):

I can do it if you don't want to do it

view this post on Zulip Patrick Massot (Oct 26 2018 at 09:07):

But it would make more sense if you do it yourself

view this post on Zulip Patrick Massot (Oct 26 2018 at 09:07):

otherwise git won't credit you

view this post on Zulip Kenny Lau (Oct 26 2018 at 09:07):

where should I put it?

view this post on Zulip Patrick Massot (Oct 26 2018 at 09:08):

Maybe in the subgroup and subring files?

view this post on Zulip Kenny Lau (Oct 26 2018 at 09:08):

maybe it'll just go to limbo like https://github.com/leanprover/mathlib/pull/425

view this post on Zulip Patrick Massot (Oct 26 2018 at 09:09):

This is much smaller scope

view this post on Zulip Patrick Massot (Oct 26 2018 at 09:09):

It should be an easy merge

view this post on Zulip Kenny Lau (Oct 28 2018 at 10:29):

https://github.com/leanprover/mathlib/pull/444

view this post on Zulip Kenny Lau (Oct 28 2018 at 10:29):

done @Patrick Massot


Last updated: May 18 2021 at 08:14 UTC