Monoid Morphism

Stream: new members

[Ken Lee]

Say I have (M N : Type u) [monoid M] [monoid N](f : M -> N), how do I say "f is a monoid morphism" in Lean?

[Scott Morrison]

Just write f : M →* N.

[Scott Morrison]

We use bundled morphisms (i.e. not just a bare function), and these have a coercion to functions so you can mostly use them just as if it was an honest function.

[Scott Morrison]

There is probably a is_monoid_hom predicate as well, but don't use it unless you're really sure you should be: the bundled hom is usually better.

[Ken Lee]

my issue though is that I'm given the bare function f and I want to say "this f is a monoid morphism"

[Ken Lee]

Scott Morrison said:

There is probably a is_monoid_hom predicate as well, but don't use it unless you're really sure you should be: the bundled hom is usually better.

because using bundled hom is morally "working in the category of monoids"?

[Scott Morrison]

This is often an #xy problem. Usually the correct fix is to find the person giving you the bare function and make them give you the bundled function instead. :-)

[Scott Morrison]

There is is_monoid_hom for exactly this purpose, but if you observe how infrequently it is used in mathlib, you'll see why I suggest you tell us here what you're doing, and we'll see if the bundled hom suits your purpose!

[Ken Lee]

I'm trying out an alternative definition of "monoids internal to a category" based on Yoneda

import algebra.category.Mon.basic
import category_theory.category

open category_theory

universes u v

structure MON (C : Type u) [category.{v} C] :=
(carrier : C)
(el_mon : Π (δ : C), monoid(δ ⟶ carrier) . tactic.apply_instance)
(funk_mon : Π (δ δ₁ : C) (f : δ₁ ⟶ δ) (d d₁ : δ ⟶ carrier),
  f ≫ (d * d₁) = f ≫ d * f ≫ d₁)

instance (C : Type u) [category.{v} C] (M : MON C) (δ : C) :
monoid (δ ⟶ M.carrier) := M.el_mon δ

structure hom (C : Type u) [category.{v} C] (M N : MON C) :=
(mor : M.carrier ⟶ N.carrier)
(el_map_one : Π (δ : C), (1 : δ ⟶ M.carrier)≫ mor = 1)
(el_map_mul : Π (δ : C), Π (x y : δ ⟶ M.carrier),
  (x * y) ≫ mor = x ≫ mor * y ≫ mor)

[Ken Lee]

it would be nice for funk_mon to say "the (contravariant) induced map on homs is a monoid morphism" and similarly for definition of hom to be "a map such that induced map on homs is a monoid morphism", hence my post.

[Scott Morrison]

Interesting!

[Ken Lee]

maybe I shld phrase everything as upgrading the Yoneda embedding "yoneda M : C^op => Type v" to "yoneda M : C^op => Mon Type v"?

[Scott Morrison]

I'm not quite sure what that would mean.

[Scott Morrison]

We do have Mon_ (C ⥤ D) ≌ C ⥤ Mon_ Din category_theory.monoidal.internal.functor_category.

[Scott Morrison]

So it would suffice to say yoneda M is an internal monoid. But we don't have unbundled internal monoids! :-)

[Scott Morrison]

I guess you could not worry about representability, and just write Mon_ (Cᵒᵖ ⥤ Type) as the entirety of the definition... (pro- internal- monoids? I don't know what these would be called)

[Scott Morrison]

Or take the subcategory which under Mon_ (Cᵒᵖ ⥤ Type) ≌ Cᵒᵖ ⥤ Mon_ Type become representable...

[Scott Morrison]

But I think my answer for now is that you should use is_monoid_hom. :-)

[Ken Lee]

I will play around with both is_monoid_hom and Mon_ (Cᵒᵖ ⥤ Type). Thanks so much!

[Ken Lee]

Scott Morrison said:

I guess you could not worry about representability, and just write Mon_ (Cᵒᵖ ⥤ Type) as the entirety of the definition... (pro- internal- monoids? I don't know what these would be called)

monoid presheaves on C maybe?