Abelianization/FreeCommMonoid

Stream: new members

[Coleton Kotch]

Hello,

As far as I can tell, we have abelianization at the level of groups defined (done through the commutator), but do not have it for more general objects. My guess would be that we would have abelianization defined more generally at the level of magmas through an inductive relation, but I cannot seem to find such. Is this operation defined and have I missed it? If it is not defined is it worth adding?

I should note that I was lead here by looking to construct a free commutative monoid. I may be missing something here on the correct way to define one through what we already have in mathlib.

Thank you,

[Coleton Kotch]

Something like this

import Mathlib.Algebra.Group.Basic

universe u

namespace Comm

variable (M : Type u) [Mul M]

inductive Rel : M → M → Prop
  | mul_compat (x x' y y' : M) : Rel x x' → Rel y y' → Rel (x * y) (x' * y')
  | mul_comm (x y : M) : Rel (x * y) (y * x)
  | refl (x : M) : Rel x x
  | symm (x y : M) : Rel x y → Rel y x
  | trans (x y z : M) : Rel x y → Rel y z → Rel x z

def Abelianization.setoid : Setoid M where
  r := Rel M
  iseqv := ⟨Rel.refl, Rel.symm _ _, Rel.trans _ _ _⟩

def Abelianization := Quotient (Abelianization.setoid M)

def Abelianization.mk : M →  Abelianization M := Quotient.mk _

instance : Mul (Abelianization M) where
  mul := Quotient.lift₂ (fun x y => Quotient.mk _ (x * y)) <|
    fun _ _ _ _ h₁ h₂ => Quotient.sound <| Rel.mul_compat _ _ _ _ h₁ h₂

lemma  Abelianization.mk_surjective : Function.Surjective (Abelianization.mk M) := by
  rintro ⟨x⟩
  exact ⟨x, rfl⟩

instance : CommMagma (Abelianization M) where
  mul_comm x y := by
    obtain ⟨x,rfl⟩ := Abelianization.mk_surjective _ x
    obtain ⟨y,rfl⟩ :=  Abelianization.mk_surjective _ y
    exact Quotient.sound <| Rel.mul_comm x y

instance (M : Type u) [MulOneClass M] : MulOneClass (Abelianization M) where
  one := Abelianization.mk M 1
  mul_one x := by
    obtain ⟨x,rfl⟩ := Abelianization.mk_surjective _ x
    apply Quotient.sound
    rw [mul_one]
    exact Rel.refl x
  one_mul x := by
    obtain ⟨x,rfl⟩ := Abelianization.mk_surjective _ x
    apply Quotient.sound
    rw [one_mul]
    exact Rel.refl x


instance (M : Type u) [Semigroup M] : CommSemigroup (Abelianization M) where
  mul_comm := mul_comm
  mul_assoc x y z := by
    obtain ⟨x,rfl⟩ := Abelianization.mk_surjective _ x
    obtain ⟨y,rfl⟩ := Abelianization.mk_surjective _ y
    obtain ⟨z,rfl⟩ := Abelianization.mk_surjective _ z
    apply Quotient.sound
    rw [mul_assoc]
    exact Rel.refl (x * (y * z))


instance (M : Type u) [Monoid M] : CommMonoid (Abelianization M) where
  mul_comm := mul_comm
  mul_one := mul_one
  one_mul := one_mul

[Eric Wieser]

Does docs#Con help here? Ideally you'd use it in place of Setoid, and it will build the multiplication for you

[Coleton Kotch]

At a quick glance it seems to be what I was looking for, though I'll take a closer look tomorrow, thank you.

[Kevin Buzzard]

The free commutative monoid on a type X is just X →₀ ℕ, you don't need to make it again.

[Adam Topaz]

The free commutative monoid is also Multiset X :-) (of course, finsupp is better because it would inherit an additive structure from Nat)

[Damiano Testa]

In Pointwise, Multiset could/should also have an additive structure, I think.

[Eric Wieser]

The additive structure is there globally

[Coleton Kotch]

Thanks for the help everyone :). Finitely supported functions should work very nicely given how the power of each character is nicely accessible.

On a different note though, I am curious about what makes some objects make the cut of inclusion in Mathlib, while others do not. I understand that there is no precise formula, but I am hoping to understand Mathlib a bit better.

Given the use of docs#Con we can nicely move forward along any of the axes of associativity, commutativity, identity, etc. and could for example use the free Magma on X to construct the free commutative Magma on X or the free Semigroup on X. The later of these objects is explicitly included in Mathlib, while the former is not (as far as I can tell at least).
For groups we have the abelianization of a group, done through the use of the commutator subgroup, though this could also be done through the use of docs#Con.
As was pointed out to me, free commutative monoid are nicely constructable, though there is no formal definition. Free monoids feel similar as the definition of the free monoid on X is the type 'List X'.

My guess is that broadly the choice of direct inclusion or not is based on how commonly used an object is, particularly in the case of Free Magmas/Semigroups/Monoids/Groups/Abelian groups and the like.
We include the abelianization of a group as the construction is done using the commutator subgroup which is distinct in flavour from the more general construction, even if ultimately giving the same object. My main curiosity here is if this inclusion is in part because of the fact that it is likely a person could know of abelianization using the commutator, while being unfamiliar with the more general idea of quotients and how abelianization could be done using them?
In the case of free commutative monoids, even though they likely come up more often than free semigroups or others which make the cut, we do not have a "formal definition" akin to what was done for standards monoids, as the constructions we already have works nicely enough and we thus do not need to build up an API around it specifically for the use case of free commutative monoids.