# Zulip Chat Archive

## Stream: maths

### Topic: add_group.closure $ monoid_closure

#### Kevin Buzzard (Mar 10 2019 at 14:56):

I think `monoid.closure (add_group.closure X) \sub add_group.closure (monoid.closure X)`

if X is a subset of a comm_ring (but I didn't prove it yet; doesn't look too hard). Is this in mathlib though?

#### Chris Hughes (Mar 10 2019 at 14:58):

I think the second one is the definition of `ring.closure`

#### Kevin Buzzard (Mar 10 2019 at 16:08):

Why are these things called `closure`

when `span`

is so much shorter? Is it a coincidence that `submodule.span`

is defined non-inductively as the intersection of all the submodules containing the set, whereas these closure operations are defined inductively?

#### Kevin Buzzard (Mar 10 2019 at 17:00):

I think the second one is the definition of

`ring.closure`

That's a really useful comment, because the hardest part of the argument can be proved by the mul_mem field of the instance saying `ring.closure`

is a subring.

#### Kevin Buzzard (Mar 10 2019 at 17:53):

[from mathlib]

namespace ring ... instance : is_subring (closure s) := ...

The instance ends up being called `ring.is_subring`

:-/

#### Kevin Buzzard (Mar 10 2019 at 17:53):

Curiouser and curiouser:

#check ring.is_subring.mul_mem /- is_submonoid.mul_mem : ∀ {a b : ?M_1}, a ∈ ring.closure ?M_3 → b ∈ ring.closure ?M_3 → a * b ∈ ring.closure ?M_3 -/

#### Kevin Buzzard (Mar 10 2019 at 18:00):

End of my proof:

/- state: Ha : a ∈ add_group.closure (monoid.closure T), Hb : b ∈ add_group.closure (monoid.closure T) ⊢ a * b ∈ add_group.closure (monoid.closure T) -/ haveI : is_subring (add_group.closure (monoid.closure T)) := ring.is_subring, -- exact ring.is_subring.mul_mem Ha Hb, -- fails /- error is: invalid field notation, function 'is_submonoid.mul_mem' does not have explicit argument with type (is_submonoid ...) -/ exact is_submonoid.mul_mem Ha Hb, -- works

#### Kevin Buzzard (Mar 10 2019 at 18:01):

This is just some weirdness with structure fields, and is_subring extending is_submonoid I guess, but I don't really understand what's going on.

Last updated: May 12 2021 at 08:14 UTC