Normal submonoids

Stream: maths

[Mario Carneiro]

Are these a thing? The natural definition of normal subgroup extends to the monoid case as a + b \in S -> b + a \in S

[Johan Commelin]

Do we need them anywhere?

[Mario Carneiro]

not particularly

[Mario Carneiro]

Do we need normal subgroups?

[Mario Carneiro]

I guess the answer is about the same

[Johan Commelin]

Well... I think the will be used quite a lot.

[Johan Commelin]

Isn't Kevin already using them?

[Mario Carneiro]

I'm working on porting the add_subgroup stuff now... I don't really get why we care about noncommutative additive groups

[Johan Commelin]

We don't care about those.

[Johan Commelin]

We just want the additive subgroups, so that we can have subrings.

[Kenny Lau]

subrings not

[Johan Commelin]

And this seemed like a very straightforward translation exercise, which I performed without thinking about whether some lines could be removed...

[Kevin Buzzard]

Normal subgroups are used all over the place in maths, they're exactly the kernels of morphisms in the category of groups. I thought a bit recently about why we would care about noncommutative additive groups, and the only half-decent answer I could come up with is that there is at least one example in maths where people use addition as a standard notation and it's not commutative, namely addition of ordinals (not that anyone outside of logic ever uses ordinals anyway). These do not form a group though. In number theory there is an implicit assumption that addition is commutative.

I am only using normal subgroups in the additive case and only in the situation where addition is commutative, so they're the same as subgroups. My only use case was that I need some lemmas about quotient rings, and I thought that the "correct" way to prove that a map R -> S whose kernel contains I induced a map R/I -> S would be to first construct the map using some universal property of quotient abelian groups and then to show it's a ring homomorphism. But I don't know whether I'm fussing over nothing and should just prove it directly.

Didn't Chris make a quotient group PR recently? I was going to make one and then Chris told me he'd made one so I shouldn't PR because of potential conflicts.

https://github.com/leanprover/mathlib/pull/212

[Mario Carneiro]

oops

[Andreas Swerdlow]

I did some basic subring and subfield stuff here https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/inner_product_spaces/subrings_subfields.lean. Is this useful at all, or should it be linked to existing stuff in mathlib?

[Reid Barton]

Normal subgroups are used all over the place in maths, they're exactly the kernels of morphisms in the category of groups.

And groups are special because the equivalence relation induced by a surjection ($x \sim y$ if $f(x) = f(y)$) is determined by the equivalence class of 0, i.e., the kernel. For general monoids, knowing the kernel of a map doesn't tell you about the behavior of the map away from 0 (consider the quotient of nat which identifies all the numbers greater than or equal to 3).
So, I don't think normal submonoids are of much interest.

[Scott Morrison]

@Andreas Swerdlow, looks useful to me. How about you PR it?

[Scott Morrison]

It might be worth doing a little renaming to get the functions as close as possible to following the pattern in mathlib/group_theory/subgroup.lean.

[Scott Morrison]

I'm not entirely certainly where to put what you've written. My suggestion would be to be ambitious, and split it into two parts, putting them in ring_theory/subring.lean and field_theory/subfield.lean, parallel to the group situation: eventually we're going to need a fair bit of other stuff in both those directories. (Although field_theory sounds very wrong...)

[Scott Morrison]

Probably it's best to create a new branch at <https://github.com/leanprover-community/mathlib>, so others can look at it first (announce here you want help?) and then once it's been tweaked a bit we can PR it to the official mathlib.

[Scott Morrison]

(If you don't have commit access at leanprover-community, either ask here for it, or just do the work in your own fork of mathlib and send a PR to leanprover-community, and announce here and somewhere will merge it to a branch.)

[Johan Commelin]

I did some basic subring and subfield stuff here https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/inner_product_spaces/subrings_subfields.lean. Is this useful at all, or should it be linked to existing stuff in mathlib?

Hi @Andreas Swerdlow Additive subgroups have just been put into mathlib: https://github.com/leanprover/mathlib/blob/0f42b279865753eb3c79f3504783c7dbd81dfc7e/group_theory/subgroup.lean#L25. I think that it is useful if Lean knows that every subring is also an additive subgroup. Some time ago I wrote https://github.com/kbuzzard/lean-perfectoid-spaces/blob/master/src/for_mathlib/subring.lean#L13, but there is nothing about fields in that file. I think a merge of your and my approach would be best.

[Andreas Swerdlow]

@Scott Morrison @Johan Commelin thanks for the help. I've rewritten the subfield part, so that it builds off of what Johan wrote for subrings, and created a fork of leanprover-community/mathlib with both Johan's subring file in ring_theory/subring.lean and the subfield stuff in field_theory/subfield.lean. The fork is here: https://github.com/amswerdlow/mathlib. Any suggestions are welcome before I PR