## Stream: maths

### Topic: comm_ring.closure

#### 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?

#### Kenny Lau (Oct 09 2018 at 20:16):

I don't think so.

#### Patrick Massot (Oct 09 2018 at 20:19):

Too bad. Do you want to sprint through it?

sure

#### 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 α, (∀x∈l, 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

variables {α : Type*} [add_group α]

theorem exists_list_of_mem_closure {s : set α} {a : α} (h : a ∈ closure s) :
(∃l:list α, (∀x∈l, x ∈ s ∨ -x ∈ s) ∧ l.sum = a) :=
sorry

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
neg_mem := λ a h, is_add_subgroup.neg_mem h,
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


#### 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

#### 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

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

#### 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) :=
neg_mem := λ a h, is_add_subgroup.neg_mem h,
mul_mem := λ a b ha hb, add_group.in_closure.rec_on hb
(λ a ha, add_group.subset_closure (is_submonoid.mul_mem ha hb))
(λ a ha hab, (neg_mul_eq_neg_mul a b) ▸ is_add_subgroup.neg_mem hab)
(λ b hb hab, (neg_mul_eq_mul_neg a b) ▸ is_add_subgroup.neg_mem hab)

end comm_ring


@Patrick Massot

Thanks!

#### Patrick Massot (Oct 09 2018 at 20:42):

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

#### Patrick Massot (Oct 09 2018 at 20:43):

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

#### 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

#### 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?

#### Patrick Massot (Oct 09 2018 at 20:49):

Is it because of the multiplicative to additive magic?

#### Patrick Massot (Oct 09 2018 at 20:49):

which is not magic enough?

#### Kenny Lau (Oct 09 2018 at 20:51):

because add_monoid.closure is not defined using to_additive

#### Patrick Massot (Oct 09 2018 at 20:55):

And why isn't it defined using to_additive?

#### 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

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

#### Kenny Lau (Oct 09 2018 at 21:01):

theorem exists_list_of_mem_closure {s : set α} {a : α} (h : a ∈ closure s) :
(∃l:list α, (∀x∈l, x ∈ s ∨ -x ∈ s) ∧ l.sum = a) :=
group.exists_list_of_mem_closure h


#### Patrick Massot (Oct 09 2018 at 21:01):

this is even more confusing

#### Patrick Massot (Oct 09 2018 at 21:03):

I thought you would be using your custom recursor

me too

#### Kenny Lau (Oct 09 2018 at 21:03):

and halfway I realized

#### 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?

somewhat.

#### Patrick Massot (Oct 09 2018 at 21:22):

What about the exists_lists_of_mem_closure in the ring case?

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


#### Patrick Massot (Oct 09 2018 at 21:23):

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

#### Kenny Lau (Oct 09 2018 at 21:24):

why do we need list (list R)?

ah I see

#### Kenny Lau (Oct 09 2018 at 21:25):

maybe we should prove the recursor for comm_ring.closure first

#### Patrick Massot (Oct 09 2018 at 21:25):

of course the maths proof is not at all by induction

#### Patrick Massot (Oct 09 2018 at 21:26):

but in Lean it would probably be easier by induction

#### Kenny Lau (Oct 09 2018 at 21:26):

oh how do you prove it in maths?

#### 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⟩,

#### 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

#### Patrick Massot (Oct 09 2018 at 21:29):

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

#### Patrick Massot (Oct 09 2018 at 21:30):

and this get you get your list of lists

#### Patrick Massot (Oct 09 2018 at 21:30):

except for the substractions

#### Patrick Massot (Oct 09 2018 at 21:30):

I guess my statement is wrong

no, it's ok

#### Reid Barton (Oct 09 2018 at 21:32):

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

edge cases...

#### 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

of what?

#### Patrick Massot (Oct 09 2018 at 21:40):

ring.exists_list_of_mem_closure

#### 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) :=

instance int.coe_hom {R : Type u} [comm_ring R] : is_ring_hom (coe : ℤ → R) :=

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) :=
(λ 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) :=
neg_mem := λ a h, is_add_subgroup.neg_mem h,
mul_mem := λ a b ha hb, add_group.in_closure.rec_on hb
(λ a ha, add_group.subset_closure (is_submonoid.mul_mem ha hb))
(λ a ha hab, (neg_mul_eq_neg_mul a b) ▸ is_add_subgroup.neg_mem hab)
(λ b hb hab, (neg_mul_eq_mul_neg a b) ▸ is_add_subgroup.neg_mem hab)

end comm_ring


#### Kenny Lau (Oct 26 2018 at 09:01):

@Patrick Massot will you PR this?

#### Patrick Massot (Oct 26 2018 at 09:07):

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

#### Patrick Massot (Oct 26 2018 at 09:07):

But it would make more sense if you do it yourself

#### Patrick Massot (Oct 26 2018 at 09:07):

otherwise git won't credit you

#### Kenny Lau (Oct 26 2018 at 09:07):

where should I put it?

#### Patrick Massot (Oct 26 2018 at 09:08):

Maybe in the subgroup and subring files?

#### Kenny Lau (Oct 26 2018 at 09:08):

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

#### Patrick Massot (Oct 26 2018 at 09:09):

This is much smaller scope

#### Patrick Massot (Oct 26 2018 at 09:09):

It should be an easy merge

#### Kenny Lau (Oct 28 2018 at 10:29):

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

#### Kenny Lau (Oct 28 2018 at 10:29):

done @Patrick Massot

Last updated: May 18 2021 at 08:14 UTC