Zulip Chat Archive

Stream: maths

Topic: add_group.closure $ monoid_closure


view this post on Zulip 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?

view this post on Zulip Chris Hughes (Mar 10 2019 at 14:58):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 :-/

view this post on Zulip 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
-/

view this post on Zulip 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

view this post on Zulip 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