AddMonoid and Monoid

Stream: new members

[Bjørn Kjos-Hanssen]

I feel like every additive monoid should be viewable as a (multiplicative) monoid. How to do this, in a way that doesn't lead to conflicting instances down the line?

import Mathlib
instance {E : Type u_2}  [NormedAddCommGroup E] :
    AddMonoid E := AddLeftCancelMonoid.toAddMonoid

instance {E : Type u_2} [NormedAddCommGroup E] : Monoid E := by sorry

[Matt Diamond]

Are you looking for docs#Multiplicative or something else?

[Bjørn Kjos-Hanssen]

How would you use that here?

[Matt Diamond]

Well, you wouldn't have an instance of Monoid E, but you would (and do) have an instance of Monoid (Multiplicative E) and the ability to convert back and forth

[Matt Diamond]

since you have NormedAddCommGroup E, you automatically get a NormedCommGroup (Multiplicative E) instance

[Bjørn Kjos-Hanssen]

Ah, very good!

[Notification Bot]

Bjørn Kjos-Hanssen has marked this topic as resolved.

[Notification Bot]

Bjørn Kjos-Hanssen has marked this topic as unresolved.

[Bjørn Kjos-Hanssen]

Still struggling with this:

import Mathlib
def extracted_1.{u_2, u_1} {𝕜 : Type u_1} (E : Fin 2 → Type u_2) [inst : RCLike 𝕜]
  [inst_1 : (i : Fin 2) → NormedAddCommGroup (E i)] :
  CommMonoid (Monoid.PushoutI fun i ↦ MonoidHom.inl 𝕜 (Multiplicative (E i))) := by
  sorry

Certainly seems like a pushout of commutative monoids should be commutative, but how to prove?

[Kevin Buzzard]

Are you sure that's true? Doesn't sound true to me. Free product of two copies of the integers is free group on two generators

[Kevin Buzzard]

docs#Monoid.PushoutI

[Kevin Buzzard]

This is amalgamated product, what you're asking is not true

[Bjørn Kjos-Hanssen]

Thanks @Kevin Buzzard I am really trying to do pushouts of vector spaces but apparently got off track!