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