saturation of a submonoid

Stream: mathlib4

[Kenny Lau]

I would like to define the saturation of a submonoid, I think it would be useful for localisation stuff

[Kenny Lau]

I haven't really seen this name elsewhere other than atiyah-macdonald (P. 44):

image.png

[Kenny Lau]

it should be { x : A | ∃ y : A, x * y ∈ s }

[Kenny Lau]

seeing this definition written explicitly perhaps it could be done as an iSup, but i'm not sure if the individual submonoids have a name (maybe absorber?)

[Aaron Liu]

Kenny Lau said:

it should be { x : A | ∃ y : A, x * y ∈ s }

that's probably something like open scoped Pointwise in x • (s : Set A)

[Aaron Liu]

wait no it's not

[Aaron Liu]

the other way around maybe

[Aaron Liu]

no

[Aaron Liu]

oh it's backwards

[Aaron Liu]

hmmm

[Aaron Liu]

yeah I don't have a clever way of writing this

[Kenny Lau]

oh also the individual parts aren't a submonoid, so nvm about iSup

[Yury G. Kudryashov]

Kenny Lau said:

it should be { x : A | ∃ y : A, x * y ∈ s }

My guess is that this works only for commutative monoids. Otherwise you should at least allow multiplication on both sides. Also, I'm not sure if the result will be closed under products after that in the noncommutative case.

[Aaron Liu]

This is some sort of root

[Kenny Lau]

so maybe we should focus on the commutative case for now?

[Kenny Lau]

oh no, why do we have AddSubgroup.Saturated

[Junyan Xu]

See #Is there code for X? > Closure of Submonoid in CommMonoids @ 💬

[Kenny Lau]

@Junyan Xu did they decide on a name?

[Aaron Liu]

isn't this like

[Aaron Liu]

dividing a submodule by a scalar action

[Aaron Liu]

but without the addition

[Kenny Lau]

#31132

[Yan Yablonovskiy 🇺🇦]

Kenny Lau said:

I haven't really seen this name elsewhere other than atiyah-macdonald (P. 44):

image.png

I was also planning to define these for my own use in my wheel theory repo, they are used in Wheels, on division by zero .

[Kenny Lau]

@Aaron Liu for the case of the smallest saturated submonoid of (Function.End Nat), is it just going to contain everything?

[Kenny Lau]

yeah i think so:

• it needs to contain id
• then it contains any f and g with fg=id, so it contains all injective and surjective maps
• if f is an arbitrary function with infinite range, then the epi-mono factorisaion gives it as a surjection then an injection
• for finite range, the surjection is to Fin n instead, but i claim this is an injection then a surjection: take the injection f(x)=2x, then for the surjection map 2x to the correct things, then the odd numbers can be mapped to Nat, so this map is surjective

[Kenny Lau]

in effect we have proved Unique (SaturatedMonoid (Function.End X)) for any Infinite X

[Kenny Lau]

for finite X, bijective iff surjective iff injective, so the bijective maps form a saturated submonoid, which is different from the top for #X > 1

[Kenny Lau]

do you think this is equivalent to choice? :upside_down:

[Kenny Lau]

@Aaron Liu i'm wondering for the definitions specialised to commmonoid whether i should have them as separate definitions or just inline them in the relevant theorems

[Aaron Liu]

some of my favorite monoids are noncommutative

[Aaron Liu]

can't we just have theorems specialized to comm monoids

[Kenny Lau]

lemme show you what i mean

[Kenny Lau]

image.png

image.png

[Kenny Lau]

this is my current setup, which feels suboptimal

[Aaron Liu]

oh that's weird

[Kenny Lau]

I kinda need to construct it once in order to prove that it is the saturation

[Kenny Lau]

so i'm wondering if i should construct it inline, i.e. in the theorem

[Aaron Liu]

can't you just use induction

[Kenny Lau]

or, i can use private

[Aaron Liu]

set up an induction principle

[Kenny Lau]

lemme try that

[Aaron Liu]

I'm talking about something like docs#Subgroup.closure_induction

[Kenny Lau]

yes, i understand, thanks

[Aaron Liu]

then you can just apply it in the theorem