# Zulip Chat Archive

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

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

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 namespace add_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 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

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

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

@Patrick Massot

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

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

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

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?

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

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

?

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

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

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

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.

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

edge cases...

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

who cares about those?

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

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

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

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