Closure of Submonoid in CommMonoids

Stream: Is there code for X?

[Xavier Xarles]

I am not sure something like this is in Mathlib4.

import Mathlib.GroupTheory.Submonoid.Basic

variable {G : Type*} [CommMonoid G] (S : Submonoid G)

def Submonoid.Closure: Submonoid G where
  carrier := {a | ∃ r, a*r ∈ S}
  one_mem':= by simp; use 1; exact Submonoid.one_mem S
  mul_mem' a b := by
    let ⟨ ra ,ha ⟩ := a
    let ⟨ rb ,hb ⟩ := b
    use ra * rb
    rw [mul_mul_mul_comm]
    exact Submonoid.mul_mem S ha hb

lemma Submonoid.Closure.mem (a:G): a ∈ (Submonoid.Closure S) ↔ ∃ r, a*r ∈ S := Iff.rfl

lemma Submonoid.Closure.sub: S ≤ (Submonoid.Closure S):= by
  rw [@SetLike.le_def]
  intro a ha
  rw [Submonoid.Closure.mem]
  use 1
  rw [@mul_one]
  exact ha

[Adam Topaz]

I think closure generally refers to the subobject generated by a subset. I would call this Submonoid.saturation or something like that.

[Adam Topaz]

And I do recall seeing something along these lines in mathlib... maybe somewhere in the localization library?

[Riccardo Brasca]

We have docs#Subgroup.Saturated that says the "saturation" isn't bigger.

[Riccardo Brasca]

But it seems saturated isn't used elsewhere.

[Junyan Xu]

That seems to be a weaker condition than the condition being discussed (∀ ⦃a b : α⦄, b ∈ s → a ∣ b → a ∈ s, which also appeared here). I guess it's what people use to talk about a saturated lattice in a real vector space, while the version discussed here is used as in a saturated multiplicatively closed set.

[Riccardo Brasca]

Is it docs#IsLocalization.invSubmonoid ?

[Riccardo Brasca]

I mean, related

[Riccardo Brasca]

No sorry

[Xavier Xarles]

It is in some sense related, yes. Indirectly...

[Xavier Xarles]

In fact, the idea is that the localization w.r.t a submonoid and w.r.t. its saturation are isomorphic (the natural map is an isomorphism).

[Junyan Xu]

(deleted)

[Riccardo Brasca]

Xavier Xarles said:

In fact, the idea is that the localization w.r.t a submonoid and w.r.t. its saturation are isomorphic (the natural map is an isomorphism).

I think we have this stated somehow. I have to go now, but there is file called localization_localozation or something similar

[Xavier Xarles]

In Localization there is a part about the saturation of a submonoid. It explains exactly what I was interested (two submonoids give "the same" localization iff they have the same saturation).
Do you think it can be interesting to have it in mathlib?

[Junyan Xu]

Yes this seems to be an interesting result; I didn't know the "only if" direction. I think for IsLocalization you can state that IsLocalization M S, IsLocalization N S, and M.saturation = N.saturation satisfy the two-out-of-three property, i.e. any two imply the third. For LocalizationMap it would be trickier to state (something like an isomorphism forming an edge of a commuting triangle) because the map is bundled.

[Junyan Xu]

Note that docs#Subgroup.Saturated is called "root closed" in this paper, and I think we should rename. However, "root" suggests multiplicative, and I'm not sure what a good additive name is.
image.png

[Kevin Buzzard]

div_closed?

[Kevin Buzzard]

But what's wrong with saturated? I think this is a standard term (in the sense that I've heard the term before and I'd never heard of "root closed" until I read this thread)

[Junyan Xu]

The issue is that it clashes with the notion of saturated multiplicative closed set (aka submonoid).

[Xavier Xarles]

In this paper, proposition 1.11, the authors call it pure (also propose radical closed). See
ipure.png

[Kevin Buzzard]

I like root-closed because it really is a name which makes you guess the definition. My comment earlier about "what's wrong with saturated" is in retrospect silly -- saturated is I think consistently used in the literature to mean "closed under divisors", whereas this means "closed under roots".

[Jz Pan]

So are there any plan to rename docs#Subgroup.Saturated ? Probably Subgroup.RootClosed and AddSubgroup.DivClosed is OK?