add_group.closure $ monoid_closure

Stream: maths

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

[from mathlib]

namespace ring

...

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

The instance ends up being called ring.is_subring :-/

[Kevin Buzzard]

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]

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]

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.